Struct biodivine_lib_bdd::BddValuation
source · pub struct BddValuation(/* private fields */);
Expand description
Exactly describes one assignment of boolean values to variables of a Bdd
.
It can be used as a witness of Bdd
non-emptiness, since one can evaluate every Bdd
in some corresponding valuation and get a true/false
result.
Implementations§
source§impl BddValuation
impl BddValuation
sourcepub fn new(values: Vec<bool>) -> BddValuation
pub fn new(values: Vec<bool>) -> BddValuation
Create a new valuation from a vector of variables.
sourcepub fn all_false(num_vars: u16) -> BddValuation
pub fn all_false(num_vars: u16) -> BddValuation
Create a valuation with all variables set to false.
sourcepub fn all_true(num_vars: u16) -> BddValuation
pub fn all_true(num_vars: u16) -> BddValuation
Create a valuation with all variables set to true.
sourcepub fn flip_value(&mut self, variable: BddVariable)
pub fn flip_value(&mut self, variable: BddVariable)
Flip the value of a given Bdd variable.
sourcepub fn clear(&mut self, variable: BddVariable)
pub fn clear(&mut self, variable: BddVariable)
Set the value of the given variable
to false
.
sourcepub fn set(&mut self, variable: BddVariable)
pub fn set(&mut self, variable: BddVariable)
Set the value of the given variable
to true
.
sourcepub fn set_value(&mut self, variable: BddVariable, value: bool)
pub fn set_value(&mut self, variable: BddVariable, value: bool)
Update value
of the given variable
.
sourcepub fn to_values(&self) -> Vec<(BddVariable, bool)>
pub fn to_values(&self) -> Vec<(BddVariable, bool)>
Convert BddValuation to a vector of tagged values in the way that is compatible with BddPartialValuation representation.
sourcepub fn value(&self, variable: BddVariable) -> bool
pub fn value(&self, variable: BddVariable) -> bool
Get a value of a specific BDD variable in this valuation.
sourcepub fn num_vars(&self) -> u16
pub fn num_vars(&self) -> u16
Number of variables in this valuation (used mostly for consistency checks).
sourcepub fn extends(&self, valuation: &BddPartialValuation) -> bool
pub fn extends(&self, valuation: &BddPartialValuation) -> bool
Returns true if the values set in this valuation match the values fixed in the given partial valuation. I.e. the two valuations agree on fixed values.
In other words this >= valuation
in terms of specificity.
Trait Implementations§
source§impl Clone for BddValuation
impl Clone for BddValuation
source§fn clone(&self) -> BddValuation
fn clone(&self) -> BddValuation
1.0.0 · source§fn clone_from(&mut self, source: &Self)
fn clone_from(&mut self, source: &Self)
source
. Read moresource§impl Debug for BddValuation
impl Debug for BddValuation
source§impl Display for BddValuation
impl Display for BddValuation
source§impl From<BddValuation> for Bdd
impl From<BddValuation> for Bdd
Convert a BddValuation to a Bdd with, well, exactly that one valuation.
source§fn from(valuation: BddValuation) -> Self
fn from(valuation: BddValuation) -> Self
source§impl From<BddValuation> for BddPartialValuation
impl From<BddValuation> for BddPartialValuation
source§fn from(value: BddValuation) -> Self
fn from(value: BddValuation) -> Self
source§impl Hash for BddValuation
impl Hash for BddValuation
source§impl Index<BddVariable> for BddValuation
impl Index<BddVariable> for BddValuation
Allow indexing of BddValuation
using BddVariables
.
source§impl IndexMut<BddVariable> for BddValuation
impl IndexMut<BddVariable> for BddValuation
source§impl Ord for BddValuation
impl Ord for BddValuation
source§fn cmp(&self, other: &BddValuation) -> Ordering
fn cmp(&self, other: &BddValuation) -> Ordering
1.21.0 · source§fn max(self, other: Self) -> Selfwhere
Self: Sized,
fn max(self, other: Self) -> Selfwhere
Self: Sized,
source§impl PartialEq for BddValuation
impl PartialEq for BddValuation
source§fn eq(&self, other: &BddValuation) -> bool
fn eq(&self, other: &BddValuation) -> bool
self
and other
values to be equal, and is used
by ==
.source§impl PartialOrd for BddValuation
impl PartialOrd for BddValuation
source§fn partial_cmp(&self, other: &BddValuation) -> Option<Ordering>
fn partial_cmp(&self, other: &BddValuation) -> Option<Ordering>
1.0.0 · source§fn le(&self, other: &Rhs) -> bool
fn le(&self, other: &Rhs) -> bool
self
and other
) and is used by the <=
operator. Read moresource§impl TryFrom<BddPartialValuation> for BddValuation
impl TryFrom<BddPartialValuation> for BddValuation
If possible, convert the given partial valuation to valuation with the same number of variables. Partial valuation must contain values of all variables.