Version abc70930

1 files changed, 0 insertions, 1137 deletions

diff --git a/src/bdd/cudd/cuddZddSetop.c b/src/bdd/cudd/cuddZddSetop.c
deleted file mode 100644
index f1bd72f3..00000000
--- a/src/bdd/cudd/cuddZddSetop.c
+++ /dev/null
@@ -1,1137 +0,0 @@
-/**CFile***********************************************************************
-
-  FileName    [cuddZddSetop.c]
-
-  PackageName [cudd]
-
-  Synopsis    [Set operations on ZDDs.]
-
-  Description [External procedures included in this module:
-            <ul>
-            <li> Cudd_zddIte()
-            <li> Cudd_zddUnion()
-            <li> Cudd_zddIntersect()
-            <li> Cudd_zddDiff()
-            <li> Cudd_zddDiffConst()
-            <li> Cudd_zddSubset1()
-            <li> Cudd_zddSubset0()
-            <li> Cudd_zddChange()
-            </ul>
-           Internal procedures included in this module:
-            <ul>
-            <li> cuddZddIte()
-            <li> cuddZddUnion()
-            <li> cuddZddIntersect()
-            <li> cuddZddDiff()
-            <li> cuddZddChangeAux()
-            <li> cuddZddSubset1()
-            <li> cuddZddSubset0()
-            </ul>
-           Static procedures included in this module:
-            <ul>
-            <li> zdd_subset1_aux()
-            <li> zdd_subset0_aux()
-            <li> zddVarToConst()
-            </ul>
-          ]
-
-  SeeAlso     []
-
-  Author      [Hyong-Kyoon Shin, In-Ho Moon]
-
-  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: cuddZddSetop.c,v 1.1.1.1 2003/02/24 22:23:54 wjiang Exp $";
-#endif
-
-/*---------------------------------------------------------------------------*/
-/* Macro declarations                                                        */
-/*---------------------------------------------------------------------------*/
-
-
-/**AutomaticStart*************************************************************/
-
-/*---------------------------------------------------------------------------*/
-/* Static function prototypes                                                */
-/*---------------------------------------------------------------------------*/
-
-static DdNode * zdd_subset1_aux ARGS((DdManager *zdd, DdNode *P, DdNode *zvar));
-static DdNode * zdd_subset0_aux ARGS((DdManager *zdd, DdNode *P, DdNode *zvar));
-static void zddVarToConst ARGS((DdNode *f, DdNode **gp, DdNode **hp, DdNode *base, DdNode *empty));
-
-/**AutomaticEnd***************************************************************/
-
-
-/*---------------------------------------------------------------------------*/
-/* Definition of exported functions                                          */
-/*---------------------------------------------------------------------------*/
-
-
-/**Function********************************************************************
-
-  Synopsis [Computes the ITE of three ZDDs.]
-
-  Description [Computes the ITE of three ZDDs. Returns a pointer to the
-  result if successful; NULL otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     []
-
-******************************************************************************/
-DdNode *
-Cudd_zddIte(
-  DdManager * dd,
-  DdNode * f,
-  DdNode * g,
-  DdNode * h)
-{
-    DdNode *res;
-
-    do {
-    dd->reordered = 0;
-    res = cuddZddIte(dd, f, g, h);
-    } while (dd->reordered == 1);
-    return(res);
-
-} /* end of Cudd_zddIte */
-
-
-/**Function********************************************************************
-
-  Synopsis [Computes the union of two ZDDs.]
-
-  Description [Computes the union of two ZDDs. Returns a pointer to the
-  result if successful; NULL otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     []
-
-******************************************************************************/
-DdNode *
-Cudd_zddUnion(
-  DdManager * dd,
-  DdNode * P,
-  DdNode * Q)
-{
-    DdNode *res;
-
-    do {
-    dd->reordered = 0;
-    res = cuddZddUnion(dd, P, Q);
-    } while (dd->reordered == 1);
-    return(res);
-
-} /* end of Cudd_zddUnion */
-
-
-/**Function********************************************************************
-
-  Synopsis [Computes the intersection of two ZDDs.]
-
-  Description [Computes the intersection of two ZDDs. Returns a pointer to
-  the result if successful; NULL otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     []
-
-******************************************************************************/
-DdNode *
-Cudd_zddIntersect(
-  DdManager * dd,
-  DdNode * P,
-  DdNode * Q)
-{
-    DdNode *res;
-
-    do {
-    dd->reordered = 0;
-    res = cuddZddIntersect(dd, P, Q);
-    } while (dd->reordered == 1);
-    return(res);
-
-} /* end of Cudd_zddIntersect */
-
-
-/**Function********************************************************************
-
-  Synopsis [Computes the difference of two ZDDs.]
-
-  Description [Computes the difference of two ZDDs. Returns a pointer to the
-  result if successful; NULL otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_zddDiffConst]
-
-******************************************************************************/
-DdNode *
-Cudd_zddDiff(
-  DdManager * dd,
-  DdNode * P,
-  DdNode * Q)
-{
-    DdNode *res;
-
-    do {
-    dd->reordered = 0;
-    res = cuddZddDiff(dd, P, Q);
-    } while (dd->reordered == 1);
-    return(res);
-
-} /* end of Cudd_zddDiff */
-
-
-/**Function********************************************************************
-
-  Synopsis [Performs the inclusion test for ZDDs (P implies Q).]
-
-  Description [Inclusion test for ZDDs (P implies Q). No new nodes are
-  generated by this procedure. Returns empty if true;
-  a valid pointer different from empty or DD_NON_CONSTANT otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_zddDiff]
-
-******************************************************************************/
-DdNode *
-Cudd_zddDiffConst(
-  DdManager * zdd,
-  DdNode * P,
-  DdNode * Q)
-{
-    int        p_top, q_top;
-    DdNode    *empty = DD_ZERO(zdd), *t, *res;
-    DdManager    *table = zdd;
-
-    statLine(zdd);
-    if (P == empty)
-    return(empty);
-    if (Q == empty)
-    return(P);
-    if (P == Q)
-    return(empty);
-
-    /* Check cache.  The cache is shared by cuddZddDiff(). */
-    res = cuddCacheLookup2Zdd(table, cuddZddDiff, P, Q);
-    if (res != NULL)
-    return(res);
-
-    if (cuddIsConstant(P))
-    p_top = P->index;
-    else
-    p_top = zdd->permZ[P->index];
-    if (cuddIsConstant(Q))
-    q_top = Q->index;
-    else
-    q_top = zdd->permZ[Q->index];
-    if (p_top < q_top) {
-    res = DD_NON_CONSTANT;
-    } else if (p_top > q_top) {
-    res = Cudd_zddDiffConst(zdd, P, cuddE(Q));
-    } else {
-    t = Cudd_zddDiffConst(zdd, cuddT(P), cuddT(Q));
-    if (t != empty)
-        res = DD_NON_CONSTANT;
-    else
-        res = Cudd_zddDiffConst(zdd, cuddE(P), cuddE(Q));
-    }
-
-    cuddCacheInsert2(table, cuddZddDiff, P, Q, res);
-
-    return(res);
-
-} /* end of Cudd_zddDiffConst */
-
-
-/**Function********************************************************************
-
-  Synopsis [Computes the positive cofactor of a ZDD w.r.t. a variable.]
-
-  Description [Computes the positive cofactor of a ZDD w.r.t. a
-  variable. In terms of combinations, the result is the set of all
-  combinations in which the variable is asserted. Returns a pointer to
-  the result if successful; NULL otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_zddSubset0]
-
-******************************************************************************/
-DdNode *
-Cudd_zddSubset1(
-  DdManager * dd,
-  DdNode * P,
-  int  var)
-{
-    DdNode    *r;
-
-    do {
-    dd->reordered = 0;
-    r = cuddZddSubset1(dd, P, var);
-    } while (dd->reordered == 1);
-
-    return(r);
-
-} /* end of Cudd_zddSubset1 */
-
-
-/**Function********************************************************************
-
-  Synopsis [Computes the negative cofactor of a ZDD w.r.t. a variable.]
-
-  Description [Computes the negative cofactor of a ZDD w.r.t. a
-  variable. In terms of combinations, the result is the set of all
-  combinations in which the variable is negated. Returns a pointer to
-  the result if successful; NULL otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_zddSubset1]
-
-******************************************************************************/
-DdNode *
-Cudd_zddSubset0(
-  DdManager * dd,
-  DdNode * P,
-  int  var)
-{
-    DdNode    *r;
-
-    do {
-    dd->reordered = 0;
-    r = cuddZddSubset0(dd, P, var);
-    } while (dd->reordered == 1);
-
-    return(r);
-
-} /* end of Cudd_zddSubset0 */
-
-
-/**Function********************************************************************
-
-  Synopsis [Substitutes a variable with its complement in a ZDD.]
-
-  Description [Substitutes a variable with its complement in a ZDD.
-  returns a pointer to the result if successful; NULL otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     []
-
-******************************************************************************/
-DdNode *
-Cudd_zddChange(
-  DdManager * dd,
-  DdNode * P,
-  int  var)
-{
-    DdNode    *res;
-
-    if ((unsigned int) var >= CUDD_MAXINDEX - 1) return(NULL);
-    
-    do {
-    dd->reordered = 0;
-    res = cuddZddChange(dd, P, var);
-    } while (dd->reordered == 1);
-    return(res);
-
-} /* end of Cudd_zddChange */
-
-
-/*---------------------------------------------------------------------------*/
-/* Definition of internal functions                                          */
-/*---------------------------------------------------------------------------*/
-
-
-/**Function********************************************************************
-
-  Synopsis    [Performs the recursive step of Cudd_zddIte.]
-
-  Description []
-
-  SideEffects [None]
-
-  SeeAlso     []
-
-******************************************************************************/
-DdNode *
-cuddZddIte(
-  DdManager * dd,
-  DdNode * f,
-  DdNode * g,
-  DdNode * h)
-{
-    DdNode *tautology, *empty;
-    DdNode *r,*Gv,*Gvn,*Hv,*Hvn,*t,*e;
-    unsigned int topf,topg,toph,v,top;
-    int index;
-
-    statLine(dd);
-    /* Trivial cases. */
-    /* One variable cases. */
-    if (f == (empty = DD_ZERO(dd))) {    /* ITE(0,G,H) = H */
-    return(h);
-    }
-    topf = cuddIZ(dd,f->index);
-    topg = cuddIZ(dd,g->index);
-    toph = cuddIZ(dd,h->index);
-    v = ddMin(topg,toph);
-    top  = ddMin(topf,v);
-
-    tautology = (top == CUDD_MAXINDEX) ? DD_ONE(dd) : dd->univ[top];
-    if (f == tautology) {            /* ITE(1,G,H) = G */
-        return(g);
-    }
-
-    /* From now on, f is known to not be a constant. */
-    zddVarToConst(f,&g,&h,tautology,empty);
-
-    /* Check remaining one variable cases. */
-    if (g == h) {            /* ITE(F,G,G) = G */
-    return(g);
-    }
-
-    if (g == tautology) {            /* ITE(F,1,0) = F */
-    if (h == empty) return(f);
-    }
-
-    /* Check cache. */
-    r = cuddCacheLookupZdd(dd,DD_ZDD_ITE_TAG,f,g,h);
-    if (r != NULL) {
-    return(r);
-    }
-
-    /* Recompute these because they may have changed in zddVarToConst. */
-    topg = cuddIZ(dd,g->index);
-    toph = cuddIZ(dd,h->index);
-    v = ddMin(topg,toph);
-
-    if (topf < v) {
-    r = cuddZddIte(dd,cuddE(f),g,h);
-    if (r == NULL) return(NULL);
-    } else if (topf > v) {
-    if (topg > v) {
-        Gvn = g;
-        index = h->index;
-    } else {
-        Gvn = cuddE(g);
-        index = g->index;
-    }
-    if (toph > v) {
-        Hv = empty; Hvn = h;
-    } else {
-        Hv = cuddT(h); Hvn = cuddE(h);
-    }
-    e = cuddZddIte(dd,f,Gvn,Hvn);
-    if (e == NULL) return(NULL);
-    cuddRef(e);
-    r = cuddZddGetNode(dd,index,Hv,e);
-    if (r == NULL) {
-        Cudd_RecursiveDerefZdd(dd,e);
-        return(NULL);
-    }
-    cuddDeref(e);
-    } else {
-    index = f->index;
-    if (topg > v) {
-        Gv = empty; Gvn = g;
-    } else {
-        Gv = cuddT(g); Gvn = cuddE(g);
-    }
-    if (toph > v) {
-        Hv = empty; Hvn = h;
-    } else {
-        Hv = cuddT(h); Hvn = cuddE(h);
-    }
-    e = cuddZddIte(dd,cuddE(f),Gvn,Hvn);
-    if (e == NULL) return(NULL);
-    cuddRef(e);
-    t = cuddZddIte(dd,cuddT(f),Gv,Hv);
-    if (t == NULL) {
-        Cudd_RecursiveDerefZdd(dd,e);
-        return(NULL);
-    }
-    cuddRef(t);
-    r = cuddZddGetNode(dd,index,t,e);
-    if (r == NULL) {
-        Cudd_RecursiveDerefZdd(dd,e);
-        Cudd_RecursiveDerefZdd(dd,t);
-        return(NULL);
-    }
-    cuddDeref(t);
-    cuddDeref(e);
-    }
-
-    cuddCacheInsert(dd,DD_ZDD_ITE_TAG,f,g,h,r);
-
-    return(r);
-
-} /* end of cuddZddIte */
-
-
-/**Function********************************************************************
-
-  Synopsis [Performs the recursive step of Cudd_zddUnion.]
-
-  Description []
-
-  SideEffects [None]
-
-  SeeAlso     []
-
-******************************************************************************/
-DdNode *
-cuddZddUnion(
-  DdManager * zdd,
-  DdNode * P,
-  DdNode * Q)
-{
-    int        p_top, q_top;
-    DdNode    *empty = DD_ZERO(zdd), *t, *e, *res;
-    DdManager    *table = zdd;
-
-    statLine(zdd);
-    if (P == empty)
-    return(Q);
-    if (Q == empty)
-    return(P);
-    if (P == Q)
-    return(P);
-
-    /* Check cache */
-    res = cuddCacheLookup2Zdd(table, cuddZddUnion, P, Q);
-    if (res != NULL)
-    return(res);
-
-    if (cuddIsConstant(P))
-    p_top = P->index;
-    else
-    p_top = zdd->permZ[P->index];
-    if (cuddIsConstant(Q))
-    q_top = Q->index;
-    else
-    q_top = zdd->permZ[Q->index];
-    if (p_top < q_top) {
-    e = cuddZddUnion(zdd, cuddE(P), Q);
-    if (e == NULL) return (NULL);
-    cuddRef(e);
-    res = cuddZddGetNode(zdd, P->index, cuddT(P), e);
-    if (res == NULL) {
-        Cudd_RecursiveDerefZdd(table, e);
-        return(NULL);
-    }
-    cuddDeref(e);
-    } else if (p_top > q_top) {
-    e = cuddZddUnion(zdd, P, cuddE(Q));
-    if (e == NULL) return(NULL);
-    cuddRef(e);
-    res = cuddZddGetNode(zdd, Q->index, cuddT(Q), e);
-    if (res == NULL) {
-        Cudd_RecursiveDerefZdd(table, e);
-        return(NULL);
-    }
-    cuddDeref(e);
-    } else {
-    t = cuddZddUnion(zdd, cuddT(P), cuddT(Q));
-    if (t == NULL) return(NULL);
-    cuddRef(t);
-    e = cuddZddUnion(zdd, cuddE(P), cuddE(Q));
-    if (e == NULL) {
-        Cudd_RecursiveDerefZdd(table, t);
-        return(NULL);
-    }
-    cuddRef(e);
-    res = cuddZddGetNode(zdd, P->index, t, e);
-    if (res == NULL) {
-        Cudd_RecursiveDerefZdd(table, t);
-        Cudd_RecursiveDerefZdd(table, e);
-        return(NULL);
-    }
-    cuddDeref(t);
-    cuddDeref(e);
-    }
-
-    cuddCacheInsert2(table, cuddZddUnion, P, Q, res);
-
-    return(res);
-
-} /* end of cuddZddUnion */
-
-
-/**Function********************************************************************
-
-  Synopsis [Performs the recursive step of Cudd_zddIntersect.]
-
-  Description []
-
-  SideEffects [None]
-
-  SeeAlso     []
-
-******************************************************************************/
-DdNode *
-cuddZddIntersect(
-  DdManager * zdd,
-  DdNode * P,
-  DdNode * Q)
-{
-    int        p_top, q_top;
-    DdNode    *empty = DD_ZERO(zdd), *t, *e, *res;
-    DdManager    *table = zdd;
-
-    statLine(zdd);
-    if (P == empty)
-    return(empty);
-    if (Q == empty)
-    return(empty);
-    if (P == Q)
-    return(P);
-
-    /* Check cache. */
-    res = cuddCacheLookup2Zdd(table, cuddZddIntersect, P, Q);
-    if (res != NULL)
-    return(res);
-
-    if (cuddIsConstant(P))
-    p_top = P->index;
-    else
-    p_top = zdd->permZ[P->index];
-    if (cuddIsConstant(Q))
-    q_top = Q->index;
-    else
-    q_top = zdd->permZ[Q->index];
-    if (p_top < q_top) {
-    res = cuddZddIntersect(zdd, cuddE(P), Q);
-    if (res == NULL) return(NULL);
-    } else if (p_top > q_top) {
-    res = cuddZddIntersect(zdd, P, cuddE(Q));
-    if (res == NULL) return(NULL);
-    } else {
-    t = cuddZddIntersect(zdd, cuddT(P), cuddT(Q));
-    if (t == NULL) return(NULL);
-    cuddRef(t);
-    e = cuddZddIntersect(zdd, cuddE(P), cuddE(Q));
-    if (e == NULL) {
-        Cudd_RecursiveDerefZdd(table, t);
-        return(NULL);
-    }
-    cuddRef(e);
-    res = cuddZddGetNode(zdd, P->index, t, e);
-    if (res == NULL) {
-        Cudd_RecursiveDerefZdd(table, t);
-        Cudd_RecursiveDerefZdd(table, e);
-        return(NULL);
-    }
-    cuddDeref(t);
-    cuddDeref(e);
-    }
-
-    cuddCacheInsert2(table, cuddZddIntersect, P, Q, res);
-
-    return(res);
-
-} /* end of cuddZddIntersect */
-
-
-/**Function********************************************************************
-
-  Synopsis [Performs the recursive step of Cudd_zddDiff.]
-
-  Description []
-
-  SideEffects [None]
-
-  SeeAlso     []
-
-******************************************************************************/
-DdNode *
-cuddZddDiff(
-  DdManager * zdd,
-  DdNode * P,
-  DdNode * Q)
-{
-    int        p_top, q_top;
-    DdNode    *empty = DD_ZERO(zdd), *t, *e, *res;
-    DdManager    *table = zdd;
-
-    statLine(zdd);
-    if (P == empty)
-    return(empty);
-    if (Q == empty)
-    return(P);
-    if (P == Q)
-    return(empty);
-
-    /* Check cache.  The cache is shared by Cudd_zddDiffConst(). */
-    res = cuddCacheLookup2Zdd(table, cuddZddDiff, P, Q);
-    if (res != NULL && res != DD_NON_CONSTANT)
-    return(res);
-
-    if (cuddIsConstant(P))
-    p_top = P->index;
-    else
-    p_top = zdd->permZ[P->index];
-    if (cuddIsConstant(Q))
-    q_top = Q->index;
-    else
-    q_top = zdd->permZ[Q->index];
-    if (p_top < q_top) {
-    e = cuddZddDiff(zdd, cuddE(P), Q);
-    if (e == NULL) return(NULL);
-    cuddRef(e);
-    res = cuddZddGetNode(zdd, P->index, cuddT(P), e);
-    if (res == NULL) {
-        Cudd_RecursiveDerefZdd(table, e);
-        return(NULL);
-    }
-    cuddDeref(e);
-    } else if (p_top > q_top) {
-    res = cuddZddDiff(zdd, P, cuddE(Q));
-    if (res == NULL) return(NULL);
-    } else {
-    t = cuddZddDiff(zdd, cuddT(P), cuddT(Q));
-    if (t == NULL) return(NULL);
-    cuddRef(t);
-    e = cuddZddDiff(zdd, cuddE(P), cuddE(Q));
-    if (e == NULL) {
-        Cudd_RecursiveDerefZdd(table, t);
-        return(NULL);
-    }
-    cuddRef(e);
-    res = cuddZddGetNode(zdd, P->index, t, e);
-    if (res == NULL) {
-        Cudd_RecursiveDerefZdd(table, t);
-        Cudd_RecursiveDerefZdd(table, e);
-        return(NULL);
-    }
-    cuddDeref(t);
-    cuddDeref(e);
-    }
-
-    cuddCacheInsert2(table, cuddZddDiff, P, Q, res);
-
-    return(res);
-
-} /* end of cuddZddDiff */
-
-
-/**Function********************************************************************
-
-  Synopsis [Performs the recursive step of Cudd_zddChange.]
-
-  Description []
-
-  SideEffects [None]
-
-  SeeAlso     []
-
-******************************************************************************/
-DdNode *
-cuddZddChangeAux(
-  DdManager * zdd,
-  DdNode * P,
-  DdNode * zvar)
-{
-    int        top_var, level;
-    DdNode    *res, *t, *e;
-    DdNode    *base = DD_ONE(zdd);
-    DdNode    *empty = DD_ZERO(zdd);
-
-    statLine(zdd);
-    if (P == empty)
-    return(empty);
-    if (P == base)
-    return(zvar);
-
-    /* Check cache. */
-    res = cuddCacheLookup2Zdd(zdd, cuddZddChangeAux, P, zvar);
-    if (res != NULL)
-    return(res);
-
-    top_var = zdd->permZ[P->index];
-    level = zdd->permZ[zvar->index];
-
-    if (top_var > level) {
-    res = cuddZddGetNode(zdd, zvar->index, P, DD_ZERO(zdd));
-    if (res == NULL) return(NULL);
-    } else if (top_var == level) {
-    res = cuddZddGetNode(zdd, zvar->index, cuddE(P), cuddT(P));
-    if (res == NULL) return(NULL);
-    } else {
-    t = cuddZddChangeAux(zdd, cuddT(P), zvar);
-    if (t == NULL) return(NULL);
-    cuddRef(t);
-    e = cuddZddChangeAux(zdd, cuddE(P), zvar);
-    if (e == NULL) {
-        Cudd_RecursiveDerefZdd(zdd, t);
-        return(NULL);
-    }
-    cuddRef(e);
-    res = cuddZddGetNode(zdd, P->index, t, e);
-    if (res == NULL) {
-        Cudd_RecursiveDerefZdd(zdd, t);
-        Cudd_RecursiveDerefZdd(zdd, e);
-        return(NULL);
-    }
-    cuddDeref(t);
-    cuddDeref(e);
-    }
-
-    cuddCacheInsert2(zdd, cuddZddChangeAux, P, zvar, res);
-
-    return(res);
-
-} /* end of cuddZddChangeAux */
-
-
-/**Function********************************************************************
-
-  Synopsis [Computes the positive cofactor of a ZDD w.r.t. a variable.]
-
-  Description [Computes the positive cofactor of a ZDD w.r.t. a
-  variable. In terms of combinations, the result is the set of all
-  combinations in which the variable is asserted. Returns a pointer to
-  the result if successful; NULL otherwise. cuddZddSubset1 performs
-  the same function as Cudd_zddSubset1, but does not restart if
-  reordering has taken place. Therefore it can be called from within a
-  recursive procedure.]
-
-  SideEffects [None]
-
-  SeeAlso     [cuddZddSubset0 Cudd_zddSubset1]
-
-******************************************************************************/
-DdNode *
-cuddZddSubset1(
-  DdManager * dd,
-  DdNode * P,
-  int  var)
-{
-    DdNode    *zvar, *r;
-    DdNode    *base, *empty;
-
-    base = DD_ONE(dd);
-    empty = DD_ZERO(dd);
-
-    zvar = cuddUniqueInterZdd(dd, var, base, empty);
-    if (zvar == NULL) {
-    return(NULL);
-    } else {
-    cuddRef(zvar);
-    r = zdd_subset1_aux(dd, P, zvar);
-    if (r == NULL) {
-        Cudd_RecursiveDerefZdd(dd, zvar);
-        return(NULL);
-    }
-    cuddRef(r);
-    Cudd_RecursiveDerefZdd(dd, zvar);
-    }
-
-    cuddDeref(r);
-    return(r);
-
-} /* end of cuddZddSubset1 */
-
-
-/**Function********************************************************************
-
-  Synopsis [Computes the negative cofactor of a ZDD w.r.t. a variable.]
-
-  Description [Computes the negative cofactor of a ZDD w.r.t. a
-  variable. In terms of combinations, the result is the set of all
-  combinations in which the variable is negated. Returns a pointer to
-  the result if successful; NULL otherwise. cuddZddSubset0 performs
-  the same function as Cudd_zddSubset0, but does not restart if
-  reordering has taken place. Therefore it can be called from within a
-  recursive procedure.]
-
-  SideEffects [None]
-
-  SeeAlso     [cuddZddSubset1 Cudd_zddSubset0]
-
-******************************************************************************/
-DdNode *
-cuddZddSubset0(
-  DdManager * dd,
-  DdNode * P,
-  int  var)
-{
-    DdNode    *zvar, *r;
-    DdNode    *base, *empty;
-
-    base = DD_ONE(dd);
-    empty = DD_ZERO(dd);
-
-    zvar = cuddUniqueInterZdd(dd, var, base, empty);
-    if (zvar == NULL) {
-    return(NULL);
-    } else {
-    cuddRef(zvar);
-    r = zdd_subset0_aux(dd, P, zvar);
-    if (r == NULL) {
-        Cudd_RecursiveDerefZdd(dd, zvar);
-        return(NULL);
-    }
-    cuddRef(r);
-    Cudd_RecursiveDerefZdd(dd, zvar);
-    }
-
-    cuddDeref(r);
-    return(r);
-
-} /* end of cuddZddSubset0 */
-
-
-/**Function********************************************************************
-
-  Synopsis [Substitutes a variable with its complement in a ZDD.]
-
-  Description [Substitutes a variable with its complement in a ZDD.
-  returns a pointer to the result if successful; NULL
-  otherwise. cuddZddChange performs the same function as
-  Cudd_zddChange, but does not restart if reordering has taken
-  place. Therefore it can be called from within a recursive
-  procedure.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_zddChange]
-
-******************************************************************************/
-DdNode *
-cuddZddChange(
-  DdManager * dd,
-  DdNode * P,
-  int  var)
-{
-    DdNode    *zvar, *res;
-
-    zvar = cuddUniqueInterZdd(dd, var, DD_ONE(dd), DD_ZERO(dd));
-    if (zvar == NULL) return(NULL);
-    cuddRef(zvar);
-
-    res = cuddZddChangeAux(dd, P, zvar);
-    if (res == NULL) {
-    Cudd_RecursiveDerefZdd(dd,zvar);
-    return(NULL);
-    }
-    cuddRef(res);
-    Cudd_RecursiveDerefZdd(dd,zvar);
-    cuddDeref(res);
-    return(res);
-
-} /* end of cuddZddChange */
-
-
-/*---------------------------------------------------------------------------*/
-/* Definition of static functions                                            */
-/*---------------------------------------------------------------------------*/
-
-
-/**Function********************************************************************
-
-  Synopsis [Performs the recursive step of Cudd_zddSubset1.]
-
-  Description []
-
-  SideEffects [None]
-
-  SeeAlso     []
-
-******************************************************************************/
-static DdNode *
-zdd_subset1_aux(
-  DdManager * zdd,
-  DdNode * P,
-  DdNode * zvar)
-{
-    int        top_var, level;
-    DdNode    *res, *t, *e;
-    DdNode    *base, *empty;
-
-    statLine(zdd);
-    base = DD_ONE(zdd);
-    empty = DD_ZERO(zdd);
-
-    /* Check cache. */
-    res = cuddCacheLookup2Zdd(zdd, zdd_subset1_aux, P, zvar);
-    if (res != NULL)
-    return(res);
-
-    if (cuddIsConstant(P)) {
-    res = empty;
-    cuddCacheInsert2(zdd, zdd_subset1_aux, P, zvar, res);
-    return(res);
-    }
-
-    top_var = zdd->permZ[P->index];
-    level = zdd->permZ[zvar->index];
-
-    if (top_var > level) {
-        res = empty;
-    } else if (top_var == level) {
-    res = cuddT(P);
-    } else {
-        t = zdd_subset1_aux(zdd, cuddT(P), zvar);
-    if (t == NULL) return(NULL);
-    cuddRef(t);
-        e = zdd_subset1_aux(zdd, cuddE(P), zvar);
-    if (e == NULL) {
-        Cudd_RecursiveDerefZdd(zdd, t);
-        return(NULL);
-    }
-    cuddRef(e);
-        res = cuddZddGetNode(zdd, P->index, t, e);
-    if (res == NULL) {
-        Cudd_RecursiveDerefZdd(zdd, t);
-        Cudd_RecursiveDerefZdd(zdd, e);
-        return(NULL);
-    }
-    cuddDeref(t);
-    cuddDeref(e);
-    }
-
-    cuddCacheInsert2(zdd, zdd_subset1_aux, P, zvar, res);
-
-    return(res);
-
-} /* end of zdd_subset1_aux */
-
-
-/**Function********************************************************************
-
-  Synopsis [Performs the recursive step of Cudd_zddSubset0.]
-
-  Description []
-
-  SideEffects [None]
-
-  SeeAlso     []
-
-******************************************************************************/
-static DdNode *
-zdd_subset0_aux(
-  DdManager * zdd,
-  DdNode * P,
-  DdNode * zvar)
-{
-    int        top_var, level;
-    DdNode    *res, *t, *e;
-    DdNode    *base, *empty;
-
-    statLine(zdd);
-    base = DD_ONE(zdd);
-    empty = DD_ZERO(zdd);
-
-    /* Check cache. */
-    res = cuddCacheLookup2Zdd(zdd, zdd_subset0_aux, P, zvar);
-    if (res != NULL)
-    return(res);
-
-    if (cuddIsConstant(P)) {
-    res = P;
-    cuddCacheInsert2(zdd, zdd_subset0_aux, P, zvar, res);
-    return(res);
-    }
-
-    top_var = zdd->permZ[P->index];
-    level = zdd->permZ[zvar->index];
-
-    if (top_var > level) {
-        res = P;
-    }
-    else if (top_var == level) {
-        res = cuddE(P);
-    }
-    else {
-        t = zdd_subset0_aux(zdd, cuddT(P), zvar);
-    if (t == NULL) return(NULL);
-    cuddRef(t);
-        e = zdd_subset0_aux(zdd, cuddE(P), zvar);
-    if (e == NULL) {
-        Cudd_RecursiveDerefZdd(zdd, t);
-        return(NULL);
-    }
-    cuddRef(e);
-        res = cuddZddGetNode(zdd, P->index, t, e);
-    if (res == NULL) {
-        Cudd_RecursiveDerefZdd(zdd, t);
-        Cudd_RecursiveDerefZdd(zdd, e);
-        return(NULL);
-    }
-    cuddDeref(t);
-    cuddDeref(e);
-    }
-
-    cuddCacheInsert2(zdd, zdd_subset0_aux, P, zvar, res);
-
-    return(res);
-
-} /* end of zdd_subset0_aux */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Replaces variables with constants if possible (part of
-  canonical form).]
-
-  Description []
-
-  SideEffects [None]
-
-  SeeAlso     []
-
-******************************************************************************/
-static void
-zddVarToConst(
-  DdNode * f,
-  DdNode ** gp,
-  DdNode ** hp,
-  DdNode * base,
-  DdNode * empty)
-{
-    DdNode *g = *gp;
-    DdNode *h = *hp;
-
-    if (f == g) { /* ITE(F,F,H) = ITE(F,1,H) = F + H */
-    *gp = base;
-    }
-
-    if (f == h) { /* ITE(F,G,F) = ITE(F,G,0) = F * G */
-    *hp = empty;
-    }
-
-} /* end of zddVarToConst */
-