From 565fef99d127ffce7b966740a2b8a9b03ab67934 Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler <71695780+ellmau@users.noreply.github.com> Date: Mon, 21 Feb 2022 10:49:27 +0100 Subject: [PATCH] ADD counting of (counter) models and variables of one BDD-Tree (#21) * ADD counting of (counter) models and variables of one BDD-Tree * ADD counting with memoization set ahoc-counting as default feature --- Cargo.toml | 7 +- src/adf.rs | 31 +++++- src/bin/adf_bdd.rs | 64 ++++++++++++- src/datatypes/bdd.rs | 5 + src/obdd.rs | 219 ++++++++++++++++++++++++++++++++++++++++++- 5 files changed, 315 insertions(+), 11 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index a29b1dd..7e7fd66 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -43,4 +43,9 @@ quickcheck = "1" quickcheck_macros = "1" assert_cmd = "2.0" predicates = "2.1" -assert_fs = "1.0" \ No newline at end of file +assert_fs = "1.0" + +[features] +default = ["adhoccounting"] +adhoccounting = [] # count models ad-hoc - disable if counting is not needed +importexport = [] \ No newline at end of file diff --git a/src/adf.rs b/src/adf.rs index d85069f..e1c0ce5 100644 --- a/src/adf.rs +++ b/src/adf.rs @@ -11,7 +11,7 @@ use crate::{ PrintDictionary, PrintableInterpretation, ThreeValuedInterpretationsIterator, TwoValuedInterpretationsIterator, VarContainer, }, - Term, Var, + ModelCounts, Term, Var, }, obdd::Bdd, parser::{AdfParser, Formula}, @@ -368,6 +368,16 @@ impl Adf { }) } + /// Returns a [Vector][std::vec::Vec] of [ModelCounts][crate::datatypes::ModelCounts] for each acceptance condition. + /// + /// `memoization` controls whether memoization is utilised or not. + pub fn formulacounts(&self, memoization: bool) -> Vec { + self.ac + .iter() + .map(|ac| self.bdd.models(*ac, memoization)) + .collect() + } + /// creates a [PrintableInterpretation] for output purposes pub fn print_interpretation<'a, 'b>( &'a self, @@ -383,6 +393,12 @@ impl Adf { pub fn print_dictionary(&self) -> PrintDictionary { 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) { + self.bdd.fix_import(); + } } #[cfg(test)] @@ -433,7 +449,7 @@ mod test { let serialized = serde_json::to_string(&adf).unwrap(); log::debug!("Serialized to {}", serialized); - let result = r#"{"ordering":{"names":["a","c","b","e","d"],"mapping":{"b":2,"a":0,"e":3,"c":1,"d":4}},"bdd":{"nodes":[{"var":18446744073709551614,"lo":0,"hi":0},{"var":18446744073709551615,"lo":1,"hi":1},{"var":0,"lo":0,"hi":1},{"var":1,"lo":0,"hi":1},{"var":2,"lo":0,"hi":1},{"var":3,"lo":0,"hi":1},{"var":4,"lo":0,"hi":1},{"var":0,"lo":1,"hi":0},{"var":0,"lo":1,"hi":4},{"var":1,"lo":1,"hi":0},{"var":2,"lo":1,"hi":0},{"var":1,"lo":10,"hi":4},{"var":0,"lo":3,"hi":11},{"var":3,"lo":1,"hi":0},{"var":4,"lo":1,"hi":0},{"var":3,"lo":6,"hi":14}],"cache":[[{"var":3,"lo":1,"hi":0},13],[{"var":3,"lo":6,"hi":14},15],[{"var":4,"lo":0,"hi":1},6],[{"var":0,"lo":0,"hi":1},2],[{"var":4,"lo":1,"hi":0},14],[{"var":2,"lo":0,"hi":1},4],[{"var":1,"lo":0,"hi":1},3],[{"var":0,"lo":1,"hi":4},8],[{"var":3,"lo":0,"hi":1},5],[{"var":0,"lo":1,"hi":0},7],[{"var":2,"lo":1,"hi":0},10],[{"var":0,"lo":3,"hi":11},12],[{"var":1,"lo":1,"hi":0},9],[{"var":1,"lo":10,"hi":4},11]]},"ac":[4,2,7,15,12]}"#; + let result = r#"{"ordering":{"names":["a","c","b","e","d"],"mapping":{"b":2,"a":0,"c":1,"e":3,"d":4}},"bdd":{"nodes":[{"var":18446744073709551614,"lo":0,"hi":0},{"var":18446744073709551615,"lo":1,"hi":1},{"var":0,"lo":0,"hi":1},{"var":1,"lo":0,"hi":1},{"var":2,"lo":0,"hi":1},{"var":3,"lo":0,"hi":1},{"var":4,"lo":0,"hi":1},{"var":0,"lo":1,"hi":0},{"var":0,"lo":1,"hi":4},{"var":1,"lo":1,"hi":0},{"var":2,"lo":1,"hi":0},{"var":1,"lo":10,"hi":4},{"var":0,"lo":3,"hi":11},{"var":3,"lo":1,"hi":0},{"var":4,"lo":1,"hi":0},{"var":3,"lo":6,"hi":14}],"cache":[[{"var":1,"lo":0,"hi":1},3],[{"var":3,"lo":6,"hi":14},15],[{"var":2,"lo":0,"hi":1},4],[{"var":0,"lo":1,"hi":0},7],[{"var":0,"lo":3,"hi":11},12],[{"var":3,"lo":1,"hi":0},13],[{"var":4,"lo":1,"hi":0},14],[{"var":0,"lo":0,"hi":1},2],[{"var":3,"lo":0,"hi":1},5],[{"var":0,"lo":1,"hi":4},8],[{"var":4,"lo":0,"hi":1},6],[{"var":1,"lo":1,"hi":0},9],[{"var":2,"lo":1,"hi":0},10],[{"var":1,"lo":10,"hi":4},11]],"count_cache":{}},"ac":[4,2,7,15,12]}"#; let mut deserialized: Adf = serde_json::from_str(&result).unwrap(); assert_eq!(adf.ac, deserialized.ac); let grounded_import = deserialized.grounded(); @@ -558,6 +574,17 @@ mod test { println!("{}", printer.print_interpretation(&model)); } } + + #[test] + fn formulacounts() { + 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)).") + .unwrap(); + let adf = Adf::from_parser(&parser); + + assert_eq!(adf.formulacounts(false), adf.formulacounts(true)); + } + #[test] fn adf_default() { let _adf = Adf::default(); diff --git a/src/bin/adf_bdd.rs b/src/bin/adf_bdd.rs index 10f905b..09f7959 100644 --- a/src/bin/adf_bdd.rs +++ b/src/bin/adf_bdd.rs @@ -56,6 +56,9 @@ struct App { /// Export the adf-bdd state after parsing and BDD instantiation to the given filename #[structopt(long)] export: Option, + /// Set if the (counter-)models shall be computed and printed, possible values are 'nai' and 'mem' for naive and memoization repectively (only works in hybrid and naive mode) + #[structopt(long)] + counter: Option, } impl App { @@ -99,12 +102,33 @@ impl App { } else { BdAdf::from_parser_with_stm_rewrite(&parser) }; + + match self.counter.as_deref() { + Some("nai") => { + let naive_adf = adf.hybrid_step_opt(false); + for ac_counts in naive_adf.formulacounts(false) { + print!("{:?} ", ac_counts); + } + println!(); + } + Some("mem") => { + let naive_adf = adf.hybrid_step_opt(false); + for ac_counts in naive_adf.formulacounts(true) { + print!("{:?}", ac_counts); + } + println!(); + } + Some(_) => {} + None => {} + } + log::info!("[Start] translate into naive representation"); + let mut naive_adf = adf.hybrid_step(); + log::info!("[Done] translate into naive representation"); if self.grounded { - let grounded = adf.hybrid_step_opt(false).grounded(); - print!("{}", adf.print_interpretation(&grounded)); + let grounded = naive_adf.grounded(); + print!("{}", naive_adf.print_interpretation(&grounded)); } - let mut naive_adf = adf.hybrid_step(); let printer = naive_adf.print_dictionary(); if self.complete { for model in naive_adf.complete() { @@ -131,6 +155,9 @@ impl App { } } "biodivine" => { + if self.counter.is_some() { + log::error!("Modelcounting not supported in biodivine mode"); + } let parser = adf_bdd::parser::AdfParser::default(); parser.parse()(&input).unwrap(); log::info!("[Done] parsing"); @@ -145,6 +172,7 @@ impl App { } else { BdAdf::from_parser_with_stm_rewrite(&parser) }; + if self.grounded { let grounded = adf.grounded(); print!("{}", adf.print_interpretation(&grounded)); @@ -170,7 +198,17 @@ impl App { } _ => { let mut adf = if self.import { - serde_json::from_str(&input).unwrap() + #[cfg(not(feature = "adhoccounting"))] + { + serde_json::from_str(&input).unwrap() + } + #[cfg(feature = "adhoccounting")] + { + let result: Adf = serde_json::from_str(&input).unwrap(); + log::debug!("test"); + result.fix_import(); + result + } } else { let parser = AdfParser::default(); parser.parse()(&input).unwrap(); @@ -201,6 +239,24 @@ impl App { }); } } + + match self.counter.as_deref() { + Some("nai") => { + for ac_counts in adf.formulacounts(false) { + print!("{:?} ", ac_counts); + } + println!(); + } + Some("mem") => { + for ac_counts in adf.formulacounts(true) { + print!("{:?}", ac_counts); + } + println!(); + } + Some(_) => {} + None => {} + } + if self.grounded { let grounded = adf.grounded(); print!("{}", adf.print_interpretation(&grounded)); diff --git a/src/datatypes/bdd.rs b/src/datatypes/bdd.rs index 2b91d1d..055d46c 100644 --- a/src/datatypes/bdd.rs +++ b/src/datatypes/bdd.rs @@ -172,6 +172,11 @@ impl BddNode { } } +/// Type alias for the pair of counter-models and models +pub type ModelCounts = (usize, usize); +/// Type alias for the Modelcounts and the depth of a given Node in a BDD +pub type CountNode = (ModelCounts, usize); + #[cfg(test)] mod test { use super::*; diff --git a/src/obdd.rs b/src/obdd.rs index f9ba161..99e2f06 100644 --- a/src/obdd.rs +++ b/src/obdd.rs @@ -2,13 +2,15 @@ pub mod vectorize; use crate::datatypes::*; use serde::{Deserialize, Serialize}; -use std::{cmp::min, collections::HashMap, fmt::Display}; +use std::{cell::RefCell, cmp::min, collections::HashMap, fmt::Display}; #[derive(Debug, Serialize, Deserialize)] pub(crate) struct Bdd { pub(crate) nodes: Vec, #[serde(with = "vectorize")] cache: HashMap, + #[serde(skip, default = "Bdd::default_count_cache")] + count_cache: RefCell>, } impl Display for Bdd { @@ -23,10 +25,35 @@ impl Display for Bdd { impl Bdd { pub fn new() -> Self { - Self { - nodes: vec![BddNode::bot_node(), BddNode::top_node()], - cache: HashMap::new(), + #[cfg(not(feature = "adhoccounting"))] + { + Self { + nodes: vec![BddNode::bot_node(), BddNode::top_node()], + cache: HashMap::new(), + count_cache: RefCell::new(HashMap::new()), + } } + #[cfg(feature = "adhoccounting")] + { + let result = Self { + nodes: vec![BddNode::bot_node(), BddNode::top_node()], + cache: HashMap::new(), + count_cache: RefCell::new(HashMap::new()), + }; + result + .count_cache + .borrow_mut() + .insert(Term::TOP, ((0, 1), 0)); + result + .count_cache + .borrow_mut() + .insert(Term::BOT, ((1, 0), 0)); + result + } + } + + fn default_count_cache() -> RefCell> { + RefCell::new(HashMap::new()) } pub fn variable(&mut self, var: Var) -> Term { @@ -126,11 +153,123 @@ impl Bdd { let new_term = Term(self.nodes.len()); self.nodes.push(node); self.cache.insert(node, new_term); + #[cfg(feature = "adhoccounting")] + { + log::debug!("newterm: {} as {:?}", new_term, node); + let mut count_cache = self.count_cache.borrow_mut(); + let ((lo_cmodel, lo_model), lodepth) = + *count_cache.get(&lo).expect("Cache corrupted"); + let ((hi_cmodel, hi_model), hidepth) = + *count_cache.get(&hi).expect("Cache corrupted"); + log::debug!("lo (cm: {}, mo: {}, dp: {})", lo_cmodel, lo_model, lodepth); + log::debug!("hi (cm: {}, mo: {}, dp: {})", hi_cmodel, hi_model, hidepth); + let (lo_exp, hi_exp) = if lodepth > hidepth { + (1, 2usize.pow((lodepth - hidepth) as u32)) + } else { + (2usize.pow((hidepth - lodepth) as u32), 1) + }; + log::debug!("lo_exp {}, hi_exp {}", lo_exp, hi_exp); + count_cache.insert( + new_term, + ( + ( + lo_cmodel * lo_exp + hi_cmodel * hi_exp, + lo_model * lo_exp + hi_model * hi_exp, + ), + std::cmp::max(lodepth, hidepth) + 1, + ), + ); + } new_term } } } } + + /// Computes the number of counter-models and models for a given BDD-tree + pub fn models(&self, term: Term, _memoization: bool) -> ModelCounts { + #[cfg(feature = "adhoccounting")] + { + return self.count_cache.borrow().get(&term).unwrap().0; + } + #[cfg(not(feature = "adhoccounting"))] + if _memoization { + self.modelcount_memoization(term).0 + } else { + self.modelcount_naive(term).0 + } + } + + #[allow(dead_code)] // dead code due to more efficient ad-hoc building, still used for a couple of tests + /// Computes the number of counter-models, models, and variables for a given BDD-tree + fn modelcount_naive(&self, term: Term) -> CountNode { + if term == Term::TOP { + ((0, 1), 0) + } else if term == Term::BOT { + ((1, 0), 0) + } else { + let node = &self.nodes[term.0]; + let mut lo_exp = 0u32; + let mut hi_exp = 0u32; + let ((lo_counter, lo_model), lodepth) = self.modelcount_naive(node.lo()); + let ((hi_counter, hi_model), hidepth) = self.modelcount_naive(node.hi()); + if lodepth > hidepth { + hi_exp = (lodepth - hidepth) as u32; + } else { + lo_exp = (hidepth - lodepth) as u32; + } + ( + ( + lo_counter * 2usize.pow(lo_exp) + hi_counter * 2usize.pow(hi_exp), + lo_model * 2usize.pow(lo_exp) + hi_model * 2usize.pow(hi_exp), + ), + std::cmp::max(lodepth, hidepth) + 1, + ) + } + } + + fn modelcount_memoization(&self, term: Term) -> CountNode { + if term == Term::TOP { + ((0, 1), 0) + } else if term == Term::BOT { + ((1, 0), 0) + } else { + if let Some(result) = self.count_cache.borrow().get(&term) { + return *result; + } + let result = { + let node = &self.nodes[term.0]; + let mut lo_exp = 0u32; + let mut hi_exp = 0u32; + let ((lo_counter, lo_model), lodepth) = self.modelcount_memoization(node.lo()); + let ((hi_counter, hi_model), hidepth) = self.modelcount_memoization(node.hi()); + if lodepth > hidepth { + hi_exp = (lodepth - hidepth) as u32; + } else { + lo_exp = (hidepth - lodepth) as u32; + } + ( + ( + lo_counter * 2usize.pow(lo_exp) + hi_counter * 2usize.pow(hi_exp), + lo_model * 2usize.pow(lo_exp) + hi_model * 2usize.pow(hi_exp), + ), + std::cmp::max(lodepth, hidepth) + 1, + ) + }; + self.count_cache.borrow_mut().insert(term, result); + result + } + } + + #[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)); + } + } } #[cfg(test)] @@ -242,4 +381,76 @@ mod test { assert_eq!(format!("{}", bdd), " \n0 BddNode: Var(18446744073709551614), lo: Term(0), hi: Term(0)\n1 BddNode: Var(18446744073709551615), lo: Term(1), hi: Term(1)\n2 BddNode: Var(0), lo: Term(0), hi: Term(1)\n3 BddNode: Var(1), lo: Term(0), hi: Term(1)\n4 BddNode: Var(2), lo: Term(0), hi: Term(1)\n5 BddNode: Var(0), lo: Term(0), hi: Term(3)\n6 BddNode: Var(1), lo: Term(4), hi: Term(1)\n7 BddNode: Var(0), lo: Term(4), hi: Term(6)\n"); } + + #[test] + fn counting() { + 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); + + assert_eq!(bdd.models(v1, false), (1, 1)); + let mut x = bdd.count_cache.get_mut().iter().collect::>(); + x.sort(); + log::debug!("{:?}", formula1); + for x in bdd.nodes.iter().enumerate() { + log::debug!("{:?}", x); + } + log::debug!("{:?}", x); + assert_eq!(bdd.models(formula1, false), (3, 1)); + assert_eq!(bdd.models(formula2, false), (1, 3)); + assert_eq!(bdd.models(formula3, false), (2, 2)); + assert_eq!(bdd.models(formula4, false), (5, 3)); + assert_eq!(bdd.models(Term::TOP, false), (0, 1)); + assert_eq!(bdd.models(Term::BOT, false), (1, 0)); + + assert_eq!(bdd.models(v1, true), (1, 1)); + assert_eq!(bdd.models(formula1, true), (3, 1)); + assert_eq!(bdd.models(formula2, true), (1, 3)); + assert_eq!(bdd.models(formula3, true), (2, 2)); + assert_eq!(bdd.models(formula4, true), (5, 3)); + assert_eq!(bdd.models(Term::TOP, true), (0, 1)); + assert_eq!(bdd.models(Term::BOT, true), (1, 0)); + + assert_eq!(bdd.modelcount_naive(v1), ((1, 1), 1)); + assert_eq!(bdd.modelcount_naive(formula1), ((3, 1), 2)); + assert_eq!(bdd.modelcount_naive(formula2), ((1, 3), 2)); + assert_eq!(bdd.modelcount_naive(formula3), ((2, 2), 2)); + assert_eq!(bdd.modelcount_naive(formula4), ((5, 3), 3)); + assert_eq!(bdd.modelcount_naive(Term::TOP), ((0, 1), 0)); + assert_eq!(bdd.modelcount_naive(Term::BOT), ((1, 0), 0)); + + assert_eq!( + bdd.modelcount_naive(formula4), + bdd.modelcount_memoization(formula4) + ); + + assert_eq!(bdd.modelcount_naive(v1), bdd.modelcount_memoization(v1)); + assert_eq!( + bdd.modelcount_naive(formula1), + bdd.modelcount_memoization(formula1) + ); + assert_eq!( + bdd.modelcount_naive(formula2), + bdd.modelcount_memoization(formula2) + ); + assert_eq!( + bdd.modelcount_naive(formula3), + bdd.modelcount_memoization(formula3) + ); + assert_eq!( + bdd.modelcount_naive(Term::TOP), + bdd.modelcount_memoization(Term::TOP) + ); + assert_eq!( + bdd.modelcount_naive(Term::BOT), + bdd.modelcount_memoization(Term::BOT) + ); + } }