Struct biodivine_lib_bdd::Bdd

pub struct Bdd(_);

An array-based encoding of the binary decision diagram implementing basic logical operations.

To create Bdds for atomic formulas, use a BddVariableSet.

Methods

impl Bdd

Basic boolean logical operations for Bdds: $\neg, \land, \lor, \Rightarrow, \Leftrightarrow, \oplus$.

pub fn not(&self) -> Bdd

Create a Bdd corresponding to the $\neg \phi$ formula, where $\phi$ is this Bdd.

pub fn and(&self, right: &Bdd) -> Bdd

Create a Bdd corresponding to the $\phi \land \psi$ formula, where $\phi$ and $\psi$ are the two given Bdds.

pub fn or(&self, right: &Bdd) -> Bdd

Create a Bdd corresponding to the $\phi \lor \psi$ formula, where $\phi$ and $\psi$ are the two given Bdds.

pub fn imp(&self, right: &Bdd) -> Bdd

Create a Bdd corresponding to the $\phi \Rightarrow \psi$ formula, where $\phi$ and $\psi$ are the two given Bdds.

pub fn iff(&self, right: &Bdd) -> Bdd

Create a Bdd corresponding to the $\phi \Leftrightarrow \psi$ formula, where $\phi$ and $\psi$ are the two given Bdds.

pub fn xor(&self, right: &Bdd) -> Bdd

Create a Bdd corresponding to the $\phi \oplus \psi$ formula, where $\phi$ and $\psi$ are the two given Bdds.

pub fn and_not(&self, right: &Bdd) -> Bdd

Create a Bdd corresponding to the $\phi \land \neg \psi$ formula, where $\phi$ and $\psi$ are the two given Bdds.

impl Bdd

.dot export procedure for Bdds.

pub fn write_as_dot_string(
    &self,
    output: &mut dyn Write,
    variables: &BddVariableSet,
    zero_pruned: bool
) -> Result<(), Error>

Output this Bdd as a .dot string into the given output writer.

Variable names in the graph are resolved from the given BddVariableSet.

If zero_pruned is true, edges leading to zero are not shown. This can greatly simplify the graph without losing information.

pub fn to_dot_string(
    &self,
    variables: &BddVariableSet,
    zero_pruned: bool
) -> String

Convert this Bdd to a .dot string.

Variable names in the graph are resolved from the given BddVariableSet.

If zero_pruned is true, edges leading to zero are not shown. This can greatly simplify the graph without losing information.

impl Bdd

Serialisation and deserialisation methods for Bdds.

pub fn write_as_bytes(&self, output: &mut dyn Write) -> Result<(), Error>

Write this Bdd into the given output writer using a simple little-endian binary encoding.

pub fn read_as_bytes(input: &mut dyn Read) -> Result<Bdd, Error>

Read a Bdd from a given input reader using a simple little-endian binary encoding.

pub fn to_string(&self) -> String

Convert this Bdd to a serialized string.

pub fn from_string(bdd: &str) -> Bdd

Read a Bdd from a serialized string.

pub fn to_bytes(&self) -> Vec<u8>

Convert this Bdd to a byte vector.

pub fn from_bytes(data: &mut &[u8]) -> Bdd

Read a Bdd from a byte vector.

impl Bdd

Several useful (mostly internal) low-level utility methods for Bdds.

pub fn size(&self) -> usize

The number of nodes in this Bdd. (Do not confuse with cardinality)

pub fn num_vars(&self) -> u16

Number of variables in the corresponding BddVariableSet.

pub fn is_true(&self) -> bool

True if this Bdd is exactly the true formula.

pub fn is_false(&self) -> bool

True if this Bdd is exactly the false formula.

pub fn cardinality(&self) -> f64

Approximately computes the number of valuations satisfying the formula given by this Bdd.

pub fn sat_witness(&self) -> Option<BddValuation>

If the Bdd is satisfiable, return some BddValuation that satisfies the Bdd.

pub fn to_boolean_expression(
    &self,
    variables: &BddVariableSet
) -> BooleanExpression

Convert this Bdd to a BooleanExpression (using the variable names from the given BddVariableSet).

impl Bdd

Methods for working with Bdd valuations.

pub fn eval_in(&self, valuation: &BddValuation) -> bool

Evaluate this Bdd in a specified BddValuation.

Panics if the number of variables in the valuation is different than the Bdd.

Trait Implementations

impl Clone for Bdd

fn clone(&self) -> Bdd

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for Bdd

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

Formats the value using the given formatter.

impl Eq for Bdd

impl Hash for Bdd

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 PartialEq<Bdd> for Bdd

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

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

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

This method tests for !=.

impl StructuralEq for Bdd

impl StructuralPartialEq for Bdd