pub mod vectorize;
use crate::datatypes::*;
use serde::{Deserialize, Serialize};
use std::collections::HashSet;
use std::{cell::RefCell, cmp::min, collections::HashMap, fmt::Display};
#[derive(Debug, Serialize, Deserialize)]
pub 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")]
count_cache: RefCell<HashMap<Term, CountNode>>,
}
impl Display for Bdd {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
writeln!(f, " ")?;
for (idx, elem) in self.nodes.iter().enumerate() {
writeln!(f, "{} {}", idx, *elem)?;
}
Ok(())
}
}
impl Default for Bdd {
fn default() -> Self {
Self::new()
}
}
impl Bdd {
pub fn new() -> Self {
#[cfg(not(feature = "adhoccounting"))]
{
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()),
}
}
#[cfg(feature = "adhoccounting")]
{
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()),
};
result
.count_cache
.borrow_mut()
.insert(Term::TOP, (ModelCounts::top(), ModelCounts::top(), 0));
result
.count_cache
.borrow_mut()
.insert(Term::BOT, (ModelCounts::bot(), ModelCounts::bot(), 0));
result
}
}
fn default_count_cache() -> RefCell<HashMap<Term, CountNode>> {
RefCell::new(HashMap::new())
}
pub fn variable(&mut self, var: Var) -> Term {
self.node(var, Term::BOT, Term::TOP)
}
pub fn constant(val: bool) -> Term {
if val {
Term::TOP
} else {
Term::BOT
}
}
pub fn not(&mut self, term: Term) -> Term {
self.if_then_else(term, Term::BOT, Term::TOP)
}
pub fn and(&mut self, term_a: Term, term_b: Term) -> Term {
self.if_then_else(term_a, term_b, Term::BOT)
}
pub fn or(&mut self, term_a: Term, term_b: Term) -> Term {
self.if_then_else(term_a, Term::TOP, term_b)
}
pub fn imp(&mut self, term_a: Term, term_b: Term) -> Term {
self.if_then_else(term_a, term_b, Term::TOP)
}
pub fn iff(&mut self, term_a: Term, term_b: Term) -> Term {
let not_b = self.not(term_b);
self.if_then_else(term_a, term_b, not_b)
}
pub fn xor(&mut self, term_a: Term, term_b: Term) -> Term {
let not_b = self.not(term_b);
self.if_then_else(term_a, not_b, term_b)
}
pub fn interpretations(
&self,
tree: Term,
goal: bool,
goal_var: Var,
negative: &[Var],
positive: &[Var],
) -> Vec<(Vec<Var>, Vec<Var>)> {
let mut result = Vec::new();
let node = self.nodes[tree.value()];
let var = node.var();
if tree.is_truth_value() {
return Vec::new();
}
if (goal_var != var) || goal {
if node.hi().is_truth_value() {
if node.hi().is_true() == goal {
result.push((negative.to_vec(), [positive, &[var]].concat()));
}
} else {
result.append(&mut self.interpretations(
node.hi(),
goal,
goal_var,
negative,
&[positive, &[var]].concat(),
));
}
}
if (goal_var != var) || !goal {
if node.lo().is_truth_value() {
if node.lo().is_true() == goal {
result.push(([negative, &[var]].concat(), positive.to_vec()));
}
} else {
result.append(&mut self.interpretations(
node.lo(),
goal,
goal_var,
&[negative, &[var]].concat(),
positive,
));
}
}
result
}
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)]
if node.var() > var || node.var() >= Var::BOT {
tree
} else if node.var() < var {
let lonode = self.restrict(node.lo(), var, val);
let hinode = self.restrict(node.hi(), var, val);
self.node(node.var(), lonode, hinode)
} else {
if val {
self.restrict(node.hi(), var, val)
} else {
self.restrict(node.lo(), var, val)
}
}
}
fn if_then_else(&mut self, i: Term, t: Term, e: Term) -> Term {
if i == Term::TOP {
t
} else if i == Term::BOT {
e
} else if t == e {
t
} else if t == Term::TOP && e == Term::BOT {
i
} else {
let minvar = Var(min(
self.nodes[i.value()].var().value(),
min(
self.nodes[t.value()].var().value(),
self.nodes[e.value()].var().value(),
),
));
let itop = self.restrict(i, minvar, true);
let ttop = self.restrict(t, minvar, true);
let etop = self.restrict(e, minvar, true);
let ibot = self.restrict(i, minvar, false);
let tbot = self.restrict(t, minvar, false);
let ebot = self.restrict(e, minvar, false);
let top_ite = self.if_then_else(itop, ttop, etop);
let bot_ite = self.if_then_else(ibot, tbot, ebot);
self.node(minvar, bot_ite, top_ite)
}
}
pub fn node(&mut self, var: Var, lo: Term, hi: Term) -> Term {
if lo == hi {
lo
} else {
let node = BddNode::new(var, lo, hi);
match self.cache.get(&node) {
Some(t) => *t,
None => {
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);
}
log::debug!("newterm: {} as {:?}", new_term, node);
#[cfg(feature = "adhoccounting")]
{
let mut count_cache = self.count_cache.borrow_mut();
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: {}, p-: {}, p+: {}, dp: {})",
lo_counts.cmodels,
lo_counts.models,
lo_paths.cmodels,
lo_paths.models,
lodepth
);
log::debug!(
"hi (cm: {}, mo: {}, p-: {}, p+: {}, dp: {})",
hi_counts.cmodels,
hi_counts.models,
hi_paths.cmodels,
hi_paths.models,
hidepth
);
#[cfg(feature = "adhoccountmodels")]
let (lo_exp, hi_exp) = if lodepth > hidepth {
(1, 2usize.pow((lodepth - hidepth) as u32))
} else {
(2usize.pow((hidepth - lodepth) as u32), 1)
};
#[cfg(not(feature = "adhoccountmodels"))]
let (lo_exp, hi_exp) = (0, 0);
log::debug!("lo_exp {}, hi_exp {}", lo_exp, hi_exp);
count_cache.insert(
new_term,
(
(
lo_counts.cmodels * lo_exp + hi_counts.cmodels * hi_exp,
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,
),
);
}
new_term
}
}
}
}
pub fn models(&self, term: Term, _memoization: bool) -> ModelCounts {
#[cfg(feature = "adhoccountmodels")]
{
return self.count_cache.borrow().get(&term).expect("The term should be originating from this bdd, otherwise the result would be inconsistent anyways").0;
}
#[cfg(not(feature = "adhoccountmodels"))]
if _memoization {
self.modelcount_memoization(term).0
} else {
self.modelcount_naive(term).0
}
}
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
}
}
#[allow(dead_code)] 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, _pc, depth)) => *depth,
None => {
if term.is_truth_value() {
0
} else {
self.max_depth(self.nodes[term.0].hi())
.max(self.max_depth(self.nodes[term.0].lo()))
}
}
}
}
#[allow(dead_code)] fn modelcount_naive(&self, term: Term) -> CountNode {
if term == Term::TOP {
(ModelCounts::top(), ModelCounts::top(), 0)
} else if term == Term::BOT {
(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, 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 {
lo_exp = (hidepth - lodepth) as u32;
}
(
(
lo_counts.cmodels * 2usize.pow(lo_exp) + hi_counts.cmodels * 2usize.pow(hi_exp),
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,
)
}
}
fn modelcount_memoization(&self, term: Term) -> CountNode {
if term == Term::TOP {
(ModelCounts::top(), ModelCounts::top(), 0)
} else if term == Term::BOT {
(ModelCounts::bot(), ModelCounts::bot(), 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_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 {
lo_exp = (hidepth - lodepth) as u32;
}
(
(
lo_counts.cmodels * 2usize.pow(lo_exp)
+ hi_counts.cmodels * 2usize.pow(hi_exp),
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,
)
};
self.count_cache.borrow_mut().insert(term, result);
result
}
}
pub fn fix_import(&mut self) {
self.generate_var_dependencies();
#[cfg(feature = "adhoccounting")]
{
self.count_cache
.borrow_mut()
.insert(Term::TOP, (ModelCounts::top(), ModelCounts::top(), 0));
self.count_cache
.borrow_mut()
.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));
}
}
}
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);
}
});
}
pub fn var_dependencies(&self, tree: Term) -> HashSet<Var> {
#[cfg(feature = "variablelist")]
{
self.var_deps[tree.value()].clone()
}
#[cfg(not(feature = "variablelist"))]
{
let node = self.nodes[tree.value()];
if node.var().is_constant() {
return HashSet::new();
}
let mut var_set = self
.var_dependencies(node.lo())
.union(&self.var_dependencies(node.hi()))
.copied()
.collect::<HashSet<Var>>();
var_set.insert(node.var());
var_set
}
}
pub fn passive_var_impact(&self, var: Var, termlist: &[Term]) -> usize {
termlist.iter().fold(0usize, |acc, val| {
if self.var_dependencies(*val).contains(&var) {
acc + 1
} else {
acc
}
})
}
pub fn active_var_impact(&self, var: Var, termlist: &[Term]) -> usize {
(0..termlist.len()).into_iter().fold(0usize, |acc, idx| {
if self
.var_dependencies(termlist[var.value()])
.contains(&Var(idx))
{
acc + 1
} else {
acc
}
})
}
}
#[cfg(test)]
mod test {
use super::*;
#[test]
fn newbdd() {
let bdd = Bdd::new();
assert_eq!(bdd.nodes.len(), 2);
}
#[test]
fn addconst() {
let bdd = Bdd::new();
assert_eq!(Bdd::constant(true), Term::TOP);
assert_eq!(Bdd::constant(false), Term::BOT);
assert_eq!(bdd.nodes.len(), 2);
}
#[test]
fn addvar() {
let mut bdd = Bdd::new();
assert_eq!(bdd.variable(Var(0)), Term(2));
assert_eq!(bdd.variable(Var(1)), Term(3));
assert_eq!(Var(1), Var(1));
bdd.variable(Var(0));
assert_eq!(bdd.variable(Var(0)), Term(2));
}
#[test]
fn use_negation() {
let mut bdd = Bdd::new();
let v1 = bdd.variable(Var(0));
assert_eq!(v1, 2.into());
assert_eq!(bdd.not(v1), Term(3));
}
#[test]
fn use_add() {
let mut bdd = Bdd::new();
let v1 = bdd.variable(Var(0));
let v2 = bdd.variable(Var(1));
let v3 = bdd.variable(Var(2));
let a1 = bdd.and(v1, v2);
let a2 = bdd.and(a1, v3);
assert_eq!(a2, Term(7));
}
#[test]
fn use_or() {
let mut bdd = Bdd::new();
let v1 = bdd.variable(Var(0));
let v2 = bdd.variable(Var(1));
let v3 = bdd.variable(Var(2));
let a1 = bdd.and(v1, v2);
let a2 = bdd.or(a1, v3);
assert_eq!(a2, Term(7));
}
#[test]
fn produce_different_conversions() {
let mut bdd = Bdd::new();
let v1 = bdd.variable(Var(0));
let v2 = bdd.variable(Var(1));
assert_eq!(v1, Term(2));
assert_eq!(v2, Term(3));
let t1 = bdd.and(v1, v2);
let nt1 = bdd.not(t1);
let ft = bdd.or(v1, nt1);
assert_eq!(ft, Term::TOP);
let v3 = bdd.variable(Var(2));
let nv3 = bdd.not(v3);
assert_eq!(bdd.and(v3, nv3), Term::BOT);
let conj = bdd.and(v1, v2);
assert_eq!(bdd.restrict(conj, Var(0), false), Term::BOT);
assert_eq!(bdd.restrict(conj, Var(0), true), v2);
let a = bdd.and(v3, v2);
let b = bdd.or(v2, v1);
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));
}
#[test]
fn display() {
let mut bdd = Bdd::new();
let v1 = bdd.variable(Var(0));
let v2 = bdd.variable(Var(1));
let v3 = bdd.variable(Var(2));
let a1 = bdd.and(v1, v2);
let _a2 = bdd.or(a1, v3);
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);
#[cfg(feature = "adhoccountmodels")]
assert_eq!(bdd.models(v1, false), (1, 1).into());
let mut x = bdd.count_cache.get_mut().iter().collect::<Vec<_>>();
x.sort();
log::debug!("{:?}", formula1);
for x in bdd.nodes.iter().enumerate() {
log::debug!("{:?}", x);
}
log::debug!("{:?}", x);
#[cfg(feature = "adhoccountmodels")]
{
assert_eq!(bdd.models(formula1, false), (3, 1).into());
assert_eq!(bdd.models(formula2, false), (1, 3).into());
assert_eq!(bdd.models(formula3, false), (2, 2).into());
assert_eq!(bdd.models(formula4, false), (5, 3).into());
assert_eq!(bdd.models(Term::TOP, false), (0, 1).into());
assert_eq!(bdd.models(Term::BOT, false), (1, 0).into());
assert_eq!(bdd.models(v1, true), (1, 1).into());
assert_eq!(bdd.models(formula1, true), (3, 1).into());
assert_eq!(bdd.models(formula2, true), (1, 3).into());
assert_eq!(bdd.models(formula3, true), (2, 2).into());
assert_eq!(bdd.models(formula4, true), (5, 3).into());
assert_eq!(bdd.models(Term::TOP, true), (0, 1).into());
assert_eq!(bdd.models(Term::BOT, true), (1, 0).into());
}
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)
);
#[cfg(feature = "adhoccountmodels")]
{
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)
);
}
assert_eq!(bdd.max_depth(Term::BOT), 0);
assert_eq!(bdd.max_depth(v1), 1);
assert_eq!(bdd.max_depth(formula3), 2);
assert_eq!(bdd.max_depth(formula4), 3);
}
#[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);
});
assert_eq!(
bdd.passive_var_impact(Var(0), &[formula1, formula2, formula3, formula4]),
4
);
assert_eq!(
bdd.passive_var_impact(Var(2), &[formula1, formula2, formula3, formula4]),
1
);
assert_eq!(
bdd.passive_var_impact(Var(2), &[formula1, formula2, formula3]),
0
);
}
#[test]
fn var_impact() {
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 ac: Vec<Term> = vec![formula1, formula2, v3];
assert_eq!(bdd.passive_var_impact(Var(0), &ac), 2);
assert_eq!(bdd.passive_var_impact(Var(1), &ac), 2);
assert_eq!(bdd.passive_var_impact(Var(2), &ac), 1);
assert_eq!(bdd.active_var_impact(Var(0), &ac), 2);
assert_eq!(bdd.active_var_impact(Var(2), &ac), 1);
}
#[test]
fn interpretations() {
let mut bdd = Bdd::new();
let v1 = bdd.variable(Var(0));
let v2 = bdd.variable(Var(1));
let formula1 = bdd.and(v1, v2);
let formula2 = bdd.xor(v1, v2);
assert_eq!(
bdd.interpretations(formula1, true, Var(2), &[], &[]),
vec![(vec![], vec![Var(0), Var(1)])]
);
assert_eq!(
bdd.interpretations(formula1, true, Var(0), &[], &[]),
vec![(vec![], vec![Var(0), Var(1)])]
);
assert_eq!(
bdd.interpretations(formula1, false, Var(2), &[], &[]),
vec![(vec![Var(1)], vec![Var(0)]), (vec![Var(0)], vec![])]
);
assert_eq!(
bdd.interpretations(formula1, false, Var(0), &[], &[]),
vec![(vec![Var(0)], vec![])]
);
assert_eq!(
bdd.interpretations(formula2, false, Var(2), &[], &[]),
vec![
(vec![], vec![Var(0), Var(1)]),
(vec![Var(0), Var(1)], vec![])
]
);
assert_eq!(
bdd.interpretations(formula2, true, Var(2), &[], &[]),
vec![(vec![Var(1)], vec![Var(0)]), (vec![Var(0)], vec![Var(1)])]
);
assert_eq!(
bdd.interpretations(formula2, true, Var(0), &[], &[]),
vec![(vec![Var(1)], vec![Var(0)])]
);
assert_eq!(
bdd.interpretations(Term::TOP, true, Var(0), &[], &[]),
vec![]
);
}
}