mirror of
https://github.com/ellmau/adf-obdd.git
synced 2025-12-19 09:29:36 +01:00
Feature/issue 30 facet counting (#31)
Add facet_count functionality. Co-authored-by: Stefan Ellmauthaler <stefan.ellmauthaler@tu-dresden.de>
This commit is contained in:
parent
e4f67261b3
commit
7cf581cd9b
@ -11,7 +11,7 @@ use crate::{
|
|||||||
PrintDictionary, PrintableInterpretation, ThreeValuedInterpretationsIterator,
|
PrintDictionary, PrintableInterpretation, ThreeValuedInterpretationsIterator,
|
||||||
TwoValuedInterpretationsIterator, VarContainer,
|
TwoValuedInterpretationsIterator, VarContainer,
|
||||||
},
|
},
|
||||||
ModelCounts, Term, Var,
|
FacetCounts, ModelCounts, Term, Var,
|
||||||
},
|
},
|
||||||
obdd::Bdd,
|
obdd::Bdd,
|
||||||
parser::{AdfParser, Formula},
|
parser::{AdfParser, Formula},
|
||||||
@ -398,12 +398,37 @@ impl Adf {
|
|||||||
pub fn fix_import(&mut self) {
|
pub fn fix_import(&mut self) {
|
||||||
self.bdd.fix_import();
|
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::<Vec<_>>()
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
#[cfg(test)]
|
#[cfg(test)]
|
||||||
mod test {
|
mod test {
|
||||||
use super::*;
|
use super::*;
|
||||||
use test_log::test;
|
use test_log::test;
|
||||||
|
|
||||||
#[test]
|
#[test]
|
||||||
fn from_parser() {
|
fn from_parser() {
|
||||||
let parser = AdfParser::default();
|
let parser = AdfParser::default();
|
||||||
@ -588,4 +613,42 @@ mod test {
|
|||||||
fn adf_default() {
|
fn adf_default() {
|
||||||
let _adf = 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<_>>(),
|
||||||
|
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::<Vec<_>>();
|
||||||
|
fcs = adf.facet_count(&v);
|
||||||
|
|
||||||
|
assert_eq!(
|
||||||
|
fcs.iter().map(|t| t.1).collect::<Vec<_>>(),
|
||||||
|
vec![(0, 0), (0, 0), (0, 0), (0, 0)]
|
||||||
|
);
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|||||||
@ -176,6 +176,8 @@ impl BddNode {
|
|||||||
pub type ModelCounts = (usize, usize);
|
pub type ModelCounts = (usize, usize);
|
||||||
/// Type alias for the Modelcounts and the depth of a given Node in a BDD
|
/// Type alias for the Modelcounts and the depth of a given Node in a BDD
|
||||||
pub type CountNode = (ModelCounts, usize);
|
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)]
|
#[cfg(test)]
|
||||||
mod test {
|
mod test {
|
||||||
|
|||||||
@ -2,7 +2,6 @@
|
|||||||
pub mod vectorize;
|
pub mod vectorize;
|
||||||
use crate::datatypes::*;
|
use crate::datatypes::*;
|
||||||
use serde::{Deserialize, Serialize};
|
use serde::{Deserialize, Serialize};
|
||||||
#[cfg(feature = "HashSet")]
|
|
||||||
use std::collections::HashSet;
|
use std::collections::HashSet;
|
||||||
use std::{cell::RefCell, cmp::min, collections::HashMap, fmt::Display};
|
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
|
/// 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 {
|
pub fn models(&self, term: Term, _memoization: bool) -> ModelCounts {
|
||||||
#[cfg(feature = "adhoccounting")]
|
#[cfg(feature = "adhoccounting")]
|
||||||
{
|
{
|
||||||
@ -314,6 +315,19 @@ impl Bdd {
|
|||||||
}
|
}
|
||||||
});
|
});
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pub fn var_dependencies(&self, tree: Term) -> HashSet<Var> {
|
||||||
|
#[cfg(feature = "variablelist")]
|
||||||
|
{
|
||||||
|
self.var_deps[tree.value()].clone()
|
||||||
|
}
|
||||||
|
#[cfg(not(feature = "variablelist"))]
|
||||||
|
{
|
||||||
|
let _ = tree;
|
||||||
|
HashSet::new()
|
||||||
|
}
|
||||||
|
// TODO!
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
#[cfg(test)]
|
#[cfg(test)]
|
||||||
|
|||||||
Loading…
x
Reference in New Issue
Block a user