use super::{Bdd, BddValuation, BddVariable};
use crate::{BddNode, BddPartialValuation, BddPointer, ValuationsOfClauseIterator};
use std::convert::TryFrom;
use std::fmt::{Display, Error, Formatter};
use std::ops::{Index, IndexMut};
impl BddValuation {
pub fn new(values: Vec<bool>) -> BddValuation {
BddValuation(values)
}
pub fn all_false(num_vars: u16) -> BddValuation {
BddValuation(vec![false; num_vars as usize])
}
pub fn all_true(num_vars: u16) -> BddValuation {
BddValuation(vec![true; num_vars as usize])
}
pub fn flip_value(&mut self, variable: BddVariable) {
let i = variable.0 as usize;
self.0[i] = !self.0[i];
}
pub fn clear(&mut self, variable: BddVariable) {
self.0[variable.0 as usize] = false;
}
pub fn set(&mut self, variable: BddVariable) {
self.0[variable.0 as usize] = true;
}
pub fn set_value(&mut self, variable: BddVariable, value: bool) {
self.0[variable.0 as usize] = value;
}
pub fn vector(self) -> Vec<bool> {
self.0
}
pub fn to_values(&self) -> Vec<(BddVariable, bool)> {
self.0
.iter()
.enumerate()
.map(|(i, v)| {
let Ok(i) = u16::try_from(i) else {
unreachable!("BddValuation is limited to u16::MAX values.")
};
(BddVariable(i), *v)
})
.collect::<Vec<_>>()
}
pub fn value(&self, variable: BddVariable) -> bool {
self.0[variable.0 as usize]
}
pub fn num_vars(&self) -> u16 {
self.0.len() as u16
}
pub fn extends(&self, valuation: &BddPartialValuation) -> bool {
for var_id in 0..self.num_vars() {
let var = BddVariable(var_id);
if let Some(value) = valuation.get_value(var) {
if value != self.value(var) {
return false;
}
}
}
true
}
pub(crate) fn next(&self, clause: &BddPartialValuation) -> Option<BddValuation> {
let mut result = self.clone();
let mut carry = true;
for var_id in 0..self.num_vars() {
let variable = BddVariable(var_id);
if clause.has_value(variable) {
assert_eq!(clause.get_value(variable), Some(self.value(variable)));
continue;
}
let new_value = self.value(variable) ^ carry;
let new_carry = self.value(variable) && carry;
result.set_value(variable, new_value);
carry = new_carry;
if !new_carry {
break;
} }
if carry {
None
} else {
Some(result)
}
}
}
impl Display for BddValuation {
fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
if self.0.is_empty() {
write!(f, "[]")?;
} else {
write!(f, "[{}", i32::from(self.0[0]))?;
for i in 1..self.0.len() {
write!(f, ",{}", i32::from(self.0[i]))?
}
write!(f, "]")?;
}
Ok(())
}
}
impl Index<BddVariable> for BddValuation {
type Output = bool;
fn index(&self, index: BddVariable) -> &Self::Output {
&self.0[usize::from(index.0)]
}
}
impl IndexMut<BddVariable> for BddValuation {
fn index_mut(&mut self, index: BddVariable) -> &mut Self::Output {
&mut self.0[usize::from(index.0)]
}
}
impl Bdd {
pub fn eval_in(&self, valuation: &BddValuation) -> bool {
debug_assert!(
valuation.num_vars() == self.num_vars(),
"Incompatible variable count."
);
let mut node = self.root_pointer();
while !node.is_terminal() {
let var = self.var_of(node);
node = if valuation[var] {
self.high_link_of(node)
} else {
self.low_link_of(node)
}
}
node.is_one()
}
}
impl From<BddValuation> for Bdd {
fn from(valuation: BddValuation) -> Self {
let mut bdd = Bdd::mk_true(valuation.num_vars());
for i_var in (0..valuation.num_vars()).rev() {
let var = BddVariable(i_var);
let is_true = valuation.value(var);
let low_link = if is_true {
BddPointer::zero()
} else {
bdd.root_pointer()
};
let high_link = if is_true {
bdd.root_pointer()
} else {
BddPointer::zero()
};
bdd.push_node(BddNode::mk_node(var, low_link, high_link));
}
bdd
}
}
impl TryFrom<BddPartialValuation> for BddValuation {
type Error = ();
fn try_from(value: BddPartialValuation) -> Result<Self, Self::Error> {
let mut result = BddValuation::all_false(value.0.len() as u16);
for var_id in 0..result.num_vars() {
let var = BddVariable(var_id);
if let Some(value) = value.get_value(var) {
result.set_value(var, value);
} else {
return Err(());
}
}
Ok(result)
}
}
#[allow(deprecated)]
impl super::BddValuationIterator {
pub fn new(num_vars: u16) -> super::BddValuationIterator {
super::BddValuationIterator(ValuationsOfClauseIterator::new_unconstrained(num_vars))
}
}
#[allow(deprecated)]
impl Iterator for super::BddValuationIterator {
type Item = BddValuation;
fn next(&mut self) -> Option<Self::Item> {
self.0.next()
}
}
#[cfg(test)]
mod tests {
use super::super::{BddValuation, BddVariableSet};
use crate::{bdd, Bdd, BddPartialValuation, BddVariable};
use num_bigint::BigInt;
#[test]
fn bdd_universe_eval() {
let universe = BddVariableSet::new_anonymous(2);
let v1 = universe.mk_var_by_name("x_0");
let v2 = universe.mk_var_by_name("x_1");
let bdd = bdd!(v1 & (!v2));
assert_eq!(true, bdd.eval_in(&BddValuation::new(vec![true, false])));
assert_eq!(false, bdd.eval_in(&BddValuation::new(vec![true, true])));
assert_eq!(false, bdd.eval_in(&BddValuation::new(vec![false, false])));
assert_eq!(false, bdd.eval_in(&BddValuation::new(vec![false, false])));
}
#[test]
#[should_panic]
#[cfg(debug_assertions)]
fn bdd_universe_eval_invalid() {
let universe = BddVariableSet::new_anonymous(2);
let tt = universe.mk_true();
tt.eval_in(&BddValuation::new(vec![true, true, true]));
}
#[test]
fn bdd_valuation_print() {
assert_eq!(
"[0,1,1,0]".to_string(),
BddValuation::new(vec![false, true, true, false]).to_string()
);
}
#[test]
fn valuation_consistency() {
let total = BddValuation::new(vec![true, false, true, false]);
let partial =
BddPartialValuation::from_values(&[(BddVariable(1), false), (BddVariable(2), true)]);
assert!(total.extends(&partial));
let total = BddValuation::new(vec![true, true, true, false]);
assert!(!total.extends(&partial));
}
#[test]
fn test_valuation_conversion() {
let valuation = BddValuation::new(vec![true, false, true, false]);
let bdd = Bdd::from(valuation);
assert!(bdd.is_valuation());
assert_eq!(bdd.exact_cardinality(), BigInt::from(1));
let variables = BddVariableSet::new_anonymous(4);
let bdd_2 = variables.eval_expression_string("x_0 & !x_1 & x_2 & !x_3");
assert!(bdd_2.iff(&bdd).is_true());
}
}