Version abc70930

1 files changed, 0 insertions, 1968 deletions

diff --git a/src/bdd/cudd/cuddGenCof.c b/src/bdd/cudd/cuddGenCof.c
deleted file mode 100644
index 142ee27e..00000000
--- a/src/bdd/cudd/cuddGenCof.c
+++ /dev/null
@@ -1,1968 +0,0 @@
-/**CFile***********************************************************************
-
-  FileName    [cuddGenCof.c]
-
-  PackageName [cudd]
-
-  Synopsis    [Generalized cofactors for BDDs and ADDs.]
-
-  Description [External procedures included in this module:
-        <ul>
-        <li> Cudd_bddConstrain()
-        <li> Cudd_bddRestrict()
-        <li> Cudd_addConstrain()
-        <li> Cudd_bddConstrainDecomp()
-        <li> Cudd_addRestrict()
-        <li> Cudd_bddCharToVect()
-        <li> Cudd_bddLICompaction()
-        <li> Cudd_bddSqueeze()
-        <li> Cudd_SubsetCompress()
-        <li> Cudd_SupersetCompress()
-        </ul>
-        Internal procedures included in this module:
-        <ul>
-        <li> cuddBddConstrainRecur()
-        <li> cuddBddRestrictRecur()
-        <li> cuddAddConstrainRecur()
-        <li> cuddAddRestrictRecur()
-        <li> cuddBddLICompaction()
-        </ul>
-        Static procedures included in this module:
-            <ul>
-        <li> cuddBddConstrainDecomp()
-        <li> cuddBddCharToVect()
-        <li> cuddBddLICMarkEdges()
-        <li> cuddBddLICBuildResult()
-        <li> cuddBddSqueeze()
-        </ul>
-        ]
-
-  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                                                     */
-/*---------------------------------------------------------------------------*/
-
-/* Codes for edge markings in Cudd_bddLICompaction.  The codes are defined
-** so that they can be bitwise ORed to implement the code priority scheme.
-*/
-#define DD_LIC_DC 0
-#define DD_LIC_1  1
-#define DD_LIC_0  2
-#define DD_LIC_NL 3
-
-/*---------------------------------------------------------------------------*/
-/* Stucture declarations                                                     */
-/*---------------------------------------------------------------------------*/
-
-
-/*---------------------------------------------------------------------------*/
-/* Type declarations                                                         */
-/*---------------------------------------------------------------------------*/
-
-/* Key for the cache used in the edge marking phase. */
-typedef struct MarkCacheKey {
-    DdNode *f;
-    DdNode *c;
-} MarkCacheKey;
-
-/*---------------------------------------------------------------------------*/
-/* Variable declarations                                                     */
-/*---------------------------------------------------------------------------*/
-
-#ifndef lint
-static char rcsid[] DD_UNUSED = "$Id: cuddGenCof.c,v 1.1.1.1 2003/02/24 22:23:52 wjiang Exp $";
-#endif
-
-/*---------------------------------------------------------------------------*/
-/* Macro declarations                                                        */
-/*---------------------------------------------------------------------------*/
-
-
-/**AutomaticStart*************************************************************/
-
-/*---------------------------------------------------------------------------*/
-/* Static function prototypes                                                */
-/*---------------------------------------------------------------------------*/
-
-static int cuddBddConstrainDecomp ARGS((DdManager *dd, DdNode *f, DdNode **decomp));
-static DdNode * cuddBddCharToVect ARGS((DdManager *dd, DdNode *f, DdNode *x));
-static int cuddBddLICMarkEdges ARGS((DdManager *dd, DdNode *f, DdNode *c, st_table *table, st_table *cache));
-static DdNode * cuddBddLICBuildResult ARGS((DdManager *dd, DdNode *f, st_table *cache, st_table *table));
-static int MarkCacheHash ARGS((char *ptr, int modulus));
-static int MarkCacheCompare ARGS((const char *ptr1, const char *ptr2));
-static enum st_retval MarkCacheCleanUp ARGS((char *key, char *value, char *arg));
-static DdNode * cuddBddSqueeze ARGS((DdManager *dd, DdNode *l, DdNode *u));
-
-/**AutomaticEnd***************************************************************/
-
-
-/*---------------------------------------------------------------------------*/
-/* Definition of exported functions                                          */
-/*---------------------------------------------------------------------------*/
-
-
-/**Function********************************************************************
-
-  Synopsis    [Computes f constrain c.]
-
-  Description [Computes f constrain c (f @ c).
-  Uses a canonical form: (f' @ c) = ( f @ c)'.  (Note: this is not true
-  for c.)  List of special cases:
-    <ul>
-    <li> f @ 0 = 0
-    <li> f @ 1 = f
-    <li> 0 @ c = 0
-    <li> 1 @ c = 1
-    <li> f @ f = 1
-    <li> f @ f'= 0
-    </ul>
-  Returns a pointer to the result if successful; NULL otherwise. Note that if
-  F=(f1,...,fn) and reordering takes place while computing F @ c, then the
-  image restriction property (Img(F,c) = Img(F @ c)) is lost.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_bddRestrict Cudd_addConstrain]
-
-******************************************************************************/
-DdNode *
-Cudd_bddConstrain(
-  DdManager * dd,
-  DdNode * f,
-  DdNode * c)
-{
-    DdNode *res;
-
-    do {
-    dd->reordered = 0;
-    res = cuddBddConstrainRecur(dd,f,c);
-    } while (dd->reordered == 1);
-    return(res);
-
-} /* end of Cudd_bddConstrain */
-
-
-/**Function********************************************************************
-
-  Synopsis [BDD restrict according to Coudert and Madre's algorithm
-  (ICCAD90).]
-
-  Description [BDD restrict according to Coudert and Madre's algorithm
-  (ICCAD90). Returns the restricted BDD if successful; otherwise NULL.
-  If application of restrict results in a BDD larger than the input
-  BDD, the input BDD is returned.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_bddConstrain Cudd_addRestrict]
-
-******************************************************************************/
-DdNode *
-Cudd_bddRestrict(
-  DdManager * dd,
-  DdNode * f,
-  DdNode * c)
-{
-    DdNode *suppF, *suppC, *commonSupport;
-    DdNode *cplus, *res;
-    int retval;
-    int sizeF, sizeRes;
-
-    /* Check terminal cases here to avoid computing supports in trivial cases.
-    ** This also allows us notto check later for the case c == 0, in which
-    ** there is no common support. */
-    if (c == Cudd_Not(DD_ONE(dd))) return(Cudd_Not(DD_ONE(dd)));
-    if (Cudd_IsConstant(f)) return(f);
-    if (f == c) return(DD_ONE(dd));
-    if (f == Cudd_Not(c)) return(Cudd_Not(DD_ONE(dd)));
-
-    /* Check if supports intersect. */
-    retval = Cudd_ClassifySupport(dd,f,c,&commonSupport,&suppF,&suppC);
-    if (retval == 0) {
-    return(NULL);
-    }
-    cuddRef(commonSupport); cuddRef(suppF); cuddRef(suppC);
-    Cudd_IterDerefBdd(dd,suppF);
-
-    if (commonSupport == DD_ONE(dd)) {
-    Cudd_IterDerefBdd(dd,commonSupport);
-    Cudd_IterDerefBdd(dd,suppC);
-    return(f);
-    }
-    Cudd_IterDerefBdd(dd,commonSupport);
-
-    /* Abstract from c the variables that do not appear in f. */
-    cplus = Cudd_bddExistAbstract(dd, c, suppC);
-    if (cplus == NULL) {
-    Cudd_IterDerefBdd(dd,suppC);
-    return(NULL);
-    }
-    cuddRef(cplus);
-    Cudd_IterDerefBdd(dd,suppC);
-
-    do {
-    dd->reordered = 0;
-    res = cuddBddRestrictRecur(dd, f, cplus);
-    } while (dd->reordered == 1);
-    if (res == NULL) {
-    Cudd_IterDerefBdd(dd,cplus);
-    return(NULL);
-    }
-    cuddRef(res);
-    Cudd_IterDerefBdd(dd,cplus);
-    /* Make restric safe by returning the smaller of the input and the
-    ** result. */
-    sizeF = Cudd_DagSize(f);
-    sizeRes = Cudd_DagSize(res);
-    if (sizeF <= sizeRes) {
-    Cudd_IterDerefBdd(dd, res);
-    return(f);
-    } else {
-    cuddDeref(res);
-    return(res);
-    }
-
-} /* end of Cudd_bddRestrict */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Computes f constrain c for ADDs.]
-
-  Description [Computes f constrain c (f @ c), for f an ADD and c a 0-1
-  ADD.  List of special cases:
-    <ul>
-    <li> F @ 0 = 0
-    <li> F @ 1 = F
-    <li> 0 @ c = 0
-    <li> 1 @ c = 1
-    <li> F @ F = 1
-    </ul>
-  Returns a pointer to the result if successful; NULL otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_bddConstrain]
-
-******************************************************************************/
-DdNode *
-Cudd_addConstrain(
-  DdManager * dd,
-  DdNode * f,
-  DdNode * c)
-{
-    DdNode *res;
-
-    do {
-    dd->reordered = 0;
-    res = cuddAddConstrainRecur(dd,f,c);
-    } while (dd->reordered == 1);
-    return(res);
-
-} /* end of Cudd_addConstrain */
-
-
-/**Function********************************************************************
-
-  Synopsis [BDD conjunctive decomposition as in McMillan's CAV96 paper.]
-
-  Description [BDD conjunctive decomposition as in McMillan's CAV96
-  paper.  The decomposition is canonical only for a given variable
-  order. If canonicity is required, variable ordering must be disabled
-  after the decomposition has been computed. Returns an array with one
-  entry for each BDD variable in the manager if successful; otherwise
-  NULL. The components of the solution have their reference counts
-  already incremented (unlike the results of most other functions in
-  the package.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_bddConstrain Cudd_bddExistAbstract]
-
-******************************************************************************/
-DdNode **
-Cudd_bddConstrainDecomp(
-  DdManager * dd,
-  DdNode * f)
-{
-    DdNode **decomp;
-    int res;
-    int i;
-
-    /* Create an initialize decomposition array. */
-    decomp = ALLOC(DdNode *,dd->size);
-    if (decomp == NULL) {
-    dd->errorCode = CUDD_MEMORY_OUT;
-    return(NULL);
-    }
-    for (i = 0; i < dd->size; i++) {
-    decomp[i] = NULL;
-    }
-    do {
-    dd->reordered = 0;
-    /* Clean up the decomposition array in case reordering took place. */
-    for (i = 0; i < dd->size; i++) {
-        if (decomp[i] != NULL) {
-        Cudd_IterDerefBdd(dd, decomp[i]);
-        decomp[i] = NULL;
-        }
-    }
-    res = cuddBddConstrainDecomp(dd,f,decomp);
-    } while (dd->reordered == 1);
-    if (res == 0) {
-    FREE(decomp);
-    return(NULL);
-    }
-    /* Missing components are constant ones. */
-    for (i = 0; i < dd->size; i++) {
-    if (decomp[i] == NULL) {
-        decomp[i] = DD_ONE(dd);
-        cuddRef(decomp[i]);
-    }
-    }
-    return(decomp);
-
-} /* end of Cudd_bddConstrainDecomp */
-
-
-/**Function********************************************************************
-
-  Synopsis [ADD restrict according to Coudert and Madre's algorithm
-  (ICCAD90).]
-
-  Description [ADD restrict according to Coudert and Madre's algorithm
-  (ICCAD90). Returns the restricted ADD if successful; otherwise NULL.
-  If application of restrict results in an ADD larger than the input
-  ADD, the input ADD is returned.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_addConstrain Cudd_bddRestrict]
-
-******************************************************************************/
-DdNode *
-Cudd_addRestrict(
-  DdManager * dd,
-  DdNode * f,
-  DdNode * c)
-{
-    DdNode *supp_f, *supp_c;
-    DdNode *res, *commonSupport;
-    int intersection;
-    int sizeF, sizeRes;
-
-    /* Check if supports intersect. */
-    supp_f = Cudd_Support(dd, f);
-    if (supp_f == NULL) {
-    return(NULL);
-    }
-    cuddRef(supp_f);
-    supp_c = Cudd_Support(dd, c);
-    if (supp_c == NULL) {
-    Cudd_RecursiveDeref(dd,supp_f);
-    return(NULL);
-    }
-    cuddRef(supp_c);
-    commonSupport = Cudd_bddLiteralSetIntersection(dd, supp_f, supp_c);
-    if (commonSupport == NULL) {
-    Cudd_RecursiveDeref(dd,supp_f);
-    Cudd_RecursiveDeref(dd,supp_c);
-    return(NULL);
-    }
-    cuddRef(commonSupport);
-    Cudd_RecursiveDeref(dd,supp_f);
-    Cudd_RecursiveDeref(dd,supp_c);
-    intersection = commonSupport != DD_ONE(dd);
-    Cudd_RecursiveDeref(dd,commonSupport);
-
-    if (intersection) {
-    do {
-        dd->reordered = 0;
-        res = cuddAddRestrictRecur(dd, f, c);
-    } while (dd->reordered == 1);
-    sizeF = Cudd_DagSize(f);
-    sizeRes = Cudd_DagSize(res);
-    if (sizeF <= sizeRes) {
-        cuddRef(res);
-        Cudd_RecursiveDeref(dd, res);
-        return(f);
-    } else {
-        return(res);
-    }
-    } else {
-    return(f);
-    }
-
-} /* end of Cudd_addRestrict */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Computes a vector whose image equals a non-zero function.]
-
-  Description [Computes a vector of BDDs whose image equals a non-zero
-  function.
-  The result depends on the variable order. The i-th component of the vector
-  depends only on the first i variables in the order.  Each BDD in the vector
-  is not larger than the BDD of the given characteristic function.  This
-  function is based on the description of char-to-vect in "Verification of
-  Sequential Machines Using Boolean Functional Vectors" by O. Coudert, C.
-  Berthet and J. C. Madre.
-  Returns a pointer to an array containing the result if successful; NULL
-  otherwise. The size of the array equals the number of variables in the
-  manager. The components of the solution have their reference counts 
-  already incremented (unlike the results of most other functions in 
-  the package.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_bddConstrain]
-
-******************************************************************************/
-DdNode **
-Cudd_bddCharToVect(
-  DdManager * dd,
-  DdNode * f)
-{
-    int i, j;
-    DdNode **vect;
-    DdNode *res = NULL;
-
-    if (f == Cudd_Not(DD_ONE(dd))) return(NULL);
-
-    vect = ALLOC(DdNode *, dd->size);
-    if (vect == NULL) {
-    dd->errorCode = CUDD_MEMORY_OUT;
-    return(NULL);
-    }
-
-    do {
-    dd->reordered = 0;
-    for (i = 0; i < dd->size; i++) {
-        res = cuddBddCharToVect(dd,f,dd->vars[dd->invperm[i]]);
-        if (res == NULL) {
-        /* Clean up the vector array in case reordering took place. */
-        for (j = 0; j < i; j++) {
-            Cudd_IterDerefBdd(dd, vect[dd->invperm[j]]);
-        }
-        break;
-        }
-        cuddRef(res);
-        vect[dd->invperm[i]] = res;
-    }
-    } while (dd->reordered == 1);
-    if (res == NULL) {
-    FREE(vect);
-    return(NULL);
-    }
-    return(vect);
-
-} /* end of Cudd_bddCharToVect */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Performs safe minimization of a BDD.]
-
-  Description [Performs safe minimization of a BDD. Given the BDD
-  <code>f</code> of a function to be minimized and a BDD
-  <code>c</code> representing the care set, Cudd_bddLICompaction
-  produces the BDD of a function that agrees with <code>f</code>
-  wherever <code>c</code> is 1.  Safe minimization means that the size
-  of the result is guaranteed not to exceed the size of
-  <code>f</code>. This function is based on the DAC97 paper by Hong et
-  al..  Returns a pointer to the result if successful; NULL
-  otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_bddRestrict]
-
-******************************************************************************/
-DdNode *
-Cudd_bddLICompaction(
-  DdManager * dd /* manager */,
-  DdNode * f /* function to be minimized */,
-  DdNode * c /* constraint (care set) */)
-{
-    DdNode *res;
-
-    do {
-    dd->reordered = 0;
-    res = cuddBddLICompaction(dd,f,c);
-    } while (dd->reordered == 1);
-    return(res);
-
-} /* end of Cudd_bddLICompaction */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Finds a small BDD in a function interval.]
-
-  Description [Finds a small BDD in a function interval. Given BDDs
-  <code>l</code> and <code>u</code>, representing the lower bound and
-  upper bound of a function interval, Cudd_bddSqueeze produces the BDD
-  of a function within the interval with a small BDD.  Returns a
-  pointer to the result if successful; NULL otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_bddRestrict Cudd_bddLICompaction]
-
-******************************************************************************/
-DdNode *
-Cudd_bddSqueeze(
-  DdManager * dd /* manager */,
-  DdNode * l /* lower bound */,
-  DdNode * u /* upper bound */)
-{
-    DdNode *res;
-    int sizeRes, sizeL, sizeU;
-
-    do {
-    dd->reordered = 0;
-    res = cuddBddSqueeze(dd,l,u);
-    } while (dd->reordered == 1);
-    if (res == NULL) return(NULL);
-    /* We now compare the result with the bounds and return the smallest.
-    ** We first compare to u, so that in case l == 0 and u == 1, we return
-    ** 0 as in other minimization algorithms. */
-    sizeRes = Cudd_DagSize(res);
-    sizeU = Cudd_DagSize(u);
-    if (sizeU <= sizeRes) {
-    cuddRef(res);
-    Cudd_IterDerefBdd(dd,res);
-    res = u;
-    sizeRes = sizeU;
-    }
-    sizeL = Cudd_DagSize(l);
-    if (sizeL <= sizeRes) {
-    cuddRef(res);
-    Cudd_IterDerefBdd(dd,res);
-    res = l;
-    sizeRes = sizeL;
-    }
-    return(res);
-
-} /* end of Cudd_bddSqueeze */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Finds a small BDD that agrees with <code>f</code> over
-  <code>c</code>.]
-
-  Description [Finds a small BDD that agrees with <code>f</code> over
-  <code>c</code>.  Returns a pointer to the result if successful; NULL
-  otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_bddRestrict Cudd_bddLICompaction Cudd_bddSqueeze]
-
-******************************************************************************/
-DdNode *
-Cudd_bddMinimize(
-  DdManager * dd,
-  DdNode * f,
-  DdNode * c)
-{
-    DdNode *cplus, *res;
-
-    if (c == Cudd_Not(DD_ONE(dd))) return(c);
-    if (Cudd_IsConstant(f)) return(f);
-    if (f == c) return(DD_ONE(dd));
-    if (f == Cudd_Not(c)) return(Cudd_Not(DD_ONE(dd)));
-
-    cplus = Cudd_RemapOverApprox(dd,c,0,0,1.0);
-    if (cplus == NULL) return(NULL);
-    cuddRef(cplus);
-    res = Cudd_bddLICompaction(dd,f,cplus);
-    if (res == NULL) {
-    Cudd_IterDerefBdd(dd,cplus);
-    return(NULL);
-    }
-    cuddRef(res);
-    Cudd_IterDerefBdd(dd,cplus);
-    cuddDeref(res);
-    return(res);
-
-} /* end of Cudd_bddMinimize */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Find a dense subset of BDD <code>f</code>.]
-
-  Description [Finds a dense subset of BDD <code>f</code>. Density is
-  the ratio of number of minterms to number of nodes.  Uses several
-  techniques in series. It is more expensive than other subsetting
-  procedures, but often produces better results. See
-  Cudd_SubsetShortPaths for a description of the threshold and nvars
-  parameters.  Returns a pointer to the result if successful; NULL
-  otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_SubsetRemap Cudd_SubsetShortPaths Cudd_SubsetHeavyBranch
-  Cudd_bddSqueeze]
-
-******************************************************************************/
-DdNode *
-Cudd_SubsetCompress(
-  DdManager * dd /* manager */,
-  DdNode * f /* BDD whose subset is sought */,
-  int  nvars /* number of variables in the support of f */,
-  int  threshold /* maximum number of nodes in the subset */)
-{
-    DdNode *res, *tmp1, *tmp2;
-
-    tmp1 = Cudd_SubsetShortPaths(dd, f, nvars, threshold, 0);
-    if (tmp1 == NULL) return(NULL);
-    cuddRef(tmp1);
-    tmp2 = Cudd_RemapUnderApprox(dd,tmp1,nvars,0,1.0);
-    if (tmp2 == NULL) {
-    Cudd_IterDerefBdd(dd,tmp1);
-    return(NULL);
-    }
-    cuddRef(tmp2);
-    Cudd_IterDerefBdd(dd,tmp1);
-    res = Cudd_bddSqueeze(dd,tmp2,f);
-    if (res == NULL) {
-    Cudd_IterDerefBdd(dd,tmp2);
-    return(NULL);
-    }
-    cuddRef(res);
-    Cudd_IterDerefBdd(dd,tmp2);
-    cuddDeref(res);
-    return(res);
-
-} /* end of Cudd_SubsetCompress */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Find a dense superset of BDD <code>f</code>.]
-
-  Description [Finds a dense superset of BDD <code>f</code>. Density is
-  the ratio of number of minterms to number of nodes.  Uses several
-  techniques in series. It is more expensive than other supersetting
-  procedures, but often produces better results. See
-  Cudd_SupersetShortPaths for a description of the threshold and nvars
-  parameters.  Returns a pointer to the result if successful; NULL
-  otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_SubsetCompress Cudd_SupersetRemap Cudd_SupersetShortPaths
-  Cudd_SupersetHeavyBranch Cudd_bddSqueeze]
-
-******************************************************************************/
-DdNode *
-Cudd_SupersetCompress(
-  DdManager * dd /* manager */,
-  DdNode * f /* BDD whose superset is sought */,
-  int  nvars /* number of variables in the support of f */,
-  int  threshold /* maximum number of nodes in the superset */)
-{
-    DdNode *subset;
-
-    subset = Cudd_SubsetCompress(dd, Cudd_Not(f),nvars,threshold);
-
-    return(Cudd_NotCond(subset, (subset != NULL)));
-
-} /* end of Cudd_SupersetCompress */
-
-
-/*---------------------------------------------------------------------------*/
-/* Definition of internal functions                                          */
-/*---------------------------------------------------------------------------*/
-
-
-/**Function********************************************************************
-
-  Synopsis    [Performs the recursive step of Cudd_bddConstrain.]
-
-  Description [Performs the recursive step of Cudd_bddConstrain.
-  Returns a pointer to the result if successful; NULL otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_bddConstrain]
-
-******************************************************************************/
-DdNode *
-cuddBddConstrainRecur(
-  DdManager * dd,
-  DdNode * f,
-  DdNode * c)
-{
-    DdNode       *Fv, *Fnv, *Cv, *Cnv, *t, *e, *r;
-    DdNode     *one, *zero;
-    unsigned int topf, topc;
-    int         index;
-    int          comple = 0;
-
-    statLine(dd);
-    one = DD_ONE(dd);
-    zero = Cudd_Not(one);
-
-    /* Trivial cases. */
-    if (c == one)        return(f);
-    if (c == zero)        return(zero);
-    if (Cudd_IsConstant(f))    return(f);
-    if (f == c)            return(one);
-    if (f == Cudd_Not(c))    return(zero);
-
-    /* Make canonical to increase the utilization of the cache. */
-    if (Cudd_IsComplement(f)) {
-    f = Cudd_Not(f);
-    comple = 1;
-    }
-    /* Now f is a regular pointer to a non-constant node; c is also
-    ** non-constant, but may be complemented.
-    */
-
-    /* Check the cache. */
-    r = cuddCacheLookup2(dd, Cudd_bddConstrain, f, c);
-    if (r != NULL) {
-    return(Cudd_NotCond(r,comple));
-    }
-    
-    /* Recursive step. */
-    topf = dd->perm[f->index];
-    topc = dd->perm[Cudd_Regular(c)->index];
-    if (topf <= topc) {
-    index = f->index;
-    Fv = cuddT(f); Fnv = cuddE(f);
-    } else {
-    index = Cudd_Regular(c)->index;
-    Fv = Fnv = f;
-    }
-    if (topc <= topf) {
-    Cv = cuddT(Cudd_Regular(c)); Cnv = cuddE(Cudd_Regular(c));
-    if (Cudd_IsComplement(c)) {
-        Cv = Cudd_Not(Cv);
-        Cnv = Cudd_Not(Cnv);
-    }
-    } else {
-    Cv = Cnv = c;
-    }
-
-    if (!Cudd_IsConstant(Cv)) {
-    t = cuddBddConstrainRecur(dd, Fv, Cv);
-    if (t == NULL)
-        return(NULL);
-    } else if (Cv == one) {
-    t = Fv;
-    } else {        /* Cv == zero: return Fnv @ Cnv */
-    if (Cnv == one) {
-        r = Fnv;
-    } else {
-        r = cuddBddConstrainRecur(dd, Fnv, Cnv);
-        if (r == NULL)
-        return(NULL);
-    }
-    return(Cudd_NotCond(r,comple));
-    }
-    cuddRef(t);
-
-    if (!Cudd_IsConstant(Cnv)) {
-    e = cuddBddConstrainRecur(dd, Fnv, Cnv);
-    if (e == NULL) {
-        Cudd_IterDerefBdd(dd, t);
-        return(NULL);
-    }
-    } else if (Cnv == one) {
-    e = Fnv;
-    } else {        /* Cnv == zero: return Fv @ Cv previously computed */
-    cuddDeref(t);
-    return(Cudd_NotCond(t,comple));
-    }
-    cuddRef(e);
-
-    if (Cudd_IsComplement(t)) {
-    t = Cudd_Not(t);
-    e = Cudd_Not(e);
-    r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
-    if (r == NULL) {
-        Cudd_IterDerefBdd(dd, e);
-        Cudd_IterDerefBdd(dd, t);
-        return(NULL);
-    }
-    r = Cudd_Not(r);
-    } else {
-    r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
-    if (r == NULL) {
-        Cudd_IterDerefBdd(dd, e);
-        Cudd_IterDerefBdd(dd, t);
-        return(NULL);
-    }
-    }
-    cuddDeref(t);
-    cuddDeref(e);
-
-    cuddCacheInsert2(dd, Cudd_bddConstrain, f, c, r);
-    return(Cudd_NotCond(r,comple));
-
-} /* end of cuddBddConstrainRecur */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Performs the recursive step of Cudd_bddRestrict.]
-
-  Description [Performs the recursive step of Cudd_bddRestrict.
-  Returns the restricted BDD if successful; otherwise NULL.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_bddRestrict]
-
-******************************************************************************/
-DdNode *
-cuddBddRestrictRecur(
-  DdManager * dd,
-  DdNode * f,
-  DdNode * c)
-{
-    DdNode     *Fv, *Fnv, *Cv, *Cnv, *t, *e, *r, *one, *zero;
-    unsigned int topf, topc;
-    int         index;
-    int         comple = 0;
-
-    statLine(dd);
-    one = DD_ONE(dd);
-    zero = Cudd_Not(one);
-
-    /* Trivial cases */
-    if (c == one)        return(f);
-    if (c == zero)        return(zero);
-    if (Cudd_IsConstant(f))    return(f);
-    if (f == c)            return(one);
-    if (f == Cudd_Not(c))    return(zero);
-
-    /* Make canonical to increase the utilization of the cache. */
-    if (Cudd_IsComplement(f)) {
-    f = Cudd_Not(f);
-    comple = 1;
-    }
-    /* Now f is a regular pointer to a non-constant node; c is also
-    ** non-constant, but may be complemented.
-    */
-
-    /* Check the cache. */
-    r = cuddCacheLookup2(dd, Cudd_bddRestrict, f, c);
-    if (r != NULL) {
-    return(Cudd_NotCond(r,comple));
-    }
-
-    topf = dd->perm[f->index];
-    topc = dd->perm[Cudd_Regular(c)->index];
-
-    if (topc < topf) {    /* abstract top variable from c */
-    DdNode *d, *s1, *s2;
-
-    /* Find complements of cofactors of c. */
-    if (Cudd_IsComplement(c)) {
-        s1 = cuddT(Cudd_Regular(c));
-        s2 = cuddE(Cudd_Regular(c));
-    } else {
-        s1 = Cudd_Not(cuddT(c));
-        s2 = Cudd_Not(cuddE(c));
-    }
-    /* Take the OR by applying DeMorgan. */
-    d = cuddBddAndRecur(dd, s1, s2);
-    if (d == NULL) return(NULL);
-    d = Cudd_Not(d);
-    cuddRef(d);
-    r = cuddBddRestrictRecur(dd, f, d);
-    if (r == NULL) {
-        Cudd_IterDerefBdd(dd, d);
-        return(NULL);
-    }
-    cuddRef(r);
-    Cudd_IterDerefBdd(dd, d);
-    cuddCacheInsert2(dd, Cudd_bddRestrict, f, c, r);
-    cuddDeref(r);
-    return(Cudd_NotCond(r,comple));
-    }
-
-    /* Recursive step. Here topf <= topc. */
-    index = f->index;
-    Fv = cuddT(f); Fnv = cuddE(f);
-    if (topc == topf) {
-    Cv = cuddT(Cudd_Regular(c)); Cnv = cuddE(Cudd_Regular(c));
-    if (Cudd_IsComplement(c)) {
-        Cv = Cudd_Not(Cv);
-        Cnv = Cudd_Not(Cnv);
-    }
-    } else {
-    Cv = Cnv = c;
-    }
-
-    if (!Cudd_IsConstant(Cv)) {
-    t = cuddBddRestrictRecur(dd, Fv, Cv);
-    if (t == NULL) return(NULL);
-    } else if (Cv == one) {
-    t = Fv;
-    } else {        /* Cv == zero: return(Fnv @ Cnv) */
-    if (Cnv == one) {
-        r = Fnv;
-    } else {
-        r = cuddBddRestrictRecur(dd, Fnv, Cnv);
-        if (r == NULL) return(NULL);
-    }
-    return(Cudd_NotCond(r,comple));
-    }
-    cuddRef(t);
-
-    if (!Cudd_IsConstant(Cnv)) {
-    e = cuddBddRestrictRecur(dd, Fnv, Cnv);
-    if (e == NULL) {
-        Cudd_IterDerefBdd(dd, t);
-        return(NULL);
-    }
-    } else if (Cnv == one) {
-    e = Fnv;
-    } else {        /* Cnv == zero: return (Fv @ Cv) previously computed */
-    cuddDeref(t);
-    return(Cudd_NotCond(t,comple));
-    }
-    cuddRef(e);
-
-    if (Cudd_IsComplement(t)) {
-    t = Cudd_Not(t);
-    e = Cudd_Not(e);
-    r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
-    if (r == NULL) {
-        Cudd_IterDerefBdd(dd, e);
-        Cudd_IterDerefBdd(dd, t);
-        return(NULL);
-    }
-    r = Cudd_Not(r);
-    } else {
-    r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
-    if (r == NULL) {
-        Cudd_IterDerefBdd(dd, e);
-        Cudd_IterDerefBdd(dd, t);
-        return(NULL);
-    }
-    }
-    cuddDeref(t);
-    cuddDeref(e);
-
-    cuddCacheInsert2(dd, Cudd_bddRestrict, f, c, r);
-    return(Cudd_NotCond(r,comple));
-
-} /* end of cuddBddRestrictRecur */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Performs the recursive step of Cudd_addConstrain.]
-
-  Description [Performs the recursive step of Cudd_addConstrain.
-  Returns a pointer to the result if successful; NULL otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_addConstrain]
-
-******************************************************************************/
-DdNode *
-cuddAddConstrainRecur(
-  DdManager * dd,
-  DdNode * f,
-  DdNode * c)
-{
-    DdNode       *Fv, *Fnv, *Cv, *Cnv, *t, *e, *r;
-    DdNode     *one, *zero;
-    unsigned int topf, topc;
-    int         index;
-
-    statLine(dd);
-    one = DD_ONE(dd);
-    zero = DD_ZERO(dd);
-
-    /* Trivial cases. */
-    if (c == one)        return(f);
-    if (c == zero)        return(zero);
-    if (Cudd_IsConstant(f))    return(f);
-    if (f == c)            return(one);
-
-    /* Now f and c are non-constant. */
-
-    /* Check the cache. */
-    r = cuddCacheLookup2(dd, Cudd_addConstrain, f, c);
-    if (r != NULL) {
-    return(r);
-    }
-    
-    /* Recursive step. */
-    topf = dd->perm[f->index];
-    topc = dd->perm[c->index];
-    if (topf <= topc) {
-    index = f->index;
-    Fv = cuddT(f); Fnv = cuddE(f);
-    } else {
-    index = c->index;
-    Fv = Fnv = f;
-    }
-    if (topc <= topf) {
-    Cv = cuddT(c); Cnv = cuddE(c);
-    } else {
-    Cv = Cnv = c;
-    }
-
-    if (!Cudd_IsConstant(Cv)) {
-    t = cuddAddConstrainRecur(dd, Fv, Cv);
-    if (t == NULL)
-        return(NULL);
-    } else if (Cv == one) {
-    t = Fv;
-    } else {        /* Cv == zero: return Fnv @ Cnv */
-    if (Cnv == one) {
-        r = Fnv;
-    } else {
-        r = cuddAddConstrainRecur(dd, Fnv, Cnv);
-        if (r == NULL)
-        return(NULL);
-    }
-    return(r);
-    }
-    cuddRef(t);
-
-    if (!Cudd_IsConstant(Cnv)) {
-    e = cuddAddConstrainRecur(dd, Fnv, Cnv);
-    if (e == NULL) {
-        Cudd_RecursiveDeref(dd, t);
-        return(NULL);
-    }
-    } else if (Cnv == one) {
-    e = Fnv;
-    } else {        /* Cnv == zero: return Fv @ Cv previously computed */
-    cuddDeref(t);
-    return(t);
-    }
-    cuddRef(e);
-
-    r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
-    if (r == NULL) {
-    Cudd_RecursiveDeref(dd, e);
-    Cudd_RecursiveDeref(dd, t);
-    return(NULL);
-    }
-    cuddDeref(t);
-    cuddDeref(e);
-
-    cuddCacheInsert2(dd, Cudd_addConstrain, f, c, r);
-    return(r);
-
-} /* end of cuddAddConstrainRecur */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Performs the recursive step of Cudd_addRestrict.]
-
-  Description [Performs the recursive step of Cudd_addRestrict.
-  Returns the restricted ADD if successful; otherwise NULL.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_addRestrict]
-
-******************************************************************************/
-DdNode *
-cuddAddRestrictRecur(
-  DdManager * dd,
-  DdNode * f,
-  DdNode * c)
-{
-    DdNode     *Fv, *Fnv, *Cv, *Cnv, *t, *e, *r, *one, *zero;
-    unsigned int topf, topc;
-    int         index;
-
-    statLine(dd);
-    one = DD_ONE(dd);
-    zero = DD_ZERO(dd);
-
-    /* Trivial cases */
-    if (c == one)        return(f);
-    if (c == zero)        return(zero);
-    if (Cudd_IsConstant(f))    return(f);
-    if (f == c)            return(one);
-
-    /* Now f and c are non-constant. */
-
-    /* Check the cache. */
-    r = cuddCacheLookup2(dd, Cudd_addRestrict, f, c);
-    if (r != NULL) {
-    return(r);
-    }
-
-    topf = dd->perm[f->index];
-    topc = dd->perm[c->index];
-
-    if (topc < topf) {    /* abstract top variable from c */
-    DdNode *d, *s1, *s2;
-
-    /* Find cofactors of c. */
-    s1 = cuddT(c);
-    s2 = cuddE(c);
-    /* Take the OR by applying DeMorgan. */
-    d = cuddAddApplyRecur(dd, Cudd_addOr, s1, s2);
-    if (d == NULL) return(NULL);
-    cuddRef(d);
-    r = cuddAddRestrictRecur(dd, f, d);
-    if (r == NULL) {
-        Cudd_RecursiveDeref(dd, d);
-        return(NULL);
-    }
-    cuddRef(r);
-    Cudd_RecursiveDeref(dd, d);
-    cuddCacheInsert2(dd, Cudd_addRestrict, f, c, r);
-    cuddDeref(r);
-    return(r);
-    }
-
-    /* Recursive step. Here topf <= topc. */
-    index = f->index;
-    Fv = cuddT(f); Fnv = cuddE(f);
-    if (topc == topf) {
-    Cv = cuddT(c); Cnv = cuddE(c);
-    } else {
-    Cv = Cnv = c;
-    }
-
-    if (!Cudd_IsConstant(Cv)) {
-    t = cuddAddRestrictRecur(dd, Fv, Cv);
-    if (t == NULL) return(NULL);
-    } else if (Cv == one) {
-    t = Fv;
-    } else {        /* Cv == zero: return(Fnv @ Cnv) */
-    if (Cnv == one) {
-        r = Fnv;
-    } else {
-        r = cuddAddRestrictRecur(dd, Fnv, Cnv);
-        if (r == NULL) return(NULL);
-    }
-    return(r);
-    }
-    cuddRef(t);
-
-    if (!Cudd_IsConstant(Cnv)) {
-    e = cuddAddRestrictRecur(dd, Fnv, Cnv);
-    if (e == NULL) {
-        Cudd_RecursiveDeref(dd, t);
-        return(NULL);
-    }
-    } else if (Cnv == one) {
-    e = Fnv;
-    } else {        /* Cnv == zero: return (Fv @ Cv) previously computed */
-    cuddDeref(t);
-    return(t);
-    }
-    cuddRef(e);
-
-    r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
-    if (r == NULL) {
-    Cudd_RecursiveDeref(dd, e);
-    Cudd_RecursiveDeref(dd, t);
-    return(NULL);
-    }
-    cuddDeref(t);
-    cuddDeref(e);
-
-    cuddCacheInsert2(dd, Cudd_addRestrict, f, c, r);
-    return(r);
-
-} /* end of cuddAddRestrictRecur */
-
-
-
-/**Function********************************************************************
-
-  Synopsis    [Performs safe minimization of a BDD.]
-
-  Description [Performs safe minimization of a BDD. Given the BDD
-  <code>f</code> of a function to be minimized and a BDD
-  <code>c</code> representing the care set, Cudd_bddLICompaction
-  produces the BDD of a function that agrees with <code>f</code>
-  wherever <code>c</code> is 1.  Safe minimization means that the size
-  of the result is guaranteed not to exceed the size of
-  <code>f</code>. This function is based on the DAC97 paper by Hong et
-  al..  Returns a pointer to the result if successful; NULL
-  otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_bddLICompaction]
-
-******************************************************************************/
-DdNode *
-cuddBddLICompaction(
-  DdManager * dd /* manager */,
-  DdNode * f /* function to be minimized */,
-  DdNode * c /* constraint (care set) */)
-{
-    st_table *marktable, *markcache, *buildcache;
-    DdNode *res, *zero;
-
-    zero = Cudd_Not(DD_ONE(dd));
-    if (c == zero) return(zero);
-
-    /* We need to use local caches for both steps of this operation.
-    ** The results of the edge marking step are only valid as long as the
-    ** edge markings themselves are available. However, the edge markings
-    ** are lost at the end of one invocation of Cudd_bddLICompaction.
-    ** Hence, the cache entries for the edge marking step must be
-    ** invalidated at the end of this function.
-    ** For the result of the building step we argue as follows. The result
-    ** for a node and a given constrain depends on the BDD in which the node
-    ** appears. Hence, the same node and constrain may give different results
-    ** in successive invocations.
-    */
-    marktable = st_init_table(st_ptrcmp,st_ptrhash);
-    if (marktable == NULL) {
-    return(NULL);
-    }
-    markcache = st_init_table(MarkCacheCompare,MarkCacheHash);
-    if (markcache == NULL) {
-    st_free_table(marktable);
-    return(NULL);
-    }
-    if (cuddBddLICMarkEdges(dd,f,c,marktable,markcache) == CUDD_OUT_OF_MEM) {
-    st_foreach(markcache, MarkCacheCleanUp, NULL);
-    st_free_table(marktable);
-    st_free_table(markcache);
-    return(NULL);
-    }
-    st_foreach(markcache, MarkCacheCleanUp, NULL);
-    st_free_table(markcache);
-    buildcache = st_init_table(st_ptrcmp,st_ptrhash);
-    if (buildcache == NULL) {
-    st_free_table(marktable);
-    return(NULL);
-    }
-    res = cuddBddLICBuildResult(dd,f,buildcache,marktable);
-    st_free_table(buildcache);
-    st_free_table(marktable);
-    return(res);
-
-} /* end of cuddBddLICompaction */
-
-
-/*---------------------------------------------------------------------------*/
-/* Definition of static functions                                            */
-/*---------------------------------------------------------------------------*/
-
-
-/**Function********************************************************************
-
-  Synopsis    [Performs the recursive step of Cudd_bddConstrainDecomp.]
-
-  Description [Performs the recursive step of Cudd_bddConstrainDecomp.
-  Returns f super (i) if successful; otherwise NULL.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_bddConstrainDecomp]
-
-******************************************************************************/
-static int
-cuddBddConstrainDecomp(
-  DdManager * dd,
-  DdNode * f,
-  DdNode ** decomp)
-{
-    DdNode *F, *fv, *fvn;
-    DdNode *fAbs;
-    DdNode *result;
-    int ok;
-
-    if (Cudd_IsConstant(f)) return(1);
-    /* Compute complements of cofactors. */
-    F = Cudd_Regular(f);
-    fv = cuddT(F);
-    fvn = cuddE(F);
-    if (F == f) {
-    fv = Cudd_Not(fv);
-    fvn = Cudd_Not(fvn);
-    }
-    /* Compute abstraction of top variable. */
-    fAbs = cuddBddAndRecur(dd, fv, fvn);
-    if (fAbs == NULL) {
-    return(0);
-    }
-    cuddRef(fAbs);
-    fAbs = Cudd_Not(fAbs);
-    /* Recursively find the next abstraction and the components of the
-    ** decomposition. */
-    ok = cuddBddConstrainDecomp(dd, fAbs, decomp);
-    if (ok == 0) {
-    Cudd_IterDerefBdd(dd,fAbs);
-    return(0);
-    }
-    /* Compute the component of the decomposition corresponding to the
-    ** top variable and store it in the decomposition array. */
-    result = cuddBddConstrainRecur(dd, f, fAbs);
-    if (result == NULL) {
-    Cudd_IterDerefBdd(dd,fAbs);
-    return(0);
-    }
-    cuddRef(result);
-    decomp[F->index] = result;
-    Cudd_IterDerefBdd(dd, fAbs);
-    return(1);
-
-} /* end of cuddBddConstrainDecomp */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Performs the recursive step of Cudd_bddCharToVect.]
-
-  Description [Performs the recursive step of Cudd_bddCharToVect.
-  This function maintains the invariant that f is non-zero.
-  Returns the i-th component of the vector if successful; otherwise NULL.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_bddCharToVect]
-
-******************************************************************************/
-static DdNode *
-cuddBddCharToVect(
-  DdManager * dd,
-  DdNode * f,
-  DdNode * x)
-{
-    unsigned int topf;
-    unsigned int level;
-    int comple;
-
-    DdNode *one, *zero, *res, *F, *fT, *fE, *T, *E;
-
-    statLine(dd);
-    /* Check the cache. */
-    res = cuddCacheLookup2(dd, cuddBddCharToVect, f, x);
-    if (res != NULL) {
-    return(res);
-    }
-
-    F = Cudd_Regular(f);
-
-    topf = cuddI(dd,F->index);
-    level = dd->perm[x->index];
-
-    if (topf > level) return(x);
-
-    one = DD_ONE(dd);
-    zero = Cudd_Not(one);
-
-    comple = F != f;
-    fT = Cudd_NotCond(cuddT(F),comple);
-    fE = Cudd_NotCond(cuddE(F),comple);
-
-    if (topf == level) {
-    if (fT == zero) return(zero);
-    if (fE == zero) return(one);
-    return(x);
-    }
-
-    /* Here topf < level. */
-    if (fT == zero) return(cuddBddCharToVect(dd, fE, x));
-    if (fE == zero) return(cuddBddCharToVect(dd, fT, x));
-
-    T = cuddBddCharToVect(dd, fT, x);
-    if (T == NULL) {
-    return(NULL);
-    }
-    cuddRef(T);
-    E = cuddBddCharToVect(dd, fE, x);
-    if (E == NULL) {
-    Cudd_IterDerefBdd(dd,T);
-    return(NULL);
-    }
-    cuddRef(E);
-    res = cuddBddIteRecur(dd, dd->vars[F->index], T, E);
-    if (res == NULL) {
-    Cudd_IterDerefBdd(dd,T);
-    Cudd_IterDerefBdd(dd,E);
-    return(NULL);
-    }
-    cuddDeref(T);
-    cuddDeref(E);
-    cuddCacheInsert2(dd, cuddBddCharToVect, f, x, res);
-    return(res);
-
-} /* end of cuddBddCharToVect */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Performs the edge marking step of Cudd_bddLICompaction.]
-
-  Description [Performs the edge marking step of Cudd_bddLICompaction.
-  Returns the LUB of the markings of the two outgoing edges of <code>f</code>
-  if successful; otherwise CUDD_OUT_OF_MEM.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_bddLICompaction cuddBddLICBuildResult]
-
-******************************************************************************/
-static int
-cuddBddLICMarkEdges(
-  DdManager * dd,
-  DdNode * f,
-  DdNode * c,
-  st_table * table,
-  st_table * cache)
-{
-    DdNode *Fv, *Fnv, *Cv, *Cnv;
-    DdNode *one, *zero;
-    unsigned int topf, topc;
-    int    index;
-    int comple;
-    int resT, resE, res, retval;
-    char **slot;
-    MarkCacheKey *key;
-
-    one = DD_ONE(dd);
-    zero = Cudd_Not(one);
-
-    /* Terminal cases. */
-    if (c == zero) return(DD_LIC_DC);
-    if (f == one)  return(DD_LIC_1);
-    if (f == zero) return(DD_LIC_0);
-
-    /* Make canonical to increase the utilization of the cache. */
-    comple = Cudd_IsComplement(f);
-    f = Cudd_Regular(f);
-    /* Now f is a regular pointer to a non-constant node; c may be
-    ** constant, or it may be complemented.
-    */
-
-    /* Check the cache. */
-    key = ALLOC(MarkCacheKey, 1);
-    if (key == NULL) {
-    dd->errorCode = CUDD_MEMORY_OUT;
-    return(CUDD_OUT_OF_MEM);
-    }
-    key->f = f; key->c = c;
-    if (st_lookup(cache, (char *)key, (char **)&res)) {
-    FREE(key);
-    if (comple) {
-        if (res == DD_LIC_0) res = DD_LIC_1;
-        else if (res == DD_LIC_1) res = DD_LIC_0;
-    }
-    return(res);
-    }
-
-    /* Recursive step. */
-    topf = dd->perm[f->index];
-    topc = cuddI(dd,Cudd_Regular(c)->index);
-    if (topf <= topc) {
-    index = f->index;
-    Fv = cuddT(f); Fnv = cuddE(f);
-    } else {
-    index = Cudd_Regular(c)->index;
-    Fv = Fnv = f;
-    }
-    if (topc <= topf) {
-    /* We know that c is not constant because f is not. */
-    Cv = cuddT(Cudd_Regular(c)); Cnv = cuddE(Cudd_Regular(c));
-    if (Cudd_IsComplement(c)) {
-        Cv = Cudd_Not(Cv);
-        Cnv = Cudd_Not(Cnv);
-    }
-    } else {
-    Cv = Cnv = c;
-    }
-
-    resT = cuddBddLICMarkEdges(dd, Fv, Cv, table, cache);
-    if (resT == CUDD_OUT_OF_MEM) {
-    FREE(key);
-    return(CUDD_OUT_OF_MEM);
-    }
-    resE = cuddBddLICMarkEdges(dd, Fnv, Cnv, table, cache);
-    if (resE == CUDD_OUT_OF_MEM) {
-    FREE(key);
-    return(CUDD_OUT_OF_MEM);
-    }
-
-    /* Update edge markings. */
-    if (topf <= topc) {
-    retval = st_find_or_add(table, (char *)f, (char ***)&slot);
-    if (retval == 0) {
-        *slot = (char *) (ptrint)((resT << 2) | resE);
-    } else if (retval == 1) {
-        *slot = (char *) (ptrint)((int)((ptrint) *slot) | (resT << 2) | resE);
-    } else {
-        FREE(key);
-        return(CUDD_OUT_OF_MEM);
-    }
-    }
-
-    /* Cache result. */
-    res = resT | resE;
-    if (st_insert(cache, (char *)key, (char *)(ptrint)res) == ST_OUT_OF_MEM) {
-    FREE(key);
-    return(CUDD_OUT_OF_MEM);
-    }
-
-    /* Take into account possible complementation. */
-    if (comple) {
-    if (res == DD_LIC_0) res = DD_LIC_1;
-    else if (res == DD_LIC_1) res = DD_LIC_0;
-    }
-    return(res);
-
-} /* end of cuddBddLICMarkEdges */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Builds the result of Cudd_bddLICompaction.]
-
-  Description [Builds the results of Cudd_bddLICompaction.
-  Returns a pointer to the minimized BDD if successful; otherwise NULL.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_bddLICompaction cuddBddLICMarkEdges]
-
-******************************************************************************/
-static DdNode *
-cuddBddLICBuildResult(
-  DdManager * dd,
-  DdNode * f,
-  st_table * cache,
-  st_table * table)
-{
-    DdNode *Fv, *Fnv, *r, *t, *e;
-    DdNode *one, *zero;
-    unsigned int topf;
-    int    index;
-    int comple;
-    int markT, markE, markings;
-
-    one = DD_ONE(dd);
-    zero = Cudd_Not(one);
-
-    if (Cudd_IsConstant(f)) return(f);
-    /* Make canonical to increase the utilization of the cache. */
-    comple = Cudd_IsComplement(f);
-    f = Cudd_Regular(f);
-
-    /* Check the cache. */
-    if (st_lookup(cache, (char *)f, (char **)&r)) {
-    return(Cudd_NotCond(r,comple));
-    }
-
-    /* Retrieve the edge markings. */
-    if (st_lookup(table, (char *)f, (char **)&markings) == 0)
-    return(NULL);
-    markT = markings >> 2;
-    markE = markings & 3;
-
-    topf = dd->perm[f->index];
-    index = f->index;
-    Fv = cuddT(f); Fnv = cuddE(f);
-
-    if (markT == DD_LIC_NL) {
-    t = cuddBddLICBuildResult(dd,Fv,cache,table);
-    if (t == NULL) {
-        return(NULL);
-    }
-    } else if (markT == DD_LIC_1) {
-    t = one;
-    } else {
-    t = zero;
-    }
-    cuddRef(t);
-    if (markE == DD_LIC_NL) {
-    e = cuddBddLICBuildResult(dd,Fnv,cache,table);
-    if (e == NULL) {
-        Cudd_IterDerefBdd(dd,t);
-        return(NULL);
-    }
-    } else if (markE == DD_LIC_1) {
-    e = one;
-    } else {
-    e = zero;
-    }
-    cuddRef(e);
-
-    if (markT == DD_LIC_DC && markE != DD_LIC_DC) {
-    r = e;
-    } else if (markT != DD_LIC_DC && markE == DD_LIC_DC) {
-    r = t;
-    } else {
-    if (Cudd_IsComplement(t)) {
-        t = Cudd_Not(t);
-        e = Cudd_Not(e);
-        r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
-        if (r == NULL) {
-        Cudd_IterDerefBdd(dd, e);
-        Cudd_IterDerefBdd(dd, t);
-        return(NULL);
-        }
-        r = Cudd_Not(r);
-    } else {
-        r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
-        if (r == NULL) {
-        Cudd_IterDerefBdd(dd, e);
-        Cudd_IterDerefBdd(dd, t);
-        return(NULL);
-        }
-    }
-    }
-    cuddDeref(t);
-    cuddDeref(e);
-
-    if (st_insert(cache, (char *)f, (char *)r) == ST_OUT_OF_MEM) {
-    cuddRef(r);
-    Cudd_IterDerefBdd(dd,r);
-    return(NULL);
-    }
-
-    return(Cudd_NotCond(r,comple));
-
-} /* end of cuddBddLICBuildResult */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Hash function for the computed table of cuddBddLICMarkEdges.]
-
-  Description [Hash function for the computed table of
-  cuddBddLICMarkEdges.  Returns the bucket number.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_bddLICompaction]
-
-******************************************************************************/
-static int
-MarkCacheHash(
-  char * ptr,
-  int  modulus)
-{
-    int val = 0;
-    MarkCacheKey *entry;
-
-    entry = (MarkCacheKey *) ptr;
-
-    val = (int) (ptrint) entry->f;
-    val = val * 997 + (int) (ptrint) entry->c;
-
-    return ((val < 0) ? -val : val) % modulus;
-
-} /* end of MarkCacheHash */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Comparison function for the computed table of
-  cuddBddLICMarkEdges.]
-
-  Description [Comparison function for the computed table of
-  cuddBddLICMarkEdges. Returns 0 if the two nodes of the key are equal; 1
-  otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_bddLICompaction]
-
-******************************************************************************/
-static int
-MarkCacheCompare(
-  const char * ptr1,
-  const char * ptr2)
-{
-    MarkCacheKey *entry1, *entry2;
-
-    entry1 = (MarkCacheKey *) ptr1;
-    entry2 = (MarkCacheKey *) ptr2;
-    
-    return((entry1->f != entry2->f) || (entry1->c != entry2->c));
-
-} /* end of MarkCacheCompare */
-
-
-
-/**Function********************************************************************
-
-  Synopsis    [Frees memory associated with computed table of
-  cuddBddLICMarkEdges.]
-
-  Description [Frees memory associated with computed table of
-  cuddBddLICMarkEdges. Returns ST_CONTINUE.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_bddLICompaction]
-
-******************************************************************************/
-static enum st_retval
-MarkCacheCleanUp(
-  char * key,
-  char * value,
-  char * arg)
-{
-    MarkCacheKey *entry;
-
-    entry = (MarkCacheKey *) key;
-    FREE(entry);
-    return ST_CONTINUE;
-
-} /* end of MarkCacheCleanUp */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Performs the recursive step of Cudd_bddSqueeze.]
-
-  Description [Performs the recursive step of Cudd_bddSqueeze.  This
-  procedure exploits the fact that if we complement and swap the
-  bounds of the interval we obtain a valid solution by taking the
-  complement of the solution to the original problem. Therefore, we
-  can enforce the condition that the upper bound is always regular.
-  Returns a pointer to the result if successful; NULL otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_bddSqueeze]
-
-******************************************************************************/
-static DdNode *
-cuddBddSqueeze(
-  DdManager * dd,
-  DdNode * l,
-  DdNode * u)
-{
-    DdNode *one, *zero, *r, *lt, *le, *ut, *ue, *t, *e;
-#if 0
-    DdNode *ar;
-#endif
-    int comple = 0;
-    unsigned int topu, topl;
-    int index;
-
-    statLine(dd);
-    if (l == u) {
-    return(l);
-    }
-    one = DD_ONE(dd);
-    zero = Cudd_Not(one);
-    /* The only case when l == zero && u == one is at the top level,
-    ** where returning either one or zero is OK. In all other cases
-    ** the procedure will detect such a case and will perform
-    ** remapping. Therefore the order in which we test l and u at this
-    ** point is immaterial. */
-    if (l == zero) return(l);
-    if (u == one)  return(u);
-
-    /* Make canonical to increase the utilization of the cache. */
-    if (Cudd_IsComplement(u)) {
-    DdNode *temp;
-    temp = Cudd_Not(l);
-    l = Cudd_Not(u);
-    u = temp;
-    comple = 1;
-    }
-    /* At this point u is regular and non-constant; l is non-constant, but
-    ** may be complemented. */
-
-    /* Here we could check the relative sizes. */
-
-    /* Check the cache. */
-    r = cuddCacheLookup2(dd, Cudd_bddSqueeze, l, u);
-    if (r != NULL) {
-    return(Cudd_NotCond(r,comple));
-    }
-
-    /* Recursive step. */
-    topu = dd->perm[u->index];
-    topl = dd->perm[Cudd_Regular(l)->index];
-    if (topu <= topl) {
-    index = u->index;
-    ut = cuddT(u); ue = cuddE(u);
-    } else {
-    index = Cudd_Regular(l)->index;
-    ut = ue = u;
-    }
-    if (topl <= topu) {
-    lt = cuddT(Cudd_Regular(l)); le = cuddE(Cudd_Regular(l));
-    if (Cudd_IsComplement(l)) {
-        lt = Cudd_Not(lt);
-        le = Cudd_Not(le);
-    }
-    } else {
-    lt = le = l;
-    }
-
-    /* If one interval is contained in the other, use the smaller
-    ** interval. This corresponds to one-sided matching. */
-    if ((lt == zero || Cudd_bddLeq(dd,lt,le)) &&
-    (ut == one  || Cudd_bddLeq(dd,ue,ut))) { /* remap */
-    r = cuddBddSqueeze(dd, le, ue);
-    if (r == NULL)
-        return(NULL);
-    return(Cudd_NotCond(r,comple));
-    } else if ((le == zero || Cudd_bddLeq(dd,le,lt)) &&
-           (ue == one  || Cudd_bddLeq(dd,ut,ue))) { /* remap */
-    r = cuddBddSqueeze(dd, lt, ut);
-    if (r == NULL)
-        return(NULL);
-    return(Cudd_NotCond(r,comple));
-    } else if ((le == zero || Cudd_bddLeq(dd,le,Cudd_Not(ut))) &&
-           (ue == one  || Cudd_bddLeq(dd,Cudd_Not(lt),ue))) { /* c-remap */
-    t = cuddBddSqueeze(dd, lt, ut);
-    cuddRef(t);
-    if (Cudd_IsComplement(t)) {
-        r = cuddUniqueInter(dd, index, Cudd_Not(t), t);
-        if (r == NULL) {
-        Cudd_IterDerefBdd(dd, t);
-        return(NULL);
-        }
-        r = Cudd_Not(r);
-    } else {
-        r = cuddUniqueInter(dd, index, t, Cudd_Not(t));
-        if (r == NULL) {
-        Cudd_IterDerefBdd(dd, t);
-        return(NULL);
-        }
-    }
-    cuddDeref(t);
-    if (r == NULL)
-        return(NULL);
-    cuddCacheInsert2(dd, Cudd_bddSqueeze, l, u, r);
-    return(Cudd_NotCond(r,comple));
-    } else if ((lt == zero || Cudd_bddLeq(dd,lt,Cudd_Not(ue))) &&
-           (ut == one  || Cudd_bddLeq(dd,Cudd_Not(le),ut))) { /* c-remap */
-    e = cuddBddSqueeze(dd, le, ue);
-    cuddRef(e);
-    if (Cudd_IsComplement(e)) {
-        r = cuddUniqueInter(dd, index, Cudd_Not(e), e);
-        if (r == NULL) {
-        Cudd_IterDerefBdd(dd, e);
-        return(NULL);
-        }
-    } else {
-        r = cuddUniqueInter(dd, index, e, Cudd_Not(e));
-        if (r == NULL) {
-        Cudd_IterDerefBdd(dd, e);
-        return(NULL);
-        }
-        r = Cudd_Not(r);
-    }
-    cuddDeref(e);
-    if (r == NULL)
-        return(NULL);
-    cuddCacheInsert2(dd, Cudd_bddSqueeze, l, u, r);
-    return(Cudd_NotCond(r,comple));
-    }
-
-#if 0
-    /* If the two intervals intersect, take a solution from
-    ** the intersection of the intervals. This guarantees that the
-    ** splitting variable will not appear in the result.
-    ** This approach corresponds to two-sided matching, and is very
-    ** expensive. */
-    if (Cudd_bddLeq(dd,lt,ue) && Cudd_bddLeq(dd,le,ut)) {
-    DdNode *au, *al;
-    au = cuddBddAndRecur(dd,ut,ue);
-    if (au == NULL)
-        return(NULL);
-    cuddRef(au);
-    al = cuddBddAndRecur(dd,Cudd_Not(lt),Cudd_Not(le));
-    if (al == NULL) {
-        Cudd_IterDerefBdd(dd,au);
-        return(NULL);
-    }
-    cuddRef(al);
-    al = Cudd_Not(al);
-    ar = cuddBddSqueeze(dd, al, au);
-    if (ar == NULL) {
-        Cudd_IterDerefBdd(dd,au);
-        Cudd_IterDerefBdd(dd,al);
-        return(NULL);
-    }
-    cuddRef(ar);
-    Cudd_IterDerefBdd(dd,au);
-    Cudd_IterDerefBdd(dd,al);
-    } else {
-    ar = NULL;
-    }
-#endif
-
-    t = cuddBddSqueeze(dd, lt, ut);
-    if (t == NULL) {
-    return(NULL);
-    }
-    cuddRef(t);
-    e = cuddBddSqueeze(dd, le, ue);
-    if (e == NULL) {
-    Cudd_IterDerefBdd(dd,t);
-    return(NULL);
-    }
-    cuddRef(e);
-
-    if (Cudd_IsComplement(t)) {
-    t = Cudd_Not(t);
-    e = Cudd_Not(e);
-    r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
-    if (r == NULL) {
-        Cudd_IterDerefBdd(dd, e);
-        Cudd_IterDerefBdd(dd, t);
-        return(NULL);
-    }
-    r = Cudd_Not(r);
-    } else {
-    r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
-    if (r == NULL) {
-        Cudd_IterDerefBdd(dd, e);
-        Cudd_IterDerefBdd(dd, t);
-        return(NULL);
-    }
-    }
-    cuddDeref(t);
-    cuddDeref(e);
-
-#if 0
-    /* Check whether there is a result obtained by abstraction and whether
-    ** it is better than the one obtained by recursion. */
-    cuddRef(r);
-    if (ar != NULL) {
-    if (Cudd_DagSize(ar) <= Cudd_DagSize(r)) {
-        Cudd_IterDerefBdd(dd, r);
-        r = ar;
-    } else {
-        Cudd_IterDerefBdd(dd, ar);
-    }
-    }
-    cuddDeref(r);
-#endif
-
-    cuddCacheInsert2(dd, Cudd_bddSqueeze, l, u, r);
-    return(Cudd_NotCond(r,comple));
-
-} /* end of cuddBddSqueeze */