milestone/nogoods

.gitignore

@@ -21,3 +21,9 @@ tramp
 *_flymake*
 
 /tests/out/
+
+# Ignore direnv data
+/.direnv/
+
+# ignore perfdata
+perf.data

README.md

@@ -8,67 +8,23 @@
 ![Crates.io](https://img.shields.io/crates/l/adf_bdd)
 [![GitHub Discussions](https://img.shields.io/github/discussions/ellmau/adf-obdd)](https://github.com/ellmau/adf-obdd/discussions) ![rust-edition](https://img.shields.io/badge/Rust--edition-2021-blue?logo=rust)
 
-# Abstract Dialectical Frameworks solved by Binary Decision Diagrams; developed in Dresden (ADF-BDD) 
+# Abstract Dialectical Frameworks solved by (ordered) Binary Decision Diagrams; developed in Dresden (ADF-oBDD project)
+
+This project is currently split into two parts:
+- a [binary (adf-bdd)](bin), which allows one to easily answer semantics questions on abstract dialectical frameworks
+- a [library (adf_bdd)](lib), which contains all the necessary algorithms and an open API which compute the answers to the semantics questions
+
+Latest documentation of the API can be found [here](https://docs.rs/adf_bdd/latest/adf_bdd/).
+The current version of the binary can be downloaded [here](https://github.com/ellmau/adf-obdd/releases).
+
+Do not hesitate to report bugs or ask about features in the [issues-section](https://github.com/ellmau/adf-obdd/issues) or have a conversation about anything of the project in the [discussion space](https://github.com/ellmau/adf-obdd/discussions)
 
 
 ## Abstract Dialectical Frameworks
 An abstract dialectical framework (ADF) consists of abstract statements. Each statement has an unique label and might be related to other statements (s) in the ADF. This relation is defined by a so-called acceptance condition (ac), which intuitively is a propositional formula, where the variable symbols are the labels of the statements. An interpretation is a three valued function which maps to each statement a truth value (true, false, undecided). We call such an interpretation a model, if each acceptance condition agrees to the interpration. 
 ## 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 of the binary
-```
-USAGE:
-    adf_bdd [OPTIONS] <INPUT>
-
-ARGS:
-    <INPUT>    Input filename
-
-OPTIONS:
-        --an                      Sorts variables in an alphanumeric manner
-        --com                     Compute the complete models
-        --counter <COUNTER>       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)
-        --export <EXPORT>         Export the adf-bdd state after parsing and BDD instantiation to
-                                  the given filename
-        --grd                     Compute the grounded model
-    -h, --help                    Print help information
-        --import                  Import an adf- bdd state instead of an adf
-        --lib <IMPLEMENTATION>    choose the bdd implementation of either 'biodivine', 'naive', or
-                                  hybrid [default: hybrid]
-        --lx                      Sorts variables in an lexicographic manner
-    -q                            Sets log verbosity to only errors
-        --rust_log <RUST_LOG>     Sets the verbosity to 'warn', 'info', 'debug' or 'trace' if -v and
-                                  -q are not use [env: RUST_LOG=debug]
-        --stm                     Compute the stable models
-        --stmca                   Compute the stable models with the help of modelcounting using
-                                  heuristics a
-        --stmcb                   Compute the stable models with the help of modelcounting using
-                                  heuristics b
-        --stmpre                  Compute the stable models with a pre-filter (only hybrid lib-mode)
-        --stmrew                  Compute the stable models with a single-formula rewriting (only
-                                  hybrid lib-mode)
-        --stmrew2                 Compute the stable models with a single-formula rewriting on
-                                  internal representation(only hybrid lib-mode)
-    -v                            Sets log verbosity (multiple times means more verbose)
-    -V, --version                 Print version information
-```
-
-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` as the command line arguments 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:
@@ -82,64 +38,22 @@ The binary predicate ac relates each statement to one propositional formula in p
 
 # Features
 
-`adhoccounting` will cache the modelcount on-the-fly during the construction of the BDD
+- `adhoccounting` will cache the modelcount on-the-fly during the construction of the BDD
+- `adhoccountmodels` allows in addition to compute the models ad-hoc too. Note that the memoization approach for modelcounting does not work correctly if `adhoccounting` is set and `adhoccountmodels` is not.
 
 # Development notes 
 Additional information for contribution, testing, and development in general can be found here.
 ## Contributing to the project
 You want to help and contribute to the project? That is great. Please see the [contributing guidelines](https://github.com/ellmau/adf-obdd/blob/main/.github/CONTRIBUTING.md) first.
 
-## Building the binary:
-To build the binary, you need to run
-```bash
-$> cargo build --workspace --release
-```
-
-To build the binary with debug-symbols, run
-```bash
-$> cargo build --workspace
-```
-
-## Testing with the `res` folder:
-To run all the tests placed in the submodule you need to run
-```bash
-$> git submodule init
-```
-at the first time.
-Afterwards you need to update the content of the submodule to be on the currently used revision by
-```bash
-$> git submodule update
-```
-
-The tests can be started by using the test-framework of cargo, i.e.
-```bash
-$> 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
-```
-
 # Acknowledgements
 This work is partly supported by Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) in projects number 389792660 (TRR 248, [Center for Perspicuous Systems](https://www.perspicuous-computing.science/)), 
 the Bundesministerium für Bildung und Forschung (BMBF, Federal Ministry of Education and Research) in the
 [Center for Scalable Data Analytics and Artificial Intelligence](https://www.scads.de) (ScaDS.AI),
 and by the [Center for Advancing Electronics Dresden](https://cfaed.tu-dresden.de) (cfaed).
 
 # Affiliation 
-This work has been party developed by the [Knowledge-Based Systems Group](http://kbs.inf.tu-dresden.de/), [Faculty of Computer Science](https://tu-dresden.de/ing/informatik)  of [TU Dresden](https://tu-dresden.de).
+This work has been partly developed by the [Knowledge-Based Systems Group](http://kbs.inf.tu-dresden.de/), [Faculty of Computer Science](https://tu-dresden.de/ing/informatik)  of [TU Dresden](https://tu-dresden.de).
 
 # Disclaimer
-Hosting content here does not establish any formal or legal relation to TU Dresden
+Hosting content here does not establish any formal or legal relation to TU Dresden.

bin/Cargo.toml

@@ -1,10 +1,12 @@
 [package]
-name = "adf_bdd-solver"
-version = "0.2.4"
+name = "adf-bdd-solver"
+version = "0.3.0"
 authors = ["Stefan Ellmauthaler <[email protected]>"]
 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"]
+exclude = ["res/", "./flake*", "*.nix", ".envrc", "_config.yml", "tarpaulin-report.*", "*~"]
 description = "Solver for ADFs grounded, complete, and stable semantics by utilising OBDDs - ordered binary decision diagrams"
 
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
@@ -14,12 +16,14 @@ name = "adf-bdd"
 path = "src/main.rs"
 
 [dependencies]
-adf_bdd = { version="0.2.4", default-features = false }
+adf_bdd = { version="0.3.0", path="../lib", default-features = false }
 clap = {version = "3.2.12", 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"
 env_logger = "0.9"
+strum = { version = "0.24" }
+crossbeam-channel = "0.5"
 
 [dev-dependencies]
 assert_cmd = "2.0"
@@ -32,3 +36,5 @@ adhoccounting = ["adf_bdd/adhoccounting"]    # count models ad-hoc - disable if
 importexport = ["adf_bdd/importexport"]
 variablelist = [ "HashSet", "adf_bdd/variablelist" ]
 HashSet = ["adf_bdd/HashSet"]
+adhoccountmodels = ["adf_bdd/adhoccountmodels"]
+benchmark = ["adf_bdd/benchmark"]