diff options
Diffstat (limited to 'src/bdd/cudd/cuddBddIte.c')
| -rw-r--r-- | src/bdd/cudd/cuddBddIte.c | 1254 |
1 files changed, 1254 insertions, 0 deletions
diff --git a/src/bdd/cudd/cuddBddIte.c b/src/bdd/cudd/cuddBddIte.c new file mode 100644 index 00000000..fe0c6500 --- /dev/null +++ b/src/bdd/cudd/cuddBddIte.c @@ -0,0 +1,1254 @@ +/**CFile*********************************************************************** + + FileName [cuddBddIte.c] + + PackageName [cudd] + + Synopsis [BDD ITE function and satellites.] + + Description [External procedures included in this module: + <ul> + <li> Cudd_bddIte() + <li> Cudd_bddIteConstant() + <li> Cudd_bddIntersect() + <li> Cudd_bddAnd() + <li> Cudd_bddOr() + <li> Cudd_bddNand() + <li> Cudd_bddNor() + <li> Cudd_bddXor() + <li> Cudd_bddXnor() + <li> Cudd_bddLeq() + </ul> + Internal procedures included in this module: + <ul> + <li> cuddBddIteRecur() + <li> cuddBddIntersectRecur() + <li> cuddBddAndRecur() + <li> cuddBddXorRecur() + </ul> + Static procedures included in this module: + <ul> + <li> bddVarToConst() + <li> bddVarToCanonical() + <li> bddVarToCanonicalSimple() + </ul>] + + SeeAlso [] + + Author [Fabio Somenzi] + + Copyright [This file was created at the University of Colorado at + Boulder. The University of Colorado at Boulder makes no warranty + about the suitability of this software for any purpose. It is + presented on an AS IS basis.] + +******************************************************************************/ + +#include "util.h" +#include "cuddInt.h" + + +/*---------------------------------------------------------------------------*/ +/* Constant declarations */ +/*---------------------------------------------------------------------------*/ + + +/*---------------------------------------------------------------------------*/ +/* Stucture declarations */ +/*---------------------------------------------------------------------------*/ + + +/*---------------------------------------------------------------------------*/ +/* Type declarations */ +/*---------------------------------------------------------------------------*/ + + +/*---------------------------------------------------------------------------*/ +/* Variable declarations */ +/*---------------------------------------------------------------------------*/ + +#ifndef lint +static char rcsid[] DD_UNUSED = "$Id: cuddBddIte.c,v 1.1.1.1 2003/02/24 22:23:51 wjiang Exp $"; +#endif + +/*---------------------------------------------------------------------------*/ +/* Macro declarations */ +/*---------------------------------------------------------------------------*/ + + +/**AutomaticStart*************************************************************/ + +/*---------------------------------------------------------------------------*/ +/* Static function prototypes */ +/*---------------------------------------------------------------------------*/ + +static void bddVarToConst ARGS((DdNode *f, DdNode **gp, DdNode **hp, DdNode *one)); +static int bddVarToCanonical ARGS((DdManager *dd, DdNode **fp, DdNode **gp, DdNode **hp, unsigned int *topfp, unsigned int *topgp, unsigned int *tophp)); +static int bddVarToCanonicalSimple ARGS((DdManager *dd, DdNode **fp, DdNode **gp, DdNode **hp, unsigned int *topfp, unsigned int *topgp, unsigned int *tophp)); + +/**AutomaticEnd***************************************************************/ + + +/*---------------------------------------------------------------------------*/ +/* Definition of exported functions */ +/*---------------------------------------------------------------------------*/ + + +/**Function******************************************************************** + + Synopsis [Implements ITE(f,g,h).] + + Description [Implements ITE(f,g,h). Returns a pointer to the + resulting BDD if successful; NULL if the intermediate result blows + up.] + + SideEffects [None] + + SeeAlso [Cudd_addIte Cudd_bddIteConstant Cudd_bddIntersect] + +******************************************************************************/ +DdNode * +Cudd_bddIte( + DdManager * dd, + DdNode * f, + DdNode * g, + DdNode * h) +{ + DdNode *res; + + do { + dd->reordered = 0; + res = cuddBddIteRecur(dd,f,g,h); + } while (dd->reordered == 1); + return(res); + +} /* end of Cudd_bddIte */ + + +/**Function******************************************************************** + + Synopsis [Implements ITEconstant(f,g,h).] + + Description [Implements ITEconstant(f,g,h). Returns a pointer to the + resulting BDD (which may or may not be constant) or DD_NON_CONSTANT. + No new nodes are created.] + + SideEffects [None] + + SeeAlso [Cudd_bddIte Cudd_bddIntersect Cudd_bddLeq Cudd_addIteConstant] + +******************************************************************************/ +DdNode * +Cudd_bddIteConstant( + DdManager * dd, + DdNode * f, + DdNode * g, + DdNode * h) +{ + DdNode *r, *Fv, *Fnv, *Gv, *Gnv, *H, *Hv, *Hnv, *t, *e; + DdNode *one = DD_ONE(dd); + DdNode *zero = Cudd_Not(one); + int comple; + unsigned int topf, topg, toph, v; + + statLine(dd); + /* Trivial cases. */ + if (f == one) /* ITE(1,G,H) => G */ + return(g); + + if (f == zero) /* ITE(0,G,H) => H */ + return(h); + + /* f now not a constant. */ + bddVarToConst(f, &g, &h, one); /* possibly convert g or h */ + /* to constants */ + + if (g == h) /* ITE(F,G,G) => G */ + return(g); + + if (Cudd_IsConstant(g) && Cudd_IsConstant(h)) + return(DD_NON_CONSTANT); /* ITE(F,1,0) or ITE(F,0,1) */ + /* => DD_NON_CONSTANT */ + + if (g == Cudd_Not(h)) + return(DD_NON_CONSTANT); /* ITE(F,G,G') => DD_NON_CONSTANT */ + /* if F != G and F != G' */ + + comple = bddVarToCanonical(dd, &f, &g, &h, &topf, &topg, &toph); + + /* Cache lookup. */ + r = cuddConstantLookup(dd, DD_BDD_ITE_CONSTANT_TAG, f, g, h); + if (r != NULL) { + return(Cudd_NotCond(r,comple && r != DD_NON_CONSTANT)); + } + + v = ddMin(topg, toph); + + /* ITE(F,G,H) = (v,G,H) (non constant) if F = (v,1,0), v < top(G,H). */ + if (topf < v && cuddT(f) == one && cuddE(f) == zero) { + return(DD_NON_CONSTANT); + } + + /* Compute cofactors. */ + if (topf <= v) { + v = ddMin(topf, v); /* v = top_var(F,G,H) */ + Fv = cuddT(f); Fnv = cuddE(f); + } else { + Fv = Fnv = f; + } + + if (topg == v) { + Gv = cuddT(g); Gnv = cuddE(g); + } else { + Gv = Gnv = g; + } + + if (toph == v) { + H = Cudd_Regular(h); + Hv = cuddT(H); Hnv = cuddE(H); + if (Cudd_IsComplement(h)) { + Hv = Cudd_Not(Hv); + Hnv = Cudd_Not(Hnv); + } + } else { + Hv = Hnv = h; + } + + /* Recursion. */ + t = Cudd_bddIteConstant(dd, Fv, Gv, Hv); + if (t == DD_NON_CONSTANT || !Cudd_IsConstant(t)) { + cuddCacheInsert(dd, DD_BDD_ITE_CONSTANT_TAG, f, g, h, DD_NON_CONSTANT); + return(DD_NON_CONSTANT); + } + e = Cudd_bddIteConstant(dd, Fnv, Gnv, Hnv); + if (e == DD_NON_CONSTANT || !Cudd_IsConstant(e) || t != e) { + cuddCacheInsert(dd, DD_BDD_ITE_CONSTANT_TAG, f, g, h, DD_NON_CONSTANT); + return(DD_NON_CONSTANT); + } + cuddCacheInsert(dd, DD_BDD_ITE_CONSTANT_TAG, f, g, h, t); + return(Cudd_NotCond(t,comple)); + +} /* end of Cudd_bddIteConstant */ + + +/**Function******************************************************************** + + Synopsis [Returns a function included in the intersection of f and g.] + + Description [Computes a function included in the intersection of f and + g. (That is, a witness that the intersection is not empty.) + Cudd_bddIntersect tries to build as few new nodes as possible. If the + only result of interest is whether f and g intersect, + Cudd_bddLeq should be used instead.] + + SideEffects [None] + + SeeAlso [Cudd_bddLeq Cudd_bddIteConstant] + +******************************************************************************/ +DdNode * +Cudd_bddIntersect( + DdManager * dd /* manager */, + DdNode * f /* first operand */, + DdNode * g /* second operand */) +{ + DdNode *res; + + do { + dd->reordered = 0; + res = cuddBddIntersectRecur(dd,f,g); + } while (dd->reordered == 1); + + return(res); + +} /* end of Cudd_bddIntersect */ + + +/**Function******************************************************************** + + Synopsis [Computes the conjunction of two BDDs f and g.] + + Description [Computes the conjunction of two BDDs f and g. Returns a + pointer to the resulting BDD if successful; NULL if the intermediate + result blows up.] + + SideEffects [None] + + SeeAlso [Cudd_bddIte Cudd_addApply Cudd_bddAndAbstract Cudd_bddIntersect + Cudd_bddOr Cudd_bddNand Cudd_bddNor Cudd_bddXor Cudd_bddXnor] + +******************************************************************************/ +DdNode * +Cudd_bddAnd( + DdManager * dd, + DdNode * f, + DdNode * g) +{ + DdNode *res; + + do { + dd->reordered = 0; + res = cuddBddAndRecur(dd,f,g); + } while (dd->reordered == 1); + return(res); + +} /* end of Cudd_bddAnd */ + + +/**Function******************************************************************** + + Synopsis [Computes the disjunction of two BDDs f and g.] + + Description [Computes the disjunction of two BDDs f and g. Returns a + pointer to the resulting BDD if successful; NULL if the intermediate + result blows up.] + + SideEffects [None] + + SeeAlso [Cudd_bddIte Cudd_addApply Cudd_bddAnd Cudd_bddNand Cudd_bddNor + Cudd_bddXor Cudd_bddXnor] + +******************************************************************************/ +DdNode * +Cudd_bddOr( + DdManager * dd, + DdNode * f, + DdNode * g) +{ + DdNode *res; + + do { + dd->reordered = 0; + res = cuddBddAndRecur(dd,Cudd_Not(f),Cudd_Not(g)); + } while (dd->reordered == 1); + res = Cudd_NotCond(res,res != NULL); + return(res); + +} /* end of Cudd_bddOr */ + + +/**Function******************************************************************** + + Synopsis [Computes the NAND of two BDDs f and g.] + + Description [Computes the NAND of two BDDs f and g. Returns a + pointer to the resulting BDD if successful; NULL if the intermediate + result blows up.] + + SideEffects [None] + + SeeAlso [Cudd_bddIte Cudd_addApply Cudd_bddAnd Cudd_bddOr Cudd_bddNor + Cudd_bddXor Cudd_bddXnor] + +******************************************************************************/ +DdNode * +Cudd_bddNand( + DdManager * dd, + DdNode * f, + DdNode * g) +{ + DdNode *res; + + do { + dd->reordered = 0; + res = cuddBddAndRecur(dd,f,g); + } while (dd->reordered == 1); + res = Cudd_NotCond(res,res != NULL); + return(res); + +} /* end of Cudd_bddNand */ + + +/**Function******************************************************************** + + Synopsis [Computes the NOR of two BDDs f and g.] + + Description [Computes the NOR of two BDDs f and g. Returns a + pointer to the resulting BDD if successful; NULL if the intermediate + result blows up.] + + SideEffects [None] + + SeeAlso [Cudd_bddIte Cudd_addApply Cudd_bddAnd Cudd_bddOr Cudd_bddNand + Cudd_bddXor Cudd_bddXnor] + +******************************************************************************/ +DdNode * +Cudd_bddNor( + DdManager * dd, + DdNode * f, + DdNode * g) +{ + DdNode *res; + + do { + dd->reordered = 0; + res = cuddBddAndRecur(dd,Cudd_Not(f),Cudd_Not(g)); + } while (dd->reordered == 1); + return(res); + +} /* end of Cudd_bddNor */ + + +/**Function******************************************************************** + + Synopsis [Computes the exclusive OR of two BDDs f and g.] + + Description [Computes the exclusive OR of two BDDs f and g. Returns a + pointer to the resulting BDD if successful; NULL if the intermediate + result blows up.] + + SideEffects [None] + + SeeAlso [Cudd_bddIte Cudd_addApply Cudd_bddAnd Cudd_bddOr + Cudd_bddNand Cudd_bddNor Cudd_bddXnor] + +******************************************************************************/ +DdNode * +Cudd_bddXor( + DdManager * dd, + DdNode * f, + DdNode * g) +{ + DdNode *res; + + do { + dd->reordered = 0; + res = cuddBddXorRecur(dd,f,g); + } while (dd->reordered == 1); + return(res); + +} /* end of Cudd_bddXor */ + + +/**Function******************************************************************** + + Synopsis [Computes the exclusive NOR of two BDDs f and g.] + + Description [Computes the exclusive NOR of two BDDs f and g. Returns a + pointer to the resulting BDD if successful; NULL if the intermediate + result blows up.] + + SideEffects [None] + + SeeAlso [Cudd_bddIte Cudd_addApply Cudd_bddAnd Cudd_bddOr + Cudd_bddNand Cudd_bddNor Cudd_bddXor] + +******************************************************************************/ +DdNode * +Cudd_bddXnor( + DdManager * dd, + DdNode * f, + DdNode * g) +{ + DdNode *res; + + do { + dd->reordered = 0; + res = cuddBddXorRecur(dd,f,Cudd_Not(g)); + } while (dd->reordered == 1); + return(res); + +} /* end of Cudd_bddXnor */ + + +/**Function******************************************************************** + + Synopsis [Determines whether f is less than or equal to g.] + + Description [Returns 1 if f is less than or equal to g; 0 otherwise. + No new nodes are created.] + + SideEffects [None] + + SeeAlso [Cudd_bddIteConstant Cudd_addEvalConst] + +******************************************************************************/ +int +Cudd_bddLeq( + DdManager * dd, + DdNode * f, + DdNode * g) +{ + DdNode *one, *zero, *tmp, *F, *fv, *fvn, *gv, *gvn; + unsigned int topf, topg, res; + + statLine(dd); + /* Terminal cases and normalization. */ + if (f == g) return(1); + + if (Cudd_IsComplement(g)) { + /* Special case: if f is regular and g is complemented, + ** f(1,...,1) = 1 > 0 = g(1,...,1). + */ + if (!Cudd_IsComplement(f)) return(0); + /* Both are complemented: Swap and complement because + ** f <= g <=> g' <= f' and we want the second argument to be regular. + */ + tmp = g; + g = Cudd_Not(f); + f = Cudd_Not(tmp); + } else if (Cudd_IsComplement(f) && g < f) { + tmp = g; + g = Cudd_Not(f); + f = Cudd_Not(tmp); + } + + /* Now g is regular and, if f is not regular, f < g. */ + one = DD_ONE(dd); + if (g == one) return(1); /* no need to test against zero */ + if (f == one) return(0); /* since at this point g != one */ + if (Cudd_Not(f) == g) return(0); /* because neither is constant */ + zero = Cudd_Not(one); + if (f == zero) return(1); + + /* Here neither f nor g is constant. */ + + /* Check cache. */ + tmp = cuddCacheLookup2(dd,(DdNode * (*)(DdManager *, DdNode *, + DdNode *))Cudd_bddLeq,f,g); + if (tmp != NULL) { + return(tmp == one); + } + + /* Compute cofactors. */ + F = Cudd_Regular(f); + topf = dd->perm[F->index]; + topg = dd->perm[g->index]; + if (topf <= topg) { + fv = cuddT(F); fvn = cuddE(F); + if (f != F) { + fv = Cudd_Not(fv); + fvn = Cudd_Not(fvn); + } + } else { + fv = fvn = f; + } + if (topg <= topf) { + gv = cuddT(g); gvn = cuddE(g); + } else { + gv = gvn = g; + } + + /* Recursive calls. Since we want to maximize the probability of + ** the special case f(1,...,1) > g(1,...,1), we consider the negative + ** cofactors first. Indeed, the complementation parity of the positive + ** cofactors is the same as the one of the parent functions. + */ + res = Cudd_bddLeq(dd,fvn,gvn) && Cudd_bddLeq(dd,fv,gv); + + /* Store result in cache and return. */ + cuddCacheInsert2(dd,(DdNode * (*)(DdManager *, DdNode *, DdNode *))Cudd_bddLeq,f,g,(res ? one : zero)); + return(res); + +} /* end of Cudd_bddLeq */ + + +/*---------------------------------------------------------------------------*/ +/* Definition of internal functions */ +/*---------------------------------------------------------------------------*/ + + +/**Function******************************************************************** + + Synopsis [Implements the recursive step of Cudd_bddIte.] + + Description [Implements the recursive step of Cudd_bddIte. Returns a + pointer to the resulting BDD. NULL if the intermediate result blows + up or if reordering occurs.] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +DdNode * +cuddBddIteRecur( + DdManager * dd, + DdNode * f, + DdNode * g, + DdNode * h) +{ + DdNode *one, *zero, *res; + DdNode *r, *Fv, *Fnv, *Gv, *Gnv, *H, *Hv, *Hnv, *t, *e; + unsigned int topf, topg, toph, v; + int index; + int comple; + + statLine(dd); + /* Terminal cases. */ + + /* One variable cases. */ + if (f == (one = DD_ONE(dd))) /* ITE(1,G,H) = G */ + return(g); + + if (f == (zero = Cudd_Not(one))) /* ITE(0,G,H) = H */ + return(h); + + /* From now on, f is known not to be a constant. */ + if (g == one || f == g) { /* ITE(F,F,H) = ITE(F,1,H) = F + H */ + if (h == zero) { /* ITE(F,1,0) = F */ + return(f); + } else { + res = cuddBddAndRecur(dd,Cudd_Not(f),Cudd_Not(h)); + return(Cudd_NotCond(res,res != NULL)); + } + } else if (g == zero || f == Cudd_Not(g)) { /* ITE(F,!F,H) = ITE(F,0,H) = !F * H */ + if (h == one) { /* ITE(F,0,1) = !F */ + return(Cudd_Not(f)); + } else { + res = cuddBddAndRecur(dd,Cudd_Not(f),h); + return(res); + } + } + if (h == zero || f == h) { /* ITE(F,G,F) = ITE(F,G,0) = F * G */ + res = cuddBddAndRecur(dd,f,g); + return(res); + } else if (h == one || f == Cudd_Not(h)) { /* ITE(F,G,!F) = ITE(F,G,1) = !F + G */ + res = cuddBddAndRecur(dd,f,Cudd_Not(g)); + return(Cudd_NotCond(res,res != NULL)); + } + + /* Check remaining one variable case. */ + if (g == h) { /* ITE(F,G,G) = G */ + return(g); + } else if (g == Cudd_Not(h)) { /* ITE(F,G,!G) = F <-> G */ + res = cuddBddXorRecur(dd,f,h); + return(res); + } + + /* From here, there are no constants. */ + comple = bddVarToCanonicalSimple(dd, &f, &g, &h, &topf, &topg, &toph); + + /* f & g are now regular pointers */ + + v = ddMin(topg, toph); + + /* A shortcut: ITE(F,G,H) = (v,G,H) if F = (v,1,0), v < top(G,H). */ + if (topf < v && cuddT(f) == one && cuddE(f) == zero) { + r = cuddUniqueInter(dd, (int) f->index, g, h); + return(Cudd_NotCond(r,comple && r != NULL)); + } + + /* Check cache. */ + r = cuddCacheLookup(dd, DD_BDD_ITE_TAG, f, g, h); + if (r != NULL) { + return(Cudd_NotCond(r,comple)); + } + + /* Compute cofactors. */ + if (topf <= v) { + v = ddMin(topf, v); /* v = top_var(F,G,H) */ + index = f->index; + Fv = cuddT(f); Fnv = cuddE(f); + } else { + Fv = Fnv = f; + } + if (topg == v) { + index = g->index; + Gv = cuddT(g); Gnv = cuddE(g); + } else { + Gv = Gnv = g; + } + if (toph == v) { + H = Cudd_Regular(h); + index = H->index; + Hv = cuddT(H); Hnv = cuddE(H); + if (Cudd_IsComplement(h)) { + Hv = Cudd_Not(Hv); + Hnv = Cudd_Not(Hnv); + } + } else { + Hv = Hnv = h; + } + + /* Recursive step. */ + t = cuddBddIteRecur(dd,Fv,Gv,Hv); + if (t == NULL) return(NULL); + cuddRef(t); + + e = cuddBddIteRecur(dd,Fnv,Gnv,Hnv); + if (e == NULL) { + Cudd_IterDerefBdd(dd,t); + return(NULL); + } + cuddRef(e); + + r = (t == e) ? t : cuddUniqueInter(dd,index,t,e); + if (r == NULL) { + Cudd_IterDerefBdd(dd,t); + Cudd_IterDerefBdd(dd,e); + return(NULL); + } + cuddDeref(t); + cuddDeref(e); + + cuddCacheInsert(dd, DD_BDD_ITE_TAG, f, g, h, r); + return(Cudd_NotCond(r,comple)); + +} /* end of cuddBddIteRecur */ + + +/**Function******************************************************************** + + Synopsis [Implements the recursive step of Cudd_bddIntersect.] + + Description [] + + SideEffects [None] + + SeeAlso [Cudd_bddIntersect] + +******************************************************************************/ +DdNode * +cuddBddIntersectRecur( + DdManager * dd, + DdNode * f, + DdNode * g) +{ + DdNode *res; + DdNode *F, *G, *t, *e; + DdNode *fv, *fnv, *gv, *gnv; + DdNode *one, *zero; + unsigned int index, topf, topg; + + statLine(dd); + one = DD_ONE(dd); + zero = Cudd_Not(one); + + /* Terminal cases. */ + if (f == zero || g == zero || f == Cudd_Not(g)) return(zero); + if (f == g || g == one) return(f); + if (f == one) return(g); + + /* At this point f and g are not constant. */ + if (f > g) { DdNode *tmp = f; f = g; g = tmp; } + res = cuddCacheLookup2(dd,Cudd_bddIntersect,f,g); + if (res != NULL) return(res); + + /* Find splitting variable. Here we can skip the use of cuddI, + ** because the operands are known to be non-constant. + */ + F = Cudd_Regular(f); + topf = dd->perm[F->index]; + G = Cudd_Regular(g); + topg = dd->perm[G->index]; + + /* Compute cofactors. */ + if (topf <= topg) { + index = F->index; + fv = cuddT(F); + fnv = cuddE(F); + if (Cudd_IsComplement(f)) { + fv = Cudd_Not(fv); + fnv = Cudd_Not(fnv); + } + } else { + index = G->index; + fv = fnv = f; + } + + if (topg <= topf) { + gv = cuddT(G); + gnv = cuddE(G); + if (Cudd_IsComplement(g)) { + gv = Cudd_Not(gv); + gnv = Cudd_Not(gnv); + } + } else { + gv = gnv = g; + } + + /* Compute partial results. */ + t = cuddBddIntersectRecur(dd,fv,gv); + if (t == NULL) return(NULL); + cuddRef(t); + if (t != zero) { + e = zero; + } else { + e = cuddBddIntersectRecur(dd,fnv,gnv); + if (e == NULL) { + Cudd_IterDerefBdd(dd, t); + return(NULL); + } + } + cuddRef(e); + + if (t == e) { /* both equal zero */ + res = t; + } else if (Cudd_IsComplement(t)) { + res = cuddUniqueInter(dd,(int)index,Cudd_Not(t),Cudd_Not(e)); + if (res == NULL) { + Cudd_IterDerefBdd(dd, t); + Cudd_IterDerefBdd(dd, e); + return(NULL); + } + res = Cudd_Not(res); + } else { + res = cuddUniqueInter(dd,(int)index,t,e); + if (res == NULL) { + Cudd_IterDerefBdd(dd, t); + Cudd_IterDerefBdd(dd, e); + return(NULL); + } + } + cuddDeref(e); + cuddDeref(t); + + cuddCacheInsert2(dd,Cudd_bddIntersect,f,g,res); + + return(res); + +} /* end of cuddBddIntersectRecur */ + + +/**Function******************************************************************** + + Synopsis [Implements the recursive step of Cudd_bddAnd.] + + Description [Implements the recursive step of Cudd_bddAnd by taking + the conjunction of two BDDs. Returns a pointer to the result is + successful; NULL otherwise.] + + SideEffects [None] + + SeeAlso [Cudd_bddAnd] + +******************************************************************************/ +DdNode * +cuddBddAndRecur( + DdManager * manager, + DdNode * f, + DdNode * g) +{ + DdNode *F, *fv, *fnv, *G, *gv, *gnv; + DdNode *one, *r, *t, *e; + unsigned int topf, topg, index; + + statLine(manager); + one = DD_ONE(manager); + + /* Terminal cases. */ + F = Cudd_Regular(f); + G = Cudd_Regular(g); + if (F == G) { + if (f == g) return(f); + else return(Cudd_Not(one)); + } + if (F == one) { + if (f == one) return(g); + else return(f); + } + if (G == one) { + if (g == one) return(f); + else return(g); + } + + /* At this point f and g are not constant. */ + if (f > g) { /* Try to increase cache efficiency. */ + DdNode *tmp = f; + f = g; + g = tmp; + F = Cudd_Regular(f); + G = Cudd_Regular(g); + } + + /* Check cache. */ + if (F->ref != 1 || G->ref != 1) { + r = cuddCacheLookup2(manager, Cudd_bddAnd, f, g); + if (r != NULL) return(r); + } + + /* Here we can skip the use of cuddI, because the operands are known + ** to be non-constant. + */ + topf = manager->perm[F->index]; + topg = manager->perm[G->index]; + + /* Compute cofactors. */ + if (topf <= topg) { + index = F->index; + fv = cuddT(F); + fnv = cuddE(F); + if (Cudd_IsComplement(f)) { + fv = Cudd_Not(fv); + fnv = Cudd_Not(fnv); + } + } else { + index = G->index; + fv = fnv = f; + } + + if (topg <= topf) { + gv = cuddT(G); + gnv = cuddE(G); + if (Cudd_IsComplement(g)) { + gv = Cudd_Not(gv); + gnv = Cudd_Not(gnv); + } + } else { + gv = gnv = g; + } + + t = cuddBddAndRecur(manager, fv, gv); + if (t == NULL) return(NULL); + cuddRef(t); + + e = cuddBddAndRecur(manager, fnv, gnv); + if (e == NULL) { + Cudd_IterDerefBdd(manager, t); + return(NULL); + } + cuddRef(e); + + if (t == e) { + r = t; + } else { + if (Cudd_IsComplement(t)) { + r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e)); + if (r == NULL) { + Cudd_IterDerefBdd(manager, t); + Cudd_IterDerefBdd(manager, e); + return(NULL); + } + r = Cudd_Not(r); + } else { + r = cuddUniqueInter(manager,(int)index,t,e); + if (r == NULL) { + Cudd_IterDerefBdd(manager, t); + Cudd_IterDerefBdd(manager, e); + return(NULL); + } + } + } + cuddDeref(e); + cuddDeref(t); + if (F->ref != 1 || G->ref != 1) + cuddCacheInsert2(manager, Cudd_bddAnd, f, g, r); + return(r); + +} /* end of cuddBddAndRecur */ + + +/**Function******************************************************************** + + Synopsis [Implements the recursive step of Cudd_bddXor.] + + Description [Implements the recursive step of Cudd_bddXor by taking + the exclusive OR of two BDDs. Returns a pointer to the result is + successful; NULL otherwise.] + + SideEffects [None] + + SeeAlso [Cudd_bddXor] + +******************************************************************************/ +DdNode * +cuddBddXorRecur( + DdManager * manager, + DdNode * f, + DdNode * g) +{ + DdNode *fv, *fnv, *G, *gv, *gnv; + DdNode *one, *zero, *r, *t, *e; + unsigned int topf, topg, index; + + statLine(manager); + one = DD_ONE(manager); + zero = Cudd_Not(one); + + /* Terminal cases. */ + if (f == g) return(zero); + if (f == Cudd_Not(g)) return(one); + if (f > g) { /* Try to increase cache efficiency and simplify tests. */ + DdNode *tmp = f; + f = g; + g = tmp; + } + if (g == zero) return(f); + if (g == one) return(Cudd_Not(f)); + if (Cudd_IsComplement(f)) { + f = Cudd_Not(f); + g = Cudd_Not(g); + } + /* Now the first argument is regular. */ + if (f == one) return(Cudd_Not(g)); + + /* At this point f and g are not constant. */ + + /* Check cache. */ + r = cuddCacheLookup2(manager, Cudd_bddXor, f, g); + if (r != NULL) return(r); + + /* Here we can skip the use of cuddI, because the operands are known + ** to be non-constant. + */ + topf = manager->perm[f->index]; + G = Cudd_Regular(g); + topg = manager->perm[G->index]; + + /* Compute cofactors. */ + if (topf <= topg) { + index = f->index; + fv = cuddT(f); + fnv = cuddE(f); + } else { + index = G->index; + fv = fnv = f; + } + + if (topg <= topf) { + gv = cuddT(G); + gnv = cuddE(G); + if (Cudd_IsComplement(g)) { + gv = Cudd_Not(gv); + gnv = Cudd_Not(gnv); + } + } else { + gv = gnv = g; + } + + t = cuddBddXorRecur(manager, fv, gv); + if (t == NULL) return(NULL); + cuddRef(t); + + e = cuddBddXorRecur(manager, fnv, gnv); + if (e == NULL) { + Cudd_IterDerefBdd(manager, t); + return(NULL); + } + cuddRef(e); + + if (t == e) { + r = t; + } else { + if (Cudd_IsComplement(t)) { + r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e)); + if (r == NULL) { + Cudd_IterDerefBdd(manager, t); + Cudd_IterDerefBdd(manager, e); + return(NULL); + } + r = Cudd_Not(r); + } else { + r = cuddUniqueInter(manager,(int)index,t,e); + if (r == NULL) { + Cudd_IterDerefBdd(manager, t); + Cudd_IterDerefBdd(manager, e); + return(NULL); + } + } + } + cuddDeref(e); + cuddDeref(t); + cuddCacheInsert2(manager, Cudd_bddXor, f, g, r); + return(r); + +} /* end of cuddBddXorRecur */ + + +/*---------------------------------------------------------------------------*/ +/* Definition of static functions */ +/*---------------------------------------------------------------------------*/ + + +/**Function******************************************************************** + + Synopsis [Replaces variables with constants if possible.] + + Description [This function performs part of the transformation to + standard form by replacing variables with constants if possible.] + + SideEffects [None] + + SeeAlso [bddVarToCanonical bddVarToCanonicalSimple] + +******************************************************************************/ +static void +bddVarToConst( + DdNode * f, + DdNode ** gp, + DdNode ** hp, + DdNode * one) +{ + DdNode *g = *gp; + DdNode *h = *hp; + + if (f == g) { /* ITE(F,F,H) = ITE(F,1,H) = F + H */ + *gp = one; + } else if (f == Cudd_Not(g)) { /* ITE(F,!F,H) = ITE(F,0,H) = !F * H */ + *gp = Cudd_Not(one); + } + if (f == h) { /* ITE(F,G,F) = ITE(F,G,0) = F * G */ + *hp = Cudd_Not(one); + } else if (f == Cudd_Not(h)) { /* ITE(F,G,!F) = ITE(F,G,1) = !F + G */ + *hp = one; + } + +} /* end of bddVarToConst */ + + +/**Function******************************************************************** + + Synopsis [Picks unique member from equiv expressions.] + + Description [Reduces 2 variable expressions to canonical form.] + + SideEffects [None] + + SeeAlso [bddVarToConst bddVarToCanonicalSimple] + +******************************************************************************/ +static int +bddVarToCanonical( + DdManager * dd, + DdNode ** fp, + DdNode ** gp, + DdNode ** hp, + unsigned int * topfp, + unsigned int * topgp, + unsigned int * tophp) +{ + register DdNode *F, *G, *H, *r, *f, *g, *h; + register unsigned int topf, topg, toph; + DdNode *one = dd->one; + int comple, change; + + f = *fp; + g = *gp; + h = *hp; + F = Cudd_Regular(f); + G = Cudd_Regular(g); + H = Cudd_Regular(h); + topf = cuddI(dd,F->index); + topg = cuddI(dd,G->index); + toph = cuddI(dd,H->index); + + change = 0; + + if (G == one) { /* ITE(F,c,H) */ + if ((topf > toph) || (topf == toph && f > h)) { + r = h; + h = f; + f = r; /* ITE(F,1,H) = ITE(H,1,F) */ + if (g != one) { /* g == zero */ + f = Cudd_Not(f); /* ITE(F,0,H) = ITE(!H,0,!F) */ + h = Cudd_Not(h); + } + change = 1; + } + } else if (H == one) { /* ITE(F,G,c) */ + if ((topf > topg) || (topf == topg && f > g)) { + r = g; + g = f; + f = r; /* ITE(F,G,0) = ITE(G,F,0) */ + if (h == one) { + f = Cudd_Not(f); /* ITE(F,G,1) = ITE(!G,!F,1) */ + g = Cudd_Not(g); + } + change = 1; + } + } else if (g == Cudd_Not(h)) { /* ITE(F,G,!G) = ITE(G,F,!F) */ + if ((topf > topg) || (topf == topg && f > g)) { + r = f; + f = g; + g = r; + h = Cudd_Not(r); + change = 1; + } + } + /* adjust pointers so that the first 2 arguments to ITE are regular */ + if (Cudd_IsComplement(f) != 0) { /* ITE(!F,G,H) = ITE(F,H,G) */ + f = Cudd_Not(f); + r = g; + g = h; + h = r; + change = 1; + } + comple = 0; + if (Cudd_IsComplement(g) != 0) { /* ITE(F,!G,H) = !ITE(F,G,!H) */ + g = Cudd_Not(g); + h = Cudd_Not(h); + change = 1; + comple = 1; + } + if (change != 0) { + *fp = f; + *gp = g; + *hp = h; + } + *topfp = cuddI(dd,f->index); + *topgp = cuddI(dd,g->index); + *tophp = cuddI(dd,Cudd_Regular(h)->index); + + return(comple); + +} /* end of bddVarToCanonical */ + + +/**Function******************************************************************** + + Synopsis [Picks unique member from equiv expressions.] + + Description [Makes sure the first two pointers are regular. This + mat require the complementation of the result, which is signaled by + returning 1 instead of 0. This function is simpler than the general + case because it assumes that no two arguments are the same or + complementary, and no argument is constant.] + + SideEffects [None] + + SeeAlso [bddVarToConst bddVarToCanonical] + +******************************************************************************/ +static int +bddVarToCanonicalSimple( + DdManager * dd, + DdNode ** fp, + DdNode ** gp, + DdNode ** hp, + unsigned int * topfp, + unsigned int * topgp, + unsigned int * tophp) +{ + register DdNode *r, *f, *g, *h; + int comple, change; + + f = *fp; + g = *gp; + h = *hp; + + change = 0; + + /* adjust pointers so that the first 2 arguments to ITE are regular */ + if (Cudd_IsComplement(f)) { /* ITE(!F,G,H) = ITE(F,H,G) */ + f = Cudd_Not(f); + r = g; + g = h; + h = r; + change = 1; + } + comple = 0; + if (Cudd_IsComplement(g)) { /* ITE(F,!G,H) = !ITE(F,G,!H) */ + g = Cudd_Not(g); + h = Cudd_Not(h); + change = 1; + comple = 1; + } + if (change) { + *fp = f; + *gp = g; + *hp = h; + } + + /* Here we can skip the use of cuddI, because the operands are known + ** to be non-constant. + */ + *topfp = dd->perm[f->index]; + *topgp = dd->perm[g->index]; + *tophp = dd->perm[Cudd_Regular(h)->index]; + + return(comple); + +} /* end of bddVarToCanonicalSimple */ + |