diff --git a/.github/CONTRIBUTING.md b/.github/CONTRIBUTING.md new file mode 100644 index 0000000..64b3263 --- /dev/null +++ b/.github/CONTRIBUTING.md @@ -0,0 +1,80 @@ +# How to contribute + +We are really glad you are reading this, because we need developers to help this project come to fruition. + +## Folder structure + +The project is divided into two different cargo-projects under one rust-workspace. + +* `lib` is where the library is located +* `bin` is where the binary is located +* `res` is a folder, where different resources for testing and benchmarks are located (usually managed through `git submodules` + +Easy first tasks for contributing will be to integrate implemented features from the library, which are not represented in the binary. + +## Testing + +Please make sure to test your additional features. + +### Unit-Testing +Unit tests are done for each module by an associated `test` sub-module. +It can either be directly in the `` file or in an additional `test` sub-directory. +Please try to generate meaningful tests, with sane data. It would be most appreciated if there are some real-world flavours. +Add `quickcheck` tests whenever it is applicable. + +### Integration-Testing +Integration testing is done in the related `tests` directory on the top-level of the crate. + +## Submitting changes + +Please send a [GitHub Pull Request to ellmau/adf-obdd](https://github.com/ellmau/adf-obdd/pull/new/main) with a clear list of what you've done (read more about [pull requests](http://help.github.com/pull-requests/)). When you send a pull request be sure to check open and claimed tickets first. We can always use more test coverage. Please follow our coding conventions (below). + +Always write a clear log message for your commits. One-line messages are fine for small changes, but bigger changes should have a commit-paragraph and/or a related and appropriately mentioned [issue](https://github.com/ellmau/adf-obdd/issues). + +Before creating the pull request be sure to check if +- [ ] all already existing tests are passing, +- [ ] new tests are passing, +- [ ] `clippy` does not complain about your code, and +- [ ] the code has been formatted with `rustfmt`. + +If you have done changes to any other folder than `lib` and `bin`, choose the `repository`-label for the pull request. + +We are monitoring our code-coverage through [coveralls](https://coveralls.io), so it is expected that additional changes do not reduce the test-coverage significantly. +Keep in mind, that the current coverage-tools have some issues with rust-code and sometimes report lower code-coverage than it is in reality. + +Finally, if you create a pull request for work in progress, please mark this by creating a draft pull request. + +### Commit messages + +To create uniform and easy to read commit messages, please stick to the following conventions: + + * Capitalise the first word + * Do not end the message title in punctuation + * Use imperative mood + * The message title shall not exceed 50 characters + * Be direct, do not use filler words (e.g. "I think", "maybe", "kind of", ...) + * Use [Github Issue/PR Keywords](https://docs.github.com/en/get-started/writing-on-github/working-with-advanced-formatting/using-keywords-in-issues-and-pull-requests) in the message description part where applicable + * Link to other related pull requests, issues, commits, comments, ... to have a concise representation of the context in the message description + * Sign your commit whenever possible + +A commit message is usually consisting of the first line, the so-called `message-title`, one free line, and the `message description` which may take the following lines. + +## Coding conventions + +Start reading our code and you'll get the hang of it. + + * We use `rustfmt` as code-convention. (you can use whatever styles you like, just let `rustfmt` format the code before you commit) + * We try to reduce redundancies in enumeration-variant names. + * We follow the code-conventions and naming-conventions of the current Rust version. + * We write `clippy`-conform code, so follow `clippy` suggestions where applicable. If you write a compiler-exception (i.e. `#[allow(...)]`) describe your decision to do so in a meaningful comment. We advise to mark this code-segment in the pull-request as a code-comment too. + * `rustdoc` is obligatory for crate-exposed structures (e.g. `enum`, `struct`, `fn`, ...). + * `rustdoc` is nice to have for non-crate-exposed structures. + * We try to have one atomic commit for refactoring work done. + * Error-handling shall follow these guidelines: + * `panic!` (and `expect()`, `assert!`, `unreachable!` etc.) is fine for situations that should not occur, e.g., if there is some invariant that makes the situation impossible, or where graceful recovery is impossible, but not otherwise, and + * `unwrap()` should (almost?) always be `expect()` instead (exceptions are in tests). + * Use `unsafe` code only if : + * It is checked that there is no safe way to achieve the functionality, + * it has been discussed with the core development team in detail, + * the unsafe part is tested even more carefully than the rest of the code, and + * you will persistently insist on a detailed code-review diff --git a/README.md b/README.md index da7b649..d787920 100644 --- a/README.md +++ b/README.md @@ -11,38 +11,41 @@ An ordered binary decision diagram is a normalised representation of binary func ## Usage of the binary ``` USAGE: - adf_bdd [FLAGS] [OPTIONS] - -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 - --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, --version Prints version information - -v Sets log verbosity (multiple times means more verbose) - -OPTIONS: - --export Export the adf-bdd state after parsing and BDD instantiation to the given filename - --lib choose the bdd implementation of either 'biodivine', 'naive', or hybrid [default: - biodivine] - --rust_log Sets the verbosity to 'warn', 'info', 'debug' or 'trace' if -v and -q are not use - [env: RUST_LOG=debug] + adf_bdd [OPTIONS] ARGS: - Input filename + Input filename + +OPTIONS: + --an Sorts variables in an alphanumeric manner + --com Compute the complete models + --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 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 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 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 + --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 the borders between the results are not obviously communicated. +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 diff --git a/bin/src/main.rs b/bin/src/main.rs index 0f2c126..3ba4acf 100644 --- a/bin/src/main.rs +++ b/bin/src/main.rs @@ -17,33 +17,36 @@ In addition some further features, like counter-model counting is not supported # Usage ```plain USAGE: - adf_bdd [FLAGS] [OPTIONS] - -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 - --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, --version Prints version information - -v Sets log verbosity (multiple times means more verbose) - -OPTIONS: - --export Export the adf-bdd state after parsing and BDD instantiation to the given filename - --lib choose the bdd implementation of either 'biodivine', 'naive', or hybrid [default: - biodivine] - --rust_log Sets the verbosity to 'warn', 'info', 'debug' or 'trace' if -v and -q are not use - [env: RUST_LOG=debug] + adf_bdd [OPTIONS] ARGS: - Input filename + Input filename + +OPTIONS: + --an Sorts variables in an alphanumeric manner + --com Compute the complete models + --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 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 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 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 + --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 ``` */ @@ -81,7 +84,7 @@ struct App { #[clap(long = "rust_log", env)] rust_log: Option, /// choose the bdd implementation of either 'biodivine', 'naive', or hybrid - #[clap(long = "lib", default_value = "biodivine")] + #[clap(long = "lib", default_value = "hybrid")] implementation: String, /// Sets log verbosity (multiple times means more verbose) #[clap(short, parse(from_occurrences), group = "verbosity")] @@ -152,8 +155,13 @@ impl App { match self.implementation.as_str() { "hybrid" => { let parser = adf_bdd::parser::AdfParser::default(); - parser.parse()(&input).unwrap(); - log::info!("[Done] parsing"); + 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") + } + } if self.sort_lex { parser.varsort_lexi(); } @@ -222,7 +230,13 @@ impl App { log::error!("Modelcounting not supported in biodivine mode"); } let parser = adf_bdd::parser::AdfParser::default(); - parser.parse()(&input).unwrap(); + 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") + } + } log::info!("[Done] parsing"); if self.sort_lex { parser.varsort_lexi(); @@ -263,18 +277,28 @@ impl App { let mut adf = if self.import { #[cfg(not(feature = "adhoccounting"))] { - serde_json::from_str(&input).unwrap() + serde_json::from_str(&input).expect("Old feature should work") } #[cfg(feature = "adhoccounting")] { - let mut result: Adf = serde_json::from_str(&input).unwrap(); + let mut result: Adf = + serde_json::from_str(&input).expect("Old feature should work"); log::debug!("test"); result.fix_import(); result } } else { let parser = AdfParser::default(); - parser.parse()(&input).unwrap(); + 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") + } + } log::info!("[Done] parsing"); if self.sort_lex { parser.varsort_lexi(); diff --git a/lib/src/adf.rs b/lib/src/adf.rs index 92ab300..195d7c5 100644 --- a/lib/src/adf.rs +++ b/lib/src/adf.rs @@ -19,6 +19,8 @@ use crate::{ #[derive(Serialize, Deserialize, Debug)] /// Representation of an ADF, with an ordering and dictionary of statement <-> number relations, a binary decision diagram, and a list of acceptance functions in Term representation +/// +/// Please note that due to the nature of the underlying reduced and ordered Bdd the concept of a [`Term`][crate::datatypes::Term] represents one (sub) formula as well as truth-values. pub struct Adf { ordering: VarContainer, bdd: Bdd, @@ -66,7 +68,9 @@ impl Adf { new_order, parser.ac_at(insert_order) ); - let result_term = result.term(&parser.ac_at(insert_order).unwrap()); + let result_term = result.term(&parser.ac_at(insert_order).expect( + "Index should exist, because the data originates from the same parser object", + )); result.ac[*new_order] = result_term; }); log::info!("[Success] instantiated"); @@ -138,7 +142,7 @@ impl Adf { Formula::Bot => Bdd::constant(false), Formula::Top => Bdd::constant(true), Formula::Atom(val) => { - let t1 = self.ordering.variable(val).unwrap(); + let t1 = self.ordering.variable(val).expect("Variable should exist, because the ordering has been filled by the same parser as the input formula comes from"); self.bdd.variable(t1) } Formula::Not(val) => { diff --git a/lib/src/adfbiodivine.rs b/lib/src/adfbiodivine.rs index db2f9b7..6c0ede9 100644 --- a/lib/src/adfbiodivine.rs +++ b/lib/src/adfbiodivine.rs @@ -22,6 +22,8 @@ use derivative::Derivative; #[derive(Derivative)] #[derivative(Debug)] /// Representation of an ADF, with an ordering and dictionary of statement <-> number relations, a binary decision diagram, and a list of acceptance functions in biodivine representation together with a variable-list (needed by biodivine) +/// +/// To be compatible with results from the own implementation of the Bdd-based [`Adf`][crate::adf::Adf], we use the [`Term`][crate::datatypes::Term]-based representation for the various computed models. pub struct Adf { ordering: VarContainer, ac: Vec, @@ -69,7 +71,7 @@ impl Adf { ); result.ac[*new_order] = result .varset - .eval_expression(&parser.ac_at(insert_order).unwrap().to_boolean_expr()); + .eval_expression(&parser.ac_at(insert_order).expect("Insert order needs to exist, as all the data originates from the same parser object").to_boolean_expr()); log::trace!("instantiated {}", result.ac[*new_order]); }); log::info!("[Success] instantiated"); @@ -97,7 +99,7 @@ impl Adf { .name(crate::datatypes::Var(*new_order)) .expect("Variable should exist"), )), - Box::new(parser.ac_at(insert_order).unwrap().to_boolean_expr()), + Box::new(parser.ac_at(insert_order).expect("Insert order needs to exist, as all the data originates from the same parser object").to_boolean_expr()), )), ) }, @@ -293,7 +295,7 @@ impl Adf { let internal_rewriting: Bdd; let sr: &Bdd; if self.has_stm_rewriting() { - sr = self.rewrite.as_ref().unwrap(); + sr = self.rewrite.as_ref().expect("self.rewrite has to exist, because it has been checked just before calling this reference"); } else { internal_rewriting = self.stable_representation(); sr = &internal_rewriting; diff --git a/lib/src/datatypes/adf.rs b/lib/src/datatypes/adf.rs index c71014d..b3ed041 100644 --- a/lib/src/datatypes/adf.rs +++ b/lib/src/datatypes/adf.rs @@ -102,8 +102,14 @@ impl Display for PrintableInterpretation<'_> { } else { write!(f, "u(").expect("writing Interpretation failed!"); } - write!(f, "{}) ", self.ordering.name(Var(pos)).unwrap()) - .expect("writing Interpretation failed!"); + write!( + f, + "{}) ", + self.ordering + .name(Var(pos)) + .expect("Variable originates from same parser object as the ordering") + ) + .expect("writing Interpretation failed!"); }); writeln!(f) } diff --git a/lib/src/lib.rs b/lib/src/lib.rs index cfa94fd..98e7307 100644 --- a/lib/src/lib.rs +++ b/lib/src/lib.rs @@ -39,18 +39,127 @@ The binary predicate ac relates each statement to one propositional formula in p - c(f): constant symbol "falsum" - inconsistency/bot */ -//! ## Example input file: -//! ```prolog -//! s(a). -//! s(b). -//! s(c). -//! s(d). -//! -//! ac(a,c(v)). -//! ac(b,or(a,b)). -//! ac(c,neg(b)). -//! ac(d,d). -//! ``` +/*! +## Example input file: +```prolog +s(a). +s(b). +s(c). +s(d). + +ac(a,c(v)). +ac(b,or(a,b)). +ac(c,neg(b)). +ac(d,d). +``` +*/ + +/*! +## Usage examples +First parse a given ADF and sort the statements, if needed. +```rust +use adf_bdd::parser::AdfParser; +use adf_bdd::adf::Adf; +// use the above example as input +let input = "s(a).s(b).s(c).s(d).ac(a,c(v)).ac(b,or(a,b)).ac(c,neg(b)).ac(d,d)."; +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") + } +} +// sort lexicographic +parser.varsort_lexi(); +``` +### use the naive/in-crate implementation +```rust +# use adf_bdd::parser::AdfParser; +# use adf_bdd::adf::Adf; +# // use the above example as input +# let input = "s(a).s(b).s(c).s(d).ac(a,c(v)).ac(b,or(a,b)).ac(c,neg(b)).ac(d,d)."; +# 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") +# } +# } +# // sort lexicographic +# parser.varsort_lexi(); +// create Adf +let mut adf = Adf::from_parser(&parser); +// compute and print the complete models +let printer = adf.print_dictionary(); +for model in adf.complete() { + print!("{}", printer.print_interpretation(&model)); +} +``` +### use the biodivine implementation +```rust +# use adf_bdd::parser::AdfParser; +# use adf_bdd::adf::Adf; +# // use the above example as input +# let input = "s(a).s(b).s(c).s(d).ac(a,c(v)).ac(b,or(a,b)).ac(c,neg(b)).ac(d,d)."; +# 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") +# } +# } +# // sort lexicographic +# parser.varsort_lexi(); +// create Adf +let adf = adf_bdd::adfbiodivine::Adf::from_parser(&parser); +// compute and print the complete models +let printer = adf.print_dictionary(); +for model in adf.complete() { + print!("{}", printer.print_interpretation(&model)); +} +``` +### use the hybrid approach implementation +```rust +# use adf_bdd::parser::AdfParser; +# use adf_bdd::adf::Adf; +# // use the above example as input +# let input = "s(a).s(b).s(c).s(d).ac(a,c(v)).ac(b,or(a,b)).ac(c,neg(b)).ac(d,d)."; +# 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") +# } +# } +# // sort lexicographic +# parser.varsort_lexi(); +// create biodivine Adf +let badf = adf_bdd::adfbiodivine::Adf::from_parser(&parser); +// instantiate the internally used adf after the reduction done by biodivine +let mut adf = badf.hybrid_step(); +// compute and print the complete models +let printer = adf.print_dictionary(); +for model in adf.complete() { + print!("{}", printer.print_interpretation(&model)); +} +``` +*/ #![deny( missing_debug_implementations, missing_copy_implementations, diff --git a/lib/src/obdd.rs b/lib/src/obdd.rs index d22a61d..0e2ac98 100644 --- a/lib/src/obdd.rs +++ b/lib/src/obdd.rs @@ -215,7 +215,7 @@ impl Bdd { pub fn models(&self, term: Term, _memoization: bool) -> ModelCounts { #[cfg(feature = "adhoccounting")] { - return self.count_cache.borrow().get(&term).unwrap().0; + return self.count_cache.borrow().get(&term).expect("The term should be originating from this bdd, otherwise the result would be inconsistent anyways").0; } #[cfg(not(feature = "adhoccounting"))] if _memoization { diff --git a/lib/src/parser.rs b/lib/src/parser.rs index f4a739c..42df9b4 100644 --- a/lib/src/parser.rs +++ b/lib/src/parser.rs @@ -370,7 +370,14 @@ impl AdfParser<'_> { self.formulaname .borrow() .iter() - .map(|name| *self.dict.as_ref().borrow().get(name).unwrap()) + .map(|name| { + *self + .dict + .as_ref() + .borrow() + .get(name) + .expect("Dictionary should contain all the used formulanames") + }) .collect() } }