Struct biodivine_lib_bdd::BddVariableSet
source · pub struct BddVariableSet { /* private fields */ }
Expand description
Maintains the set of variables that can appear in a Bdd
.
Used to create new Bdd
s for basic formulas.
Implementations§
source§impl BddVariableSet
impl BddVariableSet
Methods for evaluating boolean expressions.
sourcepub fn safe_eval_expression(
&self,
expression: &BooleanExpression
) -> Option<Bdd>
pub fn safe_eval_expression( &self, expression: &BooleanExpression ) -> Option<Bdd>
Evaluate the given BooleanExpression
in the context of this BddVariableSet
. Return None
if some
variables are unknown.
sourcepub fn eval_expression(&self, expression: &BooleanExpression) -> Bdd
pub fn eval_expression(&self, expression: &BooleanExpression) -> Bdd
Evaluate the given BooleanExpression
in the context of this BddVariableSet
. Panic if some
variables are unknown.
sourcepub fn eval_expression_string(&self, expression: &str) -> Bdd
pub fn eval_expression_string(&self, expression: &str) -> Bdd
Evaluate the given String
as a BooleanExpression
in the context of this BddVariableSet
.
Panics if the expression cannot be parsed or contains unknown variables.
source§impl BddVariableSet
impl BddVariableSet
sourcepub fn new_anonymous(num_vars: u16) -> BddVariableSet
pub fn new_anonymous(num_vars: u16) -> BddVariableSet
Create a new BddVariableSet
with anonymous variables $(x_0, \ldots, x_n)$ where $n$ is
the num_vars
parameter.
sourcepub fn new(vars: &[&str]) -> BddVariableSet
pub fn new(vars: &[&str]) -> BddVariableSet
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.
sourcepub fn var_by_name(&self, name: &str) -> Option<BddVariable>
pub fn var_by_name(&self, name: &str) -> Option<BddVariable>
Create a BddVariable
based on a variable name. If the name does not appear
in this set, return None
.
sourcepub fn variables(&self) -> Vec<BddVariable>
pub fn variables(&self) -> Vec<BddVariable>
Provides a vector of all BddVariable
s in this set.
sourcepub fn name_of(&self, variable: BddVariable) -> String
pub fn name_of(&self, variable: BddVariable) -> String
Obtain the name of a specific BddVariable
.
sourcepub fn mk_var(&self, var: BddVariable) -> Bdd
pub fn mk_var(&self, var: BddVariable) -> Bdd
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.
sourcepub fn mk_not_var(&self, var: BddVariable) -> Bdd
pub fn mk_not_var(&self, var: BddVariable) -> Bdd
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.
sourcepub fn mk_literal(&self, var: BddVariable, value: bool) -> Bdd
pub fn mk_literal(&self, var: BddVariable, value: bool) -> Bdd
Create a BDD corresponding to the $v <=> \texttt{value}$ formula.
Panics: var
must be a valid variable in this set.
sourcepub fn mk_var_by_name(&self, var: &str) -> Bdd
pub fn mk_var_by_name(&self, var: &str) -> Bdd
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.
sourcepub fn mk_not_var_by_name(&self, var: &str) -> Bdd
pub fn mk_not_var_by_name(&self, var: &str) -> Bdd
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.
sourcepub fn mk_conjunctive_clause(&self, clause: &BddPartialValuation) -> Bdd
pub fn mk_conjunctive_clause(&self, clause: &BddPartialValuation) -> Bdd
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.
sourcepub fn mk_disjunctive_clause(&self, clause: &BddPartialValuation) -> Bdd
pub fn mk_disjunctive_clause(&self, clause: &BddPartialValuation) -> Bdd
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.
sourcepub fn mk_cnf(&self, cnf: &[BddPartialValuation]) -> Bdd
pub fn mk_cnf(&self, cnf: &[BddPartialValuation]) -> Bdd
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.
sourcepub fn mk_dnf(&self, dnf: &[BddPartialValuation]) -> Bdd
pub fn mk_dnf(&self, dnf: &[BddPartialValuation]) -> Bdd
Interpret each BddPartialValuation
in dnf
as a conjunctive clause, and produce
a disjunction of such clauses. Effectively, this constructs a formula based on its
disjunctive normal form.
sourcepub fn mk_sat_up_to_k(&self, k: usize, variables: &[BddVariable]) -> Bdd
pub fn mk_sat_up_to_k(&self, k: usize, variables: &[BddVariable]) -> Bdd
Build a BDD that is satisfied by all valuations where up to $k$ variables
are true
.
Intuitively, this implements a “threshold function” $f(x) = (\sum_{i} x_i \leq k)$
over the given variables
.
sourcepub fn mk_sat_exactly_k(&self, k: usize, variables: &[BddVariable]) -> Bdd
pub fn mk_sat_exactly_k(&self, k: usize, variables: &[BddVariable]) -> Bdd
Build a BDD that is satisfied by all valuations where exactly $k$ variables
are true
.
Intuitively, this implements an “equality function” $f(x) = (\sum_{i} x_i = k)$
over the given variables
.
sourcepub fn transfer_from(&self, bdd: &Bdd, ctx: &BddVariableSet) -> Option<Bdd>
pub fn transfer_from(&self, bdd: &Bdd, ctx: &BddVariableSet) -> Option<Bdd>
This function takes a Bdd bdd
together with its BddVariableSet ctx
and attempts
to translate this bdd
using the variables of this BddVariableSet.
In other words, the source and the output Bdd are logically equivalent, but each is valid in its respective BddVariableSet.
§Limitations
Currently, this method is implemented through “unsafe” variable renaming. I.e. it will
not actually modify the structure of the Bdd in any way. As such, the method can fail
(return None
) when:
- The
bdd
contains variables that are not present in this BddVariableSet (matching is performed based on variable names and the support set ofbdd
). - The variables used in
bdd
are ordered in a way that is not compatible with this BddVariableSet.
Trait Implementations§
source§impl Clone for BddVariableSet
impl Clone for BddVariableSet
source§fn clone(&self) -> BddVariableSet
fn clone(&self) -> BddVariableSet
1.0.0 · source§fn clone_from(&mut self, source: &Self)
fn clone_from(&mut self, source: &Self)
source
. Read more