Struct biodivine_lib_bdd::BddVariableSet [−][src]
pub struct BddVariableSet { /* fields omitted */ }
Expand description
Maintains the set of variables that can appear in a Bdd
.
Used to create new Bdd
s for basic formulas.
Implementations
Methods for evaluating boolean expressions.
Evaluate the given BooleanExpression
in the context of this BddVariableSet
. Return None
if some
variables are unknown.
Evaluate the given BooleanExpression
in the context of this BddVariableSet
. Panic if some
variables are unknown.
Evaluate the given String
as a BooleanExpression
in the context of this BddVariableSet
.
Panics if the expression cannot be parsed or contains unknown variables.
Create a new BddVariableSet
with anonymous variables $(x_0, \ldots, x_n)$ where $n$ is
the num_vars
parameter.
Create a new BddVariableSet
with the given named variables. Same as using the
BddVariablesBuilder
with this name vector, but no BddVariable
objects are returned.
Panics: vars
must contain unique names which are allowed as variable names.
Create a BddVariable
based on a variable name. If the name does not appear
in this set, return None
.
Provides a vector of all BddVariable
s in this set.
Obtain the name of a specific BddVariable
.
Create a Bdd
corresponding to the $v$ formula where v
is a specific variable in
this set.
Panics: var
must be a valid variable in this set.
Create a BDD corresponding to the $\neg v$ formula where v
is a specific variable in
this set.
Panics: var
must be a valid variable in this set.
Create a BDD corresponding to the $v <=> \texttt{value}$ formula.
Panics: var
must be a valid variable in this set.
Create a BDD corresponding to the $v$ formula where v
is a variable in this set.
Panics: var
must be a name of a valid variable in this set.
Create a BDD corresponding to the $\neg v$ formula where v
is a variable in this set.
Panics: var
must be a name of a valid variable in this set.
Create a Bdd
corresponding to the conjunction of literals in the given
BddPartialValuation
.
For example, given a valuation x = true
, y = false
and z = true
, create
a Bdd
for the formula x & !y & z
. An empty valuation evaluates to true
.
Panics: All variables in the partial valuation must belong into this set.
Create a Bdd
corresponding to the disjunction of literals in the given
BddPartialValuation
.
For example, given a valuation x = true
, y = false
and z = true
, create
a Bdd
for the formula x | !y | z
. An empty valuation evaluates to false
.
Panics: All variables in the valuation must belong into this set.
Interpret each BddPartialValuation
in cnf
as a disjunctive clause, and produce
a conjunction of such clauses. Effectively, this constructs a formula based on its
conjunctive normal form.
Trait Implementations
Auto Trait Implementations
impl RefUnwindSafe for BddVariableSet
impl Send for BddVariableSet
impl Sync for BddVariableSet
impl Unpin for BddVariableSet
impl UnwindSafe for BddVariableSet
Blanket Implementations
Mutably borrows from an owned value. Read more