I am ready to give a long answer, however, it will probably not directly help you.
TL;DR: As far as I know, CUDD does not have implementation of ExistAbstract or any similar function
for ZDDs. But, I am not a CUDD guru and may have overlooked it.
And here is the long answer. You probably want to just use the functions. So I will cover this first.
Later, I will write about the implementation. Maybe, somebody is ready to add the implementation for
ZDDs to CUDD?
Function bddExistAbstract (Ex) calculates existential quantification over the given Boolean function
(use wikipedia, youtube, coursera, and similar references to learn all the mathematical
background). In short, the existential quantification of variable v in the Boolean function F
is calculated as Ex(F,v) = F|v=0 + F|v=1. In practice, if you write the Boolean function as a
sum-of-products formula than the resulting formula is obtained by simply removing the quantified
variable.
Example (+ is for disjunction, * is for conjuction, ~ is for negation):
F = ~a * c + a * b * ~c + a * ~b * c
Ex(F,b) = ~a * c + a * ~c + a * c = a + c
The universal quantification of variable v in the Boolean function F is calculated as Ax(F,v) = F|v=0 * F|v=1.
It is nothing wrong with implementing existential (and universal) quantification for ZDDs, but you should
ask yourself, why would you need it. Are you representing Boolean functions (e.g. characteristic functions) with
ZDDs? This is not recommendable because ZDDs seems to be inefficient for this or at least not more efficient
than BDDs just more complicated. ZDDs are primarily used to represent sets (more precisely,
the "combination sets"). With sets, existential quantification does not have any usable meaning.
For example, Boolean function F in the previous example coresponds to combination set
{{c},{a,b},{b,c},{a,c}} while resulting Ex(F,b) correspond to set {{c},{a,b},{b,c},{a,c},{a},{a,b,c}}.
To extend your question, observing the given example you can immediatelly think of another
function that would give result for sets but in the sense of existential quantification
for Boolean function. I will call it ElementAbstract (ElemAbst) and I am not aware of its usage outside
of my own projects. It removes the given element from all combinations. Here is the example:
S = {{c},{a,b},{b,c},{a,c}}
ElemAbst(S,b)= {{c},{a},{c},{a,c}} = {{a},{c},{a,c}}
Now, lets talk about the implementation. I will give the simplified code from our "Biddy BDD package"
which is written in C. Hopefully, I have not introduced errors by performing the simplification.
Please, use our public repository to get the complete and working code (http://svn.savannah.nongnu.org/viewvc/biddy/biddyOp.c?view=markup),
it includes support for complement edges)
We will start with a case, where only one variable is requested to be abstracted.
Biddy_Edge
BiddyE(Biddy_Manager MNG, Biddy_Edge f, Biddy_Variable v)
{
Biddy_Edge e, t, r;
Biddy_Variable fv;
...
if (f == biddyZero) return biddyZero;
if (biddyManagerType == BIDDYTYPEOBDD) {
if (BiddyIsSmaller(v,BiddyGetVariable(f))) return f;
}
...
if (biddyManagerType == BIDDYTYPEOBDD) {
if ((fv=BiddyGetVariable(f)) == v) {
r = BiddyOr(MNG,BiddyGetElse(f),BiddyGetThen(f));
}
else {
e = BiddyE(MNG,BiddyGetElse(f),v);
t = BiddyE(MNG,BiddyGetThen(f),v);
r = BiddyFoaNode(MNG,fv,e,t);
}
}
if (biddyManagerType == BIDDYTYPEZBDD) {
if ((fv=BiddyGetVariable(f)) == v) {
r = BiddyOr(MNG,BiddyGetElse(f),BiddyGetThen(f));
r = BiddyFoaNode(MNG,v,r,r);
}
else if (BiddyIsSmaller(v,fv)) {
r = BiddyFoaNode(MNG,v,f,f);
}
else {
e = BiddyE(MNG,BiddyGetElse(f),v);
t = BiddyE(MNG,BiddyGetThen(f),v);
r = BiddyFoaNode(MNG,fv,e,t);
}
}
...
return r;
}
It is more usable to implement a general case where many variables are abstracted at once. This variant is included in CUDD.
Variables to be abstracted are given as a cube which is a simple product of all variables to be abstracted.
Biddy also includes this variant for both, BDDs and ZDDs.
Biddy_Edge
BiddyExistAbstract(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge cube)
{
Biddy_Edge e, t, r;
Biddy_Variable fv,cv;
...
if (f == biddyZero) return biddyZero;
...
if (biddyManagerType == BIDDYTYPEOBDD) {
fv = BiddyGetVariable(f);
cv = BiddyGetVariable(cube);
while (!BiddyIsTerminal(cube) && BiddyIsSmaller(cv,fv)) {
cube = BiddyGetThen(cube);
cv = BiddyGetVariable(cube);
}
if (BiddyIsTerminal(cube)) {
return f;
}
if (cv == fv) {
e = BiddyExistAbstract(MNG,BiddyGetElse(f),BiddyGetThen(cube));
t = BiddyExistAbstract(MNG,BiddyGetThen(f),BiddyGetThen(cube));
r = BiddyOr(MNG,e,t);
} else {
e = BiddyExistAbstract(MNG,BiddyGetElse(f),cube);
t = BiddyExistAbstract(MNG,BiddyGetThen(f),cube);
r = BiddyFoaNode(MNG,fv,e,t);
}
}
if (biddyManagerType == BIDDYTYPEZBDD) {
if (BiddyIsTerminal(cube)) {
return f;
}
cv = BiddyGetVariable(cube);
fv = BiddyGetVariable(f);
if (BiddyIsSmaller(cv,fv)) {
r = BiddyExistAbstract(MNG,f,BiddyGetThen(cube));
r = BiddyFoaNode(MNG,cv,r,r);
}
else if (cv == fv) {
e = BiddyExistAbstract(MNG,BiddyGetElse(f),BiddyGetThen(cube));
t = BiddyExistAbstract(MNG,BiddyGetThen(f),BiddyGetThen(cube));
r = BiddyOr(MNG,e,t);
r = BiddyFoaNode(MNG,cv,r,r);
} else {
e = BiddyExistAbstract(MNG,BiddyGetElse(f),cube);
t = BiddyExistAbstract(MNG,BiddyGetThen(f),cube);
r = BiddyFoaNode(MNG,fv,e,t);
}
}
...
return r;
}
And finaly, here is the implementation for ElementAbstract for abstracting a single variable. Again, Biddy supports this function for both, BDDs and ZDDs,
without asking questions whether this is useful to somebody.
Biddy_Edge
BiddyElementAbstract(Biddy_Manager MNG, Biddy_Edge f, Biddy_Variable v)
{
Biddy_Edge e, t, r;
Biddy_Variable fv;
...
if (f == biddyZero) return biddyZero;
if (biddyManagerType == BIDDYTYPEZBDD) {
if (BiddyIsSmaller(v,BiddyGetVariable(f))) return f;
}
...
if (biddyManagerType == BIDDYTYPEOBDD) {
if ((fv=BiddyGetVariable(f)) == v) {
r = BiddyOr(MNG,BiddyGetElse(f),BiddyGetThen(f));
r = BiddyFoaNode(MNG,v,r,biddyZero);
}
else if (BiddyIsSmaller(v,fv)) {
r = BiddyFoaNode(MNG,v,f,biddyZero);
}
else {
e = BiddyElementAbstract(MNG,BiddyGetElse(f),v);
t = BiddyElementAbstract(MNG,BiddyGetThen(f),v);
r = BiddyFoaNode(MNG,fv,e,t);
}
}
if (biddyManagerType == BIDDYTYPEZBDD) {
if ((fv=BiddyGetVariable(f)) == v) {
r = BiddyOr(MNG,BiddyGetElse(f),BiddyGetThen(f));
}
else {
e = BiddyElementAbstract(MNG,BiddyGetElse(f),v);
t = BiddyElementAbstract(MNG,BiddyGetThen(f),v);
r = BiddyFoaNode(MNG,fv,e,t);
}
}
...
return r;
}
