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>

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(
-        "stefan.ellmauthaler@tu-dresden.de",
-    ));
+    cmd.assert()
+        .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,
-        "narHash": "sha256-RIFfgBuKz6Hp89yRr7+NR5tzIAbn52h8vT6vXkYjZoM=",
+        "lastModified": 1667395993,
+        "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,
-        "narHash": "sha256-wk38v/mbLsOo6+IDmmH1H0ADR87iq9QTTD1BP9X2Ags=",
+        "lastModified": 1660459072,
+        "narHash": "sha256-8DFJjXG8zqoONA1vXtgeKXy68KdJL5UaXR8NtVMUbx8=",
         "owner": "hercules-ci",
         "repo": "gitignore.nix",
-        "rev": "f2ea0f8ff1bce948ccb6b893d15d5ea3efaf1364",
+        "rev": "a20de23b925fd8264fd7fad6454652e142fd7f73",
         "type": "github"
       },
       "original": {
@@ -33,27 +33,27 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1659342832,
-        "narHash": "sha256-ePnxG4hacRd6oZMk+YeCSYMNUnHCe+qPLI0/+VaTu48=",
+        "lastModified": 1672441588,
+        "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,
-        "narHash": "sha256-pzYr5fokQPHv7CmUXioOhhzDy/XyWOIXP4LZvv/T7Mk=",
+        "lastModified": 1672350804,
+        "narHash": "sha256-jo6zkiCabUBn3ObuKXHGqqORUMH27gYDIFFfLq5P4wg=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "7b9be38c7250b22d829ab6effdee90d5e40c6e5c",
+        "rev": "677ed08a50931e38382dbef01cba08a8f7eac8f6",
         "type": "github"
       },
       "original": {
@@ -82,11 +82,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1659409092,
-        "narHash": "sha256-OBY2RCYZeeOA3FTYUb86BPMUBEyKEwpwhpU2QKboRJQ=",
+        "lastModified": 1672626196,
+        "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
-      rec {
-        devShell =
-          pkgs.mkShell {
-            RUST_LOG = "debug";
-            RUST_BACKTRACE = 1;
-            buildInputs = [
-              pkgs.rust-bin.stable.latest.rustfmt
-              pkgs.rust-bin.stable.latest.default
-              pkgs.rust-analyzer
-              pkgs.cargo-audit
-              pkgs.cargo-license
-              pkgs.cargo-tarpaulin
-              pkgs.cargo-kcov
-              pkgs.valgrind
-              pkgs.gnuplot
-              pkgs.kcov
-            ];
-          };
-      }
-    ));
+      in rec {
+        devShell = pkgs.mkShell {
+          RUST_LOG = "debug";
+          RUST_BACKTRACE = 1;
+          buildInputs = [
+            pkgs.rust-bin.stable.latest.rustfmt
+            pkgs.rust-bin.stable.latest.default
+            pkgs.rust-analyzer
+            pkgs.cargo-audit
+            pkgs.cargo-license
+            pkgs.cargo-tarpaulin
+            pkgs.cargo-kcov
+            pkgs.valgrind
+            pkgs.gnuplot
+            pkgs.kcov
+          ];
+        };
+      }));
 }

frontend/package.json

@@ -8,26 +8,26 @@
         "build": "parcel build"
     },
     "devDependencies": {
-        "@types/react": "^18.0.12",
-        "@types/react-dom": "^18.0.5",
-        "@typescript-eslint/eslint-plugin": "^5.28.0",
-        "@typescript-eslint/parser": "^5.28.0",
-        "eslint": "^8.17.0",
+        "@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.26.0",
-        "eslint-plugin-jsx-a11y": "^6.5.1",
-        "eslint-plugin-react": "^7.30.0",
-        "parcel": "^2.6.0",
+        "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.7.3"
+        "typescript": "^4.9.4"
     },
     "dependencies": {
-        "@antv/g6": "^4.6.4",
-        "@emotion/react": "^11.10.0",
-        "@emotion/styled": "^11.10.0",
+        "@antv/g6": "^4.8.3",
+        "@emotion/react": "^11.10.5",
+        "@emotion/styled": "^11.10.5",
         "@fontsource/roboto": "^4.5.8",
-        "@mui/material": "^5.10.2",
-        "react": "^18.1.0",
-        "react-dom": "^18.1.0"
+        "@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/components/app.tsx

@@ -19,7 +19,7 @@ import {
   TextField,
 } from '@mui/material';
 
-import Graph from './graph.tsx';
+import GraphG6 from './graph-g6.tsx';
 
 const { useState, useCallback } = React;
 
@@ -155,7 +155,7 @@ function App() {
           {graphs.length > 0
             && (
             <Paper elevation={3} square sx={{ marginTop: 4, marginBottom: 4 }}>
-              <Graph graph={graphs[graphIndex]} />
+              <GraphG6 graph={graphs[graphIndex]} />
             </Paper>
             )}
           {graphs.length === 0

frontend/src/components/graph-g6.tsx

@@ -131,16 +131,45 @@ G6.registerNode('nodeWithFlag', {
   },
 });
 
-interface Props {
-  graph: {
-    lo_edges: [number, number][],
-    hi_edges: [number, number][],
-    node_labels: { [key: number]: string },
-    tree_root_labels: { [key: number]: string[] },
-  }
+interface GraphProps {
+  lo_edges: [number, number][],
+  hi_edges: [number, number][],
+  node_labels: { [key: number]: string },
+  tree_root_labels: { [key: number]: string[] },
 }
 
-function Graph(props: Props) {
+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);
@@ -198,6 +227,11 @@ function Graph(props: Props) {
               opacity: 0.3,
             },
           },
+          animate: true,
+          animateCfg: {
+            duration: 500,
+            easing: 'easePolyInOut',
+          },
         });
       }
 
@@ -315,34 +349,12 @@ function Graph(props: Props) {
     () => {
       const graph = graphRef.current;
 
-      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 { nodes, edges } = nodesAndEdgesFromGraphProps(graphProps);
 
-        // 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 },
-        })));
-
-      graph.data({
+      graph.changeData({
         nodes,
         edges,
       });
-      graph.render();
     },
     [graphProps],
   );
@@ -359,4 +371,4 @@ function Graph(props: Props) {
   );
 }
 
-export default Graph;
+export default GraphG6;

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/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()];