Struct biodivine_lib_bdd::BddValuation

pub struct BddValuation(_);

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

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.

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