diff --git a/lib/src/adf.rs b/lib/src/adf.rs index 19c445d..b0e8487 100644 --- a/lib/src/adf.rs +++ b/lib/src/adf.rs @@ -11,7 +11,7 @@ use crate::{ PrintDictionary, PrintableInterpretation, ThreeValuedInterpretationsIterator, TwoValuedInterpretationsIterator, VarContainer, }, - ModelCounts, Term, Var, + FacetCounts, ModelCounts, Term, Var, }, obdd::Bdd, parser::{AdfParser, Formula}, @@ -398,12 +398,37 @@ impl Adf { pub fn fix_import(&mut self) { self.bdd.fix_import(); } + + /// Counts facets of respective [Terms][crate::datatypes::Term] + /// and returns [Vector][std::vec::Vec] containing respective + /// facet counts. + pub fn facet_count(&self, interpretation: &[Term]) -> Vec<(ModelCounts, FacetCounts)> { + interpretation + .iter() + .map(|t| { + let mcs = self.bdd.models(*t, true); + + let n_vdps = { |t| self.bdd.var_dependencies(t).len() }; + + let fc = match mcs.1 > 2 { + true => 2 * n_vdps(*t), + _ => 0, + }; + let cfc = match mcs.0 > 2 { + true => 2 * n_vdps(*t), + _ => 0, + }; + (mcs, (cfc, fc)) + }) + .collect::>() + } } #[cfg(test)] mod test { use super::*; use test_log::test; + #[test] fn from_parser() { let parser = AdfParser::default(); @@ -588,4 +613,42 @@ mod test { fn adf_default() { let _adf = Adf::default(); } + + #[cfg(feature = "variablelist")] + #[test] + fn facet_counts() { + 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 mut adf = Adf::from_parser(&parser); + + let mut v = adf.ac.clone(); + let mut fcs = adf.facet_count(&v); + assert_eq!( + fcs.iter().map(|t| t.1).collect::>(), + vec![(0, 0), (0, 0), (4, 0), (0, 0)] + ); + + v[0] = Term::TOP; + // make navigation step for each bdd in adf-bdd-represenation + v = v + .iter() + .map(|t| { + v.iter() + .enumerate() + .fold(*t, |acc, (var, term)| match term.is_truth_value() { + true => adf.bdd.restrict(acc, Var(var), term.is_true()), + _ => acc, + }) + }) + .collect::>(); + fcs = adf.facet_count(&v); + + assert_eq!( + fcs.iter().map(|t| t.1).collect::>(), + vec![(0, 0), (0, 0), (0, 0), (0, 0)] + ); + } } diff --git a/lib/src/datatypes/bdd.rs b/lib/src/datatypes/bdd.rs index 055d46c..c313008 100644 --- a/lib/src/datatypes/bdd.rs +++ b/lib/src/datatypes/bdd.rs @@ -176,6 +176,8 @@ impl BddNode { 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); +/// Type alias for Facet counts, which contains number of facets and counter facets. +pub type FacetCounts = (usize, usize); #[cfg(test)] mod test { diff --git a/lib/src/obdd.rs b/lib/src/obdd.rs index 1df1969..008920a 100644 --- a/lib/src/obdd.rs +++ b/lib/src/obdd.rs @@ -2,7 +2,6 @@ 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}; @@ -211,6 +210,8 @@ impl Bdd { } /// 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 { #[cfg(feature = "adhoccounting")] { @@ -314,6 +315,19 @@ impl Bdd { } }); } + + pub fn var_dependencies(&self, tree: Term) -> HashSet { + #[cfg(feature = "variablelist")] + { + self.var_deps[tree.value()].clone() + } + #[cfg(not(feature = "variablelist"))] + { + let _ = tree; + HashSet::new() + } + // TODO! + } } #[cfg(test)]