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.

Implementations

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.

pub fn binary_op<T>(left: &Bdd, right: &Bdd, op_function: T) -> Bdd where
    T: Fn(Option<bool>, Option<bool>) -> Option<bool>, 

Apply a general binary operation to two given Bdd objects.

The op_function specifies the actual logical operation that will be performed. See crate::op_function module for examples.

In general, this function can be used to slightly speed up less common Boolean operations or to fuse together several operations (like negation and binary operation).

pub fn fused_binary_flip_op<T>(
    left: (&Bdd, Option<BddVariable>),
    right: (&Bdd, Option<BddVariable>),
    flip_output: Option<BddVariable>,
    op_function: T
) -> Bdd where
    T: Fn(Option<bool>, Option<bool>) -> Option<bool>, 

Apply a general binary operation together with up-to three Bdd variable flips. See also binary_op.

A flip exchanges the edges of all decision nodes with the specified variable x. As a result, the set of bitvectors represented by this Bdd has the value of x negated.

With this operation, you can apply such flip to both input operands as well as the output Bdd. This can greatly simplify implementation of state space generators for asynchronous systems.

impl Bdd

Advanced relation-like operations for Bdds.

pub fn var_project(&self, variable: BddVariable) -> Bdd

Eliminates one given variable from the Bdd.

If we see the Bdd as a set of bitvectors, this is essentially existential quantification: $\exists x_i : (x_1, ..., x_i, ..., x_n) \in BDD$.

pub fn project(&self, variables: &[BddVariable]) -> Bdd

Eliminate all given variables from the Bdd. This is a generalized variant of var_projection.

This can be used to implement operations like domain and range of a certain relation.

pub fn var_pick(&self, variable: BddVariable) -> Bdd

Picks one valuation for the given BddVariable.

Essentially, what this means is that $(x_1, ..., x_i, ..., x_n) \in B \Leftrightarrow (x_1, ..., \neg x_i, ..., x_n) \not\in B$. That is, each valuation (without $x_i$) can be present only with either $x_i = 1$ or $x_i = 0$, but not both.

WARNING! var_pick is a bit troublesome in terms of composition: B.var_pick(x).var_pick(y) is probably not what you think. So make sure to prove and test thoroughly.

pub fn pick(&self, variables: &[BddVariable]) -> Bdd

Picks one "witness" valuation for the given variables. This is a generalized variant of var_pick.

After this operation, if we view Bdd as a set of bitvectors, every partial valuation in the original Bdd, disregarding the given variables, has exactly one witness valuation in the result, which was also in the original Bdd.

This can be used to implement non-trivial element picking on relations (for example, for $A \times B$, picking one $b \in B$ for every $a \in A$).

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

Fix the value of a specific BddVariable to the given value. This is just a shorthand for $B \land (x \Leftrightarrow \texttt{value})$.

pub fn select(&self, variables: &[(BddVariable, bool)]) -> Bdd

Generalized operation to var_select, allows effectively fixing multiple variables to the given values. Similar to BddValuation.into::<Bdd>(), but here you don't have to specify all variables.

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(in _impl_bdd::_impl_serialisation) fn write_as_string(
    &self,
    output: &mut dyn Write
) -> Result<(), Error>

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

pub(in _impl_bdd::_impl_serialisation) 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 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 mk_var(num_vars: u16, var: BddVariable) -> Bdd

pub(crate) fn mk_not_var(num_vars: u16, var: BddVariable) -> Bdd

pub(crate) fn mk_literal(num_vars: u16, var: BddVariable, value: bool) -> Bdd

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.

impl Bdd

pub fn sat_valuations(&self) -> BddSatisfyingValuations<'_>

pub(in _impl_bdd_satisfying_valuations) fn first_sat_path(
    &self
) -> (Vec<BddPointer>, BddValuation, BddValuation)

(internal) Find first satisfying path in the Bdd, its path mask (bits where the path has fixed values) and smallest valuation on this path.

pub(in _impl_bdd_satisfying_valuations) fn continue_sat_path(
    &self,
    sat_path: &mut Vec<BddPointer>,
    path_mask: &mut BddValuation,
    first_valuation: &mut BddValuation
)

(internal) Take last node on given sat_path and find the first satisfiable path that follows from it.

When this function returns, last pointer in sat_path is the one pointer.

Assumes path_mask and first_valuation is cleared for every variable greater than varOf(last(sat_path)).

Trait Implementations

impl Clone for Bdd

pub fn clone(&self) -> Bdd

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for Bdd

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

Formats the value using the given formatter.

impl Display for Bdd

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

Formats the value using the given formatter.

impl Eq for Bdd

impl From<BddValuation> for Bdd

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

pub fn from(valuation: BddValuation) -> Self

Performs the conversion.

impl Hash for Bdd

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

Feeds this value into the given Hasher.

pub 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

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

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

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

This method tests for !=.

impl StructuralEq for Bdd

impl StructuralPartialEq for Bdd