Struct biodivine_lib_bdd::Bdd [−][src]
pub struct Bdd(_);
Expand description
An array-based encoding of the binary decision diagram implementing basic logical operations.
To create Bdd
s for atomic formulas, use a BddVariableSet
.
Implementations
Basic boolean logical operations for Bdd
s:
$\neg, \land, \lor, \Rightarrow, \Leftrightarrow, \oplus$.
Create a Bdd
corresponding to the $\neg \phi$ formula, where $\phi$ is this Bdd
.
Create a Bdd
corresponding to the $\phi \land \psi$ formula, where $\phi$ and $\psi$
are the two given Bdd
s.
Create a Bdd
corresponding to the $\phi \lor \psi$ formula, where $\phi$ and $\psi$
are the two given Bdd
s.
Create a Bdd
corresponding to the $\phi \Rightarrow \psi$ formula, where $\phi$ and $\psi$
are the two given Bdd
s.
Create a Bdd
corresponding to the $\phi \Leftrightarrow \psi$ formula, where $\phi$ and $\psi$
are the two given Bdd
s.
Create a Bdd
corresponding to the $\phi \oplus \psi$ formula, where $\phi$ and $\psi$
are the two given Bdd
s.
Create a Bdd
corresponding to the $\phi \land \neg \psi$ formula, where $\phi$ and $\psi$
are the two given Bdd
s.
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).
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.
Advanced relation-like operations for Bdd
s.
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$.
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.
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.
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.
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$).
Same as bdd.pick
, but the preferred value for each variable is picked randomly using
the provided generator.
Fix the value of a specific BddVariable
to the given value
. This is just a shorthand
for $B \land (x \Leftrightarrow \texttt{value})$.
.dot
export procedure for Bdd
s.
pub fn write_as_dot_string(
&self,
output: &mut dyn Write,
variables: &BddVariableSet,
zero_pruned: bool
) -> Result<(), Error>
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.
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.
Serialisation and deserialisation methods for Bdd
s.
Write this Bdd
into the given output
writer using a simple little-endian binary encoding.
Read a Bdd
from a given input
reader using a simple little-endian binary encoding.
Read a Bdd
from a serialized string.
Several useful (mostly internal) low-level utility methods for Bdd
s.
Approximately computes the number of valuations satisfying the formula given
by this Bdd
.
If the Bdd
is satisfiable, return some BddValuation
that satisfies the Bdd
.
Convert this Bdd
to a BooleanExpression
(using the variable names from the given
BddVariableSet
).
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.
Utilities for extracting interesting valuations and paths from a Bdd
.
Return the lexicographically first satisfying valuation of this Bdd
.
(In this context, lexicographically means 0 < 1
, with greatest variable id
being the most significant).
Return the lexicographically last satisfying valuation of this Bdd
.
(In this context, lexicographically means 0 < 1
, with greatest variable id
being the most significant).
Return the lexicographically fist path in this Bdd
, represented as
a conjunctive clause.
Return the lexicographically last path in this Bdd
, represented as
a conjunctive clause.
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.
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.
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.
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.
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.
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.
Methods for working with Bdd
valuations.
Evaluate this Bdd
in a specified BddValuation
.
pub fn sat_valuations(&self) -> BddSatisfyingValuations<'_>ⓘNotable traits for BddSatisfyingValuations<'_>impl Iterator for BddSatisfyingValuations<'_> type Item = BddValuation;
pub fn sat_valuations(&self) -> BddSatisfyingValuations<'_>ⓘNotable traits for BddSatisfyingValuations<'_>impl Iterator for BddSatisfyingValuations<'_> type Item = BddValuation;
impl Iterator for BddSatisfyingValuations<'_> type Item = BddValuation;
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<'_>ⓘNotable traits for BddPathIterator<'_>impl Iterator for BddPathIterator<'_> type Item = BddPartialValuation;
pub fn sat_clauses(&self) -> BddPathIterator<'_>ⓘNotable traits for BddPathIterator<'_>impl Iterator for BddPathIterator<'_> type Item = BddPartialValuation;
impl Iterator for BddPathIterator<'_> type Item = BddPartialValuation;
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
Convert a BddValuation to a Bdd with, well, exactly that one valuation.
Performs the conversion.
Auto Trait Implementations
impl RefUnwindSafe for Bdd
impl UnwindSafe for Bdd
Blanket Implementations
Mutably borrows from an owned value. Read more