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

Implement list-based restriction

Browse Source 
Add tests for both variants
NG solver and grounded use the new variant now
This commit is contained in:
Stefan Ellmauthaler 2022-10-19 14:06:07 +02:00
parent 68cbab5b02
commit 3541afe4b8
Failed to extract signature
4 changed files with 205 additions and 34 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

69
Cargo.lock generated
View File

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

1
lib/Cargo.toml
View File

@ -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" ]

28
lib/src/adf.rs
View File

@ -200,8 +200,9 @@ impl Adf {
pub fn grounded(&mut self) -> Vec<Term> {
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<Term> {
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<Term> {
self.apply_interpretation(interpretation, interpretation)
self.apply_interpretation_list(interpretation, interpretation)
}
fn apply_interpretation(&mut self, ac: &[Term], interpretation: &[Term]) -> Vec<Term> {
@ -652,6 +653,27 @@ impl Adf {
.collect::<Vec<Term>>()
}
fn apply_interpretation_list(&mut self, ac: &[Term], interpretation: &[Term]) -> Vec<Term> {
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::<Vec<(Var, bool)>>(),
)
})
.collect::<Vec<Term>>()
}
fn check_consistency(&mut self, interpretation: &[Term], will_be: &[Term]) -> bool {
interpretation
.iter()

141
lib/src/obdd.rs
View File

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