Animate graph changes

.dockerignore

@@ -0,0 +1,4 @@
+frontend/node_modules
+frontend/.parcel-cache
+target/debug
+

Cargo.toml

@@ -1,5 +1,5 @@
 [workspace]
-members=[ "lib", "bin" ]
+members=[ "lib", "bin", "server" ]
 default-members = [ "lib" ]
 
 [profile.release]

Dockerfile

@@ -0,0 +1,34 @@
+# 1. BUILD-CONTAINER: Frontend
+FROM node:gallium-alpine
+
+WORKDIR /root
+
+COPY ./frontend /root
+
+RUN yarn && yarn build
+
+# 2. BUILD-CONTAINER: Server
+FROM rust:alpine
+
+WORKDIR /root
+
+RUN apk add --no-cache musl-dev
+
+COPY ./bin /root/bin
+COPY ./lib /root/lib
+COPY ./server /root/server
+COPY ./Cargo.toml /root/Cargo.toml
+COPY ./Cargo.lock /root/Cargo.lock
+
+RUN cargo build --workspace --release
+
+# 3. RUNTIME-CONTAINER: run server with frontend as assets
+FROM alpine:latest
+
+WORKDIR /root
+
+COPY --from=0 /root/dist /root/assets
+COPY --from=1 /root/target/release/adf-bdd-server /root/server
+
+ENTRYPOINT ["./server"]
+

frontend/.editorconfig

@@ -0,0 +1,13 @@
+root = true
+
+[*]
+end_of_line = lf
+insert_final_newline = true
+
+[*.{ts,tsx}]
+indent_style = space
+indent_size = 2
+
+[package.json]
+indent_style = space
+indent_size = 2

frontend/.eslintrc.js

@@ -0,0 +1,25 @@
+module.exports = {
+    "env": {
+        "browser": true,
+        "es2021": true
+    },
+    "extends": [
+        "plugin:react/recommended",
+        "airbnb"
+    ],
+    "parser": "@typescript-eslint/parser",
+    "parserOptions": {
+        "ecmaFeatures": {
+            "jsx": true
+        },
+        "ecmaVersion": "latest",
+        "sourceType": "module"
+    },
+    "plugins": [
+        "react",
+        "@typescript-eslint"
+    ],
+    "rules": {
+        "react/jsx-filename-extension": [1, { "extensions": [".tsx"] }]
+    }
+}

frontend/.gitignore

@@ -0,0 +1,5 @@
+node_modules
+dist
+.parcel-cache
+yarn-error.log
+

frontend/package.json

@@ -0,0 +1,33 @@
+{
+    "name": "ADF-OBDD-Frontend",
+    "version": "0.1.0",
+    "source": "src/index.html",
+    "browserslist": "> 0.5%, last 2 versions, not dead",
+    "scripts": {
+        "start": "parcel",
+        "build": "parcel build"
+    },
+    "devDependencies": {
+        "@types/react": "^18.0.26",
+        "@types/react-dom": "^18.0.10",
+        "@typescript-eslint/eslint-plugin": "^5.48.1",
+        "@typescript-eslint/parser": "^5.48.1",
+        "eslint": "^8.31.0",
+        "eslint-config-airbnb": "^19.0.4",
+        "eslint-plugin-import": "^2.27.4",
+        "eslint-plugin-jsx-a11y": "^6.7.1",
+        "eslint-plugin-react": "^7.32.0",
+        "parcel": "^2.8.2",
+        "process": "^0.11.10",
+        "typescript": "^4.9.4"
+    },
+    "dependencies": {
+        "@antv/g6": "^4.8.3",
+        "@emotion/react": "^11.10.5",
+        "@emotion/styled": "^11.10.5",
+        "@fontsource/roboto": "^4.5.8",
+        "@mui/material": "^5.11.4",
+        "react": "^18.2.0",
+        "react-dom": "^18.2.0"
+    }
+}

frontend/shell.nix

@@ -0,0 +1,8 @@
+{ pkgs ? import <nixpkgs> {} }:
+
+pkgs.mkShell {
+  buildInputs = [
+    pkgs.yarn
+  ];
+}
+

frontend/src/app.tsx

@@ -0,0 +1,13 @@
+import * as React from 'react';
+import { createRoot } from 'react-dom/client';
+
+import '@fontsource/roboto/300.css';
+import '@fontsource/roboto/400.css';
+import '@fontsource/roboto/500.css';
+import '@fontsource/roboto/700.css';
+
+import App from './components/app.tsx';
+
+const container = document.getElementById('app');
+const root = createRoot(container);
+root.render(<App />);

frontend/src/components/app.tsx

@@ -0,0 +1,176 @@
+import * as React from 'react';
+
+import { ThemeProvider, createTheme } from '@mui/material/styles';
+import {
+  Backdrop,
+  Button,
+  CircularProgress,
+  CssBaseline,
+  Container,
+  FormControl,
+  FormControlLabel,
+  FormLabel,
+  Link,
+  Pagination,
+  Paper,
+  Radio,
+  RadioGroup,
+  Typography,
+  TextField,
+} from '@mui/material';
+
+import GraphG6 from './graph-g6.tsx';
+
+const { useState, useCallback } = React;
+
+const darkTheme = createTheme({
+  palette: {
+    mode: 'dark',
+  },
+});
+
+const placeholder = `s(a).
+s(b).
+s(c).
+s(d).
+ac(a,c(v)).
+ac(b,b).
+ac(c,and(a,b)).
+ac(d,neg(b)).`;
+
+enum Parsing {
+  Naive = 'Naive',
+  Hybrid = 'Hybrid',
+}
+
+enum Strategy {
+  ParseOnly = 'ParseOnly',
+  Ground = 'Ground',
+  Complete = 'Complete',
+  Stable = 'Stable',
+  StableCountingA = 'StableCountingA',
+  StableCountingB = 'StableCountingB',
+  StableNogood = 'StableNogood',
+}
+
+function App() {
+  const [loading, setLoading] = useState(false);
+  const [code, setCode] = useState(placeholder);
+  const [parsing, setParsing] = useState(Parsing.Naive);
+  const [graphs, setGraphs] = useState();
+  const [graphIndex, setGraphIndex] = useState(0);
+
+  const submitHandler = useCallback(
+    (strategy: Strategy) => {
+      setLoading(true);
+
+      fetch(`${process.env.NODE_ENV === 'development' ? '//localhost:8080' : ''}/solve`, {
+        method: 'POST',
+        headers: {
+          'Content-Type': 'application/json',
+        },
+        body: JSON.stringify({ code, strategy, parsing }),
+      })
+        .then((res) => res.json())
+        .then((data) => {
+          setGraphs(data);
+          setGraphIndex(0);
+        })
+        .finally(() => setLoading(false));
+      // TODO: error handling
+    },
+    [code, parsing],
+  );
+
+  return (
+    <ThemeProvider theme={darkTheme}>
+      <CssBaseline />
+      <main>
+        <Typography variant="h2" component="h1" align="center" gutterBottom>
+          Solve your ADF Problem with OBDDs!
+        </Typography>
+
+        <Container>
+          <TextField
+            name="code"
+            label="Put your code here:"
+            helperText={(
+              <>
+                For more info on the syntax, have a
+                look
+                {' '}
+                <Link href="https://github.com/ellmau/adf-obdd" target="_blank" rel="noreferrer">here</Link>
+                .
+              </>
+            )}
+            multiline
+            fullWidth
+            variant="filled"
+            value={code}
+            onChange={(event) => { setCode(event.target.value); }}
+          />
+        </Container>
+        <Container sx={{ marginTop: 2, marginBottom: 2 }}>
+          <FormControl>
+            <FormLabel id="parsing-radio-group">Parsing Strategy</FormLabel>
+            <RadioGroup
+              row
+              aria-labelledby="parsing-radio-group"
+              name="parsing"
+              value={parsing}
+              onChange={(e) => setParsing((e.target as HTMLInputElement).value)}
+            >
+              <FormControlLabel value={Parsing.Naive} control={<Radio />} label="Naive" />
+              <FormControlLabel value={Parsing.Hybrid} control={<Radio />} label="Hybrid" />
+            </RadioGroup>
+          </FormControl>
+          <br />
+          <br />
+          <Button variant="outlined" onClick={() => submitHandler(Strategy.ParseOnly)}>Parse only</Button>
+          {' '}
+          <Button variant="outlined" onClick={() => submitHandler(Strategy.Ground)}>Grounded Model</Button>
+          {' '}
+          <Button variant="outlined" onClick={() => submitHandler(Strategy.Complete)}>Complete Models</Button>
+          {' '}
+          <Button variant="outlined" onClick={() => submitHandler(Strategy.Stable)}>Stable Models (naive heuristics)</Button>
+          {' '}
+          <Button disabled={parsing !== Parsing.Hybrid} variant="outlined" onClick={() => submitHandler(Strategy.StableCountingA)}>Stable Models (counting heuristic A)</Button>
+          {' '}
+          <Button disabled={parsing !== Parsing.Hybrid} variant="outlined" onClick={() => submitHandler(Strategy.StableCountingB)}>Stable Models (counting heuristic B)</Button>
+          {' '}
+          <Button variant="outlined" onClick={() => submitHandler(Strategy.StableNogood)}>Stable Models using nogoods (Simple Heuristic)</Button>
+        </Container>
+
+        {graphs
+        && (
+        <Container sx={{ marginTop: 4, marginBottom: 4 }}>
+          {graphs.length > 1
+            && (
+            <>
+              Models:
+              <br />
+              <Pagination variant="outlined" shape="rounded" count={graphs.length} page={graphIndex + 1} onChange={(e, value) => setGraphIndex(value - 1)} />
+            </>
+            )}
+          {graphs.length > 0
+            && (
+            <Paper elevation={3} square sx={{ marginTop: 4, marginBottom: 4 }}>
+              <GraphG6 graph={graphs[graphIndex]} />
+            </Paper>
+            )}
+          {graphs.length === 0
+            && <>No models!</>}
+        </Container>
+        )}
+      </main>
+
+      <Backdrop
+        open={loading}
+      >
+        <CircularProgress color="inherit" />
+      </Backdrop>
+    </ThemeProvider>
+  );
+}
+
+export default App;

frontend/src/components/graph-g6.tsx

@@ -0,0 +1,374 @@
+import React, { useEffect, useRef } from 'react';
+
+import G6 from '@antv/g6';
+
+G6.registerNode('nodeWithFlag', {
+  draw(cfg, group) {
+    const mainWidth = Math.max(30, 5 * cfg.mainLabel.length + 10);
+    const mainHeight = 30;
+
+    const keyShape = group.addShape('rect', {
+      attrs: {
+        width: mainWidth,
+        height: mainHeight,
+        radius: 2,
+        fill: 'white',
+        stroke: 'black',
+        cursor: 'pointer',
+      },
+      name: 'rectMainLabel',
+      draggable: true,
+    });
+
+    group.addShape('text', {
+      attrs: {
+        x: mainWidth / 2,
+        y: mainHeight / 2,
+        textAlign: 'center',
+        textBaseline: 'middle',
+        text: cfg.mainLabel,
+        fill: '#212121',
+        fontFamily: 'Roboto',
+        cursor: 'pointer',
+      },
+      // must be assigned in G6 3.3 and later versions. it can be any value you want
+      name: 'textMailLabel',
+      // allow the shape to response the drag events
+      draggable: true,
+    });
+
+    if (cfg.subLabel) {
+      const subWidth = 5 * cfg.subLabel.length + 4;
+      const subHeight = 20;
+
+      const subRectX = mainWidth - 4;
+      const subRectY = -subHeight + 4;
+
+      group.addShape('rect', {
+        attrs: {
+          x: subRectX,
+          y: subRectY,
+          width: subWidth,
+          height: subHeight,
+          radius: 1,
+          fill: '#4caf50',
+          stroke: '#1b5e20',
+          cursor: 'pointer',
+        },
+        name: 'rectMainLabel',
+        draggable: true,
+      });
+
+      group.addShape('text', {
+        attrs: {
+          x: subRectX + subWidth / 2,
+          y: subRectY + subHeight / 2,
+          textAlign: 'center',
+          textBaseline: 'middle',
+          text: cfg.subLabel,
+          fill: '#212121',
+          fontFamily: 'Roboto',
+          fontSize: 10,
+          cursor: 'pointer',
+        },
+        // must be assigned in G6 3.3 and later versions. it can be any value you want
+        name: 'textMailLabel',
+        // allow the shape to response the drag events
+        draggable: true,
+      });
+    }
+
+    return keyShape;
+  },
+  getAnchorPoints() {
+    return [[0.5, 0], [0, 0.5], [1, 0.5], [0.5, 1]];
+  },
+  // nodeStateStyles: {
+  // hover: {
+  // fill: 'lightsteelblue',
+  // },
+  // highlight: {
+  // lineWidth: 3,
+  // },
+  // lowlight: {
+  // opacity: 0.3,
+  // },
+  // },
+  setState(name, value, item) {
+    const group = item.getContainer();
+    const mainShape = group.get('children')[0]; // Find the first graphics shape of the node. It is determined by the order of being added
+    const subShape = group.get('children')[2];
+
+    if (name === 'hover') {
+      if (value) {
+        mainShape.attr('fill', 'lightsteelblue');
+      } else {
+        mainShape.attr('fill', 'white');
+      }
+    }
+
+    if (name === 'highlight') {
+      if (value) {
+        mainShape.attr('lineWidth', 3);
+      } else {
+        mainShape.attr('lineWidth', 1);
+      }
+    }
+
+    if (name === 'lowlight') {
+      if (value) {
+        mainShape.attr('opacity', 0.3);
+        if (subShape) {
+          subShape.attr('opacity', 0.3);
+        }
+      } else {
+        mainShape.attr('opacity', 1);
+        if (subShape) {
+          subShape.attr('opacity', 1);
+        }
+      }
+    }
+  },
+});
+
+interface GraphProps {
+  lo_edges: [number, number][],
+  hi_edges: [number, number][],
+  node_labels: { [key: number]: string },
+  tree_root_labels: { [key: number]: string[] },
+}
+
+function nodesAndEdgesFromGraphProps(graphProps: GraphProps) {
+  const nodes = Object.keys(graphProps.node_labels).map((id) => {
+    const mainLabel = graphProps.node_labels[id];
+    const subLabel = graphProps.tree_root_labels[id].length > 0 ? `Root for: ${graphProps.tree_root_labels[id].join(' ; ')}` : undefined;
+
+    // const label = subLabel.length > 0 ? `${mainLabel}\n${subLabel}` : mainLabel;
+
+    return {
+      id: id.toString(),
+      mainLabel,
+      subLabel,
+      // style: {
+      // height: subLabel.length > 0 ? 60 : 30,
+      // width: Math.max(30, 5 * mainLabel.length + 10, 5 * subLabel.length + 10),
+      // },
+    };
+  });
+  const edges = graphProps.lo_edges.map(([source, target]) => ({
+    id: `LO_${source}_${target}`, source: source.toString(), target: target.toString(), style: { stroke: '#ed6c02', lineWidth: 2 },
+  }))
+    .concat(graphProps.hi_edges.map(([source, target]) => ({
+      id: `HI_${source}_${target}`, source: source.toString(), target: target.toString(), style: { stroke: '#1976d2', lineWidth: 2 },
+    })));
+
+  return { nodes, edges };
+}
+
+interface Props {
+  graph: GraphProps,
+}
+
+function GraphG6(props: Props) {
+  const { graph: graphProps } = props;
+
+  const ref = useRef(null);
+
+  const graphRef = useRef();
+
+  useEffect(
+    () => {
+      if (!graphRef.current) {
+        graphRef.current = new G6.Graph({
+          container: ref.current,
+          width: 1200,
+          height: 600,
+          fitView: true,
+          rankdir: 'TB',
+          align: 'DR',
+          nodesep: 100,
+          ranksep: 100,
+          modes: {
+            default: ['drag-canvas', 'zoom-canvas', 'drag-node'],
+          },
+          layout: { type: 'dagre' },
+          // defaultNode: {
+          // anchorPoints: [[0.5, 0], [0, 0.5], [1, 0.5], [0.5, 1]],
+          // type: 'rect',
+          // style: {
+          // radius: 2,
+          // },
+          // labelCfg: {
+          // style: {
+          /// / fontWeight: 700,
+          // fontFamily: 'Roboto',
+          // },
+          // },
+          // },
+          defaultNode: { type: 'nodeWithFlag' },
+          defaultEdge: {
+            style: {
+              endArrow: true,
+            },
+          },
+          // nodeStateStyles: {
+          // hover: {
+          // fill: 'lightsteelblue',
+          // },
+          // highlight: {
+          // lineWidth: 3,
+          // },
+          // lowlight: {
+          // opacity: 0.3,
+          // },
+          // },
+          edgeStateStyles: {
+            lowlight: {
+              opacity: 0.3,
+            },
+          },
+          animate: true,
+          animateCfg: {
+            duration: 500,
+            easing: 'easePolyInOut',
+          },
+        });
+      }
+
+      const graph = graphRef.current;
+
+      // Mouse enter a node
+      graph.on('node:mouseenter', (e) => {
+        const nodeItem = e.item; // Get the target item
+        graph.setItemState(nodeItem, 'hover', true); // Set the state 'hover' of the item to be true
+      });
+
+      // Mouse leave a node
+      graph.on('node:mouseleave', (e) => {
+        const nodeItem = e.item; // Get the target item
+        graph.setItemState(nodeItem, 'hover', false); // Set the state 'hover' of the item to be false
+      });
+    },
+    [],
+  );
+
+  useEffect(
+    () => {
+      const graph = graphRef.current;
+
+      // Click a node
+      graph.on('node:click', (e) => {
+        const nodeItem = e.item; // et the clicked item
+
+        let onlyRemoveStates = false;
+        if (nodeItem.hasState('highlight')) {
+          onlyRemoveStates = true;
+        }
+
+        const clickNodes = graph.findAllByState('node', 'highlight');
+        clickNodes.forEach((cn) => {
+          graph.setItemState(cn, 'highlight', false);
+        });
+
+        const lowlightNodes = graph.findAllByState('node', 'lowlight');
+        lowlightNodes.forEach((cn) => {
+          graph.setItemState(cn, 'lowlight', false);
+        });
+        const lowlightEdges = graph.findAllByState('edge', 'lowlight');
+        lowlightEdges.forEach((cn) => {
+          graph.setItemState(cn, 'lowlight', false);
+        });
+
+        if (onlyRemoveStates) {
+          return;
+        }
+
+        graph.getNodes().forEach((node) => {
+          graph.setItemState(node, 'lowlight', true);
+        });
+        graph.getEdges().forEach((edge) => {
+          graph.setItemState(edge, 'lowlight', true);
+        });
+
+        const relevantNodeIds = [];
+        const relevantLoEdges = [];
+        const relevantHiEdges = [];
+        let newNodeIds = [nodeItem.getModel().id];
+        let newLoEdges = [];
+        let newHiEdges = [];
+
+        while (newNodeIds.length > 0 || newLoEdges.length > 0 || newHiEdges.length > 0) {
+          relevantNodeIds.push(...newNodeIds);
+          relevantLoEdges.push(...newLoEdges);
+          relevantHiEdges.push(...newHiEdges);
+
+          newLoEdges = graphProps.lo_edges
+            .filter((edge) => relevantNodeIds.includes(edge[0].toString())
+              && !relevantLoEdges.includes(edge));
+          newHiEdges = graphProps.hi_edges
+            .filter((edge) => relevantNodeIds.includes(edge[0].toString())
+              && !relevantHiEdges.includes(edge));
+
+          newNodeIds = newLoEdges
+            .concat(newHiEdges)
+            .map((edge) => edge[1].toString())
+            .filter((id) => !relevantNodeIds.includes(id));
+        }
+
+        const relevantEdgeIds = relevantLoEdges
+          .map(([source, target]) => `LO_${source}_${target}`)
+          .concat(
+            relevantHiEdges
+              .map(([source, target]) => `HI_${source}_${target}`),
+          );
+
+        relevantNodeIds
+          .forEach((id) => {
+            graph.setItemState(id, 'lowlight', false);
+            graph.setItemState(id, 'highlight', true);
+          });
+
+        relevantEdgeIds
+          .forEach((id) => {
+            graph.setItemState(id, 'lowlight', false);
+          });
+
+        // graph.setItemState(nodeItem, 'lowlight', false);
+        // graph.setItemState(nodeItem, 'highlight', true);
+        // nodeItem.getEdges().forEach((edge) => {
+        // graph.setItemState(edge, 'lowlight', false);
+        // });
+      });
+
+      return () => { graph.off('node:click'); };
+    },
+    [graphProps],
+  );
+
+  useEffect(
+    () => {
+      const graph = graphRef.current;
+
+      const { nodes, edges } = nodesAndEdgesFromGraphProps(graphProps);
+
+      graph.changeData({
+        nodes,
+        edges,
+      });
+    },
+    [graphProps],
+  );
+
+  return (
+    <>
+      <div ref={ref} style={{ overflow: 'hidden' }} />
+      <div style={{ padding: 4 }}>
+        <span style={{ color: '#ed6c02', marginRight: 8 }}>lo edge (condition is false)</span>
+        {' '}
+        <span style={{ color: '#1976d2' }}>hi edge (condition is true)</span>
+      </div>
+    </>
+  );
+}
+
+export default GraphG6;

frontend/src/index.html

@@ -0,0 +1,13 @@
+<!doctype html>
+<html lang="en">
+  <head>
+    <meta charset="utf-8"/>
+    <meta name="viewport" content="initial-scale=1, width=device-width" />
+    <title>ADF-OBDD Web Visualizer</title>
+    <script type="module" src="app.tsx"></script>
+  </head>
+  <body>
+    <div id="app"></div>
+  </body>
+</html>
+

frontend/src/test-data.ts

@@ -0,0 +1,19 @@
+const testData = [
+  { label: 'BOT', lo: 0, hi: 0 },
+  { label: 'TOP', lo: 1, hi: 1 },
+  { label: 'Var8', lo: 0, hi: 1 },
+  { label: 'Var7', lo: 1, hi: 0 },
+  { label: 'Var0', lo: 3, hi: 1 },
+  { label: 'Var9', lo: 0, hi: 1 },
+  { label: 'Var8', lo: 5, hi: 0 },
+  { label: 'Var0', lo: 6, hi: 5 },
+  { label: 'Var1', lo: 0, hi: 1 },
+  { label: 'Var0', lo: 1, hi: 0 },
+  { label: 'Var9', lo: 1, hi: 0 },
+  { label: 'Var8', lo: 0, hi: 10 },
+  { label: 'Var0', lo: 5, hi: 0 },
+  { label: 'Var8', lo: 1, hi: 0 },
+  { label: 'Var5', lo: 13, hi: 0 },
+];
+
+export default testData;

lib/src/adf.rs

@@ -7,6 +7,7 @@ This module describes the abstract dialectical framework.
 
 pub mod heuristics;
 use std::cell::RefCell;
+use std::collections::{HashMap, HashSet};
 
 use crate::{
     datatypes::{
@@ -37,6 +38,18 @@ pub struct Adf {
     rng: RefCell<StdRng>,
 }
 
+#[derive(Serialize, Debug)]
+/// This is a DTO for the graph output
+pub struct DoubleLabeledGraph {
+    // number of nodes equals the number of node labels
+    // nodes implicitly have their index as their ID
+    node_labels: HashMap<usize, String>,
+    // every node gets this label containing multiple entries (it might be empty)
+    tree_root_labels: HashMap<usize, Vec<String>>,
+    lo_edges: Vec<(usize, usize)>,
+    hi_edges: Vec<(usize, usize)>,
+}
+
 impl Default for Adf {
     fn default() -> Self {
         Self {
@@ -919,6 +932,104 @@ impl Adf {
         log::info!("{ng_store}");
         log::debug!("{:?}", ng_store);
     }
+
+    /// Turns Adf into solved graph representation
+    pub fn into_double_labeled_graph(&self, ac: Option<&Vec<Term>>) -> DoubleLabeledGraph {
+        let ac: &Vec<Term> = match ac {
+            Some(ac) => ac,
+            None => &self.ac,
+        };
+
+        let mut node_indices: HashSet<usize> = HashSet::new();
+        let mut new_node_indices: HashSet<usize> = ac.iter().map(|term| term.value()).collect();
+
+        while !new_node_indices.is_empty() {
+            node_indices = node_indices.union(&new_node_indices).copied().collect();
+            new_node_indices = HashSet::new();
+
+            for node_index in &node_indices {
+                let lo_node_index = self.bdd.nodes[*node_index].lo().value();
+                if !node_indices.contains(&lo_node_index) {
+                    new_node_indices.insert(lo_node_index);
+                }
+
+                let hi_node_index = self.bdd.nodes[*node_index].hi().value();
+                if !node_indices.contains(&hi_node_index) {
+                    new_node_indices.insert(hi_node_index);
+                }
+            }
+        }
+
+        let node_labels: HashMap<usize, String> = self
+            .bdd
+            .nodes
+            .iter()
+            .enumerate()
+            .filter(|(i, _)| node_indices.contains(i))
+            .map(|(i, &node)| {
+                let value_part = match node.var() {
+                    Var::TOP => "TOP".to_string(),
+                    Var::BOT => "BOT".to_string(),
+                    _ => self.ordering.name(node.var()).expect(
+                        "name for each var should exist; special cases are handled separately",
+                    ),
+                };
+
+                (i, value_part)
+            })
+            .collect();
+
+        let tree_root_labels: HashMap<usize, Vec<String>> = ac.iter().enumerate().fold(
+            self.bdd
+                .nodes
+                .iter()
+                .enumerate()
+                .filter(|(i, _)| node_indices.contains(i))
+                .map(|(i, _)| (i, vec![]))
+                .collect(),
+            |mut acc, (root_for, root_node)| {
+                acc.get_mut(&root_node.value())
+                    .expect("we know that the index will be in the map")
+                    .push(self.ordering.name(Var(root_for)).expect(
+                        "name for each var should exist; special cases are handled separately",
+                    ));
+
+                acc
+            },
+        );
+
+        let lo_edges: Vec<(usize, usize)> = self
+            .bdd
+            .nodes
+            .iter()
+            .enumerate()
+            .filter(|(i, _)| node_indices.contains(i))
+            .filter(|(_, node)| !vec![Var::TOP, Var::BOT].contains(&node.var()))
+            .map(|(i, &node)| (i, node.lo().value()))
+            .collect();
+
+        let hi_edges: Vec<(usize, usize)> = self
+            .bdd
+            .nodes
+            .iter()
+            .enumerate()
+            .filter(|(i, _)| node_indices.contains(i))
+            .filter(|(_, node)| !vec![Var::TOP, Var::BOT].contains(&node.var()))
+            .map(|(i, &node)| (i, node.hi().value()))
+            .collect();
+
+        log::debug!("{:?}", node_labels);
+        log::debug!("{:?}", tree_root_labels);
+        log::debug!("{:?}", lo_edges);
+        log::debug!("{:?}", hi_edges);
+
+        DoubleLabeledGraph {
+            node_labels,
+            tree_root_labels,
+            lo_edges,
+            hi_edges,
+        }
+    }
 }
 
 #[cfg(test)]

server/Cargo.toml

@@ -0,0 +1,25 @@
+[package]
+name = "adf-bdd-server"
+version = "0.3.0"
+authors = ["Lukas Gerlach <lukas.gerlach@tu-dresden.de>"]
+edition = "2021"
+homepage = "https://ellmau.github.io/adf-obdd"
+repository = "https://github.com/ellmau/adf-obdd"
+license = "MIT"
+exclude = ["res/", "./flake*", "*.nix", ".envrc", "_config.yml", "tarpaulin-report.*", "*~"]
+description = "Offer Solving ADFs as a service"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+adf_bdd = { version="0.3.1", path="../lib", features = ["frontend"] }
+actix-web = "4"
+actix-cors = "0.6"
+actix-files = "0.6"
+env_logger = "0.9"
+log = "0.4"
+serde = "1"
+
+[features]
+cors_for_local_development = []
+

server/src/main.rs

@@ -0,0 +1,136 @@
+use actix_files as fs;
+use actix_web::{post, web, App, HttpServer, Responder};
+use serde::{Deserialize, Serialize};
+
+#[cfg(feature = "cors_for_local_development")]
+use actix_cors::Cors;
+#[cfg(feature = "cors_for_local_development")]
+use actix_web::http;
+
+use adf_bdd::adf::{Adf, DoubleLabeledGraph};
+use adf_bdd::adfbiodivine::Adf as BdAdf;
+use adf_bdd::parser::AdfParser;
+
+#[derive(Deserialize)]
+enum Parsing {
+    Naive,
+    Hybrid,
+}
+
+#[derive(Deserialize)]
+enum Strategy {
+    ParseOnly,
+    Ground,
+    Complete,
+    Stable,
+    StableCountingA,
+    StableCountingB,
+    StableNogood,
+}
+
+#[derive(Deserialize)]
+struct SolveReqBody {
+    code: String,
+    parsing: Parsing,
+    strategy: Strategy,
+}
+
+#[derive(Serialize)]
+struct SolveResBody {
+    graph: DoubleLabeledGraph,
+}
+
+#[post("/solve")]
+async fn solve(req_body: web::Json<SolveReqBody>) -> impl Responder {
+    let input = &req_body.code;
+    let parsing = &req_body.parsing;
+    let strategy = &req_body.strategy;
+
+    let parser = AdfParser::default();
+    match parser.parse()(input) {
+        Ok(_) => log::info!("[Done] parsing"),
+        Err(e) => {
+            log::error!("Error during parsing:\n{} \n\n cannot continue, panic!", e);
+            panic!("Parsing failed, see log for further details")
+        }
+    }
+
+    let mut adf = match parsing {
+        Parsing::Naive => Adf::from_parser(&parser),
+        Parsing::Hybrid => {
+            let bd_adf = BdAdf::from_parser(&parser);
+            log::info!("[Start] translate into naive representation");
+            let naive_adf = bd_adf.hybrid_step_opt(false);
+            log::info!("[Done] translate into naive representation");
+
+            naive_adf
+        }
+    };
+
+    log::debug!("{:?}", adf);
+
+    let acs = match strategy {
+        Strategy::ParseOnly => vec![None],
+        Strategy::Ground => vec![Some(adf.grounded())],
+        Strategy::Complete => adf.complete().map(Some).collect(),
+        Strategy::Stable => adf.stable().map(Some).collect(),
+        // TODO: INPUT VALIDATION: only allow this for hybrid parsing
+        Strategy::StableCountingA => adf.stable_count_optimisation_heu_a().map(Some).collect(),
+        // TODO: INPUT VALIDATION: only allow this for hybrid parsing
+        Strategy::StableCountingB => adf.stable_count_optimisation_heu_b().map(Some).collect(),
+        // TODO: support more than just default heuristics
+        Strategy::StableNogood => adf
+            .stable_nogood(adf_bdd::adf::heuristics::Heuristic::default())
+            .map(Some)
+            .collect(),
+    };
+
+    let dto: Vec<DoubleLabeledGraph> = acs
+        .iter()
+        .map(|ac| adf.into_double_labeled_graph(ac.as_ref()))
+        .collect();
+
+    web::Json(dto)
+}
+
+#[actix_web::main]
+async fn main() -> std::io::Result<()> {
+    env_logger::builder()
+        .filter_level(log::LevelFilter::Debug)
+        .init();
+
+    #[cfg(feature = "cors_for_local_development")]
+    let server = HttpServer::new(|| {
+        let cors = Cors::default()
+            .allowed_origin("http://localhost:1234")
+            .allowed_methods(vec!["GET", "POST"])
+            .allowed_headers(vec![
+                http::header::AUTHORIZATION,
+                http::header::ACCEPT,
+                http::header::CONTENT_TYPE,
+            ])
+            .max_age(3600);
+
+        App::new()
+            .wrap(cors)
+            .service(solve)
+            // this mus be last to not override anything
+            .service(fs::Files::new("/", "./assets").index_file("index.html"))
+    })
+    .bind(("0.0.0.0", 8080))?
+    .run()
+    .await;
+
+    #[cfg(not(feature = "cors_for_local_development"))]
+    let server = HttpServer::new(|| {
+        App::new()
+            .service(solve)
+            // this mus be last to not override anything
+            .service(fs::Files::new("/", "./assets").index_file("index.html"))
+    })
+    .bind(("0.0.0.0", 8080))?
+    .run()
+    .await;
+
+    server
+}