Version abc70930

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 */
-