Struct biodivine_lib_bdd::BddVariableSet

pub struct BddVariableSet {
    num_vars: u16,
    var_names: Vec<String>,
    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_1, \ldots, x_n)$ where $n$ is the num_vars parameter.

pub fn new(vars: Vec<&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.

Trait Implementations

impl Clone for BddVariableSet

pub fn clone(&self) -> BddVariableSet

Returns a copy of the value.

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

Performs copy-assignment from source.