Struct biodivine_lib_bdd::Bdd

pub struct Bdd(Vec<BddNode>);

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.

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

Write this Bdd into the given output writer using a simple string format.

fn read_as_string(input: &mut dyn Read) -> Result<Bdd, String>

Read a Bdd from the given input reader, assuming a simple string format.

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).

pub(crate) fn root_pointer(&self) -> BddPointer

(internal) Pointer to the root of the decision diagram.

pub(crate) fn low_link_of(&self, node: BddPointer) -> BddPointer

(internal) Get the low link of the node at a specified location.

pub(crate) fn high_link_of(&self, node: BddPointer) -> BddPointer

(internal) Get the high link of the node at a specified location.

pub(crate) fn var_of(&self, node: BddPointer) -> BddVariable

(internal) Get the conditioning variable of the node at a specified location.

Panics: node must not be a terminal.

pub(crate) fn mk_false(num_vars: u16) -> Bdd

(internal) Create a new Bdd for the false formula.

pub(crate) fn mk_true(num_vars: u16) -> Bdd

(internal) Create a new Bdd for the true formula.

pub(crate) fn push_node(&mut self, node: BddNode)

(internal) Add a new node to an existing Bdd, making the new node the root of the Bdd.

pub(crate) fn pointers(&self) -> Map<Range<usize>, fn(_: usize) -> BddPointer>

(internal) Create an iterator over all pointers of the Bdd (including terminals!).

The iteration order is the same as the underlying representation, so you can expect terminals to be the first two nodes.

pub(crate) fn nodes(&self) -> Iter<BddNode>

(internal) Create an iterator over all nodes of the Bdd (including terminals).

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