From 904d0b107ef3223b3bf7ed88c84f951e63905835 Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Mon, 4 Apr 2022 10:34:47 +0200 Subject: [PATCH] Add path-counting functionality to the obdd --- lib/src/adf.rs | 2 +- lib/src/datatypes/bdd.rs | 6 +- lib/src/obdd.rs | 133 +++++++++++++++++++++++++++++++-------- 3 files changed, 111 insertions(+), 30 deletions(-) diff --git a/lib/src/adf.rs b/lib/src/adf.rs index 6853b11..5a72c67 100644 --- a/lib/src/adf.rs +++ b/lib/src/adf.rs @@ -7,7 +7,7 @@ This module describes the abstract dialectical framework use std::collections::HashSet; -use serde::{ser::SerializeMap, Deserialize, Serialize}; +use serde::{Deserialize, Serialize}; use crate::{ datatypes::{ diff --git a/lib/src/datatypes/bdd.rs b/lib/src/datatypes/bdd.rs index 6237239..8e59890 100644 --- a/lib/src/datatypes/bdd.rs +++ b/lib/src/datatypes/bdd.rs @@ -185,7 +185,7 @@ impl BddNode { } } -/// Type alias for the pair of counter-models and models +/// Represents the pair of counts, related to counter-models and models. #[derive(Debug, Clone, Copy, Eq, PartialEq, PartialOrd, Ord)] pub struct ModelCounts { /// Contains the number of counter-models @@ -225,8 +225,8 @@ impl From<(usize, usize)> for ModelCounts { } } } -/// Type alias for the Modelcounts and the depth of a given Node in a BDD -pub type CountNode = (ModelCounts, usize); +/// Type alias for the Modelcounts, Count of paths to bot resp top, and the depth of a given Node in a BDD +pub type CountNode = (ModelCounts, ModelCounts, usize); /// Type alias for Facet counts, which contains number of facets and counter facets. pub type FacetCounts = (usize, usize); diff --git a/lib/src/obdd.rs b/lib/src/obdd.rs index 3f4e718..45dccc8 100644 --- a/lib/src/obdd.rs +++ b/lib/src/obdd.rs @@ -51,11 +51,11 @@ impl Bdd { result .count_cache .borrow_mut() - .insert(Term::TOP, (ModelCounts::top(), 0)); + .insert(Term::TOP, (ModelCounts::top(), ModelCounts::top(), 0)); result .count_cache .borrow_mut() - .insert(Term::BOT, (ModelCounts::bot(), 0)); + .insert(Term::BOT, (ModelCounts::bot(), ModelCounts::bot(), 0)); result } } @@ -228,22 +228,28 @@ impl Bdd { var_set.insert(var); self.var_deps.push(var_set); } + log::debug!("newterm: {} as {:?}", new_term, node); #[cfg(feature = "adhoccounting")] { - log::debug!("newterm: {} as {:?}", new_term, node); let mut count_cache = self.count_cache.borrow_mut(); - let (lo_counts, lodepth) = *count_cache.get(&lo).expect("Cache corrupted"); - let (hi_counts, hidepth) = *count_cache.get(&hi).expect("Cache corrupted"); + let (lo_counts, lo_paths, lodepth) = + *count_cache.get(&lo).expect("Cache corrupted"); + let (hi_counts, hi_paths, hidepth) = + *count_cache.get(&hi).expect("Cache corrupted"); log::debug!( - "lo (cm: {}, mo: {}, dp: {})", + "lo (cm: {}, mo: {}, p-: {}, p+: {}, dp: {})", lo_counts.cmodels, lo_counts.models, + lo_paths.cmodels, + lo_paths.models, lodepth ); log::debug!( - "hi (cm: {}, mo: {}, dp: {})", + "hi (cm: {}, mo: {}, p-: {}, p+: {}, dp: {})", hi_counts.cmodels, hi_counts.models, + hi_paths.cmodels, + hi_paths.models, hidepth ); let (lo_exp, hi_exp) = if lodepth > hidepth { @@ -260,6 +266,11 @@ impl Bdd { lo_counts.models * lo_exp + hi_counts.models * hi_exp, ) .into(), + ( + lo_paths.cmodels + hi_paths.cmodels, + lo_paths.models + hi_paths.models, + ) + .into(), std::cmp::max(lodepth, hidepth) + 1, ), ); @@ -270,7 +281,7 @@ impl Bdd { } } - /// Computes the number of counter-models and models for a given BDD-tree + /// Computes the number of counter-models and models for a given BDD-tree. /// /// Use the flag `_memoization` to choose between using the memoization approach or not. (This flag does nothing if the feature `adhoccounting` is used) pub fn models(&self, term: Term, _memoization: bool) -> ModelCounts { @@ -286,12 +297,29 @@ impl Bdd { } } - pub fn max_depth(&self, term: Term) -> usize { + /// Computes the number of paths which lead to Bot respectively Top. + /// + /// Use the flag `_memoization` to choose between using the memoization approach or not. (This flag does nothing if the feature `adhoccounting` is used) + pub fn paths(&self, term: Term, _memoization: bool) -> ModelCounts { #[cfg(feature = "adhoccounting")] { return self.count_cache.borrow().get(&term).expect("The term should be originating from this bdd, otherwise the result would be inconsistent anyways").1; } #[cfg(not(feature = "adhoccounting"))] + if _memoization { + self.modelcount_memoization(term).1 + } else { + self.modelcount_naive(term).1 + } + } + + /// Computes the maximal depth of the given sub-tree. + pub fn max_depth(&self, term: Term) -> usize { + #[cfg(feature = "adhoccounting")] + { + return self.count_cache.borrow().get(&term).expect("The term should be originating from this bdd, otherwise the result would be inconsistent anyways").2; + } + #[cfg(not(feature = "adhoccounting"))] match self.count_cache.borrow().get(&term) { Some((mc, depth)) => *depth, None => { @@ -309,15 +337,15 @@ impl Bdd { /// 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 { - (ModelCounts::top(), 0) + (ModelCounts::top(), ModelCounts::top(), 0) } else if term == Term::BOT { - (ModelCounts::bot(), 0) + (ModelCounts::bot(), ModelCounts::bot(), 0) } else { let node = &self.nodes[term.0]; let mut lo_exp = 0u32; let mut hi_exp = 0u32; - let (lo_counts, lodepth) = self.modelcount_naive(node.lo()); - let (hi_counts, hidepth) = self.modelcount_naive(node.hi()); + let (lo_counts, lo_paths, lodepth) = self.modelcount_naive(node.lo()); + let (hi_counts, hi_paths, hidepth) = self.modelcount_naive(node.hi()); if lodepth > hidepth { hi_exp = (lodepth - hidepth) as u32; } else { @@ -329,6 +357,11 @@ impl Bdd { lo_counts.models * 2usize.pow(lo_exp) + hi_counts.models * 2usize.pow(hi_exp), ) .into(), + ( + lo_paths.cmodels + hi_paths.cmodels, + lo_paths.models + hi_paths.models, + ) + .into(), std::cmp::max(lodepth, hidepth) + 1, ) } @@ -336,9 +369,9 @@ impl Bdd { fn modelcount_memoization(&self, term: Term) -> CountNode { if term == Term::TOP { - (ModelCounts::top(), 0) + (ModelCounts::top(), ModelCounts::top(), 0) } else if term == Term::BOT { - (ModelCounts::bot(), 0) + (ModelCounts::bot(), ModelCounts::bot(), 0) } else { if let Some(result) = self.count_cache.borrow().get(&term) { return *result; @@ -347,8 +380,8 @@ impl Bdd { let node = &self.nodes[term.0]; let mut lo_exp = 0u32; let mut hi_exp = 0u32; - let (lo_counts, lodepth) = self.modelcount_memoization(node.lo()); - let (hi_counts, hidepth) = self.modelcount_memoization(node.hi()); + let (lo_counts, lo_paths, lodepth) = self.modelcount_memoization(node.lo()); + let (hi_counts, hi_paths, hidepth) = self.modelcount_memoization(node.hi()); if lodepth > hidepth { hi_exp = (lodepth - hidepth) as u32; } else { @@ -362,6 +395,11 @@ impl Bdd { + hi_counts.models * 2usize.pow(hi_exp), ) .into(), + ( + lo_paths.cmodels + hi_paths.cmodels, + lo_paths.models + hi_paths.models, + ) + .into(), std::cmp::max(lodepth, hidepth) + 1, ) }; @@ -377,10 +415,10 @@ impl Bdd { { self.count_cache .borrow_mut() - .insert(Term::TOP, (ModelCounts::top(), 0)); + .insert(Term::TOP, (ModelCounts::top(), ModelCounts::top(), 0)); self.count_cache .borrow_mut() - .insert(Term::BOT, (ModelCounts::bot(), 0)); + .insert(Term::BOT, (ModelCounts::bot(), ModelCounts::bot(), 0)); for i in 0..self.nodes.len() { log::debug!("fixing Term({})", i); self.modelcount_memoization(Term(i)); @@ -583,13 +621,46 @@ mod test { assert_eq!(bdd.models(Term::TOP, true), (0, 1).into()); assert_eq!(bdd.models(Term::BOT, true), (1, 0).into()); - assert_eq!(bdd.modelcount_naive(v1), ((1, 1).into(), 1)); - assert_eq!(bdd.modelcount_naive(formula1), ((3, 1).into(), 2)); - assert_eq!(bdd.modelcount_naive(formula2), ((1, 3).into(), 2)); - assert_eq!(bdd.modelcount_naive(formula3), ((2, 2).into(), 2)); - assert_eq!(bdd.modelcount_naive(formula4), ((5, 3).into(), 3)); - assert_eq!(bdd.modelcount_naive(Term::TOP), ((0, 1).into(), 0)); - assert_eq!(bdd.modelcount_naive(Term::BOT), ((1, 0).into(), 0)); + assert_eq!(bdd.paths(formula1, false), (2, 1).into()); + assert_eq!(bdd.paths(formula2, false), (1, 2).into()); + assert_eq!(bdd.paths(formula3, false), (2, 2).into()); + assert_eq!(bdd.paths(formula4, false), (3, 2).into()); + assert_eq!(bdd.paths(Term::TOP, false), (0, 1).into()); + assert_eq!(bdd.paths(Term::BOT, false), (1, 0).into()); + + assert_eq!(bdd.paths(v1, true), (1, 1).into()); + assert_eq!(bdd.paths(formula1, true), (2, 1).into()); + assert_eq!(bdd.paths(formula2, true), (1, 2).into()); + assert_eq!(bdd.paths(formula3, true), (2, 2).into()); + assert_eq!(bdd.paths(formula4, true), (3, 2).into()); + assert_eq!(bdd.paths(Term::TOP, true), (0, 1).into()); + assert_eq!(bdd.paths(Term::BOT, true), (1, 0).into()); + + assert_eq!(bdd.modelcount_naive(v1), ((1, 1).into(), (1, 1).into(), 1)); + assert_eq!( + bdd.modelcount_naive(formula1), + ((3, 1).into(), (2, 1).into(), 2) + ); + assert_eq!( + bdd.modelcount_naive(formula2), + ((1, 3).into(), (1, 2).into(), 2) + ); + assert_eq!( + bdd.modelcount_naive(formula3), + ((2, 2).into(), (2, 2).into(), 2) + ); + assert_eq!( + bdd.modelcount_naive(formula4), + ((5, 3).into(), (3, 2).into(), 3) + ); + assert_eq!( + bdd.modelcount_naive(Term::TOP), + ((0, 1).into(), (0, 1).into(), 0) + ); + assert_eq!( + bdd.modelcount_naive(Term::BOT), + ((1, 0).into(), (1, 0).into(), 0) + ); assert_eq!( bdd.modelcount_naive(formula4), @@ -651,6 +722,16 @@ mod test { .for_each(|(left, right)| { assert!(left == right); }); + + assert_eq!( + bdd.var_impact(Var(0), &[formula1, formula2, formula3, formula4]), + 4 + ); + assert_eq!( + bdd.var_impact(Var(2), &[formula1, formula2, formula3, formula4]), + 1 + ); + assert_eq!(bdd.var_impact(Var(2), &[formula1, formula2, formula3]), 0); } #[test]