Feature/issue 17 biodivine (#18)

State of the art BDD library, naive implementation, and Hybrid-approach available in the first beta-release version 0.2.0

* ADD biodivine as an obdd library to adf-obdd

* Implement restrict-wrapper on Biodivine

* Testcases changed to use biodivine for grounded.

* API unified

* ADD stable and complete with biodivine

* moved main.rs to bin folder

* ADD biodivine -> naive translation

* ADD hybrid approach
  instantiation + grounded by biodivine, then naive approach with memoization

* TIDY Readme, doc, tests

Cargo.toml

@@ -1,18 +1,19 @@
 [package]
 name = "adf_bdd"
-version = "0.1.4"
+version = "0.2.0"
 authors = ["Stefan Ellmauthaler <[email protected]>"]
 edition = "2021"
 repository = "https://github.com/ellmau/adf-obdd/"
 license = "GPL-3.0-only"
 exclude = ["res/", "./flake*", "*.nix", ".envrc", "_config.yml"]
 
-description = "Solver for ADFs grounded semantics by utilising OBDDs - ordered binary decision diagrams"
+description = "Solver for ADFs grounded, complete, and stable semantics by utilising OBDDs - ordered binary decision diagrams"
 build = "build.rs"
 
 
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
-
+[[bin]]
+name="adf_bdd"
 [dependencies]
 clap = "2.33.*"
 structopt = "0.3.25"
@@ -22,6 +23,7 @@ nom = "7.1.0"
 lexical-sort = "0.3.1"
 serde = { version = "1.0", features = ["derive","rc"] }
 serde_json = "1.0"
+biodivine-lib-bdd = "0.3.0"
 
 [dev-dependencies]
 test-log = "0.2.*"

README.md

@@ -7,6 +7,48 @@ An abstract dialectical framework (ADF) consists of abstract statements. Each st
 ## Ordered Binary Decision Diagram
 An ordered binary decision diagram is a normalised representation of binary functions, where satisfiability- and validity checks can be done relatively cheap.
 
+## Usage
+```
+USAGE:
+    adf_bdd [FLAGS] [OPTIONS] <input>
+
+FLAGS:
+        --com        Compute the complete models
+        --grd        Compute the grounded model
+    -h, --help       Prints help information
+        --import     Import an adf- bdd state instead of an adf
+    -q               Sets log verbosity to only errors
+        --an         Sorts variables in an alphanumeric manner
+        --lx         Sorts variables in an lexicographic manner
+        --stm        Compute the stable models
+    -V, --version    Prints version information
+    -v               Sets log verbosity (multiple times means more verbose)
+
+OPTIONS:
+        --export <export>         Export the adf-bdd state after parsing and BDD instantiation to the given filename
+        --lib <implementation>    choose the bdd implementation of either 'biodivine', 'naive', or hybrid [default:
+                                  biodivine]
+        --rust_log <rust-log>     Sets the verbosity to 'warn', 'info', 'debug' or 'trace' if -v and -q are not use
+                                  [env: RUST_LOG=debug]
+
+ARGS:
+    <input>    Input filename
+```
+
+Note that import and export only works if the naive library is chosen
+
+Right now there is no additional information to the computed models, so if you use --com --grd --stm the borders between the results are not obviously communicated.
+They can be easily identified though:
+- The computation is always in the same order
+  - grd
+  - com
+  - stm
+- We know that there is always exactly one grounded model
+- We know that there always exist at least one complete model (i.e. the grounded one)
+- We know that there does not need to exist a stable model
+- We know that every stable model is a complete model too
+
+
 ## Input-file format:
 Each statement is defined by an ASP-style unary predicate s, where the enclosed term represents the label of the statement.
 The binary predicate ac relates each statement to one propositional formula in prefix notation, with the logical operations and constants as follows:
@@ -35,3 +77,17 @@ $> cargo test
 ```
 Note that some of the instances are quite big and it might take some time to finish all the tests.
 If you do not initialise the submodule, tests will "only" run on the other unit-tests and (possibly forthcoming) other integration tests.
+Due to the way of the generated test-modules you need to call 
+```bash
+$> cargo clean
+```
+if you change some of your test-cases.
+
+To remove the tests just type
+```bash
+$> git submodule deinit res/adf-instances
+```
+or
+```bash
+$> git submodule deinit --all
+```

build.rs

@@ -58,7 +58,7 @@ fn write_header(test_file: &mut File) {
     write!(
         test_file,
         r#"
-use adf_bdd::adf::Adf;
+use adf_bdd::adfbiodivine::Adf;
 use adf_bdd::parser::AdfParser;
 use test_log::test;
 "#