Struct biodivine_lib_bdd::BddVariableSet

pub struct BddVariableSet { /* private fields */ }

Maintains the set of variables that can appear in a Bdd. Used to create new Bdds for basic formulas.

Implementations

impl BddVariableSet

Methods for evaluating boolean expressions.

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.

pub fn eval_expression(&self, expression: &BooleanExpression) -> Bdd

Evaluate the given BooleanExpression in the context of this BddVariableSet. Panic if some variables are unknown.

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.

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

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.

pub fn num_vars(&self) -> u16

Return the number of variables in this set.

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.

pub fn variables(&self) -> Vec<BddVariable>

Provides a vector of all BddVariables in this set.

pub fn name_of(&self, variable: BddVariable) -> String

Obtain the name of a specific BddVariable.

pub fn mk_true(&self) -> Bdd

Create a Bdd corresponding to the true formula.

pub fn mk_false(&self) -> Bdd

Create a Bdd corresponding to the false formula.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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 of bdd).
• The variables used in bdd are ordered in a way that is not compatible with this BddVariableSet.

Trait Implementations

impl Clone for BddVariableSet

fn clone(&self) -> BddVariableSet

Returns a copy of the value.

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

Performs copy-assignment from source.

impl From<Vec<&str>> for BddVariableSet

fn from(value: Vec<&str>) -> Self

Converts to this type from the input type.

impl From<Vec<String>> for BddVariableSet

fn from(value: Vec<String>) -> Self

Converts to this type from the input type.

impl FromIterator<String> for BddVariableSet

fn from_iter<T: IntoIterator<Item = String>>(iter: T) -> Self

Creates a value from an iterator.