Struct biodivine_lib_bdd::BddVariableSet

pub struct BddVariableSet {
    pub(crate) num_vars: u16,
    pub(crate) var_names: Vec<String>,
    pub(crate) var_index_mapping: HashMap<String, u16>,
}

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

Fields

num_vars: u16

var_names: Vec<String>

var_index_mapping: HashMap<String, u16>

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.

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.