Module biodivine_lib_bdd::tutorial::p02_bdd_variable_set

Creating a BddVariableSet and BddVariables

In order to create and manipulate Bdds, you have to first create a BddVariableSet. The set maintains knowledge about individual Boolean variables and their ordering. Once the set is created, it is immutable.

Using BddVariableSetBuilder

There are multiple ways to create a BddVariableSet. First is to initialize the set with explicitly named variables using a safe builder:

use biodivine_lib_bdd::BddVariableSetBuilder;

let mut var = BddVariableSetBuilder::new();
let v1 = var.make_variable("v1");                   // a new individual variable
let [v2, v3] = var.make(&["v2", "v3"]);             // a new batch of variables
let var_set = var.build();

assert_eq!(Some(v1), var_set.var_by_name("v1"));
assert_eq!(None, var_set.var_by_name("unknown"));

Here, each BddVariable (v1 and elements of vars) can be later used to create Bdds conditioning on these variables. The purpose of the set builder is to check for duplicate or invalid variable names (some special characters are also not allowed because it would break export to .dot). Once the set is created, you can use var_by_name to obtain a specific variable based on the names you used.

Creating the set directly

If you don’t need the BddVariable objects right away and all variables are known beforehand (this may sound trivial, but sometimes different parts of your application can have different requirements regarding the variables and it is just simpler to let them manipulate the builder directly instead of collecting all the variable names in one place), you can also skip the builder and just provide the names explicitly:

use biodivine_lib_bdd::BddVariableSet;

let variables = BddVariableSet::new(&["v1", "v2", "v3"]);
assert_eq!(3, variables.num_vars());

Anonymous sets

Finally, another option is to create an anonymous variable set, where the variables have default names:

use biodivine_lib_bdd::BddVariableSet;

let variables = BddVariableSet::new_anonymous(4);   // new set with 4 variables

let vars = variables.variables();
assert_eq!(4, vars.len());
assert_eq!("x_3", variables.name_of(vars[3]));   // default name is always x_{var index}

By default, anonymous variables are named x_{index}, but you can use name_of to obtain the name of any variable at runtime. You can also use the variables function to get a vector of all available variables.

Working with variable sets

Once we have a variable set, we can use it to create basic Bdd objects:

use biodivine_lib_bdd::BddVariableSet;

let set = BddVariableSet::new_anonymous(4);
let v = set.variables();

let tt = set.mk_true();     // constant true formula
let v0 = set.mk_var(v[0]);  // bdd for formula (v0)
let not_v1 = set.mk_not_var_by_name("x_1"); // bdd for formula (!v1)

In order to create complex boolean combinations of these basic Bdds, we can use different techniques which are described in the next section of this tutorial.

Notice that BddVariableSet can be cloned. This creates a new set with the exact same variables. The BddVariable and Bdd objects can be then used with both the original and cloned set interchangeably. Bdd objects are also cloneable (since they are just vectors of BDD nodes) and can be used with any compatible BddVariableSet. This way, you can quickly and easily share BDDs between different threads (each thread has its own clone of the BddVariableSet).