Struct biodivine_lib_bdd::BddValuation

pub struct BddValuation(pub(crate) Vec<bool>);

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.

Tuple Fields

0: Vec<bool>

Implementations

impl BddValuation

pub fn new(values: Vec<bool>) -> BddValuation

Create a new valuation from a vector of variables.

pub fn all_false(num_vars: u16) -> BddValuation

Create a valuation with all variables set to false.

pub fn all_true(num_vars: u16) -> BddValuation

Create a valuation with all variables set to true.

pub fn flip_value(&mut self, variable: BddVariable)

Flip the value of a given Bdd variable.

pub fn clear(&mut self, variable: BddVariable)

Set the value of the given variable to false.

pub fn set(&mut self, variable: BddVariable)

Set the value of the given variable to true.

pub fn set_value(&mut self, variable: BddVariable, value: bool)

Update value of the given variable.

pub fn vector(self) -> Vec<bool>

Convert the valuation to its underlying vector.

pub fn value(&self, variable: BddVariable) -> bool

Get a value of a specific BDD variable in this valuation.

pub fn num_vars(&self) -> u16

Number of variables in this valuation (used mostly for consistency checks).

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.

pub(crate) fn next(&self, clause: &BddPartialValuation) -> Option<BddValuation>

(internal) “Increment” this valuation if possible. Interpret the valuation as bit-vector and perform a standard increment. This can be used to iterate over all valuations.

You can provide a clause which restricts which variables of the valuation can change. That is, any variable that has a fixed value in clause is considered to be fixed. Note that the method also checks whether the fixed values are the same as in the clause (i.e. the valuation and clause are mutually compatible) and panics if inconsistencies are found.

Trait Implementations

impl Clone for BddValuation

fn clone(&self) -> BddValuation

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for BddValuation

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Display for BddValuation

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl From<BddValuation> for Bdd

Convert a BddValuation to a Bdd with, well, exactly that one valuation.

fn from(valuation: BddValuation) -> Self

Performs the conversion.

impl Hash for BddValuation

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H) where
    H: Hasher, 

Feeds a slice of this type into the given Hasher.

impl Index<BddVariable> for BddValuation

Allow indexing of BddValuation using BddVariables.

type Output = bool

The returned type after indexing.

fn index(&self, index: BddVariable) -> &Self::Output

Performs the indexing (container[index]) operation.

impl Ord for BddValuation

fn cmp(&self, other: &BddValuation) -> Ordering

This method returns an Ordering between self and other.

fn max(self, other: Self) -> Self

Compares and returns the maximum of two values.

fn min(self, other: Self) -> Self

Compares and returns the minimum of two values.

fn clamp(self, min: Self, max: Self) -> Self

Restrict a value to a certain interval.

impl PartialEq<BddValuation> for BddValuation

fn eq(&self, other: &BddValuation) -> bool

This method tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &BddValuation) -> bool

This method tests for !=.

impl PartialOrd<BddValuation> for BddValuation

fn partial_cmp(&self, other: &BddValuation) -> Option<Ordering>

This method returns an ordering between self and other values if one exists.

fn lt(&self, other: &Rhs) -> bool

This method tests less than (for self and other) and is used by the < operator.

fn le(&self, other: &Rhs) -> bool

This method tests less than or equal to (for self and other) and is used by the <= operator.

fn gt(&self, other: &Rhs) -> bool

This method tests greater than (for self and other) and is used by the > operator.

fn ge(&self, other: &Rhs) -> bool

This method tests greater than or equal to (for self and other) and is used by the >= operator.

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.

type Error = ()

The type returned in the event of a conversion error.

fn try_from(value: BddPartialValuation) -> Result<Self, Self::Error>

Performs the conversion.

impl Eq for BddValuation

impl StructuralEq for BddValuation

impl StructuralPartialEq for BddValuation