Animate graph changes

* Bump predicates from 2.1.1 to 2.1.5

Bumps [predicates](https://github.com/assert-rs/predicates-rs) from 2.1.1 to 2.1.5.
- [Release notes](https://github.com/assert-rs/predicates-rs/releases)
- [Changelog](https://github.com/assert-rs/predicates-rs/blob/master/CHANGELOG.md)
- [Commits](https://github.com/assert-rs/predicates-rs/compare/v2.1.1...v2.1.5)

---
updated-dependencies:
- dependency-name: predicates
  dependency-type: direct:production
  update-type: version-update:semver-patch
...

Signed-off-by: dependabot[bot] <support@github.com>

* Bump serde from 1.0.147 to 1.0.152

Bumps [serde](https://github.com/serde-rs/serde) from 1.0.147 to 1.0.152.
- [Release notes](https://github.com/serde-rs/serde/releases)
- [Commits](https://github.com/serde-rs/serde/compare/v1.0.147...v1.0.152)

---
updated-dependencies:
- dependency-name: serde
  dependency-type: direct:production
  update-type: version-update:semver-patch
...

Signed-off-by: dependabot[bot] <support@github.com>

* Bump serde_json from 1.0.87 to 1.0.91

Bumps [serde_json](https://github.com/serde-rs/json) from 1.0.87 to 1.0.91.
- [Release notes](https://github.com/serde-rs/json/releases)
- [Commits](https://github.com/serde-rs/json/compare/v1.0.87...v1.0.91)

---
updated-dependencies:
- dependency-name: serde_json
  dependency-type: direct:production
  update-type: version-update:semver-patch
...

Signed-off-by: dependabot[bot] <support@github.com>

* Bump clap from 4.0.18 to 4.0.32

Bumps [clap](https://github.com/clap-rs/clap) from 4.0.18 to 4.0.32.
- [Release notes](https://github.com/clap-rs/clap/releases)
- [Changelog](https://github.com/clap-rs/clap/blob/master/CHANGELOG.md)
- [Commits](https://github.com/clap-rs/clap/compare/v4.0.18...v4.0.32)

---
updated-dependencies:
- dependency-name: clap
  dependency-type: direct:production
  update-type: version-update:semver-patch
...

Signed-off-by: dependabot[bot] <support@github.com>

* Bump assert_fs from 1.0.7 to 1.0.10

Bumps [assert_fs](https://github.com/assert-rs/assert_fs) from 1.0.7 to 1.0.10.
- [Release notes](https://github.com/assert-rs/assert_fs/releases)
- [Changelog](https://github.com/assert-rs/assert_fs/blob/master/CHANGELOG.md)
- [Commits](https://github.com/assert-rs/assert_fs/compare/v1.0.7...v1.0.10)

---
updated-dependencies:
- dependency-name: assert_fs
  dependency-type: direct:production
  update-type: version-update:semver-patch
...

Signed-off-by: dependabot[bot] <support@github.com>

* Update to NixOS 22.11

* flake.lock: Update

Flake lock file updates:

• Updated input 'nixpkgs-unstable':
    'github:NixOS/nixpkgs/fc07622617a373a742ed96d4dd536849d4bc1ec6' (2022-11-13)
  → 'github:NixOS/nixpkgs/677ed08a50931e38382dbef01cba08a8f7eac8f6' (2022-12-29)
• Updated input 'rust-overlay':
    'github:oxalica/rust-overlay/2342f70f7257046effc031333c4cfdea66c91d82' (2022-11-15)
  → 'github:oxalica/rust-overlay/c8bf9c162bb3f734cf357846e995eb70b94e2bcd' (2023-01-02)

* Fix clippy issue in testcase-builder

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>

.dockerignore

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

Cargo.toml

@@ -1,7 +1,7 @@
 [workspace]
-members=[ "lib", "bin" ]
+members=[ "lib", "bin", "server" ]
 default-members = [ "lib" ]
 
 [profile.release]
 lto = "fat"
-codegen-units = 1
+codegen-units = 1

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"]
+

bin/Cargo.toml

@@ -17,7 +17,7 @@ path = "src/main.rs"
 
 [dependencies]
 adf_bdd = { version="0.3.1", path="../lib", default-features = false }
-clap = {version = "3.2.16", features = [ "derive", "cargo", "env" ]}
+clap = {version = "4.0.32", features = [ "derive", "cargo", "env" ]}
 log = { version = "0.4", features = [ "max_level_trace", "release_max_level_info" ] }
 serde = { version = "1.0", features = ["derive","rc"] }
 serde_json = "1.0"

bin/src/main.rs

@@ -87,70 +87,70 @@ use crossbeam_channel::unbounded;
 use strum::VariantNames;
 
 #[derive(Parser, Debug)]
-#[clap(author, version, about)]
+#[command(author, version, about)]
 struct App {
     /// Input filename
-    #[clap(parse(from_os_str))]
+    #[arg(value_parser)]
     input: PathBuf,
     /// Sets the verbosity to 'warn', 'info', 'debug' or 'trace' if -v and -q are not use
-    #[clap(long = "rust_log", env)]
+    #[arg(long = "rust_log", env)]
     rust_log: Option<String>,
     /// Choose the bdd implementation of either 'biodivine', 'naive', or hybrid
-    #[clap(long = "lib", default_value = "hybrid")]
+    #[arg(long = "lib", default_value = "hybrid")]
     implementation: String,
     /// Sets log verbosity (multiple times means more verbose)
-    #[clap(short, parse(from_occurrences), group = "verbosity")]
+    #[arg(short, action = clap::builder::ArgAction::Count, group = "verbosity")]
     verbose: u8,
     /// Sets log verbosity to only errors
-    #[clap(short, group = "verbosity")]
+    #[arg(short, group = "verbosity")]
     quiet: bool,
     /// Sorts variables in an lexicographic manner
-    #[clap(long = "lx", group = "sorting")]
+    #[arg(long = "lx", group = "sorting")]
     sort_lex: bool,
     /// Sorts variables in an alphanumeric manner
-    #[clap(long = "an", group = "sorting")]
+    #[arg(long = "an", group = "sorting")]
     sort_alphan: bool,
     /// Compute the grounded model
-    #[clap(long = "grd")]
+    #[arg(long = "grd")]
     grounded: bool,
     /// Compute the stable models
-    #[clap(long = "stm")]
+    #[arg(long = "stm")]
     stable: bool,
     /// Compute the stable models with the help of modelcounting using heuristics a
-    #[clap(long = "stmca")]
+    #[arg(long = "stmca")]
     stable_counting_a: bool,
     /// Compute the stable models with the help of modelcounting using heuristics b
-    #[clap(long = "stmcb")]
+    #[arg(long = "stmcb")]
     stable_counting_b: bool,
     /// Compute the stable models with a pre-filter (only hybrid lib-mode)
-    #[clap(long = "stmpre")]
+    #[arg(long = "stmpre")]
     stable_pre: bool,
     /// Compute the stable models with a single-formula rewriting (only hybrid lib-mode)
-    #[clap(long = "stmrew")]
+    #[arg(long = "stmrew")]
     stable_rew: bool,
     /// Compute the stable models with a single-formula rewriting on internal representation(only hybrid lib-mode)
-    #[clap(long = "stmrew2")]
+    #[arg(long = "stmrew2")]
     stable_rew2: bool,
     /// Compute the stable models with the nogood-learning based approach
-    #[clap(long = "stmng")]
+    #[arg(long = "stmng")]
     stable_ng: bool,
     /// Choose which heuristics shall be used by the nogood-learning approach
-    #[clap(long, possible_values = adf_bdd::adf::heuristics::Heuristic::VARIANTS.iter().filter(|&v| v != &"Custom"))]
+    #[arg(long, value_parser = clap::builder::PossibleValuesParser::new(adf_bdd::adf::heuristics::Heuristic::VARIANTS.iter().filter(|&v| v != &"Custom").collect::<Vec<_>>()))]
     heu: Option<adf_bdd::adf::heuristics::Heuristic<'static>>,
     /// Compute the two valued models with the nogood-learning based approach
-    #[clap(long = "twoval")]
+    #[arg(long = "twoval")]
     two_val: bool,
     /// Compute the complete models
-    #[clap(long = "com")]
+    #[arg(long = "com")]
     complete: bool,
     /// Import an adf- bdd state instead of an adf
-    #[clap(long)]
+    #[arg(long)]
     import: bool,
     /// Export the adf-bdd state after parsing and BDD instantiation to the given filename
-    #[clap(long)]
+    #[arg(long)]
     export: Option<PathBuf>,
     /// Set if the (counter-)models shall be computed and printed, possible values are 'nai' and 'mem' for naive and memoization repectively (only works in hybrid and naive mode)
-    #[clap(long)]
+    #[arg(long)]
     counter: Option<String>,
 }
 
@@ -369,7 +369,7 @@ impl App {
                             export.to_string_lossy()
                         );
                     } else {
-                        let export_file = match File::create(&export) {
+                        let export_file = match File::create(export) {
                             Err(reason) => {
                                 panic!("couldn't create {}: {}", export.to_string_lossy(), reason)
                             }

bin/tests/cli.rs

@@ -19,9 +19,9 @@ fn arguments() -> Result<(), Box<dyn std::error::Error>> {
 
     cmd = Command::cargo_bin("adf-bdd")?;
     cmd.arg("-h");
-    cmd.assert().success().stdout(predicate::str::contains(
+    cmd.assert()
-        "stefan.ellmauthaler@tu-dresden.de",
+        .success()
-    ));
+        .stdout(predicate::str::contains("adf-bdd [OPTIONS] <INPUT>"));
 
     cmd = Command::cargo_bin("adf-bdd")?;
     cmd.arg("--version");

flake.lock

@@ -2,11 +2,11 @@
   "nodes": {
     "flake-utils": {
       "locked": {
-        "lastModified": 1656928814,
+        "lastModified": 1667395993,
-        "narHash": "sha256-RIFfgBuKz6Hp89yRr7+NR5tzIAbn52h8vT6vXkYjZoM=",
+        "narHash": "sha256-nuEHfE/LcWyuSWnS8t12N1wc105Qtau+/OdUAjtQ0rA=",
         "owner": "numtide",
         "repo": "flake-utils",
-        "rev": "7e2a3b3dfd9af950a856d66b0a7d01e3c18aa249",
+        "rev": "5aed5285a952e0b949eb3ba02c12fa4fcfef535f",
         "type": "github"
       },
       "original": {
@@ -18,11 +18,11 @@
     "gitignoresrc": {
       "flake": false,
       "locked": {
-        "lastModified": 1658402513,
+        "lastModified": 1660459072,
-        "narHash": "sha256-wk38v/mbLsOo6+IDmmH1H0ADR87iq9QTTD1BP9X2Ags=",
+        "narHash": "sha256-8DFJjXG8zqoONA1vXtgeKXy68KdJL5UaXR8NtVMUbx8=",
         "owner": "hercules-ci",
         "repo": "gitignore.nix",
-        "rev": "f2ea0f8ff1bce948ccb6b893d15d5ea3efaf1364",
+        "rev": "a20de23b925fd8264fd7fad6454652e142fd7f73",
         "type": "github"
       },
       "original": {
@@ -33,27 +33,27 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1659342832,
+        "lastModified": 1672441588,
-        "narHash": "sha256-ePnxG4hacRd6oZMk+YeCSYMNUnHCe+qPLI0/+VaTu48=",
+        "narHash": "sha256-jx5kxOyeObnVD44HRebKYL3cjWrcKhhcDmEYm0/naDY=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "e43cf1748462c81202a32b26294e9f8eefcc3462",
+        "rev": "6a0d2701705c3cf6f42c15aa92b7885f1f8a477f",
         "type": "github"
       },
       "original": {
         "owner": "NixOS",
-        "ref": "nixos-22.05",
+        "ref": "nixos-22.11",
         "repo": "nixpkgs",
         "type": "github"
       }
     },
     "nixpkgs-unstable": {
       "locked": {
-        "lastModified": 1659219666,
+        "lastModified": 1672350804,
-        "narHash": "sha256-pzYr5fokQPHv7CmUXioOhhzDy/XyWOIXP4LZvv/T7Mk=",
+        "narHash": "sha256-jo6zkiCabUBn3ObuKXHGqqORUMH27gYDIFFfLq5P4wg=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "7b9be38c7250b22d829ab6effdee90d5e40c6e5c",
+        "rev": "677ed08a50931e38382dbef01cba08a8f7eac8f6",
         "type": "github"
       },
       "original": {
@@ -82,11 +82,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1659409092,
+        "lastModified": 1672626196,
-        "narHash": "sha256-OBY2RCYZeeOA3FTYUb86BPMUBEyKEwpwhpU2QKboRJQ=",
+        "narHash": "sha256-BfdLrMqxqa4YA1I1wgPBQyu4FPzL0Tp4WI2C5S6BuYo=",
         "owner": "oxalica",
         "repo": "rust-overlay",
-        "rev": "9055cb4f33f062c0dd33aa7e3c89140da8f70057",
+        "rev": "c8bf9c162bb3f734cf357846e995eb70b94e2bcd",
         "type": "github"
       },
       "original": {

flake.nix

@@ -2,7 +2,7 @@
   description = "basic rust flake";
 
   inputs = {
-    nixpkgs.url = "github:NixOS/nixpkgs/nixos-22.05";
+    nixpkgs.url = "github:NixOS/nixpkgs/nixos-22.11";
     nixpkgs-unstable.url = "github:NixOS/nixpkgs/nixos-unstable";
     rust-overlay = {
       url = "github:oxalica/rust-overlay";
@@ -18,7 +18,8 @@
     };
   };
 
-  outputs = { self, nixpkgs, nixpkgs-unstable, flake-utils, gitignoresrc, rust-overlay, ... }@inputs:
+  outputs = { self, nixpkgs, nixpkgs-unstable, flake-utils, gitignoresrc
+    , rust-overlay, ... }@inputs:
     {
       #overlay = import ./nix { inherit gitignoresrc; };
     } // (flake-utils.lib.eachDefaultSystem (system:
@@ -26,27 +27,24 @@
         unstable = import nixpkgs-unstable { inherit system; };
         pkgs = import nixpkgs {
           inherit system;
-          overlays = [ (import rust-overlay)];
+          overlays = [ (import rust-overlay) ];
         };
-      in
+      in rec {
-      rec {
+        devShell = pkgs.mkShell {
-        devShell =
+          RUST_LOG = "debug";
-          pkgs.mkShell {
+          RUST_BACKTRACE = 1;
-            RUST_LOG = "debug";
+          buildInputs = [
-            RUST_BACKTRACE = 1;
+            pkgs.rust-bin.stable.latest.rustfmt
-            buildInputs = [
+            pkgs.rust-bin.stable.latest.default
-              pkgs.rust-bin.stable.latest.rustfmt
+            pkgs.rust-analyzer
-              pkgs.rust-bin.stable.latest.default
+            pkgs.cargo-audit
-              pkgs.rust-analyzer
+            pkgs.cargo-license
-              pkgs.cargo-audit
+            pkgs.cargo-tarpaulin
-              pkgs.cargo-license
+            pkgs.cargo-kcov
-              pkgs.cargo-tarpaulin
+            pkgs.valgrind
-              pkgs.cargo-kcov
+            pkgs.gnuplot
-              pkgs.valgrind
+            pkgs.kcov
-              pkgs.gnuplot
+          ];
-              pkgs.kcov
+        };
-            ];
+      }));
-          };
-      }
-    ));
 }

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/Cargo.toml

@@ -28,9 +28,9 @@ nom = "7.1.1"
 lexical-sort = "0.3.1"
 serde = { version = "1.0", features = ["derive","rc"] }
 serde_json = "1.0"
-biodivine-lib-bdd = "0.4.0"
+biodivine-lib-bdd = "0.4.1"
 derivative = "2.2.0"
-roaring = "0.9.0"
+roaring = "0.10.1"
 strum = { version = "0.24", features = ["derive"] }
 crossbeam-channel = "0.5"
 rand = {version = "0.8.5", features = ["std_rng"]}

lib/build.rs

@@ -15,7 +15,7 @@ fn main() {
 fn gen_tests() {
     let out_dir = env::var("OUT_DIR").unwrap();
     let destination = Path::new(&out_dir).join("tests.rs");
-    let mut test_file = File::create(&destination).unwrap();
+    let mut test_file = File::create(destination).unwrap();
 
     if let Ok(test_data_directory) = read_dir("../res/adf-instances/instances/") {
         // write test file header, put `use`, `const` etc there

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)]

lib/src/adf/heuristics.rs

@@ -11,7 +11,7 @@ use strum::{EnumString, EnumVariantNames};
 /// Return value for heuristics.
 pub type RetVal = Option<(Var, Term)>;
 /// Signature for heuristics functions.
-pub type HeuristicFn = dyn Fn(&Adf, &[Term]) -> RetVal;
+pub type HeuristicFn = dyn Fn(&Adf, &[Term]) -> RetVal + Sync;
 
 pub(crate) fn heu_simple(_adf: &Adf, interpr: &[Term]) -> Option<(Var, Term)> {
     for (idx, term) in interpr.iter().enumerate() {

lib/src/datatypes/adf.rs

@@ -148,7 +148,7 @@ impl TwoValuedInterpretationsIterator {
         let indexes = term
             .iter()
             .enumerate()
-            .filter_map(|(idx, &v)| (!v.is_truth_value()).then(|| idx))
+            .filter_map(|(idx, &v)| (!v.is_truth_value()).then_some(idx))
             .rev()
             .collect::<Vec<_>>();
         let current = term
@@ -212,7 +212,7 @@ impl ThreeValuedInterpretationsIterator {
         let indexes = term
             .iter()
             .enumerate()
-            .filter_map(|(idx, &v)| (!v.is_truth_value()).then(|| idx))
+            .filter_map(|(idx, &v)| (!v.is_truth_value()).then_some(idx))
             .rev()
             .collect::<Vec<_>>();
         let current = vec![2; indexes.len()];

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
+}