I'm working with CUDD C++ interface (https://github.com/ivmai/cudd) but there is almost no information about this library. I would like to know how to remove one variable according to its value.
For example, I have now the next table stored in a bdd:
|-----|-----|-----|
| x1 | x2 | y |
|-----|-----|-----|
| 0 | 0 | 1 |
|-----|-----|-----|
| 0 | 1 | 1 |
|-----|-----|-----|
| 1 | 0 | 1 |
|-----|-----|-----|
| 1 | 1 | 0 |
|-----|-----|-----|
And I want to split the previous table in two separate bdds according to the value of x2 and remove that node afterwards:
If x2 = 0:
|-----|-----|
| x1 | y |
|-----|-----|
| 0 | 1 |
|-----|-----|
| 1 | 1 |
|-----|-----|
If x2 = 1:
|-----|-----|
| x1 | y |
|-----|-----|
| 0 | 1 |
|-----|-----|
| 1 | 0 |
|-----|-----|
Is it possible?
The reason that there is almost no documentation on the C++ interface of the CUDD library is that it is just a wrapper for the C functions, for which there is plenty of documentation.
The C++ wrapper is mainly useful for getting rid of all the Cudd_Ref(...) and Cudd_RecursiveDeref(...) calls that code using the C interface would need to do. Note that you can use the C interface from C++ code as well, if you want.
To do what you want to do, you have to combine the Boolean operators offered by CUDD in a way that you obtain a new Boolean function with the desired properties.
The first step is to restrict s to the x=0 and x=1 case:
BDD s0 = s & !x;
BDD s1 = s & x;
As you noticed, the new BDDs are not (yet) oblivious to the value of the x variable. You want them to be "don't care" w.r.t to the value of x. Since you already know that x is restricted to one particular value in s0 and s1, you can use the existential abstraction operator:
s0 = s0.ExistAbstract(x);
s1 = s1.ExistAbstract(x);
Note that x is used here as a so-called cube (see below).
These are now the BDDs that you want.
Cube explanation: If you abstract from multiple variables at the same time, you should compute such a cube from all the variables to be abstracted from first. A cube is mainly used for representing a set of variables. From mathematical logic, it is known that if you existentially or universally abstract away multiple variables, then the order to abstracting away these variables does not matter. Since the recursive BDD operations in CUDD are implemented over pairs (or triples) of BDDs whenever possible, CUDD internally represents a set of variables as a cube as well, so that an existential abstraction operation can just work on (1) the BDD for which existential abstraction is to be performed, and (2) the BDD representing the set of variables to be abstracted from. The internal representation of a cube as a BDD should not be of relevance to a developer just using CUDD (rather than extending CUDD), except that a BDDD representing a variable can also be used as a cube.