CUDD: Converting variables to outputs

I'm working with CUDD C++ and I would like to know if it is possible to do the following:

For now, I have the next table stored in a bdd:

|-----|-----|-----||-----|
|  x1 |  x2 |  x3 ||  y  |
|-----|-----|-----||-----|
|  0  |  0  |  0  ||  0  |
|-----|-----|-----||-----|
|  0  |  0  |  1  ||  0  |
|-----|-----|-----||-----|
|  0  |  1  |  0  ||  1  |
|-----|-----|-----||-----|
|  0  |  1  |  1  ||  0  |
|-----|-----|-----||-----|
|  1  |  0  |  0  ||  0  |
|-----|-----|-----||-----|
|  1  |  0  |  1  ||  1  |
|-----|-----|-----||-----|
|  1  |  1  |  0  ||  0  |
|-----|-----|-----||-----|
|  1  |  1  |  1  ||  0  |
|-----|-----|-----||-----|

Is it possible to create another table with 2 outputs extracting the value of x2, x3 if the value of the original output is 1?:

Desired output:

|-----||-----|-----|
|  x1 ||  x2 |  x3 |
|-----||-----|-----|
|  0  ||  1  |  0  |
|-----||-----|-----|
|  1  ||  0  |  1  |
|-----||-----|-----|

I already tried using the ExistAbastract() command and I obtain 2 bdds with the correct data but x2 and x3 are still inputs. Is it possible to convert x2 and x3 from variables to outputs according to the value of y?

Solution

Your first table is a value table, which defines, for every combination of x1,x2,x3 a value of y, and hence can be represented as a BDD over the variables x1,x2,x3.

Your desired output table only has y1 left of the double line. Hence, you want two BDDs x2 and x3 that only range over the value of x1.

Note that your question is ambiguous if for some value of x1, there are multiple combinations of x2,x3 such that y(x1,x2,x3)=True. But here is a solution that works if that is not the case.

Let's only consider the case that you want the function for x2 (the other case is analogous). You existentially abstract x3 and get:

|-----|-----||-----|
|  x1 |  x2 ||  y  |
|-----|-----||-----|
|  0  |  0  ||  0  |
|-----|-----||-----|
|  0  |  1  ||  1  |
|-----|-----||-----|
|  1  |  0  ||  1  |
|-----|-----||-----|
|  1  |  1  ||  0  |
|-----|-----||-----|

Not a bad start. Now what you want as final function is the value for x2 in the row for which y is true. Let's decompose this:

For all values for x1, if the output of the final function is true, then y(x1,true) is true
For all values for x1, if the output of the final function is false, then y1(x1,false) is true.

we can build the first case as:

(y & x2).ExistAbstract(x2)

and this one already suffices as this expression is a function that returns FALSE for all other input values anyway.