diff --git a/Cargo.lock b/Cargo.lock index 28c4a1c..7af9853 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -10,6 +10,7 @@ dependencies = [ "assert_fs", "biodivine-lib-bdd", "clap", + "derivative", "env_logger 0.9.0", "lexical-sort", "log", @@ -156,6 +157,17 @@ dependencies = [ "lazy_static", ] +[[package]] +name = "derivative" +version = "2.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "fcc3dd5e9e9c0b295d6e1e4d811fb6f157d5ffd784b8d202fc62eac8035a770b" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + [[package]] name = "difflib" version = "0.4.0" diff --git a/Cargo.toml b/Cargo.toml index 7316014..a29b1dd 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -14,6 +14,17 @@ build = "build.rs" # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html [[bin]] name="adf_bdd" +[lib] +name="adf_bdd" +path = "src/lib.rs" +test = true +doctest = true # Documentation examples are tested by default. +bench = true # Is benchmarked by default. +doc = true # Is documented by default. +harness = true # Use libtest harness. +edition = "2021" # The edition of the target. +crate-type = ["lib"] # The crate types to generate. + [dependencies] clap = "2.33.*" structopt = "0.3.25" @@ -24,6 +35,7 @@ lexical-sort = "0.3.1" serde = { version = "1.0", features = ["derive","rc"] } serde_json = "1.0" biodivine-lib-bdd = "0.3.0" +derivative = "2.2.0" [dev-dependencies] test-log = "0.2.*" diff --git a/README.md b/README.md index d3f0bd0..37479f1 100644 --- a/README.md +++ b/README.md @@ -21,6 +21,10 @@ FLAGS: --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) diff --git a/flake.lock b/flake.lock index d121a64..2d18ef5 100644 --- a/flake.lock +++ b/flake.lock @@ -3,11 +3,11 @@ "flake-compat": { "flake": false, "locked": { - "lastModified": 1627913399, - "narHash": "sha256-hY8g6H2KFL8ownSiFeMOjwPC8P0ueXpCVEbxgda3pko=", + "lastModified": 1641205782, + "narHash": "sha256-4jY7RCWUoZ9cKD8co0/4tFARpWB+57+r1bLLvXNJliY=", "owner": "edolstra", "repo": "flake-compat", - "rev": "12c64ca55c1014cdc1b16ed5a804aa8576601ff2", + "rev": "b7547d3eed6f32d06102ead8991ec52ab0a4f1a7", "type": "github" }, "original": { @@ -18,11 +18,11 @@ }, "flake-utils": { "locked": { - "lastModified": 1637014545, - "narHash": "sha256-26IZAc5yzlD9FlDT54io1oqG/bBoyka+FJk5guaX4x4=", + "lastModified": 1642700792, + "narHash": "sha256-XqHrk7hFb+zBvRg6Ghl+AZDq03ov6OshJLiSWOoX5es=", "owner": "numtide", "repo": "flake-utils", - "rev": "bba5dcc8e0b20ab664967ad83d24d64cb64ec4f4", + "rev": "846b2ae0fc4cc943637d3d1def4454213e203cba", "type": "github" }, "original": { @@ -64,16 +64,16 @@ }, "nixpkgs": { "locked": { - "lastModified": 1637448181, - "narHash": "sha256-ujcXli4esmtIHUBjE1BjmMuBWrcNvlHZrVXx56i5B1M=", + "lastModified": 1643788601, + "narHash": "sha256-6l5Ax44pC/Oo/Muj5Y/NA27Pd38Wty/7GtGSSmYNug4=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "d5b65f812cd4f5a8fa74b406075b59a46f1cfd98", + "rev": "f6ddd55d5f9d5eca08df138c248008c1ba73ecec", "type": "github" }, "original": { "owner": "NixOS", - "ref": "nixos-21.05", + "ref": "nixos-21.11", "repo": "nixpkgs", "type": "github" } @@ -109,11 +109,11 @@ "nixpkgs": "nixpkgs_2" }, "locked": { - "lastModified": 1637633693, - "narHash": "sha256-4EqHaQrpevUcGGcWIoNuZWJEhA1GhcApCSBggR0r2MM=", + "lastModified": 1643941258, + "narHash": "sha256-uHyEuICSu8qQp6adPTqV33ajiwoF0sCh+Iazaz5r7fo=", "owner": "oxalica", "repo": "rust-overlay", - "rev": "885ef5bf9d2857dff8689292aedb511dfc952862", + "rev": "674156c4c2f46dd6a6846466cb8f9fee84c211ca", "type": "github" }, "original": { diff --git a/src/adf.rs b/src/adf.rs index 828eb2d..d85069f 100644 --- a/src/adf.rs +++ b/src/adf.rs @@ -260,6 +260,89 @@ impl Adf { .map(|(int, _grd)| int) } + /// Computes the stable models + /// Returns a vector with all stable models, using a single-formula representation in biodivine to enumerate the possible models + /// Note that the biodivine adf needs to be the one which instantiated the adf (if applicable) + pub fn stable_bdd_representation( + &mut self, + biodivine: &crate::adfbiodivine::Adf, + ) -> Vec> { + biodivine + .stable_model_candidates() + .into_iter() + .filter(|terms| { + let mut interpr = self.ac.clone(); + for ac in interpr.iter_mut() { + *ac = terms.iter().enumerate().fold(*ac, |acc, (var, term)| { + if term.is_truth_value() && !term.is_true() { + self.bdd.restrict(acc, Var(var), false) + } else { + acc + } + }); + } + let grounded_check = self.grounded_internal(&interpr); + terms + .iter() + .zip(grounded_check.iter()) + .all(|(left, right)| left.compare_inf(right)) + }) + .collect::>>() + } + + /// Computes the stable models + /// Returns an Iterator which contains all stable models + pub fn stable_with_prefilter<'a, 'c>(&'a mut self) -> impl Iterator> + 'c + where + 'a: 'c, + { + let grounded = self.grounded(); + TwoValuedInterpretationsIterator::new(&grounded) + .map(|interpretation| { + if interpretation.iter().enumerate().all(|(ac_idx, it)| { + it.compare_inf(&interpretation.iter().enumerate().fold( + self.ac[ac_idx], + |acc, (var, term)| { + if term.is_truth_value() { + self.bdd.restrict(acc, Var(var), term.is_true()) + } else { + acc + } + }, + )) + }) { + let mut interpr = self.ac.clone(); + for ac in interpr.iter_mut() { + *ac = interpretation + .iter() + .enumerate() + .fold(*ac, |acc, (var, term)| { + if term.is_truth_value() && !term.is_true() { + self.bdd.restrict(acc, Var(var), false) + } else { + acc + } + }); + } + let grounded_check = self.grounded_internal(&interpr); + log::debug!( + "grounded candidate\n{:?}\n{:?}", + interpretation, + grounded_check + ); + (interpretation, grounded_check) + } else { + (vec![Term::BOT], vec![Term::TOP]) + } + }) + .filter(|(int, grd)| { + int.iter() + .zip(grd.iter()) + .all(|(it, gr)| it.compare_inf(gr)) + }) + .map(|(int, _grd)| int) + } + /// Computes the complete models /// Returns an Iterator which contains all complete models pub fn complete<'a, 'c>(&'a mut self) -> impl Iterator> + 'c @@ -475,4 +558,8 @@ mod test { println!("{}", printer.print_interpretation(&model)); } } + #[test] + fn adf_default() { + let _adf = Adf::default(); + } } diff --git a/src/adfbiodivine.rs b/src/adfbiodivine.rs index ee43b89..db2f9b7 100644 --- a/src/adfbiodivine.rs +++ b/src/adfbiodivine.rs @@ -16,14 +16,19 @@ use crate::{ parser::AdfParser, }; -use biodivine_lib_bdd::Bdd; +use biodivine_lib_bdd::{boolean_expression::BooleanExpression, Bdd, BddVariableSet}; +use derivative::Derivative; -#[derive(Debug)] +#[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) pub struct Adf { ordering: VarContainer, ac: Vec, vars: Vec, + #[derivative(Debug = "ignore")] + varset: BddVariableSet, + rewrite: Option, // stable rewrite } impl Adf { @@ -45,6 +50,8 @@ impl Adf { parser.namelist_rc_refcell().as_ref().borrow().len() ], vars: bdd_variables.variables(), + varset: bdd_variables, + rewrite: None, }; log::trace!("variable order: {:?}", result.vars); log::debug!("[Start] adding acs"); @@ -60,7 +67,8 @@ impl Adf { new_order, parser.ac_at(insert_order) ); - result.ac[*new_order] = bdd_variables + result.ac[*new_order] = result + .varset .eval_expression(&parser.ac_at(insert_order).unwrap().to_boolean_expr()); log::trace!("instantiated {}", result.ac[*new_order]); }); @@ -68,6 +76,41 @@ impl Adf { result } + /// 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"); + result.stm_rewriting(parser); + log::debug!("[Done] rewriting"); + result + } + + pub(crate) fn stm_rewriting(&mut self, parser: &AdfParser) { + let expr = parser.formula_order().iter().enumerate().fold( + biodivine_lib_bdd::boolean_expression::BooleanExpression::Const(true), + |acc, (insert_order, new_order)| { + BooleanExpression::And( + Box::new(acc), + Box::new(BooleanExpression::Iff( + Box::new(BooleanExpression::Variable( + self.ordering + .name(crate::datatypes::Var(*new_order)) + .expect("Variable should exist"), + )), + Box::new(parser.ac_at(insert_order).unwrap().to_boolean_expr()), + )), + ) + }, + ); + log::trace!("{:?}", expr); + self.rewrite = Some(self.varset.eval_expression(&expr)); + } + + /// returns `true` if the stable rewriting for this adf exists + pub fn has_stm_rewriting(&self) -> bool { + self.rewrite.is_some() + } + pub(crate) fn var_container(&self) -> &VarContainer { &self.ordering } @@ -158,13 +201,27 @@ impl Adf { ) } - /// shifts the representation and allows to use the naive approach + /// Shifts the representation and allows to use the naive approach. + /// + /// The grounded interpretation is computed by the biodivine library first. pub fn hybrid_step(&self) -> crate::adf::Adf { crate::adf::Adf::from_biodivine_vector( self.var_container(), &self.grounded_internal(self.ac()), ) } + + /// Shifts the representation and allows to use the naive approach. + /// + /// `bio_grounded` will compute the grounded, based on biodivine, first. + pub fn hybrid_step_opt(&self, bio_grounded: bool) -> crate::adf::Adf { + if bio_grounded { + self.hybrid_step() + } else { + crate::adf::Adf::from_biodivine_vector(self.var_container(), self.ac()) + } + } + /// Computes the stable models /// Returns an Iterator which contains all the stable models pub fn stable<'a, 'b>(&'a self) -> impl Iterator> + 'b @@ -190,15 +247,96 @@ impl Adf { .iter() .map(|ac| ac.restrict(&reduction_list)) .collect::>(); - let complete = self.grounded_internal(&reduct); + let grounded = self.grounded_internal(&reduct); terms .iter() - .zip(complete.iter()) + .zip(grounded.iter()) .all(|(left, right)| left.cmp_information(right)) }, ) } + /// Computes the stable models + /// This variant returns all stable models and utilises a rewrite of the adf as one big conjunction of equalities (iff) + pub fn stable_bdd_representation(&self) -> Vec> { + let smc = self.stable_model_candidates(); + log::debug!("[Start] checking for stability"); + smc.into_iter() + .filter(|terms| { + let reduction_list = self + .vars + .iter() + .enumerate() + .filter_map(|(idx, elem)| { + if terms[idx].is_truth_value() && !terms[idx].is_true() { + Some((*elem, false)) + } else { + None + } + }) + .collect::>(); + let reduct = self + .ac + .iter() + .map(|ac| ac.restrict(&reduction_list)) + .collect::>(); + let grounded = self.grounded_internal(&reduct); + terms + .iter() + .zip(grounded.iter()) + .all(|(left, right)| left.cmp_information(right)) + }) + .collect::>>() + } + + pub(crate) fn stable_model_candidates(&self) -> Vec> { + let internal_rewriting: Bdd; + let sr: &Bdd; + if self.has_stm_rewriting() { + sr = self.rewrite.as_ref().unwrap(); + } else { + internal_rewriting = self.stable_representation(); + sr = &internal_rewriting; + } + log::debug!("[Start] construct stable model candidates"); + sr.sat_valuations() + .map(|valuation| { + self.vars + .iter() + .map(|var| { + if valuation.value(*var) { + Term::TOP + } else { + Term::BOT + } + }) + .collect::>() + }) + .collect::>>() + } + + fn stable_representation(&self) -> Bdd { + log::debug!("[Start] stable representation rewriting"); + self.ac.iter().enumerate().fold( + self.varset.eval_expression( + &biodivine_lib_bdd::boolean_expression::BooleanExpression::Const(true), + ), + |acc, (idx, formula)| { + acc.and( + &formula.iff( + &self.varset.eval_expression( + &biodivine_lib_bdd::boolean_expression::BooleanExpression::Variable( + self.ordering + .name(crate::datatypes::Var(idx)) + .expect("Variable should exist"), + ), + ), + ), + ) + }, + ) + } + /// creates a [PrintableInterpretation] for output purposes pub fn print_interpretation<'a, 'b>( &'a self, @@ -348,6 +486,26 @@ mod test { ); } + #[test] + fn grounded_eq_naive() { + 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 adf = Adf::from_parser(&parser); + + let adf_grd = adf.grounded(); + let adf_hybrid_true = adf.hybrid_step_opt(true).grounded(); + let adf_hybrid_false = adf.hybrid_step_opt(false).grounded(); + adf_grd + .iter() + .zip(adf_hybrid_false.iter()) + .zip(adf_hybrid_true.iter()) + .for_each(|((a, b), c)| { + assert!(a.compare_inf(b)); + assert!(b.compare_inf(c)); + }); + } + #[test] fn complete() { let parser = AdfParser::default(); @@ -464,4 +622,23 @@ mod test { let adf = Adf::from_parser(&parser); assert_eq!(adf.stable().next(), None); } + + #[test] + fn stable_version2() { + 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 adf = Adf::from_parser(&parser); + + let mut stable_naive: Vec> = adf.stable().collect(); + let mut stable_v2 = adf.stable_bdd_representation(); + let adf2 = Adf::from_parser_with_stm_rewrite(&parser); + let mut stable_v3 = adf2.stable_bdd_representation(); + stable_naive.sort(); + stable_v2.sort(); + stable_v3.sort(); + + assert_eq!(stable_naive, stable_v2); + assert_eq!(stable_v2, stable_v3); + } } diff --git a/src/bin/adf_bdd.rs b/src/bin/adf_bdd.rs index 11a3d83..10f905b 100644 --- a/src/bin/adf_bdd.rs +++ b/src/bin/adf_bdd.rs @@ -38,6 +38,15 @@ struct App { /// Compute the stable models #[structopt(long = "stm")] stable: bool, + /// Compute the stable models with a pre-filter (only hybrid lib-mode) + #[structopt(long = "stmpre")] + stable_pre: bool, + /// Compute the stable models with a single-formula rewriting (only hybrid lib-mode) + #[structopt(long = "stmrew")] + stable_rew: bool, + /// Compute the stable models with a single-formula rewriting on internal representation(only hybrid lib-mode) + #[structopt(long = "stmrew2")] + stable_rew2: bool, /// Compute the complete models #[structopt(long = "com")] complete: bool, @@ -85,9 +94,13 @@ impl App { if self.sort_alphan { parser.varsort_alphanum(); } - let adf = BdAdf::from_parser(&parser); + let adf = if !self.stable_rew { + BdAdf::from_parser(&parser) + } else { + BdAdf::from_parser_with_stm_rewrite(&parser) + }; if self.grounded { - let grounded = adf.grounded(); + let grounded = adf.hybrid_step_opt(false).grounded(); print!("{}", adf.print_interpretation(&grounded)); } @@ -104,6 +117,18 @@ impl App { print!("{}", printer.print_interpretation(&model)); } } + + if self.stable_pre { + for model in naive_adf.stable_with_prefilter() { + print!("{}", printer.print_interpretation(&model)); + } + } + + if self.stable_rew || self.stable_rew2 { + for model in naive_adf.stable_bdd_representation(&adf) { + print!("{}", printer.print_interpretation(&model)); + } + } } "biodivine" => { let parser = adf_bdd::parser::AdfParser::default(); @@ -115,7 +140,11 @@ impl App { if self.sort_alphan { parser.varsort_alphanum(); } - let adf = BdAdf::from_parser(&parser); + let adf = if !self.stable_rew { + BdAdf::from_parser(&parser) + } else { + BdAdf::from_parser_with_stm_rewrite(&parser) + }; if self.grounded { let grounded = adf.grounded(); print!("{}", adf.print_interpretation(&grounded)); @@ -132,6 +161,12 @@ impl App { print!("{}", adf.print_interpretation(&model)); } } + + if self.stable_rew || self.stable_rew2 { + for model in adf.stable_bdd_representation() { + print!("{}", adf.print_interpretation(&model)); + } + } } _ => { let mut adf = if self.import { diff --git a/src/datatypes/adf.rs b/src/datatypes/adf.rs index dd7ac20..c71014d 100644 --- a/src/datatypes/adf.rs +++ b/src/datatypes/adf.rs @@ -181,7 +181,6 @@ pub struct ThreeValuedInterpretationsIterator { indexes: Vec, current: Option>, started: bool, - last_iteration: bool, } impl ThreeValuedInterpretationsIterator { @@ -200,7 +199,6 @@ impl ThreeValuedInterpretationsIterator { started: false, current: Some(current), original: term.into(), - last_iteration: false, } } diff --git a/src/lib.rs b/src/lib.rs index 6a3a788..393c9ba 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -1,64 +1,75 @@ -//! 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. -//! -//! # Usage -//! ```plain -//! USAGE: -//! adf_bdd [FLAGS] [OPTIONS] -//! -//! FLAGS: -//! --com Compute the complete models -//! --grd Compute the grounded model -//! -h, --help Prints help information -//! --import Import an adf- bdd state instead of an adf -//! -q Sets log verbosity to only errors -//! --an Sorts variables in an alphanumeric manner -//! --lx Sorts variables in an lexicographic manner -//! --stm Compute the stable models -//! -V, --version Prints version information -//! -v Sets log verbosity (multiple times means more verbose) -//! -//! OPTIONS: -//! --export Export the adf-bdd state after parsing and BDD instantiation to the given filename -//! --lib choose the bdd implementation of either 'biodivine', 'naive', or hybrid [default: -//! biodivine] -//! --rust_log Sets the verbosity to 'warn', 'info', 'debug' or 'trace' if -v and -q are not use -//! [env: RUST_LOG=debug] -//! -//! ARGS: -//! Input filename -//! ``` -//! -//! Note that import and export only works if the naive library is chosen -//! -//! Right now there is no additional information to the computed models, so if you use --com --grd --stm the borders between the results are not obviously communicated. -//! They can be easily identified though: -//! - The computation is always in the same order -//! - grd -//! - com -//! - stm -//! - We know that there is always exactly one grounded model -//! - We know that there always exist at least one complete model (i.e. the grounded one) -//! - We know that there does not need to exist a stable model -//! - We know that every stable model is a complete model too -//! -//! # Input-file format: -//! Each statement is defined by an ASP-style unary predicate s, where the enclosed term represents the label of the statement. -//! The binary predicate ac relates each statement to one propositional formula in prefix notation, with the logical operations and constants as follows: -//! - 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 +/*! +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. + +# Usage +```plain +USAGE: + adf_bdd [FLAGS] [OPTIONS] + +FLAGS: + --com Compute the complete models + --grd Compute the grounded model + -h, --help Prints help information + --import Import an adf- bdd state instead of an adf + -q Sets log verbosity to only errors + --an Sorts variables in an alphanumeric manner + --lx Sorts variables in an lexicographic manner + --stm Compute the stable models + --stmpre Compute the stable models with a pre-filter (only hybrid lib-mode) + --stmrew Compute the stable models with a single-formula rewriting (only hybrid lib-mode) + --stmrew2 Compute the stable models with a single-formula rewriting on internal representation(only hybrid + lib-mode) + -V, --version Prints version information + -v Sets log verbosity (multiple times means more verbose) + +OPTIONS: + --export Export the adf-bdd state after parsing and BDD instantiation to the given filename + --lib choose the bdd implementation of either 'biodivine', 'naive', or hybrid [default: + biodivine] + --rust_log Sets the verbosity to 'warn', 'info', 'debug' or 'trace' if -v and -q are not use + [env: RUST_LOG=debug] + +ARGS: + Input filename +``` + +Note that import and export only works if the naive library is chosen + +Right now there is no additional information to the computed models, so if you use --com --grd --stm the borders between the results are not obviously communicated. +They can be easily identified though: +- The computation is always in the same order + - grd + - com + - stm +- We know that there is always exactly one grounded model +- We know that there always exist at least one complete model (i.e. the grounded one) +- We know that there does not need to exist a stable model +- We know that every stable model is a complete model too + +# Input-file format: +Each statement is defined by an ASP-style unary predicate s, where the enclosed term represents the label of the statement. +The binary predicate ac relates each statement to one propositional formula in prefix notation, with the logical operations and constants as follows: +- 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: //! ```prolog diff --git a/src/parser.rs b/src/parser.rs index cf03939..f4a739c 100644 --- a/src/parser.rs +++ b/src/parser.rs @@ -119,7 +119,8 @@ impl std::fmt::Debug for Formula<'_> { } } -/// A parse structure to hold all the information given by the input file in one place +/// 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. /// @@ -220,7 +221,7 @@ impl AdfParser<'_> { self } - /// Sort the variables in alphanumerical order + /// Sort the variables in alphanumerical order. /// Results which got used before might become corrupted. pub fn varsort_alphanum(&self) -> &Self { self.namelist diff --git a/src/test.rs b/src/test.rs index 132423d..c749769 100644 --- a/src/test.rs +++ b/src/test.rs @@ -147,3 +147,26 @@ fn adf_biodivine_cmp_2() { assert_eq!(str1, str2); assert_eq!(str1, str3); } + +#[test] +fn stable_variants_cmp() { + 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 adf = Adf::from_parser_with_stm_rewrite(&parser); + let mut naive_adf = NaiveAdf::from_biodivine(&adf); + + let mut stable_naive: Vec> = naive_adf.stable().collect(); + let mut stable_pre: Vec> = naive_adf.stable_with_prefilter().collect(); + let mut stable_v2 = adf.stable_bdd_representation(); + let mut stable_v2_hybrid = naive_adf.stable_bdd_representation(&adf); + + stable_naive.sort(); + stable_pre.sort(); + stable_v2.sort(); + stable_v2_hybrid.sort(); + + assert_eq!(stable_naive, stable_v2); + assert_eq!(stable_v2, stable_v2_hybrid); + assert_eq!(stable_pre, stable_v2); +}