diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index d5b7ef1..6b49f0c 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -1,3 +1,4 @@ +name: Build Releases on: release: types: [created] @@ -9,7 +10,7 @@ jobs: strategy: fail-fast: false matrix: - target: [x86_64-pc-windows-gnu, x86_64-unknown-linux-musl] + target: [x86_64-pc-windows-gnu, x86_64-unknown-linux-musl,x86_64-apple-darwin] steps: - uses: actions/checkout@master - name: Compile and release diff --git a/.gitmodules b/.gitmodules new file mode 100644 index 0000000..589526a --- /dev/null +++ b/.gitmodules @@ -0,0 +1,3 @@ +[submodule "res/adf-instances"] + path = res/adf-instances + url = https://github.com/ellmau/adf-instances.git diff --git a/Cargo.lock b/Cargo.lock index bd031c5..a87da58 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -8,8 +8,11 @@ version = "0.1.1" dependencies = [ "clap", "env_logger", + "lexical-sort", "log", - "test-env-log", + "nom", + "test-generator", + "test-log", ] [[package]] @@ -30,6 +33,12 @@ dependencies = [ "winapi", ] +[[package]] +name = "any_ascii" +version = "0.1.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "70033777eb8b5124a81a1889416543dddef2de240019b674c81285a2635a7e1e" + [[package]] name = "atty" version = "0.2.14" @@ -81,6 +90,12 @@ dependencies = [ "termcolor", ] +[[package]] +name = "glob" +version = "0.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9b919933a397b79c37e33b77bb2aa3dc8eb6e165ad809e58ff75bc7db2e34574" + [[package]] name = "hermit-abi" version = "0.1.19" @@ -96,6 +111,15 @@ version = "2.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9a3a5bfb195931eeb336b2a7b4d761daec841b97f947d34394601737a7bba5e4" +[[package]] +name = "lexical-sort" +version = "0.3.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c09e4591611e231daf4d4c685a66cb0410cc1e502027a20ae55f2bb9e997207a" +dependencies = [ + "any_ascii", +] + [[package]] name = "libc" version = "0.2.107" @@ -117,13 +141,48 @@ version = "2.4.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "308cc39be01b73d0d18f82a0e7b2a3df85245f84af96fdddc5d202d27e47b86a" +[[package]] +name = "minimal-lexical" +version = "0.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "68354c5c6bd36d73ff3feceb05efa59b6acb7626617f4962be322a825e61f79a" + +[[package]] +name = "nom" +version = "7.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1b1d11e1ef389c76fe5b81bcaf2ea32cf88b62bc494e19f493d0b30e7a930109" +dependencies = [ + "memchr", + "minimal-lexical", + "version_check", +] + +[[package]] +name = "proc-macro2" +version = "0.4.30" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cf3d2011ab5c909338f7887f4fc896d35932e29146c12c8d01da6b22a80ba759" +dependencies = [ + "unicode-xid 0.1.0", +] + [[package]] name = "proc-macro2" version = "1.0.32" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "ba508cc11742c0dc5c1659771673afbab7a0efab23aa17e854cbab0837ed0b43" dependencies = [ - "unicode-xid", + "unicode-xid 0.2.2", +] + +[[package]] +name = "quote" +version = "0.6.13" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6ce23b6b870e8f94f81fb0a363d65d86675884b34a09043c81e5562f11c1f8e1" +dependencies = [ + "proc-macro2 0.4.30", ] [[package]] @@ -132,7 +191,7 @@ version = "1.0.10" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "38bc8cc6a5f2e3655e0899c1b848643b2562f853f114bfec7be120678e3ace05" dependencies = [ - "proc-macro2", + "proc-macro2 1.0.32", ] [[package]] @@ -158,15 +217,26 @@ version = "0.8.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "8ea5119cdb4c55b55d432abb513a0429384878c15dde60cc77b1c99de1a95a6a" +[[package]] +name = "syn" +version = "0.15.44" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9ca4b3b69a77cbe1ffc9e198781b7acb0c7365a883670e8f1c1bc66fba79a5c5" +dependencies = [ + "proc-macro2 0.4.30", + "quote 0.6.13", + "unicode-xid 0.1.0", +] + [[package]] name = "syn" version = "1.0.81" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "f2afee18b8beb5a596ecb4a2dce128c719b4ba399d34126b9e4396e3f9860966" dependencies = [ - "proc-macro2", - "quote", - "unicode-xid", + "proc-macro2 1.0.32", + "quote 1.0.10", + "unicode-xid 0.2.2", ] [[package]] @@ -179,14 +249,26 @@ dependencies = [ ] [[package]] -name = "test-env-log" +name = "test-generator" +version = "0.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ea97be90349ab3574f6e74d1566e1c5dd3a4bc74b89f4af4cc10ca010af103c0" +dependencies = [ + "glob", + "proc-macro2 0.4.30", + "quote 0.6.13", + "syn 0.15.44", +] + +[[package]] +name = "test-log" version = "0.2.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "877189d680101869f65ef94168105d6c188b3a143c13a2d42cf8a09c4c704f8a" +checksum = "eb78caec569a40f42c078c798c0e35b922d9054ec28e166f0d6ac447563d91a4" dependencies = [ - "proc-macro2", - "quote", - "syn", + "proc-macro2 1.0.32", + "quote 1.0.10", + "syn 1.0.81", ] [[package]] @@ -204,6 +286,12 @@ version = "0.1.9" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "3ed742d4ea2bd1176e236172c8429aaf54486e7ac098db29ffe6529e0ce50973" +[[package]] +name = "unicode-xid" +version = "0.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "fc72304796d0818e357ead4e000d19c9c174ab23dc11093ac919054d20a6a7fc" + [[package]] name = "unicode-xid" version = "0.2.2" @@ -216,6 +304,12 @@ version = "0.8.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "f1bddf1187be692e79c5ffeab891132dfb0f236ed36a43c7ed39f1165ee20191" +[[package]] +name = "version_check" +version = "0.9.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5fecdca9a5291cc2b8dcf7dc02453fee791a280f3743cb0905f8822ae463b3fe" + [[package]] name = "winapi" version = "0.3.9" diff --git a/Cargo.toml b/Cargo.toml index d6b685b..f93f2b5 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,9 +1,11 @@ [package] name = "adf_bdd" -version = "0.1.1" +version = "0.1.2" authors = ["Stefan Ellmauthaler "] edition = "2021" +repository = "https://github.com/ellmau/adf-obdd/" license = "GPL-3.0-only" +exclude = ["res/", "./flake*", "*.nix", ".envrc", "_config.yml"] description = "Solver for ADFs grounded semantics by utilising OBDDs - ordered binary decision diagrams" @@ -12,8 +14,11 @@ description = "Solver for ADFs grounded semantics by utilising OBDDs - ordered b [dependencies] clap = "2.33.*" -log = "0.4" +log = { version = "0.4", features = [ "max_level_trace", "release_max_level_info" ] } +env_logger = "0.9" +nom = "7.1.0" +lexical-sort = "0.3.1" [dev-dependencies] -env_logger = "*" -test-env-log = "0.2.*" \ No newline at end of file +test-log = "0.2.*" +test-generator = "0.3.0" diff --git a/README.md b/README.md index 52a0104..72d5d5d 100644 --- a/README.md +++ b/README.md @@ -1,4 +1,4 @@ -[![.github/workflows/build.yml](https://github.com/ellmau/adf-obdd/actions/workflows/build.yml/badge.svg)](https://github.com/ellmau/adf-obdd/actions/workflows/build.yml) ![GitHub release (latest by date including pre-releases)](https://img.shields.io/github/v/release/ellmau/adf-obdd?include_prereleases) ![GitHub all releases](https://img.shields.io/github/downloads/ellmau/adf-obdd/total) +[![.github/workflows/build.yml](https://github.com/ellmau/adf-obdd/actions/workflows/build.yml/badge.svg)](https://github.com/ellmau/adf-obdd/actions/workflows/build.yml) [![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 @@ -17,3 +17,21 @@ The binary predicate ac relates each statement to one propositional formula in p - neg(x): classical negation - c(v): constant symbol "verum" - tautology/top - c(f): constant symbol "falsum" - inconsistency/bot + +# Development notes +To run all the tests placed in the submodule you need to run +```bash +$> git submodule init +``` +at the first time. +Afterwards you need to update the content of the submodule to be on the currently used revision by +```bash +$> git submodule update +``` + +The tests can be started by using the test-framework of cargo, i.e. +```bash +$> cargo test +``` +Note that some of the instances are quite big and it might take some time to finish all the tests. +If you do not initialise the submodule, tests will "only" run on the other unit-tests and (possibly forthcoming) other integration tests. diff --git a/flake.nix b/flake.nix index 008e3ca..668ef00 100644 --- a/flake.nix +++ b/flake.nix @@ -37,6 +37,8 @@ pkgs.cargo-audit pkgs.cargo-license pkgs.cargo-tarpaulin + pkgs.cargo-kcov + pkgs.kcov ]; }; } diff --git a/res/adf-instances b/res/adf-instances new file mode 160000 index 0000000..322d7d4 --- /dev/null +++ b/res/adf-instances @@ -0,0 +1 @@ +Subproject commit 322d7d44662450f25caa09c569b5f8362547907b diff --git a/src/adf.rs b/src/adf.rs index 810b835..e935ba3 100644 --- a/src/adf.rs +++ b/src/adf.rs @@ -6,469 +6,202 @@ //! - computing fixpoints //! - computing the least fixpoint by using a shortcut -#![warn(missing_docs)] - -use std::{ - collections::HashMap, - str::{self, FromStr}, - usize, +use crate::{ + datatypes::{ + adf::{PrintableInterpretation, VarContainer}, + Term, Var, + }, + obdd::Bdd, + parser::{AdfParser, Formula}, }; - -use crate::datatypes::{Term, Var}; - -use crate::obdd::Bdd; - -struct Statement { - label: String, // label of the statement - var: usize, // variable node in bdd - ac: Option, // node in bdd -} - -impl Statement { - pub fn new(label: &str, var: usize) -> Self { - Statement { - label: String::from_str(label).unwrap(), - var, - ac: None, - } - } - - pub fn _add_ac(&mut self, ac: usize) { - self.ac = Some(ac); - } -} - -/// ADF structure which offers some statice and instance methods for handling ADFs. +/// 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 pub struct Adf { + ordering: VarContainer, bdd: Bdd, - stmts: Vec, - dict: HashMap, // label to pos in vec -} - -impl Default for Adf { - fn default() -> Self { - Adf::new() - } + ac: Vec, } impl Adf { - /// Creates a new and empty ADF. - /// - /// To add statements call [`init_statements`](Adf::init_statements()) and then add to each statement it's corresponding acceptance contidion via - /// [`add_ac`](Adf::add_ac()). - pub fn new() -> Self { - Adf { + /// Instantiates a new ADF, based on the parser-data + pub fn from_parser(parser: &AdfParser) -> Self { + log::info!("[Start] instantiating BDD"); + let mut result = Self { + ordering: VarContainer::from_parser( + parser.namelist_rc_refcell(), + parser.dict_rc_refcell(), + ), bdd: Bdd::new(), - stmts: Vec::new(), - dict: HashMap::new(), + ac: vec![Term(0); parser.namelist_rc_refcell().as_ref().borrow().len()], + }; + (0..parser.namelist_rc_refcell().borrow().len()) + .into_iter() + .for_each(|value| { + log::trace!("adding variable {}", Var(value)); + result.bdd.variable(Var(value)); + }); + log::debug!("[Start] adding acs"); + parser + .formula_order() + .iter() + .enumerate() + .for_each(|(insert_order, new_order)| { + log::trace!( + "Pos {}/{} formula {}, {:?}", + insert_order + 1, + parser.formula_count(), + new_order, + parser.ac_at(insert_order) + ); + let result_term = result.term(&parser.ac_at(insert_order).unwrap()); + result.ac[*new_order] = result_term; + }); + log::info!("[Success] instantiated"); + result + } + + fn term(&mut self, formula: &Formula) -> Term { + match formula { + Formula::Bot => Bdd::constant(false), + Formula::Top => Bdd::constant(true), + Formula::Atom(val) => { + let t1 = self.ordering.variable(val).unwrap(); + self.bdd.variable(t1) + } + Formula::Not(val) => { + let t1 = self.term(val); + self.bdd.not(t1) + } + Formula::And(val1, val2) => { + let t1 = self.term(val1); + let t2 = self.term(val2); + self.bdd.and(t1, t2) + } + Formula::Or(val1, val2) => { + let t1 = self.term(val1); + let t2 = self.term(val2); + self.bdd.or(t1, t2) + } + Formula::Iff(val1, val2) => { + let t1 = self.term(val1); + let t2 = self.term(val2); + self.bdd.iff(t1, t2) + } + Formula::Xor(val1, val2) => { + let t1 = self.term(val1); + let t2 = self.term(val2); + self.bdd.xor(t1, t2) + } + Formula::Imp(val1, val2) => { + let t1 = self.term(val1); + let t2 = self.term(val2); + self.bdd.imp(t1, t2) + } } } - fn add_statement(&mut self, statement: &str) { - if self.dict.get(statement).is_none() { - let pos = self.stmts.len(); - //self.bdd.variable(pos); - //self.stmts - // .push(Statement::new(statement, pos.clone())); - self.stmts.push(Statement::new( - statement, - self.bdd.variable(Var(pos)).value(), - )); - self.dict.insert(self.stmts[pos].label.to_string(), pos); - } - } - - /// Initialise statements - /// - /// The order of statements given as a parameter will determine die ordering for the OBDD. - /// Note that only initialised statements will be regocnised as variables later on. - /// This method can be called multiple times to add more statements. - pub fn init_statements(&mut self, stmts: Vec<&str>) -> usize { - for i in stmts.iter() { - self.add_statement(*i); - } - self.stmts.len() - } - - /// Adds to a given statement its acceptance condition. - /// - /// This ac needs to be in the prefix notation for ADFs as defined by the DIAMOND implementation. - /// Every statement needs to be initialised before by [`init_statements'](Adf::init_statements()). - pub fn add_ac(&mut self, statement: &str, ac: &str) { - if let Some(stmt) = self.dict.get(statement) { - let st = *stmt; - self.add_ac_by_number(st, ac) - } - } - - fn add_ac_by_number(&mut self, st: usize, ac: &str) { - let ac_num = self.parse_formula(ac); - self.set_ac(st, ac_num); - } - - fn set_ac(&mut self, st: usize, ac: usize) { - self.stmts[st].ac = Some(ac); - } - - /// Computes the grounded model of the adf. - /// - /// Note that this computation will shortcut interpretation updates and needs less steps than computing the least fixpoint by an usual fixpoint-construction - pub fn grounded(&mut self) -> Vec { - let mut interpretation: Vec = Vec::new(); - let mut change: bool; - - for it in self.stmts.iter() { - interpretation.push((*it).ac.unwrap()) - } + /// Computes the grounded extension and returns it as a list + pub fn grounded(&mut self) -> Vec { + log::info!("[Start] grounded"); + let mut t_vals: usize = + self.ac.iter().fold( + 0, + |acc, elem| { + if elem.is_truth_value() { + acc + 1 + } else { + acc + } + }, + ); + let mut new_interpretation = self.ac.clone(); loop { - change = false; - for pos in 0..self.stmts.len() - 1 { - let curint = interpretation.clone(); - match Term(curint[pos]) { - Term::BOT => { - if let Some(n) = self.setvarvalue( - curint, - self.bdd.nodes[self.stmts[pos].var].var().value(), - false, - ) { - interpretation.clone_from(&n); - change = true; - } + let old_t_vals = t_vals; + for ac in new_interpretation + .iter_mut() + .filter(|term| !term.is_truth_value()) + { + *ac = self.ac.iter().enumerate().fold(*ac, |acc, (var, term)| { + if term.is_truth_value() { + self.bdd.restrict(acc, Var(var), term.is_true()) + } else { + acc } - Term::TOP => { - if let Some(n) = self.setvarvalue( - curint, - self.bdd.nodes[self.stmts[pos].var].var().value(), - true, - ) { - interpretation.clone_from(&n); - change = true; - } - } - _ => (), + }); + if ac.is_truth_value() { + t_vals += 1; } } - if !change { + if t_vals == old_t_vals { break; } } - interpretation - } - - /// Function not working - do not use - pub(crate) fn _complete(&mut self) -> Vec> { - let base_int = self.cur_interpretation(); - let mut complete: Vec> = Vec::new(); - let mut change: bool; - let mut pos: usize = 0; - let mut cache: HashMap, usize> = HashMap::new(); - - // compute grounded interpretation - complete.push(self.compute_fixpoint(base_int.as_ref()).unwrap()); - loop { - change = false; - let interpr = complete.get(pos).unwrap().clone(); - for (pos, it) in interpr.iter().enumerate() { - if *it > 1 { - let mut int1 = interpr.clone(); - int1[pos] = 0; - if let Some(n) = self.compute_fixpoint(int1.as_ref()) { - if !cache.contains_key(&n) { - cache.insert(n.clone(), complete.len()); - complete.push(n); - change = true; - } - } - int1[pos] = 1; - if let Some(n) = self.compute_fixpoint(int1.as_ref()) { - if !cache.contains_key(&n) { - cache.insert(n.clone(), complete.len()); - complete.push(n); - change = true; - } - } - } - } - if !change { - break; - }; - pos += 1; - // println!("{}",complete.len()); - } - complete - } - - /// represents the starting interpretation due to the acceptance conditions. (i.e. the currently represented set of formulae) - pub fn cur_interpretation(&self) -> Vec { - let mut interpretation: Vec = Vec::new(); - for it in self.stmts.iter() { - interpretation.push((*it).ac.unwrap()) - } - interpretation - } - - /// Given an Interpretation, follow the `Γ`-Operator to a fixpoint. Returns `None` if no valid fixpoint can be reached from the given interpretation and - /// the interpretation which represents the fixpoint otherwise. - #[allow(clippy::ptr_arg)] - pub fn compute_fixpoint(&mut self, interpretation: &Vec) -> Option> { - let new_interpretation = self.apply_interpretation(interpretation.as_ref()); - match Adf::information_enh(interpretation, new_interpretation.as_ref()) { - Some(n) => { - if n { - self.compute_fixpoint(new_interpretation.as_ref()) - } else { - Some(new_interpretation) - } - } - None => None, - } - } - - #[allow(clippy::ptr_arg)] - fn apply_interpretation(&mut self, interpretation: &Vec) -> Vec { - let mut new_interpretation = interpretation.clone(); - for (pos, it) in interpretation.iter().enumerate() { - match Term(*it) { - Term::BOT => { - if let Some(n) = self.setvarvalue( - new_interpretation.clone(), - self.bdd.nodes[self.stmts[pos].var].var().value(), - false, - ) { - new_interpretation.clone_from(&n); - } - } - Term::TOP => { - if let Some(n) = self.setvarvalue( - new_interpretation.clone(), - self.bdd.nodes[self.stmts[pos].var].var().value(), - true, - ) { - new_interpretation.clone_from(&n); - } - } - _ => (), - } - } + log::info!("[Done] grounded"); new_interpretation } - #[allow(clippy::ptr_arg)] - fn information_enh(i1: &Vec, i2: &Vec) -> Option { - let mut enhanced = false; - for i in 0..i1.len() { - if i1[i] < 2 { - if i1[i] != i2[i] { - return None; - } - } else if (i1[i] >= 2) & (i2[i] < 2) { - enhanced = true; - } - } - Some(enhanced) - } - - fn setvarvalue( - &mut self, - interpretation: Vec, - var: usize, - val: bool, - ) -> Option> { - let mut interpretation2: Vec = vec![0; interpretation.len()]; - let mut change: bool = false; - for (pos, _it) in interpretation.iter().enumerate() { - interpretation2[pos] = self - .bdd - .restrict(Term(interpretation[pos]), Var(var), val) - .value(); - if interpretation[pos] != interpretation2[pos] { - change = true - } - } - if change { - Some(interpretation2) - } else { - None - } - } - - fn parse_formula(&mut self, ac: &str) -> usize { - if ac.len() > 3 { - match &ac[..4] { - "and(" => { - let (left, right) = Adf::findpairs(&ac[4..]); - let lterm: Term = self.parse_formula(left).into(); - let rterm: Term = self.parse_formula(right).into(); - return self.bdd.and(lterm, rterm).value(); - } - "iff(" => { - let (left, right) = Adf::findpairs(&ac[4..]); - let lterm: Term = self.parse_formula(left).into(); - let rterm: Term = self.parse_formula(right).into(); - return self.bdd.iff(lterm, rterm).value(); - } - "xor(" => { - let (left, right) = Adf::findpairs(&ac[4..]); - let lterm: Term = self.parse_formula(left).into(); - let rterm: Term = self.parse_formula(right).into(); - return self.bdd.xor(lterm, rterm).value(); - } - "imp(" => { - let (left, right) = Adf::findpairs(&ac[4..]); - let lterm: Term = self.parse_formula(left).into(); - let rterm: Term = self.parse_formula(right).into(); - return self.bdd.imp(lterm, rterm).value(); - } - "neg(" => { - let pos = Adf::findterm(&ac[4..]).unwrap() + 4; - let term: Term = self.parse_formula(&ac[4..pos]).into(); - return self.bdd.not(term).value(); - } - "c(f)" => return Bdd::constant(false).value(), - "c(v)" => return Bdd::constant(true).value(), - _ if &ac[..3] == "or(" => { - let (left, right) = Adf::findpairs(&ac[3..]); - let lterm: Term = self.parse_formula(left).into(); - let rterm: Term = self.parse_formula(right).into(); - return self.bdd.or(lterm, rterm).value(); - } - _ => (), - } - } - match self.dict.get(ac) { - Some(it) => self.bdd.variable(Var(*it)).value(), - _ => { - println!("{}", ac); - unreachable!() - } - } - } - - /// Given a pair of literals, returns both literals as strings - /// # Example - /// ```rust - /// use adf_bdd::adf::Adf; - /// assert_eq!(Adf::findpairs("a,or(b,c))"), ("a", "or(b,c)")); - /// assert_eq!(Adf::findpairs("a,or(b,c)"), ("a", "or(b,c)")); - /// ``` - pub fn findpairs(formula: &str) -> (&str, &str) { - let lpos = Adf::findterm(formula).unwrap(); - let rpos = Adf::findterm(&formula[lpos + 1..]).unwrap() + lpos; - (&formula[..lpos], &formula[lpos + 1..rpos + 1]) - } - - /// Returns the first term in the given slice as a string slice - /// # Example - /// ```rust - /// use adf_bdd::adf::Adf; - /// assert_eq!(Adf::findterm_str("formula"), "formula"); - /// assert_eq!(Adf::findterm_str("and(a,b),or(a,b)"), "and(a,b)"); - /// assert_eq!(Adf::findterm_str("neg(atom(a.d.ee))"), "neg(atom(a.d.ee))"); - /// assert_eq!(Adf::findterm_str("formula)"), "formula"); - /// ``` - pub fn findterm_str(formula: &str) -> &str { - &formula[..Adf::findterm(formula).unwrap()] - } - - fn findterm(formula: &str) -> Option { - let mut sqbrack: i16 = 0; - let mut cobrack: i16 = 0; - - for (i, c) in formula.chars().enumerate() { - match c { - '(' => sqbrack += 1, - '[' => cobrack += 1, - ',' => { - if sqbrack + cobrack == 0 { - return Some(i); - } - } - ')' => { - if sqbrack > 0 { - sqbrack -= 1; - } else { - return Some(i); - } - } - ']' => { - if cobrack > 0 { - cobrack -= 1; - } else { - return Some(i); - } - } - _ => (), - } - } - Some(formula.len()) + /// creates a [PrintableInterpretation] for output purposes + pub fn print_interpretation<'a, 'b>( + &'a self, + interpretation: &'b [Term], + ) -> PrintableInterpretation<'b> + where + 'a: 'b, + { + PrintableInterpretation::new(interpretation, &self.ordering) } } #[cfg(test)] mod test { use super::*; - + use test_log::test; #[test] - fn add_statement() { - let mut adf = Adf::new(); + fn from_parser() { + let parser = AdfParser::default(); + let input = "s(a).s(c).ac(a,b).ac(b,neg(a)).s(b).ac(c,and(c(v),or(c(f),a))).s(e).s(d).ac(d,iff(imp(a,b),c)).ac(e,xor(d,e))."; - adf.add_statement("A"); - adf.add_statement("B"); - adf.add_statement("A"); + parser.parse()(input).unwrap(); - assert_eq!(adf.stmts.len(), 2); + let adf = Adf::from_parser(&parser); + assert_eq!(adf.ordering.names().as_ref().borrow()[0], "a"); + assert_eq!(adf.ordering.names().as_ref().borrow()[1], "c"); + assert_eq!(adf.ordering.names().as_ref().borrow()[2], "b"); + assert_eq!(adf.ordering.names().as_ref().borrow()[3], "e"); + assert_eq!(adf.ordering.names().as_ref().borrow()[4], "d"); - adf.add_statement("C"); - assert_eq!(adf.stmts.len(), 3); + assert_eq!(adf.ac, vec![Term(4), Term(2), Term(7), Term(15), Term(12)]); + + let parser = AdfParser::default(); + let input = "s(a).s(c).ac(a,b).ac(b,neg(a)).s(b).ac(c,and(c(v),or(c(f),a))).s(e).s(d).ac(d,iff(imp(a,b),c)).ac(e,xor(d,e))."; + + parser.parse()(input).unwrap(); + parser.varsort_alphanum(); + + let adf = Adf::from_parser(&parser); + assert_eq!(adf.ordering.names().as_ref().borrow()[0], "a"); + assert_eq!(adf.ordering.names().as_ref().borrow()[1], "b"); + assert_eq!(adf.ordering.names().as_ref().borrow()[2], "c"); + assert_eq!(adf.ordering.names().as_ref().borrow()[3], "d"); + assert_eq!(adf.ordering.names().as_ref().borrow()[4], "e"); + + assert_eq!(adf.ac, vec![Term(3), Term(7), Term(2), Term(11), Term(13)]); } #[test] - fn parse_formula() { - let mut adf = Adf::new(); + fn complete() { + let parser = AdfParser::default(); + parser.parse()("s(a).s(b).s(c).s(d).ac(a,c(v)).ac(b,b).ac(c,and(a,b)).ac(d,neg(b)).\ns(e).ac(e,and(b,or(neg(b),c(f)))).s(f).\n\nac(f,xor(a,e)).") + .unwrap(); + let mut adf = Adf::from_parser(&parser); + let result = adf.grounded(); - adf.add_statement("a"); - adf.add_statement("b"); - adf.add_statement("c"); - - assert_eq!(adf.parse_formula("and(a,or(b,c))"), 6); - assert_eq!(adf.parse_formula("xor(a,b)"), 8); - assert_eq!(adf.parse_formula("or(c(f),b)"), 3); // is b - - adf.parse_formula("and(or(c(f),a),and(b,c))"); - } - - #[test] - #[should_panic] - fn parse_formula_panic() { - let mut adf = Adf::new(); - - adf.add_statement("a"); - adf.add_statement("b"); - adf.add_statement("c"); - - adf.parse_formula("and(a,or(b,d))"); - } - - #[test] - fn findterm() { - assert_eq!(Adf::findterm("formula"), Some(7)); - assert_eq!(Adf::findterm("and(a,b),or(a,b)"), Some(8)); - assert_eq!(Adf::findterm("neg(atom(a.d.ee))"), Some(17)); - assert_eq!(Adf::findterm("formula)"), Some(7)); - } - - #[test] - fn findpairs() { - assert_eq!(Adf::findpairs("a,or(b,c))"), ("a", "or(b,c)")); - } - - #[test] - fn init_statements() { - let mut adf = Adf::new(); - - let stmts: Vec<&str> = vec!["a", "b", "c", "extra long text type statement"]; - - assert_eq!(adf.init_statements(stmts), 4); - assert_eq!(adf.stmts[3].label, "extra long text type statement"); + assert_eq!( + result, + vec![Term(1), Term(3), Term(3), Term(9), Term(0), Term(1)] + ); + assert_eq!( + format!("{}", adf.print_interpretation(&result)), + "T(a) u(b) u(c) u(d) F(e) T(f) \n" + ); } } diff --git a/src/datatypes.rs b/src/datatypes.rs index 4a8eb38..1711c12 100644 --- a/src/datatypes.rs +++ b/src/datatypes.rs @@ -1,114 +1,4 @@ -use std::{fmt::Display, ops::Deref}; - -#[derive(Debug, Eq, PartialEq, PartialOrd, Ord, Hash, Copy, Clone)] -pub struct Term(pub usize); - -impl Deref for Term { - type Target = usize; - fn deref(&self) -> &Self::Target { - &self.0 - } -} - -impl From for Term { - fn from(val: usize) -> Self { - Self(val) - } -} - -impl Display for Term { - fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - write!(f, "Term({})", self.0) - } -} - -impl Term { - pub const BOT: Term = Term(0); - pub const TOP: Term = Term(1); - - pub fn new(val: usize) -> Term { - Term(val) - } - - pub fn value(self) -> usize { - self.0 - } -} - -#[derive(Debug, Eq, PartialEq, PartialOrd, Ord, Hash, Clone, Copy)] -pub struct Var(pub usize); - -impl Deref for Var { - type Target = usize; - fn deref(&self) -> &Self::Target { - &self.0 - } -} - -impl From for Var { - fn from(val: usize) -> Self { - Self(val) - } -} - -impl Display for Var { - fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - write!(f, "Var({})", self.0) - } -} - -impl Var { - pub const TOP: Var = Var(usize::MAX); - pub const BOT: Var = Var(usize::MAX - 1); - - pub fn value(self) -> usize { - self.0 - } -} - -#[derive(Debug, Eq, PartialEq, PartialOrd, Ord, Hash, Clone, Copy)] -pub(crate) struct BddNode { - var: Var, - lo: Term, - hi: Term, -} - -impl Display for BddNode { - fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - write!(f, "BddNode: {}, lo: {}, hi: {}", self.var, self.lo, self.hi) - } -} - -impl BddNode { - pub fn new(var: Var, lo: Term, hi: Term) -> Self { - Self { var, lo, hi } - } - - pub fn var(self) -> Var { - self.var - } - - pub fn lo(self) -> Term { - self.lo - } - - pub fn hi(self) -> Term { - self.hi - } - - pub fn bot_node() -> Self { - Self { - var: Var::BOT, - lo: Term::BOT, - hi: Term::BOT, - } - } - - pub fn top_node() -> Self { - Self { - var: Var::TOP, - lo: Term::TOP, - hi: Term::TOP, - } - } -} +//! A collection of all the necessary datatypes of the system. +pub mod adf; +mod bdd; +pub use bdd::*; diff --git a/src/datatypes/adf.rs b/src/datatypes/adf.rs new file mode 100644 index 0000000..663b2cf --- /dev/null +++ b/src/datatypes/adf.rs @@ -0,0 +1,87 @@ +//! Repesentation of all needed ADF based datatypes + +use std::{cell::RefCell, collections::HashMap, fmt::Display, rc::Rc}; + +use super::{Term, Var}; + +pub(crate) struct VarContainer { + names: Rc>>, + mapping: Rc>>, +} + +impl Default for VarContainer { + fn default() -> Self { + VarContainer { + names: Rc::new(RefCell::new(Vec::new())), + mapping: Rc::new(RefCell::new(HashMap::new())), + } + } +} + +impl VarContainer { + pub fn from_parser( + names: Rc>>, + mapping: Rc>>, + ) -> VarContainer { + VarContainer { names, mapping } + } + + pub fn variable(&self, name: &str) -> Option { + self.mapping.borrow().get(name).map(|val| Var(*val)) + } + + pub fn name(&self, var: Var) -> Option { + self.names.borrow().get(var.value()).cloned() + } + + pub fn names(&self) -> Rc>> { + Rc::clone(&self.names) + } +} + +/// A struct to print a representation, it will be instantiated by [Adf] by calling the method [`Adf::print_interpretation`]. +pub struct PrintableInterpretation<'a> { + interpretation: &'a [Term], + ordering: &'a VarContainer, +} + +impl<'a> PrintableInterpretation<'a> { + pub(crate) fn new(interpretation: &'a [Term], ordering: &'a VarContainer) -> Self { + Self { + interpretation, + ordering, + } + } +} + +impl Display for PrintableInterpretation<'_> { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + self.interpretation + .iter() + .enumerate() + .for_each(|(pos, term)| { + if term.is_truth_value() { + if term.is_true() { + write!(f, "T(").expect("writing Interpretation failed!"); + } else { + write!(f, "F(").expect("writing Interpretation failed!"); + } + } else { + write!(f, "u(").expect("writing Interpretation failed!"); + } + write!(f, "{}) ", self.ordering.name(Var(pos)).unwrap()) + .expect("writing Interpretation failed!"); + }); + writeln!(f) + } +} + +#[cfg(test)] +mod test { + use super::*; + #[test] + fn init_varcontainer() { + let vc = VarContainer::default(); + assert_eq!(vc.variable("foo"), None); + } +} diff --git a/src/datatypes/bdd.rs b/src/datatypes/bdd.rs new file mode 100644 index 0000000..0a788a7 --- /dev/null +++ b/src/datatypes/bdd.rs @@ -0,0 +1,146 @@ +//! 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] +use std::{fmt::Display, ops::Deref}; + +/// Representation of a Term +/// Each Term is represented in a number ([usize]) and relates to a +/// Node in the decision diagram +#[derive(Debug, Eq, PartialEq, PartialOrd, Ord, Hash, Copy, Clone)] +pub struct Term(pub usize); + +impl Deref for Term { + type Target = usize; + fn deref(&self) -> &Self::Target { + &self.0 + } +} + +impl From for Term { + fn from(val: usize) -> Self { + Self(val) + } +} + +impl Display for Term { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + write!(f, "Term({})", self.0) + } +} + +impl Term { + /// Represents the truth-value bottom, i.e. false + pub const BOT: Term = Term(0); + /// Represents the truth-value top, i.e. true + pub const TOP: Term = Term(1); + + /// Get the value of the Term, i.e. the corresponding [usize] + pub fn value(self) -> usize { + self.0 + } + + /// Checks if the [Term] represents a truth-value ([Term::TOP] or [Term::BOT]), or + /// another compound formula. + pub fn is_truth_value(&self) -> bool { + self.0 <= Term::TOP.0 + } + + /// Returns true, if the Term is true, i.e. [Term::TOP] + pub fn is_true(&self) -> bool { + *self == Self::TOP + } +} + +/// 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. +#[derive(Debug, Eq, PartialEq, PartialOrd, Ord, Hash, Clone, Copy)] +pub struct Var(pub usize); + +impl Deref for Var { + type Target = usize; + fn deref(&self) -> &Self::Target { + &self.0 + } +} + +impl From for Var { + fn from(val: usize) -> Self { + Self(val) + } +} + +impl Display for Var { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + write!(f, "Var({})", self.0) + } +} + +impl Var { + /// Represents the constant symbol "Top" + pub const TOP: Var = Var(usize::MAX); + /// Represents the constant symbol "Bot" + pub const BOT: Var = Var(usize::MAX - 1); + + /// Returns the value of the [Var] as [usize] + pub fn value(self) -> usize { + self.0 + } +} + +/// 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. +#[derive(Debug, Eq, PartialEq, PartialOrd, Ord, Hash, Clone, Copy)] +pub(crate) struct BddNode { + var: Var, + lo: Term, + hi: Term, +} + +impl Display for BddNode { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + write!(f, "BddNode: {}, lo: {}, hi: {}", self.var, self.lo, self.hi) + } +} + +impl BddNode { + /// Creates a new Node + pub fn new(var: Var, lo: Term, hi: Term) -> Self { + Self { var, lo, hi } + } + + /// Returns the current Variable-value + pub fn var(self) -> Var { + self.var + } + + /// Returns the `lo`-branch + pub fn lo(self) -> Term { + self.lo + } + + /// Returns the `hi`-branch + pub fn hi(self) -> Term { + self.hi + } + + /// Creates a node, which represents the `Bot`-truth value + pub fn bot_node() -> Self { + Self { + var: Var::BOT, + lo: Term::BOT, + hi: Term::BOT, + } + } + + /// Creates a node, which represents the `Top`-truth value + pub fn top_node() -> Self { + Self { + var: Var::TOP, + lo: Term::TOP, + hi: Term::TOP, + } + } +} diff --git a/src/lib.rs b/src/lib.rs index e309ce6..7086f4d 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -31,7 +31,22 @@ //! ac(c,neg(b)). //! ac(d,d). //! ``` +#![deny( + missing_copy_implementations, + trivial_casts, + trivial_numeric_casts, + unsafe_code +)] +#![warn( + missing_docs, + unused_import_braces, + unused_qualifications, + unused_extern_crates, + variant_size_differences +)] + pub mod adf; pub mod datatypes; pub mod obdd; +pub mod parser; //pub mod obdd2; diff --git a/src/main.rs b/src/main.rs index b9dd763..5c6ae29 100644 --- a/src/main.rs +++ b/src/main.rs @@ -1,134 +1,81 @@ -use std::fs::File; -use std::io::{self, BufRead}; -use std::path::Path; -use std::time::Instant; -use std::usize; - pub mod adf; pub mod datatypes; pub mod obdd; +pub mod parser; + +use std::str::FromStr; use adf::Adf; -#[macro_use] -extern crate clap; +use clap::{clap_app, crate_authors, crate_description, crate_name, crate_version}; +use parser::AdfParser; fn main() { let matches = clap_app!(myapp => - (version: crate_version!()) - (author: crate_authors!()) - (name: crate_name!()) - (about: crate_description!()) - (@arg fast: -f --fast "fast algorithm instead of the direct fixpoint-computation") - (@arg verbose: -v +multiple "Sets verbosity") - (@arg INPUT: +required "Input file") + (version: crate_version!()) + (author: crate_authors!()) + (name: crate_name!()) + (about: crate_description!()) + //(@arg fast: -f --fast "fast algorithm instead of the direct fixpoint-computation") + (@arg verbose: -v +multiple "Sets log verbosity") + (@arg INPUT: +required "Input file") + (@group sorting => + (@arg sort_lex: --lx "Sorts variables in a lexicographic manner") + (@arg sort_alphan: --an "Sorts variables in an alphanumeric manner") + ) ) - .get_matches(); - let verbose = matches.occurrences_of("verbose") > 0; - let start_time = Instant::now(); - //let args: Vec = env::args().collect(); - //if args.len() != 2 { - // eprintln!("No Filename given"); - // exit(1); - //} - let mut statements: Vec = Vec::new(); - let mut ac: Vec<(String, String)> = Vec::new(); - let path = Path::new(matches.value_of("INPUT").unwrap()); - if let Ok(lines) = read_lines(path) { - for line in lines.flatten() { - //if let Ok(line) = resline { - //let slice = line.as_str(); - if line.starts_with("s(") { - // let slice = line.as_str(); - // statements.push(Adf::findterm_str(&slice[2..]).clone()); - statements - .push(Adf::findterm_str(line.strip_prefix("s(").unwrap()).replace(" ", "")); - } else if line.starts_with("ac(") { - let (s, c) = Adf::findpairs(line.strip_prefix("ac(").unwrap()); - ac.push((s.replace(" ", ""), c.replace(" ", ""))); - } - //} + .get_matches_safe() + .unwrap_or_else(|e| match e.kind { + clap::ErrorKind::HelpDisplayed => { + e.exit(); } - } - - let file_read = start_time.elapsed(); - let start_shortcut = Instant::now(); - - if verbose { - println!( - "parsed {} statements after {}ms", - statements.len(), - file_read.as_millis() - ); - } - - if !statements.is_empty() && !ac.is_empty() { - if matches.is_present("fast") { - let mut my_adf = Adf::new(); - my_adf.init_statements(statements.iter().map(AsRef::as_ref).collect()); - for (s, c) in ac.clone() { - my_adf.add_ac(s.as_str(), c.as_str()); - } - - let result = my_adf.grounded(); - print_interpretation(result); - if verbose { - println!("finished after {}ms", start_shortcut.elapsed().as_millis()); - } - } else { - let start_fp = Instant::now(); - - let mut my_adf = Adf::default(); - my_adf.init_statements(statements.iter().map(AsRef::as_ref).collect()); - for (s, c) in ac.clone() { - my_adf.add_ac(s.as_str(), c.as_str()); - } - let empty_int = my_adf.cur_interpretation(); - let result = my_adf.compute_fixpoint(empty_int.as_ref()).unwrap(); - - print_interpretation(result); - if verbose { - println!("finished after {}ms", start_fp.elapsed().as_millis()); + clap::ErrorKind::VersionDisplayed => { + e.exit(); + } + _ => { + eprintln!("{} Version {{{}}}", crate_name!(), crate_version!()); + e.exit(); + } + }); + let filter_level = match matches.occurrences_of("verbose") { + 1 => log::LevelFilter::Info, + 2 => log::LevelFilter::Debug, + 3 => log::LevelFilter::Trace, + _ => { + match std::env::vars().find_map(|(var, val)| { + if var.eq("RUST_LOG") { + Some(log::LevelFilter::from_str(val.as_str())) + } else { + None + } + }) { + Some(v) => v.unwrap_or(log::LevelFilter::Error), + None => log::LevelFilter::Error, } } - // optional test of complete extensions - // let mut my_adf3 = Adf::default(); - // my_adf3.init_statements(statements.iter().map(AsRef::as_ref).collect()); - // for (s, c) in ac.clone() { - // my_adf3.add_ac(s.as_str(), c.as_str()); - // } + }; + env_logger::builder().filter_level(filter_level).init(); + log::info!("Version: {}", crate_version!()); - // let result3 = my_adf3.complete(); - // for it in result3.iter() { - // print_interpretation(it.to_vec()); - // } - // println!("{}",result3.len()); - } -} + let input = std::fs::read_to_string( + matches + .value_of("INPUT") + .expect("Input Filename should be given"), + ) + .expect("Error Reading File"); + let parser = AdfParser::default(); + parser.parse()(&input).unwrap(); + log::info!("[Done] parsing"); -fn read_lines

(filename: P) -> io::Result>> -where - P: AsRef, -{ - let file = File::open(filename)?; - Ok(io::BufReader::new(file).lines()) -} + if matches.is_present("sort_lex") { + parser.varsort_lexi(); + } + if matches.is_present("sort_alphan") { + parser.varsort_alphanum(); + } -fn print_interpretation(interpretation: Vec) { - let mut stable = true; - for it in interpretation.iter() { - match *it { - 0 => print!("f"), - 1 => print!("t"), - _ => { - print!("u"); - stable = false - } - } - } - if stable { - println!(" stm"); - } else { - println!(); - } + let mut adf = Adf::from_parser(&parser); + let grounded = adf.grounded(); + + println!("{}", adf.print_interpretation(&grounded)); } diff --git a/src/obdd.rs b/src/obdd.rs index 016444e..853f6bc 100644 --- a/src/obdd.rs +++ b/src/obdd.rs @@ -1,3 +1,4 @@ +//! Represents an obdd use crate::datatypes::*; use std::{cmp::min, collections::HashMap, fmt::Display}; @@ -198,6 +199,9 @@ mod test { let v1 = bdd.variable(Var(0)); let v2 = bdd.variable(Var(1)); + assert_eq!(v1, Term(2)); + assert_eq!(v2, Term(3)); + let t1 = bdd.and(v1, v2); let nt1 = bdd.not(t1); let ft = bdd.or(v1, nt1); diff --git a/src/parser.rs b/src/parser.rs new file mode 100644 index 0000000..ec84e1a --- /dev/null +++ b/src/parser.rs @@ -0,0 +1,479 @@ +//! A 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, + bytes::complete::{tag, take_until}, + character::complete::{alphanumeric1, multispace0}, + combinator::{all_consuming, value}, + multi::many1, + sequence::{delimited, preceded, separated_pair, terminated}, + IResult, +}; +use std::{cell::RefCell, collections::HashMap, rc::Rc}; + +/// 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 + Bot, + /// c(f) in the input format + Top, + /// Some atomic variable in the input format + Atom(&'a str), + /// Negation of a subformula + Not(Box>), + /// Conjunction of two subformulae + And(Box>, Box>), + /// Disjunction of two subformulae + Or(Box>, Box>), + /// Implication of two subformulae + Imp(Box>, Box>), + /// Exclusive-Or of two subformulae + Xor(Box>, Box>), + /// If and only if connective between two formulae + Iff(Box>, Box>), +} + +impl std::fmt::Debug for Formula<'_> { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + match self { + Formula::Atom(a) => { + write!(f, "{}", a)?; + } + Formula::Not(n) => { + write!(f, "not({:?})", n)?; + } + Formula::And(f1, f2) => { + write!(f, "and({:?},{:?})", f1, f2)?; + } + Formula::Or(f1, f2) => { + write!(f, "or({:?},{:?})", f1, f2)?; + } + Formula::Imp(f1, f2) => { + write!(f, "imp({:?},{:?})", f1, f2)?; + } + Formula::Xor(f1, f2) => { + write!(f, "xor({:?},{:?})", f1, f2)?; + } + Formula::Iff(f1, f2) => { + write!(f, "iff({:?},{:?})", f1, f2)?; + } + Formula::Bot => { + write!(f, "Const(B)")?; + } + Formula::Top => { + write!(f, "Const(T)")?; + } + } + write!(f, "") + } +} + +/// 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. +/// +/// Note that the parser can be utilised by an [ADF][`crate::datatypes::adf::Adf`] to initialise it with minimal overhead. +pub struct AdfParser<'a> { + namelist: Rc>>, + dict: Rc>>, + formulae: RefCell>>, + formulaname: RefCell>, +} + +impl Default for AdfParser<'_> { + fn default() -> Self { + AdfParser { + namelist: Rc::new(RefCell::new(Vec::new())), + dict: Rc::new(RefCell::new(HashMap::new())), + formulae: RefCell::new(Vec::new()), + formulaname: RefCell::new(Vec::new()), + } + } +} + +impl<'a, 'b> AdfParser<'b> +where + 'a: 'b, +{ + fn parse_statements(&'a self) -> impl FnMut(&'a str) -> IResult<&'a str, ()> { + move |input| { + let (rem, _) = many1(self.parse_statement())(input)?; + Ok((rem, ())) + } + } + + /// Parses a full input file and creates internal structures. + /// Note that this method returns a closure (see the following Example for the correct usage). + /// # Example + /// ``` + /// let parser = adf_bdd::parser::AdfParser::default(); + /// parser.parse()("s(a).ac(a,c(v)).s(b).ac(b,a).s(c).ac(c,neg(b))."); + /// let adf = adf_bdd::adf::Adf::from_parser(&parser); + /// ``` + pub fn parse(&'a self) -> impl FnMut(&'a str) -> IResult<&'a str, ()> { + log::info!("[Start] parsing"); + |input| { + value( + (), + all_consuming(many1(alt((self.parse_statement(), self.parse_ac())))), + )(input) + } + } + + fn parse_statement(&'a self) -> impl FnMut(&'a str) -> IResult<&'a str, ()> { + |input| { + let mut dict = self.dict.borrow_mut(); + let mut namelist = self.namelist.borrow_mut(); + let (remain, statement) = + terminated(AdfParser::statement, terminated(tag("."), multispace0))(input)?; + if !dict.contains_key(statement) { + let pos = namelist.len(); + namelist.push(String::from(statement)); + dict.insert(namelist[pos].clone(), pos); + } + Ok((remain, ())) + } + } + + fn parse_ac(&'a self) -> impl FnMut(&'a str) -> IResult<&'a str, ()> { + |input| { + let (remain, (name, formula)) = + terminated(AdfParser::ac, terminated(tag("."), multispace0))(input)?; + self.formulae.borrow_mut().push(formula); + self.formulaname.borrow_mut().push(String::from(name)); + Ok((remain, ())) + } + } +} + +impl AdfParser<'_> { + /// after an update to the namelist, all indizes are updated + fn regenerate_indizes(&self) { + self.namelist + .as_ref() + .borrow() + .iter() + .enumerate() + .for_each(|(i, elem)| { + self.dict.as_ref().borrow_mut().insert(elem.clone(), i); + }); + } + + /// Sort the variables in lexicographical order. + /// Results which got used before might become corrupted. + pub fn varsort_lexi(&self) -> &Self { + self.namelist.as_ref().borrow_mut().sort_unstable(); + self.regenerate_indizes(); + self + } + + /// Sort the variables in alphanumerical order + /// Results which got used before might become corrupted. + pub fn varsort_alphanum(&self) -> &Self { + self.namelist + .as_ref() + .borrow_mut() + .string_sort_unstable(natural_lexical_cmp); + self.regenerate_indizes(); + self + } + + fn statement(input: &str) -> IResult<&str, &str> { + preceded(tag("s"), delimited(tag("("), AdfParser::atomic, tag(")")))(input) + } + + fn ac(input: &str) -> IResult<&str, (&str, Formula)> { + preceded( + tag("ac"), + delimited( + tag("("), + separated_pair( + AdfParser::atomic, + delimited(multispace0, tag(","), multispace0), + AdfParser::formula, + ), + tag(")"), + ), + )(input) + } + + fn atomic_term(input: &str) -> IResult<&str, Formula> { + AdfParser::atomic(input).map(|(input, result)| (input, Formula::Atom(result))) + } + + fn formula(input: &str) -> IResult<&str, Formula> { + alt(( + AdfParser::constant, + AdfParser::binary_op, + AdfParser::unary_op, + AdfParser::atomic_term, + ))(input) + } + + fn unary_op(input: &str) -> IResult<&str, Formula> { + preceded( + tag("neg"), + delimited(tag("("), AdfParser::formula, tag(")")), + )(input) + .map(|(input, result)| (input, Formula::Not(Box::new(result)))) + } + + fn constant(input: &str) -> IResult<&str, Formula> { + alt(( + preceded(tag("c"), delimited(tag("("), tag("v"), tag(")"))), + preceded(tag("c"), delimited(tag("("), tag("f"), tag(")"))), + ))(input) + .map(|(input, result)| { + ( + input, + match result { + "v" => Formula::Top, + "f" => Formula::Bot, + _ => unreachable!(), + }, + ) + }) + } + + fn formula_pair(input: &str) -> IResult<&str, (Formula, Formula)> { + separated_pair( + preceded(tag("("), AdfParser::formula), + delimited(multispace0, tag(","), multispace0), + terminated(AdfParser::formula, tag(")")), + )(input) + } + + fn and(input: &str) -> IResult<&str, Formula> { + preceded(tag("and"), AdfParser::formula_pair)(input) + .map(|(input, (f1, f2))| (input, Formula::And(Box::new(f1), Box::new(f2)))) + } + + fn or(input: &str) -> IResult<&str, Formula> { + preceded(tag("or"), AdfParser::formula_pair)(input) + .map(|(input, (f1, f2))| (input, Formula::Or(Box::new(f1), Box::new(f2)))) + } + fn imp(input: &str) -> IResult<&str, Formula> { + preceded(tag("imp"), AdfParser::formula_pair)(input) + .map(|(input, (f1, f2))| (input, Formula::Imp(Box::new(f1), Box::new(f2)))) + } + + fn xor(input: &str) -> IResult<&str, Formula> { + preceded(tag("xor"), AdfParser::formula_pair)(input) + .map(|(input, (f1, f2))| (input, Formula::Xor(Box::new(f1), Box::new(f2)))) + } + + fn iff(input: &str) -> IResult<&str, Formula> { + preceded(tag("iff"), AdfParser::formula_pair)(input) + .map(|(input, (f1, f2))| (input, Formula::Iff(Box::new(f1), Box::new(f2)))) + } + + fn binary_op(input: &str) -> IResult<&str, Formula> { + alt(( + AdfParser::and, + AdfParser::or, + AdfParser::imp, + AdfParser::xor, + AdfParser::iff, + ))(input) + } + + fn atomic(input: &str) -> IResult<&str, &str> { + alt(( + delimited(tag("\""), take_until("\""), tag("\"")), + alphanumeric1, + ))(input) + } + + /// 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 + 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 + pub fn ac_at(&self, idx: usize) -> Option { + self.formulae.borrow().get(idx).cloned() + } + + pub(crate) fn dict_rc_refcell(&self) -> Rc>> { + Rc::clone(&self.dict) + } + + pub(crate) fn namelist_rc_refcell(&self) -> Rc>> { + Rc::clone(&self.namelist) + } + + pub(crate) fn formula_count(&self) -> usize { + self.formulae.borrow().len() + } + + pub(crate) fn formula_order(&self) -> Vec { + self.formulaname + .borrow() + .iter() + .map(|name| *self.dict.as_ref().borrow().get(name).unwrap()) + .collect() + } +} + +#[cfg(test)] +mod test { + + use clap::ErrorKind; + + use super::*; + + #[test] + fn atomic_parse() { + assert_eq!( + AdfParser::atomic("\" 123 21 ())) ((( {}||| asfjklj fsajfj039409u902 jfi a \""), + Ok(( + "", + " 123 21 ())) ((( {}||| asfjklj fsajfj039409u902 jfi a " + )) + ); + assert_eq!(AdfParser::atomic("foo"), Ok(("", "foo"))); + assert_eq!(AdfParser::atomic("foo()"), Ok(("()", "foo"))); + assert_eq!( + AdfParser::atomic("()foo"), + Err(nom::Err::Error(nom::error::Error::new( + "()foo", + nom::error::ErrorKind::AlphaNumeric + ))) + ); + assert!(AdfParser::atomic(" adf").is_err()); + } + + #[test] + fn statement_parse() { + assert_eq!(AdfParser::statement("s(ab)"), Ok(("", "ab"))); + assert_eq!(AdfParser::statement("s(\"a b\")"), Ok(("", "a b"))); + assert!(AdfParser::statement("s(a_b)").is_err()); + } + + #[test] + fn parse_statement() { + let parser: AdfParser = AdfParser::default(); + + let input = "s(a). s(b). s(c).s(d).s(b).s(c)."; + // many1(parser.parse_statement())(input).unwrap(); + let (_remain, _) = parser.parse_statement()(input).unwrap(); + assert_eq!(parser.dict_size(), 1); + assert_eq!(parser.dict_value("c"), None); + + let (_remain, _) = parser.parse_statements()(input).unwrap(); + assert_eq!(parser.dict_size(), 4); + assert_eq!(parser.dict_value("c"), Some(2usize)); + } + + #[test] + fn parse_formula() { + let input = "and(or(neg(a),iff(\" iff left \",b)),xor(imp(c,d),e))"; + let (_remain, result) = AdfParser::formula(input).unwrap(); + + assert_eq!( + format!("{:?}", result), + "and(or(not(a),iff( iff left ,b)),xor(imp(c,d),e))" + ); + + assert_eq!( + AdfParser::formula("and(c(v),c(f))").unwrap(), + ( + "", + Formula::And(Box::new(Formula::Top), Box::new(Formula::Bot)) + ) + ); + } + + #[test] + fn parse() { + let parser = AdfParser::default(); + let input = "s(a).s(c).ac(a,b).ac(b,neg(a)).s(b).ac(c,and(c(v),or(c(f),a)))."; + + let (remain, _) = parser.parse()(input).unwrap(); + assert_eq!(remain, ""); + assert_eq!(parser.dict_size(), 3); + assert_eq!(parser.dict_value("b"), Some(2usize)); + assert_eq!( + format!("{:?}", parser.ac_at(1).unwrap()), + format!("{:?}", Formula::Not(Box::new(Formula::Atom("a")))) + ); + assert_eq!(parser.formula_count(), 3); + assert_eq!(parser.formula_order(), vec![0, 2, 1]); + } + + #[test] + fn non_consuming_parse() { + let parser = AdfParser::default(); + let input = "s(a).s(c).ac(a,b).ac(b,neg(a)).s(b).ac(c,and(c(v),or(c(f),a))). wee"; + + let x = parser.parse()(input); + assert!(x.is_err()); + assert_eq!( + x.err().unwrap(), + nom::Err::Error(nom::error::Error::new("wee", nom::error::ErrorKind::Eof)) + ); + } + + #[test] + fn constant() { + assert_eq!(AdfParser::constant("c(v)").unwrap().1, Formula::Top); + assert_eq!(AdfParser::constant("c(f)").unwrap().1, Formula::Bot); + assert_eq!(format!("{:?}", Formula::Top), "Const(T)"); + assert_eq!(format!("{:?}", Formula::Bot), "Const(B)"); + } + + #[test] + fn sort_updates() { + let parser = AdfParser::default(); + let input = "s(a).s(c).ac(a,b).ac(b,neg(a)).s(b).ac(c,and(c(v),or(c(f),a)))."; + + parser.parse()(input).unwrap(); + assert_eq!(parser.dict_value("a"), Some(0)); + assert_eq!(parser.dict_value("b"), Some(2)); + assert_eq!(parser.dict_value("c"), Some(1)); + + parser.varsort_lexi(); + + assert_eq!(parser.dict_value("a"), Some(0)); + assert_eq!(parser.dict_value("b"), Some(1)); + assert_eq!(parser.dict_value("c"), Some(2)); + + let parser = AdfParser::default(); + let input = "s(a2).s(0).s(1).s(2).s(10).s(11).s(20).ac(0,c(v)).ac(1,c(v)).ac(2,c(v)).ac(10,c(v)).ac(20,c(v)).ac(11,c(v)).ac(a2,c(f))."; + + parser.parse()(input).unwrap(); + assert_eq!(parser.dict_value("a2"), Some(0)); + assert_eq!(parser.dict_value("0"), Some(1)); + assert_eq!(parser.dict_value("1"), Some(2)); + assert_eq!(parser.dict_value("2"), Some(3)); + assert_eq!(parser.dict_value("10"), Some(4)); + assert_eq!(parser.dict_value("11"), Some(5)); + assert_eq!(parser.dict_value("20"), Some(6)); + + parser.varsort_lexi(); + assert_eq!(parser.dict_value("0"), Some(0)); + assert_eq!(parser.dict_value("1"), Some(1)); + assert_eq!(parser.dict_value("2"), Some(4)); + assert_eq!(parser.dict_value("10"), Some(2)); + assert_eq!(parser.dict_value("11"), Some(3)); + assert_eq!(parser.dict_value("20"), Some(5)); + assert_eq!(parser.dict_value("a2"), Some(6)); + + parser.varsort_alphanum(); + assert_eq!(parser.dict_value("0"), Some(0)); + assert_eq!(parser.dict_value("1"), Some(1)); + assert_eq!(parser.dict_value("2"), Some(2)); + assert_eq!(parser.dict_value("10"), Some(3)); + assert_eq!(parser.dict_value("11"), Some(4)); + assert_eq!(parser.dict_value("20"), Some(5)); + assert_eq!(parser.dict_value("a2"), Some(6)); + } +} diff --git a/tests/automated.rs b/tests/automated.rs new file mode 100644 index 0000000..f391751 --- /dev/null +++ b/tests/automated.rs @@ -0,0 +1,26 @@ +use adf_bdd::{adf::Adf, parser::AdfParser}; +use test_generator::test_resources; +use test_log::test; + +#[test_resources("res/adf-instances/instances/*.adf")] +fn compute_grounded(resource: &str) { + let grounded = &[ + "res/adf-instances/grounded-interpretations/", + &resource[28..resource.len() - 8], + ".apx.adf-grounded.txt", + ] + .concat(); + log::debug!("Grounded: {}", grounded); + let parser = AdfParser::default(); + let expected_result = std::fs::read_to_string(grounded); + assert!(expected_result.is_ok()); + let input = std::fs::read_to_string(resource).unwrap(); + parser.parse()(&input).unwrap(); + parser.varsort_alphanum(); + let mut adf = Adf::from_parser(&parser); + let grounded = adf.grounded(); + assert_eq!( + format!("{}", adf.print_interpretation(&grounded)), + expected_result.unwrap() + ); +}