Struct biodivine_lib_bdd::Bdd

pub struct Bdd(pub(crate) Vec<BddNode>);

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

To create Bdds for atomic formulas, use a BddVariableSet.

Tuple Fields

0: Vec<BddNode>

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

pub fn ternary_op<T>(a: &Bdd, b: &Bdd, c: &Bdd, op_function: T) -> Bdd where
    T: Fn(Option<bool>, Option<bool>, Option<bool>) -> Option<bool>, 

A ternary logical operation on three Bdd objects. Works the same as Bdd::binary_op, but with three arguments.

Note that this may not necessarily be faster than performing two (or more) binary operations. However, in some cases it can significantly reduce overhead incurred by creating large intermediate decision diagrams.

pub fn fused_ternary_flip_op<T>(
    a: (&Bdd, Option<BddVariable>),
    b: (&Bdd, Option<BddVariable>),
    c: (&Bdd, Option<BddVariable>),
    flip_output: Option<BddVariable>,
    op_function: T
) -> Bdd where
    T: Fn(Option<bool>, Option<bool>, Option<bool>) -> Option<bool>, 

A ternary version of Bdd::fused_binary_flip_op that makes it possible to flip the meaning of a single variable the input and output diagrams.

Note that this may not necessarily be faster than performing two (or more) binary operations. However, in some cases it can significantly reduce overhead incurred by creating large intermediate decision diagrams.

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 var_pick_random<R: Rng>(&self, variable: BddVariable, rng: &mut R) -> Bdd

Same as bdd.var_pick, but the preferred value is picked randomly using the provided generator, instead of defaulting to false.

Note that this is not the same as having a random value picked on each path in the Bdd. Instead, there is one “global” value that is preferred on every path.

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 pick_random<R: Rng>(&self, variables: &[BddVariable], rng: &mut R) -> Bdd

Same as bdd.pick, but the preferred value for each variable is picked randomly using the provided generator.

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.

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

Fixes a variable to the given value, and then eliminates said variable using projection.

A valuation v satisfies the resulting formula B' if and only if v[variable = value] satisfied the original formula B.

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

Generalized operation to var_restrict. Allows fixing multiple Bdd variables and eliminating them at the same time.

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_string(&self, output: &mut dyn Write) -> Result<(), Error>

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

pub 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 exact_cardinality(&self) -> BigInt

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.

Note that this also technically works for terminals, but the returned BddVariable is not valid in this Bdd.

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

pub fn is_valuation(&self) -> bool

Check if this Bdd represents a single valuation with all variables fixed to a specific value.

This can be used for example to verify that a set represented by a Bdd is a singleton.

pub fn is_clause(&self) -> bool

Check if this Bdd represents a single conjunctive clause, i.e. that the formula represented by this Bdd is for example x & !y & z & ... (here x, !y, z are some positive/negative literals).

impl Bdd

Utilities for extracting interesting valuations and paths from a Bdd.

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

Return the lexicographically first satisfying valuation of this Bdd.

(In this context, lexicographically means 0 < 1, with greatest variable id being the most significant).

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

Return the lexicographically last satisfying valuation of this Bdd.

(In this context, lexicographically means 0 < 1, with greatest variable id being the most significant).

pub fn first_clause(&self) -> Option<BddPartialValuation>

Return the lexicographically fist path in this Bdd, represented as a conjunctive clause.

pub fn last_clause(&self) -> Option<BddPartialValuation>

Return the lexicographically last path in this Bdd, represented as a conjunctive clause.

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

Return a valuation in this Bdd that contains the greatest amount of positive literals.

If such valuation is not unique, the method should return the one that is first lexicographically.

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

Return a valuation in this Bdd that contains the greatest amount of negative literals.

If such valuation is not unique, the method should return the one that is first lexicographically.

pub fn most_fixed_clause(&self) -> Option<BddPartialValuation>

Compute the path in this Bdd that has the highest amount of fixed variables.

If there are multiple such paths, try to order them lexicographically.

pub fn most_free_clause(&self) -> Option<BddPartialValuation>

Compute the path in this Bdd that has the highest amount of free variables.

If there are multiple such paths, try to order them lexicographically.

pub fn random_valuation<R: Rng>(&self, rng: &mut R) -> Option<BddValuation>

Pick a random valuation that satisfies this Bdd, using a provided random number generator.

Note that the random distribution with which the valuations are picked depends on the structure of the Bdd and is not necessarily uniform.

pub fn random_clause<R: Rng>(&self, rng: &mut R) -> Option<BddPartialValuation>

Pick a random path that appears in this Bdd, using a provided random number generator.

Note that the distribution with which the path is picked depends on the structure of the Bdd and is not necessarily uniform.

impl Bdd

Methods for working with Bdd valuations.

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

Evaluate this Bdd in a specified BddValuation.

impl Bdd

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

Create an iterator that goes through all the satisfying valuations of this Bdd.

Note that the number of such valuations can be substantial and can be approximated using Bdd.cardinality.

pub fn sat_clauses(&self) -> BddPathIterator<'_>

Create an iterator that goes through all paths of this Bdd. Each path is represented as a conjunctive clause in the form of BddPartialValuation.

The whole formula represented by a Bdd can be then seen as a disjunction of these clauses/paths.

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

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

fn into_bdd(self, _variables: &BddVariableSet) -> Bdd

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

impl StructuralEq for Bdd

impl StructuralPartialEq for Bdd