diff --git a/README.md b/README.md index 9ace703..ee31d04 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,6 @@ ![GitHub Workflow Status](https://img.shields.io/github/workflow/status/ellmau/adf-obdd/Code%20coverage%20with%20tarpaulin) [![Coveralls](https://img.shields.io/coveralls/github/ellmau/adf-obdd)](https://coveralls.io/github/ellmau/adf-obdd) ![GitHub release (latest by date including pre-releases)](https://img.shields.io/github/v/release/ellmau/adf-obdd?include_prereleases) ![GitHub (Pre-)Release Date](https://img.shields.io/github/release-date-pre/ellmau/adf-obdd?label=release%20from) ![GitHub top language](https://img.shields.io/github/languages/top/ellmau/adf-obdd) [![GitHub all releases](https://img.shields.io/github/downloads/ellmau/adf-obdd/total)](https://github.com/ellmau/adf-obdd/releases) [![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) -# Solver for ADFs grounded semantics by utilising OBDDs - ordered binary decision diagrams +# Abstract Dialectical Frameworks solved by Binary Decision Diagrams; developed in Dresden (ADF-BDD) ## Abstract Dialectical Frameworks @@ -34,6 +34,10 @@ OPTIONS: --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) @@ -77,6 +81,17 @@ Additional information for contribution, testing, and development in general can ## 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 diff --git a/bin/README.md b/bin/README.md index 37479f1..f5d1cba 100644 --- a/bin/README.md +++ b/bin/README.md @@ -1,6 +1,7 @@ -![GitHub Workflow Status](https://img.shields.io/github/workflow/status/ellmau/adf-obdd/Code%20coverage%20with%20tarpaulin) [![Coveralls](https://img.shields.io/coveralls/github/ellmau/adf-obdd)](https://coveralls.io/github/ellmau/adf-obdd) ![GitHub release (latest by date including pre-releases)](https://img.shields.io/github/v/release/ellmau/adf-obdd?include_prereleases) ![GitHub (Pre-)Release Date](https://img.shields.io/github/release-date-pre/ellmau/adf-obdd?label=release%20from) ![GitHub top language](https://img.shields.io/github/languages/top/ellmau/adf-obdd) ![GitHub all releases](https://img.shields.io/github/downloads/ellmau/adf-obdd/total) ![GitHub Discussions](https://img.shields.io/github/discussions/ellmau/adf-obdd) -# Solver for ADFs grounded semantics by utilising OBDDs - ordered binary decision diagrams +![GitHub Workflow Status](https://img.shields.io/github/workflow/status/ellmau/adf-obdd/Code%20coverage%20with%20tarpaulin) [![Coveralls](https://img.shields.io/coveralls/github/ellmau/adf-obdd)](https://coveralls.io/github/ellmau/adf-obdd) ![GitHub release (latest by date including pre-releases)](https://img.shields.io/github/v/release/ellmau/adf-obdd?include_prereleases) ![GitHub (Pre-)Release Date](https://img.shields.io/github/release-date-pre/ellmau/adf-obdd?label=release%20from) ![GitHub top language](https://img.shields.io/github/languages/top/ellmau/adf-obdd) [![GitHub all releases](https://img.shields.io/github/downloads/ellmau/adf-obdd/total)](https://github.com/ellmau/adf-obdd/releases) [![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) +This is the readme for the executable solver. ## 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. @@ -10,33 +11,40 @@ An ordered binary decision diagram is a normalised representation of binary func ## Usage ``` USAGE: - adf_bdd [FLAGS] [OPTIONS] + adf_bdd [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) +ARGS: + Input filename 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] - -ARGS: - Input filename + --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 + --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 @@ -65,6 +73,16 @@ The binary predicate ac relates each statement to one propositional formula in p - c(f): constant symbol "falsum" - inconsistency/bot # Development notes +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 +``` + To run all the tests placed in the submodule you need to run ```bash $> git submodule init diff --git a/lib/Cargo.toml b/lib/Cargo.toml index d5c8a72..06f4be8 100644 --- a/lib/Cargo.toml +++ b/lib/Cargo.toml @@ -3,6 +3,7 @@ name = "adf_bdd" version = "0.2.4" authors = ["Stefan Ellmauthaler "] edition = "2021" +homepage = "https://ellmau.github.io/adf-obdd/" repository = "https://github.com/ellmau/adf-obdd/" license = "GPL-3.0-only" exclude = ["res/", "./flake*", "flake.lock", "*.nix", ".envrc", "_config.yml", "tarpaulin-report.*", "*~"] diff --git a/lib/README.md b/lib/README.md deleted file mode 120000 index 32d46ee..0000000 --- a/lib/README.md +++ /dev/null @@ -1 +0,0 @@ -../README.md \ No newline at end of file diff --git a/lib/README.md b/lib/README.md new file mode 100644 index 0000000..b910504 --- /dev/null +++ b/lib/README.md @@ -0,0 +1,115 @@ +![GitHub Workflow Status](https://img.shields.io/github/workflow/status/ellmau/adf-obdd/Code%20coverage%20with%20tarpaulin) [![Coveralls](https://img.shields.io/coveralls/github/ellmau/adf-obdd)](https://coveralls.io/github/ellmau/adf-obdd) ![GitHub release (latest by date including pre-releases)](https://img.shields.io/github/v/release/ellmau/adf-obdd?include_prereleases) ![GitHub (Pre-)Release Date](https://img.shields.io/github/release-date-pre/ellmau/adf-obdd?label=release%20from) ![GitHub top language](https://img.shields.io/github/languages/top/ellmau/adf-obdd) [![GitHub all releases](https://img.shields.io/github/downloads/ellmau/adf-obdd/total)](https://github.com/ellmau/adf-obdd/releases) [![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) +This library contains an efficient representation of Abstract Dialectical Frameworks (ADf) by utilising an implementation of Ordered Binary Decision Diagrams (OBDD) + +## Abstract Dialectical Frameworks + +An abstract dialectical framework 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. + +### Noteworthy relations between semantics + +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 + + +## 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. + +Note that one advantage of this implementation is that only one oBDD is used for all acceptance conditions. This can be done because all of them have the identical signature (i.e. the set of all statements + top and bottom concepts). Due to this uniform representation reductions on subformulae which are shared by two or more statements only need to be computed once and is already cached in the data structure for further applications. + +The used algorithm to create a BDD, based on a given formula does not perform well on bigger formulae, therefore it is possible to use a state-of-the art library to instantiate the BDD (https://github.com/sybila/biodivine-lib-bdd). It is possible to either stay with the biodivine library or switch back to the variant implemented by adf-bdd. The variant implemented in this library offers reuse of already done reductions and memoisation techniques, which are not offered by biodivine. In addition some further features, like counter-model counting is not supported by biodivine. + +Note that import and export only works if the naive library is chosen + +## 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: +```plain +and(x,y): conjunction +or(x,y): disjunctin +iff(x,Y): if and only if +xor(x,y): exclusive or +neg(x): classical negation +c(v): constant symbol “verum” - tautology/top +c(f): constant symbol “falsum” - inconsistency/bot +``` + +### Example input file: +```plain +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 +// 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 +// 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 +// 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)); +} +``` diff --git a/lib/src/adf.rs b/lib/src/adf.rs index fafb08b..03ebffc 100644 --- a/lib/src/adf.rs +++ b/lib/src/adf.rs @@ -1,5 +1,5 @@ /*! -This module describes the abstract dialectical framework +This module describes the abstract dialectical framework. - computing interpretations and models - computing fixpoints @@ -20,7 +20,7 @@ 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. +/// Representation of an ADF, with an ordering and dictionary which relates statements to numbers, a binary decision diagram, and a list of acceptance conditions in [`Term`][crate::datatypes::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 { @@ -40,7 +40,7 @@ impl Default for Adf { } impl Adf { - /// Instantiates a new ADF, based on the parser-data + /// Instantiates a new ADF, based on the [parser-data][crate::parser::AdfParser]. pub fn from_parser(parser: &AdfParser) -> Self { log::info!("[Start] instantiating BDD"); let mut result = Self { @@ -134,7 +134,7 @@ impl Adf { result } - /// Instantiates a new ADF, based on a biodivine adf + /// Instantiates a new ADF, based on a [biodivine adf][crate::adfbiodivine::Adf]. pub fn from_biodivine(bio_adf: &super::adfbiodivine::Adf) -> Self { Self::from_biodivine_vector(bio_adf.var_container(), bio_adf.ac()) } @@ -179,7 +179,7 @@ impl Adf { } } - /// Computes the grounded extension and returns it as a list + /// Computes the grounded extension and returns it as a list. pub fn grounded(&mut self) -> Vec { log::info!("[Start] grounded"); let ac = &self.ac.clone(); @@ -351,7 +351,7 @@ impl Adf { /// Computes the stable models. /// Returns an iterator which contains all stable models. - /// This variant uses the heuristic, which uses maximal var impact, minimal self-cyclye impact and the minimal amount of paths . + /// This variant uses the heuristic, which uses maximal [var impact][crate::obdd::Bdd::passive_var_impact], minimal [self-cycle impact][crate::obdd::Bdd::active_var_impact] and the minimal amount of [paths][crate::obdd::Bdd::paths]. pub fn stable_count_optimisation_heu_a<'a, 'c>( &'a mut self, ) -> impl Iterator> + 'c @@ -367,7 +367,7 @@ impl Adf { /// Computes the stable models. /// Returns an iterator which contains all stable models. - /// This variant uses the heuristic, which uses minimal number of paths and maximal variable-impact. + /// This variant uses the heuristic, which uses minimal number of [paths][crate::obdd::Bdd::paths] and maximal [variable-impact][crate::obdd::Bdd::passive_var_impact]. pub fn stable_count_optimisation_heu_b<'a, 'c>( &'a mut self, ) -> impl Iterator> + 'c @@ -420,13 +420,13 @@ impl Adf { ) -> std::cmp::Ordering { match self .bdd - .var_impact(rhs.0, interpr) - .cmp(&self.bdd.var_impact(lhs.0, interpr)) + .passive_var_impact(rhs.0, interpr) + .cmp(&self.bdd.passive_var_impact(lhs.0, interpr)) { std::cmp::Ordering::Equal => match self .bdd - .nacyc_var_impact(lhs.0, interpr) - .cmp(&self.bdd.nacyc_var_impact(rhs.0, interpr)) + .active_var_impact(lhs.0, interpr) + .cmp(&self.bdd.active_var_impact(rhs.0, interpr)) { std::cmp::Ordering::Equal => self .bdd @@ -453,8 +453,8 @@ impl Adf { { std::cmp::Ordering::Equal => self .bdd - .var_impact(rhs.0, interpr) - .cmp(&self.bdd.var_impact(lhs.0, interpr)), + .passive_var_impact(rhs.0, interpr) + .cmp(&self.bdd.passive_var_impact(lhs.0, interpr)), value => value, } @@ -653,7 +653,7 @@ impl Adf { .collect() } - /// creates a [PrintableInterpretation] for output purposes + /// Creates a [PrintableInterpretation] for output purposes. pub fn print_interpretation<'a, 'b>( &'a self, interpretation: &'b [Term], @@ -664,12 +664,12 @@ impl Adf { PrintableInterpretation::new(interpretation, &self.ordering) } - /// creates a [PrintDictionary] for output purposes + /// Creates a [PrintDictionary] for output purposes. pub fn print_dictionary(&self) -> PrintDictionary { PrintDictionary::new(&self.ordering) } - /// Fixes the bdd after an import with serde + /// Fixes the bdd after an import with serde. pub fn fix_import(&mut self) { self.bdd.fix_import(); } diff --git a/lib/src/adfbiodivine.rs b/lib/src/adfbiodivine.rs index 6c0ede9..6d57370 100644 --- a/lib/src/adfbiodivine.rs +++ b/lib/src/adfbiodivine.rs @@ -1,5 +1,7 @@ //! This module describes the abstract dialectical framework -//! utilising the biodivine-lib-bdd (see ) BDD implementation to compute the +//! utilising the biodivine-lib-bdd (see ) BDD implementation to compute various semantics. +//! +//! These are currently the //! - grounded //! - stable //! - complete @@ -21,7 +23,7 @@ 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) +/// Representation of an ADF, with an ordering and dictionary which relates statements to numbers, 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 { @@ -34,7 +36,7 @@ pub struct Adf { } impl Adf { - /// Instantiates a new ADF, based on the parser-data + /// Instantiates a new ADF, based on the parser-data. pub fn from_parser(parser: &AdfParser) -> Self { log::info!("[Start] instantiating BDD"); let mut bdd_var_builder = biodivine_lib_bdd::BddVariableSetBuilder::new(); @@ -78,7 +80,7 @@ impl Adf { result } - /// Instantiates a new ADF and prepares a rewriting for the stable model computation based on the parser-data + /// Instantiates a new ADF and prepares a rewriting for the stable model computation based on the parser-data. pub fn from_parser_with_stm_rewrite(parser: &AdfParser) -> Self { let mut result = Self::from_parser(parser); log::debug!("[Start] rewriting"); @@ -108,7 +110,7 @@ impl Adf { self.rewrite = Some(self.varset.eval_expression(&expr)); } - /// returns `true` if the stable rewriting for this adf exists + /// returns `true` if the stable rewriting for this ADF exists. pub fn has_stm_rewriting(&self) -> bool { self.rewrite.is_some() } @@ -120,7 +122,7 @@ impl Adf { pub(crate) fn ac(&self) -> &[Bdd] { &self.ac } - /// Computes the grounded extension and returns it as a list + /// Computes the grounded extension and returns it as a list. pub fn grounded(&self) -> Vec { log::info!("[Start] grounded"); let ac = &self.ac.clone(); @@ -186,8 +188,8 @@ impl Adf { new_interpretation } - /// Computes the complete models - /// Returns an Iterator which contains all the complete models + /// Computes the complete models. + /// Returns an [Iterator][std::iter::Iterator] which contains all the complete models. pub fn complete<'a, 'b>(&'a self) -> impl Iterator> + 'b where 'a: 'b, @@ -205,7 +207,7 @@ impl Adf { /// Shifts the representation and allows to use the naive approach. /// - /// The grounded interpretation is computed by the biodivine library first. + /// The grounded interpretation is computed by the [biodivine library](https://github.com/sybila/biodivine-lib-bdd) first. pub fn hybrid_step(&self) -> crate::adf::Adf { crate::adf::Adf::from_biodivine_vector( self.var_container(), @@ -215,7 +217,7 @@ impl Adf { /// Shifts the representation and allows to use the naive approach. /// - /// `bio_grounded` will compute the grounded, based on biodivine, first. + /// `bio_grounded` will compute the grounded, based on [biodivine](https://github.com/sybila/biodivine-lib-bdd), first. pub fn hybrid_step_opt(&self, bio_grounded: bool) -> crate::adf::Adf { if bio_grounded { self.hybrid_step() @@ -224,8 +226,8 @@ impl Adf { } } - /// Computes the stable models - /// Returns an Iterator which contains all the stable models + /// Computes the stable models. + /// Returns an [Iterator][std::iter::Iterator] which contains all the stable models. pub fn stable<'a, 'b>(&'a self) -> impl Iterator> + 'b where 'a: 'b, @@ -258,8 +260,8 @@ impl Adf { ) } - /// Computes the stable models - /// This variant returns all stable models and utilises a rewrite of the adf as one big conjunction of equalities (iff) + /// Computes the stable models. + /// This variant returns all stable models and utilises a rewrite of the ADF as one big conjunction of equalities (`if and only if`). pub fn stable_bdd_representation(&self) -> Vec> { let smc = self.stable_model_candidates(); log::debug!("[Start] checking for stability"); @@ -339,7 +341,7 @@ impl Adf { ) } - /// creates a [PrintableInterpretation] for output purposes + /// Creates a [PrintableInterpretation] for output purposes. pub fn print_interpretation<'a, 'b>( &'a self, interpretation: &'b [Term], @@ -350,18 +352,18 @@ impl Adf { PrintableInterpretation::new(interpretation, &self.ordering) } - /// creates a [PrintDictionary] for output purposes + /// Creates a [PrintDictionary] for output purposes. pub fn print_dictionary(&self) -> PrintDictionary { PrintDictionary::new(&self.ordering) } } -/// Provides Adf-Specific operations on truth valuations +/// Provides ADF-Specific operations on truth valuations. pub trait AdfOperations { - /// Returns `true` if the BDD is either valid or unsatisfiable + /// Returns `true` if the roBDD is either valid or unsatisfiable. fn is_truth_value(&self) -> bool; - /// Compares whether the information between two given BDDs are the same + /// Compares whether the information between two given roBDDs are the same. fn cmp_information(&self, other: &Self) -> bool; } @@ -375,11 +377,11 @@ impl AdfOperations for Bdd { } } -/// Implementations of the restrict-operations on BDDs +/// Implementations of the restrict-operations on roBDDs. pub trait BddRestrict { - /// Provides an implementation of the restrict-operation on BDDs for one variable + /// Provides an implementation of the restrict-operation on roBDDs for one variable. fn var_restrict(&self, variable: biodivine_lib_bdd::BddVariable, value: bool) -> Self; - /// Provides an implementation of the restrict-operation on a set of variables + /// Provides an implementation of the restrict-operation on a set of variables. fn restrict(&self, variables: &[(biodivine_lib_bdd::BddVariable, bool)]) -> Self; } diff --git a/lib/src/datatypes.rs b/lib/src/datatypes.rs index 1711c12..f9f29c5 100644 --- a/lib/src/datatypes.rs +++ b/lib/src/datatypes.rs @@ -1,4 +1,4 @@ -//! A collection of all the necessary datatypes of the system. +//! Collection of all the necessary datatypes of the system. pub mod adf; mod bdd; pub use bdd::*; diff --git a/lib/src/datatypes/adf.rs b/lib/src/datatypes/adf.rs index e6e4edd..2716d4f 100644 --- a/lib/src/datatypes/adf.rs +++ b/lib/src/datatypes/adf.rs @@ -1,4 +1,4 @@ -//! Repesentation of all needed ADF based datatypes +//! Representation of all needed ADF based datatypes. use super::{Term, Var}; use serde::{Deserialize, Serialize}; @@ -47,7 +47,7 @@ impl VarContainer { Rc::clone(&self.names) } } -/// A struct which holds the dictionary to print interpretations and allows to instantiate printable interpretations +/// A struct which holds the dictionary to print interpretations and allows to instantiate printable interpretations. #[derive(Debug)] pub struct PrintDictionary { ordering: VarContainer, @@ -115,8 +115,8 @@ impl Display for PrintableInterpretation<'_> { } } -/// Provides an Iterator, which contains all two valued Interpretations, with respect to the given -/// 3-valued interpretation. +/// Provides an [Iterator][std::iter::Iterator], which contains all two valued interpretations, with respect to the given +/// three valued interpretation. #[derive(Debug)] pub struct TwoValuedInterpretationsIterator { @@ -126,7 +126,7 @@ pub struct TwoValuedInterpretationsIterator { } impl TwoValuedInterpretationsIterator { - /// Creates a new iterable structure, which represents all two-valued interpretations wrt. the given 3-valued interpretation + /// Creates a new iterable structure, which represents all two-valued interpretations wrt. the given three valued interpretation. pub fn new(term: &[Term]) -> Self { let indexes = term .iter() diff --git a/lib/src/datatypes/bdd.rs b/lib/src/datatypes/bdd.rs index 8e59890..b1c2975 100644 --- a/lib/src/datatypes/bdd.rs +++ b/lib/src/datatypes/bdd.rs @@ -1,14 +1,14 @@ //! To represent a BDD, a couple of datatypes is needed. //! This module consists of all internally and externally used datatypes, such as -//! [Term], [Var], and [BddNode] +//! [Term], [Var], and [BddNode]. use serde::{Deserialize, Serialize}; use std::{fmt::Display, ops::Deref}; use crate::adfbiodivine::AdfOperations; -/// Representation of a Term -/// Each Term is represented in a number ([usize]) and relates to a -/// Node in the decision diagram +/// Representation of a Term. +/// Each [`Term`] is represented in a number ([usize]) and relates to a +/// node in the [BDD][crate::obdd::Bdd]. #[derive(Debug, Eq, PartialEq, PartialOrd, Ord, Hash, Copy, Clone, Serialize, Deserialize)] pub struct Term(pub usize); @@ -44,14 +44,16 @@ impl Display for Term { } impl Term { - /// Represents the truth-value bottom, i.e. false + /// Represents the truth-value bottom, i.e., false. pub const BOT: Term = Term(0); - /// Represents the truth-value top, i.e. true + /// Represents the truth-value top, i.e., true. pub const TOP: Term = Term(1); - /// Represents the truth-value undecided, i.e. sat, but not valid + /// Represents the truth-value undecided, i.e., sat, but not valid. + /// + /// In other words, we are describing a truth-value, which still allows a consistent solution, but is not necessarily decided yet. pub const UND: Term = Term(2); - /// Get the value of the Term, i.e. the corresponding [usize] + /// Get the value of the [Term], i.e., the corresponding [usize]. pub fn value(self) -> usize { self.0 } @@ -62,17 +64,17 @@ impl Term { self.0 <= Term::TOP.0 } - /// Returns true, if the Term is true, i.e. [Term::TOP] + /// Returns [true], if the [Term] is true, i.e., [Term::TOP]. pub fn is_true(&self) -> bool { *self == Self::TOP } - /// Returns true, if the Terms have the same information-value + /// Returns [true], if the [Term]s have the same information-value. pub fn compare_inf(&self, other: &Self) -> bool { self.is_truth_value() == other.is_truth_value() && self.is_true() == other.is_true() } - /// Returns true if the information of *other* does not decrease and it is not inconsistent. + /// Returns [true] if the information of **other** does not decrease and it is not inconsistent. pub fn no_inf_inconsistency(&self, other: &Self) -> bool { if self.compare_inf(other) { return true; @@ -80,15 +82,15 @@ impl Term { !self.is_truth_value() } - /// Returns true, if the Term and the BDD have the same information-value + /// Returns [true], if the [Term] and the roBDD have the same information-value. pub fn cmp_information(&self, other: &biodivine_lib_bdd::Bdd) -> bool { self.is_truth_value() == other.is_truth_value() && self.is_true() == other.is_true() } } -/// Representation of Variables +/// Representation of variables. /// Note that the algorithm only uses [usize] values to identify variables. -/// The order of these values will be defining for the Variable order of the decision diagram. +/// The order of these values will be defining for the [variable][Var] order of the roBDD. #[derive(Debug, Eq, PartialEq, PartialOrd, Ord, Hash, Clone, Copy, Serialize, Deserialize)] pub struct Var(pub usize); @@ -112,23 +114,23 @@ impl Display for Var { } impl Var { - /// Represents the constant symbol "Top" + /// Represents the constant symbol "⊤", which stands for the "verum" concept. pub const TOP: Var = Var(usize::MAX); - /// Represents the constant symbol "Bot" + /// Represents the constant symbol "⊥", which stands for the "falsum" concept. pub const BOT: Var = Var(usize::MAX - 1); - /// Returns the value of the [Var] as [usize] + /// Returns the value of the [variable][Var] as [usize]. pub fn value(self) -> usize { self.0 } - /// Returns true if the value of the variable is a constant (i.e. Top or Bot) + /// Returns [true] if the value of the [variable][Var] is a constant (i.e., [BOT][Var::BOT] or [TOP][Var::TOP]). pub fn is_constant(&self) -> bool { self.value() >= Var::BOT.value() } } -/// A [BddNode] is representing one Node in the decision diagram +/// A [BddNode] is representing one Node in the decision diagram. /// /// Intuitively this is a binary tree structure, where the diagram is allowed to /// pool same values to the same Node. @@ -146,27 +148,27 @@ impl Display for BddNode { } impl BddNode { - /// Creates a new Node + /// Creates a new Node. pub fn new(var: Var, lo: Term, hi: Term) -> Self { Self { var, lo, hi } } - /// Returns the current Variable-value + /// Returns the current Variable-value. pub fn var(self) -> Var { self.var } - /// Returns the `lo`-branch + /// Returns the `lo`-branch. pub fn lo(self) -> Term { self.lo } - /// Returns the `hi`-branch + /// Returns the `hi`-branch. pub fn hi(self) -> Term { self.hi } - /// Creates a node, which represents the `Bot`-truth value + /// Creates a node, which represents the `Bot`-truth value. pub fn bot_node() -> Self { Self { var: Var::BOT, @@ -175,7 +177,7 @@ impl BddNode { } } - /// Creates a node, which represents the `Top`-truth value + /// Creates a node, which represents the `Top`-truth value. pub fn top_node() -> Self { Self { var: Var::TOP, @@ -186,21 +188,24 @@ impl BddNode { } /// Represents the pair of counts, related to counter-models and models. +/// +/// A model of a formula is an interpretation such that the formula evaluates to true with respect to the interpretation. +/// A counter-model of a formula is an interpretation such that the formula evaluates to false with respect to the interpretation. #[derive(Debug, Clone, Copy, Eq, PartialEq, PartialOrd, Ord)] pub struct ModelCounts { - /// Contains the number of counter-models + /// Contains the number of counter-models. pub cmodels: usize, - /// Contains the number of models + /// Contains the number of models. pub models: usize, } impl ModelCounts { - /// Represents the top-node model-counts + /// Represents the top-node model-counts. pub fn top() -> ModelCounts { (0, 1).into() } - /// Represents the bot-node model-counts + /// Represents the bot-node model-counts. pub fn bot() -> ModelCounts { (1, 0).into() } @@ -210,8 +215,8 @@ impl ModelCounts { self.models.min(self.cmodels) } - /// Returns true, if there are more models than counter-models. - /// If they are equal, the function returns true too. + /// Returns [true], if there are more models than counter-models. + /// If they are equal, the function returns [true] too. pub fn more_models(&self) -> bool { self.models >= self.minimum() } @@ -225,9 +230,9 @@ impl From<(usize, usize)> for ModelCounts { } } } -/// Type alias for the Modelcounts, Count of paths to bot resp top, and the depth of a given Node in a BDD +/// Type alias for the [Modelcounts][ModelCounts], count of paths to ⊥ respectively ⊤, and the depth of a given node in an roBDD. pub type CountNode = (ModelCounts, ModelCounts, usize); -/// Type alias for Facet counts, which contains number of facets and counter facets. +/// Type alias for [Facet counts][FacetCounts], which contains the number of facets and counter-facets. pub type FacetCounts = (usize, usize); #[cfg(test)] diff --git a/lib/src/lib.rs b/lib/src/lib.rs index 98e7307..f50c4df 100644 --- a/lib/src/lib.rs +++ b/lib/src/lib.rs @@ -1,42 +1,43 @@ /*! -This library contains an efficient representation of `Abstract Dialectical Frameworks (ADf)` by utilising an implementation of `Ordered Binary Decision Diagrams (OBDD)` +This library contains an efficient representation of `Abstract Dialectical Frameworks (ADF)` by utilising an implementation of `Ordered Binary Decision Diagrams (OBDD)` # Abstract Dialectical Frameworks -An `abstract dialectical framework` 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. - -Note that one advantage of this implementation is that only one oBDD is used for all acceptance conditions. This can be done because all of them have the identical signature (i.e. the set of all statements + top and bottom concepts). -Due to this uniform representation reductions on subformulae which are shared by two or more statements only need to be computed once and is already cached in the data structure for further applications. - -The used algorithm to create a BDD, based on a given formula does not perform well on bigger formulae, therefore it is possible to use a state-of-the art library to instantiate the BDD (). -It is possible to either stay with the biodivine library or switch back to the variant implemented by adf-bdd. -The variant implemented in this library offers reuse of already done reductions and memoisation techniques, which are not offered by biodivine. -In addition some further features, like counter-model counting is not supported by biodivine. - -Note that import and export only works if the naive library is chosen +An `abstract dialectical framework` consists of abstract statements. Each statement has a 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 interpretation. ## Noteworthy relations between semantics -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 always exists 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: -- and(x,y): conjunction -- or(x,y): disjunctin -- iff(x,Y): if and only if -- xor(x,y): exclusive or -- neg(x): classical negation -- c(v): constant symbol "verum" - tautology/top -- c(f): constant symbol "falsum" - inconsistency/bot +# Reduced Ordered Binary Decision Diagram (roBDD) +A `reduced ordered binary decision diagram` is a normalised representation of binary functions, where satisfiability- and validity checks can be done relatively cheap and no redundant information is stored. + +Note that one advantage of this implementation is that only one structure is used for all acceptance conditions. This can be done because all of them have the identical signature (i.e., the set of all statements + top and bottom concepts). +Due to this uniform representation reductions on subformulae which are shared by two or more statements only need to be computed once and will be cached in the data structure for further applications. + +The naively used algorithm to create an roBDD, based on a given formula does not perform well on bigger formulae, therefore it is possible to use a state-of-the art library to instantiate the roBDD (). +It is possible to either stay with the biodivine library or switch back to the variant implemented by adf-bdd. +The variant implemented in this library offers reuse of already done reductions and memoisation techniques, which are not offered by biodivine. +In addition some further features, like counter-model counting is not supported by biodivine. + +Note that import and export only works if the naive library is chosen. + +# 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: +- `and(x,y)`: conjunction +- `or(x,y)`: disjunction +- `iff(x,Y)`: if and only if +- `xor(x,y)`: exclusive or +- `neg(x)`: classical negation +- `c(v)`: constant symbol "verum" - tautology/top +- `c(f)`: constant symbol "falsum" - inconsistency/bot */ /*! diff --git a/lib/src/obdd.rs b/lib/src/obdd.rs index edb4570..97f9268 100644 --- a/lib/src/obdd.rs +++ b/lib/src/obdd.rs @@ -1,12 +1,16 @@ -//! Represents an obdd +//! Module which represents obdds. +//! pub mod vectorize; use crate::datatypes::*; use serde::{Deserialize, Serialize}; use std::collections::HashSet; use std::{cell::RefCell, cmp::min, collections::HashMap, fmt::Display}; +/// Contains the data of (possibly) multiple roBDDs, managed over one collection of nodes. +/// It has a couple of methods to instantiate, update, and query properties on a given roBDD. +/// Each roBDD is identified by its corresponding [`Term`], which implicitly identifies the root node of a roBDD. #[derive(Debug, Serialize, Deserialize)] -pub(crate) struct Bdd { +pub struct Bdd { pub(crate) nodes: Vec, #[cfg(feature = "variablelist")] #[serde(skip)] @@ -27,7 +31,15 @@ impl Display for Bdd { } } +impl Default for Bdd { + fn default() -> Self { + Self::new() + } +} + impl Bdd { + /// Instantiate a new roBDD structures. + /// Constants for the [`⊤`][crate::datatypes::Term::TOP] and [`⊥`][crate::datatypes::Term::BOT] concepts are prepared in that step too. pub fn new() -> Self { #[cfg(not(feature = "adhoccounting"))] { @@ -64,10 +76,12 @@ impl Bdd { RefCell::new(HashMap::new()) } + /// Instantiates a [variable][crate::datatypes::Var] and returns the representing roBDD as a [`Term`][crate::datatypes::Term]. pub fn variable(&mut self, var: Var) -> Term { self.node(var, Term::BOT, Term::TOP) } + /// Instantiates a constant, which is either [true] or [false]. pub fn constant(val: bool) -> Term { if val { Term::TOP @@ -76,35 +90,41 @@ impl Bdd { } } + /// Returns an roBDD, which represents the negation of the given roBDD. pub fn not(&mut self, term: Term) -> Term { self.if_then_else(term, Term::BOT, Term::TOP) } + /// Returns an roBDD, which represents the conjunction of the two given roBDDs. pub fn and(&mut self, term_a: Term, term_b: Term) -> Term { self.if_then_else(term_a, term_b, Term::BOT) } + /// Returns an roBDD, which represents the disjunction of the two given roBDDs. pub fn or(&mut self, term_a: Term, term_b: Term) -> Term { self.if_then_else(term_a, Term::TOP, term_b) } + /// Returns an roBDD, which represents the implication of the two given roBDDs. pub fn imp(&mut self, term_a: Term, term_b: Term) -> Term { self.if_then_else(term_a, term_b, Term::TOP) } + /// Returns an roBDD, which represents the if and only if relation of the two given roBDDs. pub fn iff(&mut self, term_a: Term, term_b: Term) -> Term { let not_b = self.not(term_b); self.if_then_else(term_a, term_b, not_b) } + /// Returns an roBDD, which represents the exclusive disjunction of the two given roBDDs. pub fn xor(&mut self, term_a: Term, term_b: Term) -> Term { let not_b = self.not(term_b); self.if_then_else(term_a, not_b, term_b) } - /// Computes the interpretations represented in the reduced BDD, which are either models or none. - /// *goal_var* is the variable to which the BDD is related to and it is ensured that the goal is consistent with the respective interpretation - /// *goal* is a boolean variable, which defines whether the models or inconsistent interpretations are of interest + /// Computes the interpretations represented in the roBDD, which are either models or counter-models. + /// **goal_var** is the [variable][Var] to which the roBDD is related to and it is ensured that the goal is consistent with the respective interpretation. + /// **goal** is a boolean [variable][Var], which defines whether the models or counter-models are of interest. pub fn interpretations( &self, tree: Term, @@ -154,6 +174,7 @@ impl Bdd { result } + /// Restrict the value of a given [variable][crate::datatypes::Var] to **val**. pub fn restrict(&mut self, tree: Term, var: Var, val: bool) -> Term { let node = self.nodes[tree.0]; #[cfg(feature = "variablelist")] @@ -179,6 +200,7 @@ impl Bdd { } } + /// Creates an roBDD, based on the relation of three roBDDs, which are in an `if-then-else` relation. fn if_then_else(&mut self, i: Term, t: Term, e: Term) -> Term { if i == Term::TOP { t @@ -208,6 +230,9 @@ impl Bdd { self.node(minvar, bot_ite, top_ite) } } + + /// Creates a new node in the roBDD. + /// It will not create duplicate nodes and uses already existing nodes, if applicable. pub fn node(&mut self, var: Var, lo: Term, hi: Term) -> Term { if lo == hi { lo @@ -281,9 +306,9 @@ impl Bdd { } } - /// Computes the number of counter-models and models for a given BDD-tree. + /// Computes the number of counter-models and models for a given roBDD. /// - /// Use the flag `_memoization` to choose between using the memoization approach or not. (This flag does nothing if the feature `adhoccounting` is used) + /// Use the flag `_memoization` to choose between using the memoization approach or not. (This flag does nothing, if the feature `adhoccounting` is used) pub fn models(&self, term: Term, _memoization: bool) -> ModelCounts { #[cfg(feature = "adhoccounting")] { @@ -297,9 +322,9 @@ impl Bdd { } } - /// Computes the number of paths which lead to Bot respectively Top. + /// Computes the number of paths, which lead to ⊥ respectively ⊤. /// - /// Use the flag `_memoization` to choose between using the memoization approach or not. (This flag does nothing if the feature `adhoccounting` is used) + /// Use the flag `_memoization` to choose between using the memoization approach or not. (This flag does nothing, if the feature `adhoccounting` is used) pub fn paths(&self, term: Term, _memoization: bool) -> ModelCounts { #[cfg(feature = "adhoccounting")] { @@ -313,7 +338,9 @@ impl Bdd { } } - /// Computes the maximal depth of the given sub-tree. + /// Computes the maximal depth of the given sub-diagram. + /// + /// Intuitively this will compute the longest possible path from **term** to a leaf-node (i.e., ⊥ or ⊤). #[allow(dead_code)] // max depth may be used in future heuristics pub fn max_depth(&self, term: Term) -> usize { #[cfg(feature = "adhoccounting")] @@ -335,7 +362,7 @@ impl Bdd { } #[allow(dead_code)] // dead code due to more efficient ad-hoc building, still used for a couple of tests - /// Computes the number of counter-models, models, and variables for a given BDD-tree + /// Computes the number of counter-models, models, and variables for a given roBDD fn modelcount_naive(&self, term: Term) -> CountNode { if term == Term::TOP { (ModelCounts::top(), ModelCounts::top(), 0) @@ -409,7 +436,7 @@ impl Bdd { } } - /// repairs the internal structures after an import + /// Repairs the internal structures after an import. pub fn fix_import(&mut self) { self.generate_var_dependencies(); #[cfg(feature = "adhoccounting")] @@ -443,6 +470,7 @@ impl Bdd { }); } + /// Returns a [HashSet] of [variables][crate::datatypes::Var], which occur in a given roBDD. pub fn var_dependencies(&self, tree: Term) -> HashSet { #[cfg(feature = "variablelist")] { @@ -464,7 +492,8 @@ impl Bdd { } } - pub fn var_impact(&self, var: Var, termlist: &[Term]) -> usize { + /// Returns the variable impact of a [variable][crate::datatypes::Var] with respect to a given set of roBDDs. + pub fn passive_var_impact(&self, var: Var, termlist: &[Term]) -> usize { termlist.iter().fold(0usize, |acc, val| { if self.var_dependencies(*val).contains(&var) { acc + 1 @@ -474,7 +503,8 @@ impl Bdd { }) } - pub fn nacyc_var_impact(&self, var: Var, termlist: &[Term]) -> usize { + /// Counts how often another roBDD uses a [variable][crate::datatypes::Var], which occurs in this roBDD. + pub fn active_var_impact(&self, var: Var, termlist: &[Term]) -> usize { (0..termlist.len()).into_iter().fold(0usize, |acc, idx| { if self .var_dependencies(termlist[var.value()]) @@ -738,14 +768,17 @@ mod test { }); assert_eq!( - bdd.var_impact(Var(0), &[formula1, formula2, formula3, formula4]), + bdd.passive_var_impact(Var(0), &[formula1, formula2, formula3, formula4]), 4 ); assert_eq!( - bdd.var_impact(Var(2), &[formula1, formula2, formula3, formula4]), + bdd.passive_var_impact(Var(2), &[formula1, formula2, formula3, formula4]), 1 ); - assert_eq!(bdd.var_impact(Var(2), &[formula1, formula2, formula3]), 0); + assert_eq!( + bdd.passive_var_impact(Var(2), &[formula1, formula2, formula3]), + 0 + ); } #[test] @@ -760,12 +793,12 @@ mod test { let ac: Vec = vec![formula1, formula2, v3]; - assert_eq!(bdd.var_impact(Var(0), &ac), 2); - assert_eq!(bdd.var_impact(Var(1), &ac), 2); - assert_eq!(bdd.var_impact(Var(2), &ac), 1); + assert_eq!(bdd.passive_var_impact(Var(0), &ac), 2); + assert_eq!(bdd.passive_var_impact(Var(1), &ac), 2); + assert_eq!(bdd.passive_var_impact(Var(2), &ac), 1); - assert_eq!(bdd.nacyc_var_impact(Var(0), &ac), 2); - assert_eq!(bdd.nacyc_var_impact(Var(2), &ac), 1); + assert_eq!(bdd.active_var_impact(Var(0), &ac), 2); + assert_eq!(bdd.active_var_impact(Var(2), &ac), 1); } #[test] diff --git a/lib/src/obdd/vectorize.rs b/lib/src/obdd/vectorize.rs index 9619288..706de46 100644 --- a/lib/src/obdd/vectorize.rs +++ b/lib/src/obdd/vectorize.rs @@ -1,8 +1,8 @@ -//! vectorize maps with non-standard keys +//! Vectorize maps with non-standard keys. use serde::{Deserialize, Deserializer, Serialize, Serializer}; use std::iter::FromIterator; -/// Serialise into a Vector from a Map +/// Serialize into a [Vector][std::vec::Vec] from a [Map][std::collections::HashMap]. pub fn serialize<'a, T, K, V, S>(target: T, ser: S) -> Result where S: Serializer, @@ -14,7 +14,7 @@ where serde::Serialize::serialize(&container, ser) } -/// Deserialize from a Vector to a Map +/// Deserialize from a [Vector][std::vec::Vec] to a [Map][std::collections::HashMap]. pub fn deserialize<'de, T, K, V, D>(des: D) -> Result where D: Deserializer<'de>, diff --git a/lib/src/parser.rs b/lib/src/parser.rs index 42df9b4..acac346 100644 --- a/lib/src/parser.rs +++ b/lib/src/parser.rs @@ -1,5 +1,5 @@ -//! A Parser for ADFs with all needed helper-methods. -//! It utilises the [nom-crate](https://crates.io/crates/nom) +//! Parser for ADFs with all needed helper-methods. +//! It utilises the [nom-crate](https://crates.io/crates/nom). use lexical_sort::{natural_lexical_cmp, StringSort}; use nom::{ branch::alt, @@ -12,26 +12,26 @@ use nom::{ }; use std::{cell::RefCell, collections::HashMap, rc::Rc}; -/// A representation of a formula, still using the strings from the input +/// A representation of a formula, still using the strings from the input. #[derive(Clone, PartialEq, Eq)] pub enum Formula<'a> { - /// c(v) in the input format + /// `c(f)` in the input format. Bot, - /// c(f) in the input format + /// `c(v)` in the input format. Top, - /// Some atomic variable in the input format + /// Some atomic variable in the input format. Atom(&'a str), - /// Negation of a subformula + /// Negation of a subformula. Not(Box>), - /// Conjunction of two subformulae + /// Conjunction of two subformulae. And(Box>, Box>), - /// Disjunction of two subformulae + /// Disjunction of two subformulae. Or(Box>, Box>), - /// Implication of two subformulae + /// Implication of two subformulae. Imp(Box>, Box>), - /// Exclusive-Or of two subformulae + /// Exclusive-Or of two subformulae. Xor(Box>, Box>), - /// If and only if connective between two formulae + /// If and only if connective between two formulae. Iff(Box>, Box>), } @@ -122,7 +122,7 @@ impl std::fmt::Debug for Formula<'_> { /// A parse structure to hold all the information given by the input file in one place. /// /// Due to an internal representation with [RefCell][std::cell::RefCell] and [Rc][std::rc::Rc] the values can be -/// handed over to other structures without further storage needs. +/// handed over to other structures without further memory needs. /// /// Note that the parser can be utilised by an [ADF][`crate::adf::Adf`] to initialise it with minimal overhead. #[derive(Debug)] @@ -157,7 +157,7 @@ where } /// Parses a full input file and creates internal structures. - /// Note that this method returns a closure (see the following Example for the correct usage). + /// Note that this method returns a closure (see the following example for the correct usage). /// # Example /// ``` /// let parser = adf_bdd::parser::AdfParser::default(); @@ -214,7 +214,8 @@ impl AdfParser<'_> { } /// Sort the variables in lexicographical order. - /// Results which got used before might become corrupted. + /// Results, which got used before might become corrupted. + /// Ensure that all used data is physically copied. pub fn varsort_lexi(&self) -> &Self { self.namelist.as_ref().borrow_mut().sort_unstable(); self.regenerate_indizes(); @@ -222,7 +223,8 @@ impl AdfParser<'_> { } /// Sort the variables in alphanumerical order. - /// Results which got used before might become corrupted. + /// Results, which got used before might become corrupted. + /// Ensure that all used data is physically copied. pub fn varsort_alphanum(&self) -> &Self { self.namelist .as_ref() @@ -338,18 +340,22 @@ impl AdfParser<'_> { ))(input) } - /// Allows insight of the number of parsed Statements + /// Allows insight of the number of parsed statements. pub fn dict_size(&self) -> usize { //self.dict.borrow().len() self.dict.as_ref().borrow().len() } - /// Returns the number-representation and position of a given variable/statement in string-representation + /// Returns the number-representation and position of a given statement in string-representation. + /// + /// Will return [None] if the string does no occur in the dictionary. pub fn dict_value(&self, value: &str) -> Option { self.dict.as_ref().borrow().get(value).copied() } - /// Returns the acceptance condition of a statement at the given positon + /// Returns the acceptance condition of a statement at the given position. + /// + /// Will return [None] if the position does not map to a formula. pub fn ac_at(&self, idx: usize) -> Option { self.formulae.borrow().get(idx).cloned() }