From 3541afe4b8a77d8beadaa49c51983c5dfde0c8aa Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Wed, 19 Oct 2022 14:06:07 +0200 Subject: [PATCH] Implement list-based restriction Add tests for both variants NG solver and grounded use the new variant now --- Cargo.lock | 69 +++++++++++++++++++++++- lib/Cargo.toml | 1 + lib/src/adf.rs | 28 ++++++++-- lib/src/obdd.rs | 141 ++++++++++++++++++++++++++++++++++++++---------- 4 files changed, 205 insertions(+), 34 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index a3b49ac..6eef66e 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -29,6 +29,7 @@ dependencies = [ "env_logger 0.9.1", "lexical-sort", "log", + "mimicry", "nom", "quickcheck", "quickcheck_macros", @@ -203,6 +204,41 @@ dependencies = [ "lazy_static", ] +[[package]] +name = "darling" +version = "0.14.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4529658bdda7fd6769b8614be250cdcfc3aeb0ee72fe66f9e41e5e5eb73eac02" +dependencies = [ + "darling_core", + "darling_macro", +] + +[[package]] +name = "darling_core" +version = "0.14.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "649c91bc01e8b1eac09fb91e8dbc7d517684ca6be8ebc75bb9cafc894f9fdb6f" +dependencies = [ + "fnv", + "ident_case", + "proc-macro2", + "quote", + "strsim", + "syn", +] + +[[package]] +name = "darling_macro" +version = "0.14.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ddfc69c5bfcbd2fc09a0f38451d2daf0e372e367986a83906d1b0dbc88134fb5" +dependencies = [ + "darling_core", + "quote", + "syn", +] + [[package]] name = "derivative" version = "2.2.0" @@ -355,6 +391,12 @@ version = "2.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9a3a5bfb195931eeb336b2a7b4d761daec841b97f947d34394601737a7bba5e4" +[[package]] +name = "ident_case" +version = "1.0.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b9e0384b61958566e926dc50660321d12159025e767c18e043daf26b70104c39" + [[package]] name = "ignore" version = "0.4.18" @@ -433,6 +475,29 @@ version = "2.4.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "308cc39be01b73d0d18f82a0e7b2a3df85245f84af96fdddc5d202d27e47b86a" +[[package]] +name = "mimicry" +version = "0.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d070adda34f833eceb5c7fe3fb57713d80d785daf449958e7e26e7eedbf53311" +dependencies = [ + "mimicry-derive", + "once_cell", + "thread_local", +] + +[[package]] +name = "mimicry-derive" +version = "0.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e43e23477e725f3549155c0ab230932dc7b8e648575252a76e5b9729a2bf59b9" +dependencies = [ + "darling", + "proc-macro2", + "quote", + "syn", +] + [[package]] name = "minimal-lexical" version = "0.2.1" @@ -590,9 +655,9 @@ dependencies = [ [[package]] name = "quote" -version = "1.0.15" +version = "1.0.21" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "864d3e96a899863136fc6e99f3d7cae289dafe43bf2c5ac19b70df7210c0a145" +checksum = "bbe448f377a7d6961e30f5955f9b8d106c3f5e449d493ee1b125c1d43c2b5179" dependencies = [ "proc-macro2", ] diff --git a/lib/Cargo.toml b/lib/Cargo.toml index b43e469..cfc103d 100644 --- a/lib/Cargo.toml +++ b/lib/Cargo.toml @@ -40,6 +40,7 @@ test-log = "0.2" env_logger = "0.9" quickcheck = "1" quickcheck_macros = "1" +mimicry = "0.1.0" # mock for tests [features] default = ["adhoccounting", "variablelist", "frontend" ] diff --git a/lib/src/adf.rs b/lib/src/adf.rs index 3b007a1..f198955 100644 --- a/lib/src/adf.rs +++ b/lib/src/adf.rs @@ -200,8 +200,9 @@ impl Adf { pub fn grounded(&mut self) -> Vec { log::info!("[Start] grounded"); let ac = &self.ac.clone(); - let result = self.grounded_internal(ac); + let result = self.update_interpretation_fixpoint(ac); log::info!("[Done] grounded"); + log::debug!("{:?}", self.bdd); result } @@ -602,7 +603,7 @@ impl Adf { fn update_interpretation_fixpoint(&mut self, interpretation: &[Term]) -> Vec { let mut cur_int = interpretation.to_vec(); loop { - let new_int = self.update_interpretation(interpretation); + let new_int = self.update_interpretation(&cur_int); if cur_int == new_int { return cur_int; } else { @@ -632,7 +633,7 @@ impl Adf { } fn update_interpretation(&mut self, interpretation: &[Term]) -> Vec { - self.apply_interpretation(interpretation, interpretation) + self.apply_interpretation_list(interpretation, interpretation) } fn apply_interpretation(&mut self, ac: &[Term], interpretation: &[Term]) -> Vec { @@ -652,6 +653,27 @@ impl Adf { .collect::>() } + fn apply_interpretation_list(&mut self, ac: &[Term], interpretation: &[Term]) -> Vec { + ac.iter() + .map(|ac| { + self.bdd.restrict_list( + *ac, + &interpretation + .iter() + .enumerate() + .filter_map(|(idx, val)| { + if val.is_truth_value() { + Some((Var(idx), val.is_true())) + } else { + None + } + }) + .collect::>(), + ) + }) + .collect::>() + } + fn check_consistency(&mut self, interpretation: &[Term], will_be: &[Term]) -> bool { interpretation .iter() diff --git a/lib/src/obdd.rs b/lib/src/obdd.rs index a54cb70..c3e976c 100644 --- a/lib/src/obdd.rs +++ b/lib/src/obdd.rs @@ -8,6 +8,9 @@ use serde::{Deserialize, Serialize}; use std::collections::HashSet; use std::{cell::RefCell, cmp::min, collections::HashMap, fmt::Display}; +#[cfg(test)] +use mimicry::mock; + /// 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. @@ -198,39 +201,37 @@ 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 { - if let Some(result) = self.restrict_cache.get(&(tree, var, val)) { - *result - } else { - let node = self.nodes[tree.0]; - #[cfg(feature = "variablelist")] - { - if !self.var_deps[tree.value()].contains(&var) { - return tree; - } - } - #[allow(clippy::collapsible_else_if)] - // Readability of algorithm > code-elegance - if node.var() > var || node.var() >= Var::BOT { - tree - } else if node.var() < var { - let lonode = self.restrict(node.lo(), var, val); - let hinode = self.restrict(node.hi(), var, val); - let result = self.node(node.var(), lonode, hinode); - self.restrict_cache.insert((tree, var, val), result); - result + /// Restrict the bdd to the given list of [variables][crate::datatypes::Var] and [values][bool]. + pub fn restrict_list(&mut self, tree: Term, list: &[(Var, bool)]) -> Term { + if let Some(&(var, val)) = list.first() { + if let Some(result) = self.restrict_cache.get(&(tree, var, val)) { + self.restrict_list(*result, &list[1..]) } else { - if val { - let result = self.restrict(node.hi(), var, val); - self.restrict_cache.insert((tree, var, val), result); - result + let node = self.nodes[tree.value()]; + #[cfg(feature = "variablelist")] + { + if !self.var_deps[tree.value()].contains(&var) { + return self.restrict_list(tree, &list[1..]); + } + } + if node.var() >= Var::BOT { + tree + } else if node.var() > var { + self.restrict_list(tree, &list[1..]) + } else if node.var() < var { + let lonode = self.restrict_list(node.lo(), list); + let hinode = self.restrict_list(node.hi(), list); + let result = self.node(node.var(), lonode, hinode); + self.restrict_list(result, &list[1..]) } else { - let result = self.restrict(node.lo(), var, val); + let result = if val { node.hi() } else { node.lo() }; self.restrict_cache.insert((tree, var, val), result); - result + self.restrict_list(result, &list[1..]) } } + } else { + // No elements in list + tree } } @@ -569,9 +570,87 @@ impl Bdd { } } +#[cfg_attr(test, mock(using = "test::TestBdd"))] +impl Bdd { + /// Restrict the value of a given [variable][crate::datatypes::Var] to **val**. + pub fn restrict(&mut self, tree: Term, var: Var, val: bool) -> Term { + if let Some(result) = self.restrict_cache.get(&(tree, var, val)) { + *result + } else { + let node = self.nodes[tree.0]; + #[cfg(feature = "variablelist")] + { + if !self.var_deps[tree.value()].contains(&var) { + return tree; + } + } + #[allow(clippy::collapsible_else_if)] + // Readability of algorithm > code-elegance + if node.var() > var || node.var() >= Var::BOT { + tree + } else if node.var() < var { + let lonode = self.restrict(node.lo(), var, val); + let hinode = self.restrict(node.hi(), var, val); + let result = self.node(node.var(), lonode, hinode); + self.restrict_cache.insert((tree, var, val), result); + result + } else { + if val { + let result = self.restrict(node.hi(), var, val); + self.restrict_cache.insert((tree, var, val), result); + result + } else { + let result = self.restrict(node.lo(), var, val); + self.restrict_cache.insert((tree, var, val), result); + result + } + } + } + } +} + #[cfg(test)] mod test { use super::*; + use mimicry::Mock; + + #[derive(Default, Mock)] + pub struct TestBdd {} + impl mimicry::CheckRealCall for TestBdd {} + impl TestBdd { + pub fn restrict<'s>(&self, recv: &'s mut Bdd, tree: Term, var: Var, val: bool) -> Term { + recv.restrict_list(tree, &[(var, val)]) + } + } + + macro_rules! genmockguard { + ($func: ident) => { + let _guard = TestBdd::default().set_as_mock(); + $func(); + }; + } + + macro_rules! test { + ($func: ident, $func2: ident) => { + #[test] + fn $func2() { + genmockguard!($func); + } + }; + } + + test!(newbdd, mock_newbdd); + test!(addconst, mock_addconst); + test!(addvar, mock_addvar); + test!(use_negation, mock_use_negation); + test!(use_and, mock_use_and); + test!(use_or, mock_use_or); + test!( + produce_different_conversions, + mock_produce_different_conversions + ); + test!(display, mock_display); + test!(counting, mock_counting); #[test] fn newbdd() { @@ -588,6 +667,8 @@ mod test { assert_eq!(bdd.nodes.len(), 2); } + test!(addconst, addconst_list); + #[test] fn addvar() { let mut bdd = Bdd::new(); @@ -607,7 +688,7 @@ mod test { } #[test] - fn use_add() { + fn use_and() { let mut bdd = Bdd::new(); let v1 = bdd.variable(Var(0)); let v2 = bdd.variable(Var(1)); @@ -652,8 +733,10 @@ mod test { assert_eq!(bdd.and(v3, nv3), Term::BOT); let conj = bdd.and(v1, v2); + assert_eq!(bdd.restrict_list(conj, &[(Var(0), true)]), v2); assert_eq!(bdd.restrict(conj, Var(0), false), Term::BOT); assert_eq!(bdd.restrict(conj, Var(0), true), v2); + assert_eq!(bdd.restrict_list(conj, &[(Var(0), false)]), Term::BOT); let a = bdd.and(v3, v2); let b = bdd.or(v2, v1);