ellmau/adf-obdd
1
0
Fork 0
mirror of https://github.com/ellmau/adf-obdd.git synced 2025-12-19 09:29:36 +01:00
Code Issues Projects Releases Wiki Activity

code-style and documentation tidying (#34)

Browse Source 
* Remove `unwrap()` from code
Remove `unwrap()` from the code (except tests).
Replaced it by either using `expect()` or handling the error more
gracefully.

* Improve documentation
Add examples on how to use the library
Add explanaitions on the dual use of crate::datatypes::Term
Relates to #33 

* Update README
* Add contributing guidelines
This commit is contained in:
Stefan Ellmauthaler 2022-03-14 21:05:53 +01:00 committed by GitHub
parent 31d6c88d90
commit 80915b1df8
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
9 changed files with 314 additions and 79 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

80
.github/CONTRIBUTING.md vendored Normal file
View File

@ -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 `<module.rs>` 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

55
README.md
View File

@ -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] <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
--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> 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]
adf_bdd [OPTIONS] <INPUT>
ARGS:
<input> Input filename
<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
--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

88
bin/src/main.rs
View File

@ -17,33 +17,36 @@ In addition some further features, like counter-model counting is not supported
# Usage
```plain
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
--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> 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]
adf_bdd [OPTIONS] <INPUT>
ARGS:
<input> Input filename
<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
--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<String>,
/// 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();

8
lib/src/adf.rs
View File

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

8
lib/src/adfbiodivine.rs
View File

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

10
lib/src/datatypes/adf.rs
View File

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

133
lib/src/lib.rs
View File

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

2
lib/src/obdd.rs
View File

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

9
lib/src/parser.rs
View File

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