1
0
mirror of https://github.com/ellmau/adf-obdd.git synced 2025-12-20 09:39:38 +01:00

Compare commits

...

25 Commits

Author SHA1 Message Date
monsterkrampe
d905776952
Animate graph changes 2023-01-13 12:01:11 +01:00
monsterkrampe
e615a1fb86
Upgrade frontend dependencies 2023-01-13 11:31:14 +01:00
b23f342a4e
Use unoptimised hybrid step for better presentation 2023-01-13 09:05:50 +01:00
92954cf87b
Use standard example for adfs on the frontend 2023-01-13 09:05:50 +01:00
monsterkrampe
07537c6d25
Support more options and multiple models 2023-01-13 09:05:50 +01:00
monsterkrampe
e88e6bbfa1
Fix code formatting 2023-01-13 09:05:49 +01:00
monsterkrampe
addb774cc1
Introduce custom node type for nicer layout 2023-01-13 09:05:49 +01:00
monsterkrampe
daf4e21f77
Support stable model semantics with nogoods 2023-01-13 09:05:49 +01:00
monsterkrampe
8d6e0a19de
Support multiple solving strategies 2023-01-13 09:05:49 +01:00
monsterkrampe
f8f1ca968e
Add Dockerfile as example for server with frontend 2023-01-13 09:05:49 +01:00
monsterkrampe
5a409712bc
Serve static files from './assets' directory 2023-01-13 09:05:49 +01:00
monsterkrampe
393ee39f0c
Introduce features flag for localhost cors support 2023-01-13 09:05:49 +01:00
monsterkrampe
e5df39206c
Make fetch endpoint depend on environment 2023-01-13 09:05:49 +01:00
monsterkrampe
b0e57cf7e1
Finish basic visualization of solve response 2023-01-13 09:05:49 +01:00
monsterkrampe
7c47d6aa28
Continue implementing basic solving endpoint 2023-01-13 09:05:48 +01:00
monsterkrampe
18952323eb
Build basic ui with mui 2023-01-13 09:05:48 +01:00
monsterkrampe
4d0f52c164
Start implementing endpoint to solve ADF on demand 2023-01-13 09:05:46 +01:00
monsterkrampe
4e5a1fc1ff
Introduce separate server package 2023-01-13 08:50:00 +01:00
monsterkrampe
f7302511be
Experiment with basic graph visualization 2023-01-13 08:49:58 +01:00
Stefan Ellmauthaler
11083098a2
Update/depbot flake (#133)
* 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>
2023-01-02 10:07:24 +01:00
Stefan Ellmauthaler
68acf25a39
Dependabot/bump (#121)
* Bump biodivine-lib-bdd from 0.4.0 to 0.4.1

Bumps [biodivine-lib-bdd](https://github.com/sybila/biodivine-lib-bdd) from 0.4.0 to 0.4.1.
- [Release notes](https://github.com/sybila/biodivine-lib-bdd/releases)
- [Commits](https://github.com/sybila/biodivine-lib-bdd/compare/v0.4.0...v0.4.1)

---
updated-dependencies:
- dependency-name: biodivine-lib-bdd
  dependency-type: direct:production
  update-type: version-update:semver-patch
...

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

* Bump serde from 1.0.145 to 1.0.147

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

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

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

* Bump assert_cmd from 2.0.4 to 2.0.5

Bumps [assert_cmd](https://github.com/assert-rs/assert_cmd) from 2.0.4 to 2.0.5.
- [Release notes](https://github.com/assert-rs/assert_cmd/releases)
- [Changelog](https://github.com/assert-rs/assert_cmd/blob/master/CHANGELOG.md)
- [Commits](https://github.com/assert-rs/assert_cmd/compare/v2.0.4...v2.0.5)

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

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

* Bump clap from 4.0.9 to 4.0.18

Bumps [clap](https://github.com/clap-rs/clap) from 4.0.9 to 4.0.18.
- [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.9...v4.0.18)

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

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

* Bump serde_json from 1.0.85 to 1.0.87

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

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

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

* flake.lock: Update

Flake lock file updates:

• Updated input 'flake-utils':
    'github:numtide/flake-utils/c0e246b9b83f637f4681389ecabcb2681b4f3af0' (2022-08-07)
  → 'github:numtide/flake-utils/5aed5285a952e0b949eb3ba02c12fa4fcfef535f' (2022-11-02)
• Updated input 'nixpkgs':
    'github:NixOS/nixpkgs/81a3237b64e67b66901c735654017e75f0c50943' (2022-10-03)
  → 'github:NixOS/nixpkgs/16f4e04658c2ab10114545af2f39db17d51bd1bd' (2022-11-14)
• Updated input 'nixpkgs-unstable':
    'github:NixOS/nixpkgs/fd54651f5ffb4a36e8463e0c327a78442b26cbe7' (2022-10-03)
  → 'github:NixOS/nixpkgs/fc07622617a373a742ed96d4dd536849d4bc1ec6' (2022-11-13)
• Updated input 'rust-overlay':
    'github:oxalica/rust-overlay/148815c92641976b798efb2805a50991de4bac7f' (2022-10-04)
  → 'github:oxalica/rust-overlay/2342f70f7257046effc031333c4cfdea66c91d82' (2022-11-15)

* Fix new clippy comments due to rust 1.65

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
2022-11-15 09:41:52 +01:00
dependabot[bot]
68cbab5b02
Bump clap from 4.0.7 to 4.0.9 (#114) 2022-10-04 14:53:59 +00:00
Stefan Ellmauthaler
6d687a3839
Dependabot/bump (#113)
* Bump clap from 3.2.20 to 4.0.7

Bumps [clap](https://github.com/clap-rs/clap) from 3.2.20 to 4.0.7.
- [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/v3.2.20...v4.0.7)

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

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

* Bump serde from 1.0.144 to 1.0.145

Bumps [serde](https://github.com/serde-rs/serde) from 1.0.144 to 1.0.145.
- [Release notes](https://github.com/serde-rs/serde/releases)
- [Commits](https://github.com/serde-rs/serde/compare/v1.0.144...v1.0.145)

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

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

* Bump env_logger from 0.9.0 to 0.9.1

Bumps [env_logger](https://github.com/env-logger-rs/env_logger) from 0.9.0 to 0.9.1.
- [Release notes](https://github.com/env-logger-rs/env_logger/releases)
- [Changelog](https://github.com/env-logger-rs/env_logger/blob/main/CHANGELOG.md)
- [Commits](https://github.com/env-logger-rs/env_logger/compare/v0.9.0...v0.9.1)

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

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

* Bump roaring from 0.9.0 to 0.10.1

Bumps [roaring](https://github.com/RoaringBitmap/roaring-rs) from 0.9.0 to 0.10.1.
- [Release notes](https://github.com/RoaringBitmap/roaring-rs/releases)
- [Commits](https://github.com/RoaringBitmap/roaring-rs/compare/v0.9.0...v0.10.1)

---
updated-dependencies:
- dependency-name: roaring
  dependency-type: direct:production
  update-type: version-update:semver-minor
...

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

* flake.lock: Update

Flake lock file updates:

• Updated input 'flake-utils':
    'github:numtide/flake-utils/7e2a3b3dfd9af950a856d66b0a7d01e3c18aa249' (2022-07-04)
  → 'github:numtide/flake-utils/c0e246b9b83f637f4681389ecabcb2681b4f3af0' (2022-08-07)
• Updated input 'gitignoresrc':
    'github:hercules-ci/gitignore.nix/f2ea0f8ff1bce948ccb6b893d15d5ea3efaf1364' (2022-07-21)
  → 'github:hercules-ci/gitignore.nix/a20de23b925fd8264fd7fad6454652e142fd7f73' (2022-08-14)
• Updated input 'nixpkgs':
    'github:NixOS/nixpkgs/e43cf1748462c81202a32b26294e9f8eefcc3462' (2022-08-01)
  → 'github:NixOS/nixpkgs/81a3237b64e67b66901c735654017e75f0c50943' (2022-10-03)
• Updated input 'nixpkgs-unstable':
    'github:NixOS/nixpkgs/7b9be38c7250b22d829ab6effdee90d5e40c6e5c' (2022-07-30)
  → 'github:NixOS/nixpkgs/fd54651f5ffb4a36e8463e0c327a78442b26cbe7' (2022-10-03)
• Updated input 'rust-overlay':
    'github:oxalica/rust-overlay/9055cb4f33f062c0dd33aa7e3c89140da8f70057' (2022-08-02)
  → 'github:oxalica/rust-overlay/148815c92641976b798efb2805a50991de4bac7f' (2022-10-04)

* Update code to use clap version 4 and use then_some(..)

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
2022-10-04 16:47:46 +02:00
dependabot[bot]
d807089884
Bump clap from 3.2.19 to 3.2.20 (#108) 2022-09-06 10:29:53 +00:00
Stefan Ellmauthaler
683c12a525
Dependabot/2022sep06 merge (#107)
* Bump serde from 1.0.141 to 1.0.144

Bumps [serde](https://github.com/serde-rs/serde) from 1.0.141 to 1.0.144.
- [Release notes](https://github.com/serde-rs/serde/releases)
- [Commits](https://github.com/serde-rs/serde/compare/v1.0.141...v1.0.144)

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

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

* Bump clap from 3.2.16 to 3.2.19

Bumps [clap](https://github.com/clap-rs/clap) from 3.2.16 to 3.2.19.
- [Release notes](https://github.com/clap-rs/clap/releases)
- [Changelog](https://github.com/clap-rs/clap/blob/v3.2.19/CHANGELOG.md)
- [Commits](https://github.com/clap-rs/clap/compare/v3.2.16...v3.2.19)

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

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

* Bump serde_json from 1.0.82 to 1.0.85

Bumps [serde_json](https://github.com/serde-rs/json) from 1.0.82 to 1.0.85.
- [Release notes](https://github.com/serde-rs/json/releases)
- [Commits](https://github.com/serde-rs/json/compare/v1.0.82...v1.0.85)

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

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

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
2022-09-06 12:16:33 +02:00
27 changed files with 6319 additions and 262 deletions

4
.dockerignore Normal file
View File

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

1345
Cargo.lock generated

File diff suppressed because it is too large Load Diff

View File

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

34
Dockerfile Normal file
View File

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

View File

@ -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"

View File

@ -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)
}

View File

@ -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");

32
flake.lock generated
View File

@ -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": {

View File

@ -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:
@ -28,10 +29,8 @@
inherit system;
overlays = [ (import rust-overlay) ];
};
in
rec {
devShell =
pkgs.mkShell {
in rec {
devShell = pkgs.mkShell {
RUST_LOG = "debug";
RUST_BACKTRACE = 1;
buildInputs = [
@ -47,6 +46,5 @@
pkgs.kcov
];
};
}
));
}));
}

13
frontend/.editorconfig Normal file
View File

@ -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

25
frontend/.eslintrc.js Normal file
View File

@ -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"] }]
}
}

5
frontend/.gitignore vendored Normal file
View File

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

33
frontend/package.json Normal file
View File

@ -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"
}
}

8
frontend/shell.nix Normal file
View File

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

13
frontend/src/app.tsx Normal file
View File

@ -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 />);

View File

@ -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;

View File

@ -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;

13
frontend/src/index.html Normal file
View File

@ -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>

19
frontend/src/test-data.ts Normal file
View File

@ -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;

4099
frontend/yarn.lock Normal file

File diff suppressed because it is too large Load Diff

View File

@ -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"]}

View File

@ -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

View File

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

View File

@ -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() {

View File

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

25
server/Cargo.toml Normal file
View File

@ -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 = []

136
server/src/main.rs Normal file
View File

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