mirror of
https://github.com/ellmau/adf-obdd.git
synced 2025-12-19 09:29:36 +01:00
ADD variable list mechanics (#27)
* directly hooked into the internal BDD-primitive functions
* has worse performance than the approach without the primitive functions
* foreseeable for easy problems
* surprise for more complex problems, because recursion can be
escaped much earlier
* ADD the default-feature "variablelist" to have a compile-flag to either
enable or disable this feature.
* updated rust to the current version
This commit is contained in:
Stefan Ellmauthaler
GitHub
parent
a2fa3adfe9
commit
3f32db45ee
@ -37,7 +37,8 @@ quickcheck = "1"
|
||||
quickcheck_macros = "1"
|
||||
|
||||
[features]
|
||||
default = ["adhoccounting"]
|
||||
default = ["adhoccounting", "variablelist" ]
|
||||
adhoccounting = [] # count models ad-hoc - disable if counting is not needed
|
||||
importexport = []
|
||||
|
||||
variablelist = [ "HashSet" ]
|
||||
HashSet = []
|
||||
128
bin/Cargo.lock
generated
128
bin/Cargo.lock
generated
@ -5,23 +5,6 @@ version = 3
|
||||
[[package]]
|
||||
name = "adf_bdd"
|
||||
version = "0.2.1"
|
||||
dependencies = [
|
||||
"adf_bdd 0.2.1 (git+https://github.com/ellmau/adf-obdd?branch=main)",
|
||||
"assert_cmd",
|
||||
"assert_fs",
|
||||
"clap 3.1.3",
|
||||
"env_logger",
|
||||
"log",
|
||||
"predicates",
|
||||
"serde",
|
||||
"serde_json",
|
||||
"structopt",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "adf_bdd"
|
||||
version = "0.2.1"
|
||||
source = "git+https://github.com/ellmau/adf-obdd?branch=main#b18bbe0ed4755f03e5878ecc7ef87ffc7fc71bce"
|
||||
dependencies = [
|
||||
"biodivine-lib-bdd",
|
||||
"derivative",
|
||||
@ -32,6 +15,21 @@ dependencies = [
|
||||
"serde_json",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "adf_bdd-solver"
|
||||
version = "0.2.1"
|
||||
dependencies = [
|
||||
"adf_bdd",
|
||||
"assert_cmd",
|
||||
"assert_fs",
|
||||
"clap",
|
||||
"env_logger",
|
||||
"log",
|
||||
"predicates",
|
||||
"serde",
|
||||
"serde_json",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "aho-corasick"
|
||||
version = "0.7.18"
|
||||
@ -41,15 +39,6 @@ dependencies = [
|
||||
"memchr",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "ansi_term"
|
||||
version = "0.12.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "d52a9bb7ec0cf484c551830a7ce27bd20d67eac647e1befb56b0be4ee39a55d2"
|
||||
dependencies = [
|
||||
"winapi",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "any_ascii"
|
||||
version = "0.1.7"
|
||||
@ -140,21 +129,6 @@ version = "1.0.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"
|
||||
|
||||
[[package]]
|
||||
name = "clap"
|
||||
version = "2.34.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "a0610544180c38b88101fecf2dd634b174a62eef6946f84dfc6a7127512b381c"
|
||||
dependencies = [
|
||||
"ansi_term",
|
||||
"atty",
|
||||
"bitflags",
|
||||
"strsim 0.8.0",
|
||||
"textwrap 0.11.0",
|
||||
"unicode-width",
|
||||
"vec_map",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "clap"
|
||||
version = "3.1.3"
|
||||
@ -167,9 +141,9 @@ dependencies = [
|
||||
"indexmap",
|
||||
"lazy_static",
|
||||
"os_str_bytes",
|
||||
"strsim 0.10.0",
|
||||
"strsim",
|
||||
"termcolor",
|
||||
"textwrap 0.14.2",
|
||||
"textwrap",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
@ -178,7 +152,7 @@ version = "3.1.2"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "01d42c94ce7c2252681b5fed4d3627cc807b13dfc033246bd05d5b252399000e"
|
||||
dependencies = [
|
||||
"heck 0.4.0",
|
||||
"heck",
|
||||
"proc-macro-error",
|
||||
"proc-macro2",
|
||||
"quote",
|
||||
@ -311,15 +285,6 @@ version = "0.11.2"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "ab5ef0d4909ef3724cc8cce6ccc8572c5c817592e9285f5464f8e86f8bd3726e"
|
||||
|
||||
[[package]]
|
||||
name = "heck"
|
||||
version = "0.3.3"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "6d621efb26863f0e9924c6ac577e8275e5e6b77455db64ffa6c65c904e9e132c"
|
||||
dependencies = [
|
||||
"unicode-segmentation",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "heck"
|
||||
version = "0.4.0"
|
||||
@ -682,42 +647,12 @@ dependencies = [
|
||||
"serde",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "strsim"
|
||||
version = "0.8.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "8ea5119cdb4c55b55d432abb513a0429384878c15dde60cc77b1c99de1a95a6a"
|
||||
|
||||
[[package]]
|
||||
name = "strsim"
|
||||
version = "0.10.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "73473c0e59e6d5812c5dfe2a064a6444949f089e20eec9a2e5506596494e4623"
|
||||
|
||||
[[package]]
|
||||
name = "structopt"
|
||||
version = "0.3.26"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "0c6b5c64445ba8094a6ab0c3cd2ad323e07171012d9c98b0b15651daf1787a10"
|
||||
dependencies = [
|
||||
"clap 2.34.0",
|
||||
"lazy_static",
|
||||
"structopt-derive",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "structopt-derive"
|
||||
version = "0.4.18"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "dcb5ae327f9cc13b68763b5749770cb9e048a99bd9dfdfa58d0cf05d5f64afe0"
|
||||
dependencies = [
|
||||
"heck 0.3.3",
|
||||
"proc-macro-error",
|
||||
"proc-macro2",
|
||||
"quote",
|
||||
"syn",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "syn"
|
||||
version = "1.0.86"
|
||||
@ -758,15 +693,6 @@ version = "0.2.4"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "507e9898683b6c43a9aa55b64259b721b52ba226e0f3779137e50ad114a4c90b"
|
||||
|
||||
[[package]]
|
||||
name = "textwrap"
|
||||
version = "0.11.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "d326610f408c7a4eb6f51c37c330e496b08506c9457c9d34287ecc38809fb060"
|
||||
dependencies = [
|
||||
"unicode-width",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "textwrap"
|
||||
version = "0.14.2"
|
||||
@ -782,30 +708,12 @@ dependencies = [
|
||||
"once_cell",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "unicode-segmentation"
|
||||
version = "1.9.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "7e8820f5d777f6224dc4be3632222971ac30164d4a258d595640799554ebfd99"
|
||||
|
||||
[[package]]
|
||||
name = "unicode-width"
|
||||
version = "0.1.9"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "3ed742d4ea2bd1176e236172c8429aaf54486e7ac098db29ffe6529e0ce50973"
|
||||
|
||||
[[package]]
|
||||
name = "unicode-xid"
|
||||
version = "0.2.2"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "8ccb82d61f80a663efe1f787a51b16b5a51e3314d6ac365b08639f52387b33f3"
|
||||
|
||||
[[package]]
|
||||
name = "vec_map"
|
||||
version = "0.8.2"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "f1bddf1187be692e79c5ffeab891132dfb0f236ed36a43c7ed39f1165ee20191"
|
||||
|
||||
[[package]]
|
||||
name = "version_check"
|
||||
version = "0.9.4"
|
||||
|
||||
@ -1,5 +1,5 @@
|
||||
[package]
|
||||
name = "adf_bdd"
|
||||
name = "adf_bdd-solver"
|
||||
version = "0.2.1"
|
||||
authors = ["Stefan Ellmauthaler <stefan.ellmauthaler@tu-dresden.de>"]
|
||||
edition = "2021"
|
||||
@ -9,8 +9,12 @@ description = "Solver for ADFs grounded, complete, and stable semantics by utili
|
||||
|
||||
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
|
||||
|
||||
[[bin]]
|
||||
name = "adf_bdd"
|
||||
path = "src/main.rs"
|
||||
|
||||
[dependencies]
|
||||
adf_bdd = { git = "https://github.com/ellmau/adf-obdd", branch = "main" }
|
||||
adf_bdd = { path = "../" }
|
||||
clap = {version = "3.1.3", features = [ "derive", "cargo", "env" ]}
|
||||
log = { version = "0.4", features = [ "max_level_trace", "release_max_level_info" ] }
|
||||
serde = { version = "1.0", features = ["derive","rc"] }
|
||||
|
||||
@ -267,7 +267,7 @@ impl App {
|
||||
}
|
||||
#[cfg(feature = "adhoccounting")]
|
||||
{
|
||||
let result: Adf = serde_json::from_str(&input).unwrap();
|
||||
let mut result: Adf = serde_json::from_str(&input).unwrap();
|
||||
log::debug!("test");
|
||||
result.fix_import();
|
||||
result
|
||||
|
||||
@ -27,7 +27,7 @@ fn arguments() -> Result<(), Box<dyn std::error::Error>> {
|
||||
cmd.arg("--version");
|
||||
cmd.assert()
|
||||
.success()
|
||||
.stdout(predicate::str::contains("adf_bdd "));
|
||||
.stdout(predicate::str::contains("adf_bdd-solver "));
|
||||
Ok(())
|
||||
}
|
||||
|
||||
|
||||
18
flake.lock
generated
18
flake.lock
generated
@ -18,11 +18,11 @@
|
||||
},
|
||||
"flake-utils": {
|
||||
"locked": {
|
||||
"lastModified": 1642700792,
|
||||
"narHash": "sha256-XqHrk7hFb+zBvRg6Ghl+AZDq03ov6OshJLiSWOoX5es=",
|
||||
"lastModified": 1644229661,
|
||||
"narHash": "sha256-1YdnJAsNy69bpcjuoKdOYQX0YxZBiCYZo4Twxerqv7k=",
|
||||
"owner": "numtide",
|
||||
"repo": "flake-utils",
|
||||
"rev": "846b2ae0fc4cc943637d3d1def4454213e203cba",
|
||||
"rev": "3cecb5b042f7f209c56ffd8371b2711a290ec797",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
@ -64,11 +64,11 @@
|
||||
},
|
||||
"nixpkgs": {
|
||||
"locked": {
|
||||
"lastModified": 1643788601,
|
||||
"narHash": "sha256-6l5Ax44pC/Oo/Muj5Y/NA27Pd38Wty/7GtGSSmYNug4=",
|
||||
"lastModified": 1646162891,
|
||||
"narHash": "sha256-Yoyur5LD3nRKFZRwVi2lHZi2HKoWUJFAHgIFcYsRhho=",
|
||||
"owner": "NixOS",
|
||||
"repo": "nixpkgs",
|
||||
"rev": "f6ddd55d5f9d5eca08df138c248008c1ba73ecec",
|
||||
"rev": "b099eaa0e01a45fc3459bbe987c3405c425ef05c",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
@ -109,11 +109,11 @@
|
||||
"nixpkgs": "nixpkgs_2"
|
||||
},
|
||||
"locked": {
|
||||
"lastModified": 1643941258,
|
||||
"narHash": "sha256-uHyEuICSu8qQp6adPTqV33ajiwoF0sCh+Iazaz5r7fo=",
|
||||
"lastModified": 1646274381,
|
||||
"narHash": "sha256-kglX5g7HhSWiTGKz1WOA8DWclj0Wwsq8I50wgY4eS3I=",
|
||||
"owner": "oxalica",
|
||||
"repo": "rust-overlay",
|
||||
"rev": "674156c4c2f46dd6a6846466cb8f9fee84c211ca",
|
||||
"rev": "245c2712f502849041a1b1d0cc6a7588e94b2e3f",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
|
||||
@ -394,9 +394,8 @@ impl Adf {
|
||||
PrintDictionary::new(&self.ordering)
|
||||
}
|
||||
|
||||
#[cfg(feature = "adhoccounting")]
|
||||
/// If the feature for adhoccounting is enabled, this fixes the bdd after an import with serde
|
||||
pub fn fix_import(&self) {
|
||||
/// Fixes the bdd after an import with serde
|
||||
pub fn fix_import(&mut self) {
|
||||
self.bdd.fix_import();
|
||||
}
|
||||
}
|
||||
|
||||
86
src/obdd.rs
86
src/obdd.rs
@ -2,11 +2,16 @@
|
||||
pub mod vectorize;
|
||||
use crate::datatypes::*;
|
||||
use serde::{Deserialize, Serialize};
|
||||
#[cfg(feature = "HashSet")]
|
||||
use std::collections::HashSet;
|
||||
use std::{cell::RefCell, cmp::min, collections::HashMap, fmt::Display};
|
||||
|
||||
#[derive(Debug, Serialize, Deserialize)]
|
||||
pub(crate) struct Bdd {
|
||||
pub(crate) nodes: Vec<BddNode>,
|
||||
#[cfg(feature = "variablelist")]
|
||||
#[serde(skip)]
|
||||
var_deps: Vec<HashSet<Var>>,
|
||||
#[serde(with = "vectorize")]
|
||||
cache: HashMap<BddNode, Term>,
|
||||
#[serde(skip, default = "Bdd::default_count_cache")]
|
||||
@ -29,6 +34,8 @@ impl Bdd {
|
||||
{
|
||||
Self {
|
||||
nodes: vec![BddNode::bot_node(), BddNode::top_node()],
|
||||
#[cfg(feature = "variablelist")]
|
||||
var_deps: vec![HashSet::new(), HashSet::new()],
|
||||
cache: HashMap::new(),
|
||||
count_cache: RefCell::new(HashMap::new()),
|
||||
}
|
||||
@ -37,6 +44,8 @@ impl Bdd {
|
||||
{
|
||||
let result = Self {
|
||||
nodes: vec![BddNode::bot_node(), BddNode::top_node()],
|
||||
#[cfg(feature = "variablelist")]
|
||||
var_deps: vec![HashSet::new(), HashSet::new()],
|
||||
cache: HashMap::new(),
|
||||
count_cache: RefCell::new(HashMap::new()),
|
||||
};
|
||||
@ -96,6 +105,10 @@ impl Bdd {
|
||||
|
||||
pub fn restrict(&mut self, tree: Term, var: Var, val: bool) -> Term {
|
||||
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 {
|
||||
@ -153,6 +166,15 @@ impl Bdd {
|
||||
let new_term = Term(self.nodes.len());
|
||||
self.nodes.push(node);
|
||||
self.cache.insert(node, new_term);
|
||||
#[cfg(feature = "variablelist")]
|
||||
{
|
||||
let mut var_set: HashSet<Var> = self.var_deps[lo.value()]
|
||||
.union(&self.var_deps[hi.value()])
|
||||
.copied()
|
||||
.collect();
|
||||
var_set.insert(var);
|
||||
self.var_deps.push(var_set);
|
||||
}
|
||||
#[cfg(feature = "adhoccounting")]
|
||||
{
|
||||
log::debug!("newterm: {} as {:?}", new_term, node);
|
||||
@ -261,15 +283,35 @@ impl Bdd {
|
||||
}
|
||||
}
|
||||
|
||||
#[cfg(feature = "adhoccounting")]
|
||||
pub fn fix_import(&self) {
|
||||
self.count_cache.borrow_mut().insert(Term::TOP, ((0, 1), 0));
|
||||
self.count_cache.borrow_mut().insert(Term::BOT, ((1, 0), 0));
|
||||
for i in 0..self.nodes.len() {
|
||||
log::debug!("fixing Term({})", i);
|
||||
self.modelcount_memoization(Term(i));
|
||||
/// repairs the internal structures after an import
|
||||
pub fn fix_import(&mut self) {
|
||||
self.generate_var_dependencies();
|
||||
#[cfg(feature = "adhoccounting")]
|
||||
{
|
||||
self.count_cache.borrow_mut().insert(Term::TOP, ((0, 1), 0));
|
||||
self.count_cache.borrow_mut().insert(Term::BOT, ((1, 0), 0));
|
||||
for i in 0..self.nodes.len() {
|
||||
log::debug!("fixing Term({})", i);
|
||||
self.modelcount_memoization(Term(i));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn generate_var_dependencies(&mut self) {
|
||||
#[cfg(feature = "variablelist")]
|
||||
self.nodes.iter().for_each(|node| {
|
||||
if node.var() >= Var::BOT {
|
||||
self.var_deps.push(HashSet::new());
|
||||
} else {
|
||||
let mut var_set: HashSet<Var> = self.var_deps[node.lo().value()]
|
||||
.union(&self.var_deps[node.hi().value()])
|
||||
.copied()
|
||||
.collect();
|
||||
var_set.insert(node.var());
|
||||
self.var_deps.push(var_set);
|
||||
}
|
||||
});
|
||||
}
|
||||
}
|
||||
|
||||
#[cfg(test)]
|
||||
@ -364,6 +406,7 @@ mod test {
|
||||
let con1 = bdd.and(a, conj);
|
||||
|
||||
let end = bdd.or(con1, b);
|
||||
log::debug!("Restrict test: restrict({},{},false)", end, Var(1));
|
||||
let x = bdd.restrict(end, Var(1), false);
|
||||
assert_eq!(x, Term(2));
|
||||
}
|
||||
@ -453,4 +496,33 @@ mod test {
|
||||
bdd.modelcount_memoization(Term::BOT)
|
||||
);
|
||||
}
|
||||
|
||||
#[cfg(feature = "variablelist")]
|
||||
#[test]
|
||||
fn generate_var_dependencies() {
|
||||
let mut bdd = Bdd::new();
|
||||
|
||||
let v1 = bdd.variable(Var(0));
|
||||
let v2 = bdd.variable(Var(1));
|
||||
let v3 = bdd.variable(Var(2));
|
||||
|
||||
let formula1 = bdd.and(v1, v2);
|
||||
let formula2 = bdd.or(v1, v2);
|
||||
let formula3 = bdd.xor(v1, v2);
|
||||
let formula4 = bdd.and(v3, formula2);
|
||||
|
||||
bdd.iff(formula1, formula3);
|
||||
bdd.not(formula4);
|
||||
|
||||
let constructed = bdd.var_deps.clone();
|
||||
bdd.var_deps = Vec::new();
|
||||
bdd.generate_var_dependencies();
|
||||
|
||||
constructed
|
||||
.iter()
|
||||
.zip(bdd.var_deps.iter())
|
||||
.for_each(|(left, right)| {
|
||||
assert!(left == right);
|
||||
});
|
||||
}
|
||||
}
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user