diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2007-09-30 08:01:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2007-09-30 08:01:00 -0700 |
commit | e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7 (patch) | |
tree | de3ffe87c3e17950351e3b7d97fa18318bd5ea9a /src/bdd/cudd/cuddBddIte.c | |
parent | 7d7e60f2dc84393cd4c5db22d2eaf7b1fb1a79b2 (diff) | |
download | abc-e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7.tar.gz abc-e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7.tar.bz2 abc-e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7.zip |
Version abc70930
Diffstat (limited to 'src/bdd/cudd/cuddBddIte.c')
-rw-r--r-- | src/bdd/cudd/cuddBddIte.c | 1254 |
1 files changed, 0 insertions, 1254 deletions
diff --git a/src/bdd/cudd/cuddBddIte.c b/src/bdd/cudd/cuddBddIte.c deleted file mode 100644 index b44e40de..00000000 --- a/src/bdd/cudd/cuddBddIte.c +++ /dev/null @@ -1,1254 +0,0 @@ -/**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_hack.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 */ - |