Version abc70930

1 files changed, 0 insertions, 689 deletions

diff --git a/src/bdd/cudd/cuddBddAbs.c b/src/bdd/cudd/cuddBddAbs.c
deleted file mode 100644
index 9552464e..00000000
--- a/src/bdd/cudd/cuddBddAbs.c
+++ /dev/null
@@ -1,689 +0,0 @@
-/**CFile***********************************************************************
-
-  FileName    [cuddBddAbs.c]
-
-  PackageName [cudd]
-
-  Synopsis    [Quantification functions for BDDs.]
-
-  Description [External procedures included in this module:
-        <ul>
-        <li> Cudd_bddExistAbstract()
-        <li> Cudd_bddXorExistAbstract()
-        <li> Cudd_bddUnivAbstract()
-        <li> Cudd_bddBooleanDiff()
-        <li> Cudd_bddVarIsDependent()
-        </ul>
-    Internal procedures included in this module:
-        <ul>
-        <li> cuddBddExistAbstractRecur()
-        <li> cuddBddXorExistAbstractRecur()
-        <li> cuddBddBooleanDiffRecur()
-        </ul>
-    Static procedures included in this module:
-        <ul>
-        <li> bddCheckPositiveCube()
-        </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                                                     */
-/*---------------------------------------------------------------------------*/
-
-
-/*---------------------------------------------------------------------------*/
-/* Stucture declarations                                                     */
-/*---------------------------------------------------------------------------*/
-
-
-/*---------------------------------------------------------------------------*/
-/* Type declarations                                                         */
-/*---------------------------------------------------------------------------*/
-
-
-/*---------------------------------------------------------------------------*/
-/* Variable declarations                                                     */
-/*---------------------------------------------------------------------------*/
-
-#ifndef lint
-static char rcsid[] DD_UNUSED = "$Id: cuddBddAbs.c,v 1.1.1.1 2003/02/24 22:23:51 wjiang Exp $";
-#endif
-
-/*---------------------------------------------------------------------------*/
-/* Macro declarations                                                        */
-/*---------------------------------------------------------------------------*/
-
-
-/**AutomaticStart*************************************************************/
-
-/*---------------------------------------------------------------------------*/
-/* Static function prototypes                                                */
-/*---------------------------------------------------------------------------*/
-
-static int bddCheckPositiveCube ARGS((DdManager *manager, DdNode *cube));
-
-/**AutomaticEnd***************************************************************/
-
-
-/*---------------------------------------------------------------------------*/
-/* Definition of exported functions                                          */
-/*---------------------------------------------------------------------------*/
-
-
-/**Function********************************************************************
-
-  Synopsis [Existentially abstracts all the variables in cube from f.]
-
-  Description [Existentially abstracts all the variables in cube from f.
-  Returns the abstracted BDD if successful; NULL otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_bddUnivAbstract Cudd_addExistAbstract]
-
-******************************************************************************/
-DdNode *
-Cudd_bddExistAbstract(
-  DdManager * manager,
-  DdNode * f,
-  DdNode * cube)
-{
-    DdNode *res;
-
-    if (bddCheckPositiveCube(manager, cube) == 0) {
-        (void) fprintf(manager->err,
-               "Error: Can only abstract positive cubes\n");
-    manager->errorCode = CUDD_INVALID_ARG;
-        return(NULL);
-    }
-
-    do {
-    manager->reordered = 0;
-    res = cuddBddExistAbstractRecur(manager, f, cube);
-    } while (manager->reordered == 1);
-
-    return(res);
-
-} /* end of Cudd_bddExistAbstract */
-
-
-/**Function********************************************************************
-
-  Synopsis [Takes the exclusive OR of two BDDs and simultaneously abstracts the
-  variables in cube.]
-
-  Description [Takes the exclusive OR of two BDDs and simultaneously abstracts
-  the variables in cube. The variables are existentially abstracted.  Returns a
-  pointer to the result is successful; NULL otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_bddUnivAbstract Cudd_bddExistAbstract Cudd_bddAndAbstract]
-
-******************************************************************************/
-DdNode *
-Cudd_bddXorExistAbstract(
-  DdManager * manager,
-  DdNode * f,
-  DdNode * g,
-  DdNode * cube)
-{
-    DdNode *res;
-
-    if (bddCheckPositiveCube(manager, cube) == 0) {
-        (void) fprintf(manager->err,
-               "Error: Can only abstract positive cubes\n");
-    manager->errorCode = CUDD_INVALID_ARG;
-        return(NULL);
-    }
-
-    do {
-    manager->reordered = 0;
-    res = cuddBddXorExistAbstractRecur(manager, f, g, cube);
-    } while (manager->reordered == 1);
-
-    return(res);
-
-} /* end of Cudd_bddXorExistAbstract */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Universally abstracts all the variables in cube from f.]
-
-  Description [Universally abstracts all the variables in cube from f.
-  Returns the abstracted BDD if successful; NULL otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_bddExistAbstract Cudd_addUnivAbstract]
-
-******************************************************************************/
-DdNode *
-Cudd_bddUnivAbstract(
-  DdManager * manager,
-  DdNode * f,
-  DdNode * cube)
-{
-    DdNode    *res;
-
-    if (bddCheckPositiveCube(manager, cube) == 0) {
-    (void) fprintf(manager->err,
-               "Error: Can only abstract positive cubes\n");
-    manager->errorCode = CUDD_INVALID_ARG;
-    return(NULL);
-    }
-
-    do {
-    manager->reordered = 0;
-    res = cuddBddExistAbstractRecur(manager, Cudd_Not(f), cube);
-    } while (manager->reordered == 1);
-    if (res != NULL) res = Cudd_Not(res);
-
-    return(res);
-
-} /* end of Cudd_bddUnivAbstract */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Computes the boolean difference of f with respect to x.]
-
-  Description [Computes the boolean difference of f with respect to the
-  variable with index x.  Returns the BDD of the boolean difference if
-  successful; NULL otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     []
-
-******************************************************************************/
-DdNode *
-Cudd_bddBooleanDiff(
-  DdManager * manager,
-  DdNode * f,
-  int  x)
-{
-    DdNode *res, *var;
-
-    /* If the variable is not currently in the manager, f cannot
-    ** depend on it.
-    */
-    if (x >= manager->size) return(Cudd_Not(DD_ONE(manager)));
-    var = manager->vars[x];
-
-    do {
-    manager->reordered = 0;
-    res = cuddBddBooleanDiffRecur(manager, Cudd_Regular(f), var);
-    } while (manager->reordered == 1);
-
-    return(res);
-
-} /* end of Cudd_bddBooleanDiff */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Checks whether a variable is dependent on others in a
-  function.]
-
-  Description [Checks whether a variable is dependent on others in a
-  function.  Returns 1 if the variable is dependent; 0 otherwise. No
-  new nodes are created.]
-
-  SideEffects [None]
-
-  SeeAlso     []
-
-******************************************************************************/
-int
-Cudd_bddVarIsDependent(
-  DdManager *dd,        /* manager */
-  DdNode *f,            /* function */
-  DdNode *var            /* variable */)
-{
-    DdNode *F, *res, *zero, *ft, *fe;
-    unsigned topf, level;
-    DdNode *(*cacheOp)(DdManager *, DdNode *, DdNode *);
-    int retval;
-
-    zero = Cudd_Not(DD_ONE(dd));
-    if (Cudd_IsConstant(f)) return(f == zero);
-
-    /* From now on f is not constant. */
-    F = Cudd_Regular(f);
-    topf = (unsigned) dd->perm[F->index];
-    level = (unsigned) dd->perm[var->index];
-
-    /* Check terminal case. If topf > index of var, f does not depend on var.
-    ** Therefore, var is not dependent in f. */
-    if (topf > level) {
-    return(0);
-    }
-
-    cacheOp =
-    (DdNode *(*)(DdManager *, DdNode *, DdNode *)) Cudd_bddVarIsDependent;
-    res = cuddCacheLookup2(dd,cacheOp,f,var);
-    if (res != NULL) {
-    return(res != zero);
-    }
-
-    /* Compute cofactors. */
-    ft = Cudd_NotCond(cuddT(F), f != F);
-    fe = Cudd_NotCond(cuddE(F), f != F);
-
-    if (topf == level) {
-    retval = Cudd_bddLeq(dd,ft,Cudd_Not(fe));
-    } else {
-    retval = Cudd_bddVarIsDependent(dd,ft,var) &&
-        Cudd_bddVarIsDependent(dd,fe,var);
-    }
-
-    cuddCacheInsert2(dd,cacheOp,f,var,Cudd_NotCond(zero,retval));
-
-    return(retval);
-
-} /* Cudd_bddVarIsDependent */
-
-
-/*---------------------------------------------------------------------------*/
-/* Definition of internal functions                                          */
-/*---------------------------------------------------------------------------*/
-
-
-/**Function********************************************************************
-
-  Synopsis    [Performs the recursive steps of Cudd_bddExistAbstract.]
-
-  Description [Performs the recursive steps of Cudd_bddExistAbstract.
-  Returns the BDD obtained by abstracting the variables
-  of cube from f if successful; NULL otherwise. It is also used by
-  Cudd_bddUnivAbstract.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_bddExistAbstract Cudd_bddUnivAbstract]
-
-******************************************************************************/
-DdNode *
-cuddBddExistAbstractRecur(
-  DdManager * manager,
-  DdNode * f,
-  DdNode * cube)
-{
-    DdNode    *F, *T, *E, *res, *res1, *res2, *one;
-
-    statLine(manager);
-    one = DD_ONE(manager);
-    F = Cudd_Regular(f);
-
-    /* Cube is guaranteed to be a cube at this point. */    
-    if (cube == one || F == one) {  
-        return(f);
-    }
-    /* From now on, f and cube are non-constant. */
-
-    /* Abstract a variable that does not appear in f. */
-    while (manager->perm[F->index] > manager->perm[cube->index]) {
-    cube = cuddT(cube);
-    if (cube == one) return(f);
-    }
-
-    /* Check the cache. */
-    if (F->ref != 1 && (res = cuddCacheLookup2(manager, Cudd_bddExistAbstract, f, cube)) != NULL) {
-    return(res);
-    }
-
-    /* Compute the cofactors of f. */
-    T = cuddT(F); E = cuddE(F);
-    if (f != F) {
-    T = Cudd_Not(T); E = Cudd_Not(E);
-    }
-
-    /* If the two indices are the same, so are their levels. */
-    if (F->index == cube->index) {
-    if (T == one || E == one || T == Cudd_Not(E)) {
-        return(one);
-    }
-    res1 = cuddBddExistAbstractRecur(manager, T, cuddT(cube));
-    if (res1 == NULL) return(NULL);
-    if (res1 == one) {
-        if (F->ref != 1)
-        cuddCacheInsert2(manager, Cudd_bddExistAbstract, f, cube, one);
-        return(one);
-    }
-        cuddRef(res1);
-    res2 = cuddBddExistAbstractRecur(manager, E, cuddT(cube));
-    if (res2 == NULL) {
-        Cudd_IterDerefBdd(manager,res1);
-        return(NULL);
-    }
-        cuddRef(res2);
-    res = cuddBddAndRecur(manager, Cudd_Not(res1), Cudd_Not(res2));
-    if (res == NULL) {
-        Cudd_IterDerefBdd(manager, res1);
-        Cudd_IterDerefBdd(manager, res2);
-        return(NULL);
-    }
-    res = Cudd_Not(res);
-    cuddRef(res);
-    Cudd_IterDerefBdd(manager, res1);
-    Cudd_IterDerefBdd(manager, res2);
-    if (F->ref != 1)
-        cuddCacheInsert2(manager, Cudd_bddExistAbstract, f, cube, res);
-    cuddDeref(res);
-        return(res);
-    } else { /* if (cuddI(manager,F->index) < cuddI(manager,cube->index)) */
-    res1 = cuddBddExistAbstractRecur(manager, T, cube);
-    if (res1 == NULL) return(NULL);
-        cuddRef(res1);
-    res2 = cuddBddExistAbstractRecur(manager, E, cube);
-    if (res2 == NULL) {
-        Cudd_IterDerefBdd(manager, res1);
-        return(NULL);
-    }
-        cuddRef(res2);
-    /* ITE takes care of possible complementation of res1 and of the
-        ** case in which res1 == res2. */
-    res = cuddBddIteRecur(manager, manager->vars[F->index], res1, res2);
-    if (res == NULL) {
-        Cudd_IterDerefBdd(manager, res1);
-        Cudd_IterDerefBdd(manager, res2);
-        return(NULL);
-    }
-    cuddDeref(res1);
-    cuddDeref(res2);
-    if (F->ref != 1)
-        cuddCacheInsert2(manager, Cudd_bddExistAbstract, f, cube, res);
-        return(res);
-    }        
-
-} /* end of cuddBddExistAbstractRecur */
-
-
-/**Function********************************************************************
-
-  Synopsis [Takes the exclusive OR of two BDDs and simultaneously abstracts the
-  variables in cube.]
-
-  Description [Takes the exclusive OR of two BDDs and simultaneously abstracts
-  the variables in cube. The variables are existentially abstracted.  Returns a
-  pointer to the result is successful; NULL otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_bddAndAbstract]
-
-******************************************************************************/
-DdNode *
-cuddBddXorExistAbstractRecur(
-  DdManager * manager,
-  DdNode * f,
-  DdNode * g,
-  DdNode * cube)
-{
-    DdNode *F, *fv, *fnv, *G, *gv, *gnv;
-    DdNode *one, *zero, *r, *t, *e, *Cube;
-    unsigned int topf, topg, topcube, top, 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 (cube == one) {
-    return(cuddBddXorRecur(manager, f, g));
-    }
-    if (f == one) {
-    return(cuddBddExistAbstractRecur(manager, Cudd_Not(g), cube));
-    }
-    if (g == one) {
-    return(cuddBddExistAbstractRecur(manager, Cudd_Not(f), cube));
-    }
-    if (f == zero) {
-    return(cuddBddExistAbstractRecur(manager, g, cube));
-    }
-    if (g == zero) {
-    return(cuddBddExistAbstractRecur(manager, f, cube));
-    }
-
-    /* At this point f, g, and cube are not constant. */
-
-    if (f > g) { /* Try to increase cache efficiency. */
-    DdNode *tmp = f;
-    f = g;
-    g = tmp;
-    }
-
-    /* Check cache. */
-    r = cuddCacheLookup(manager, DD_BDD_XOR_EXIST_ABSTRACT_TAG, f, g, cube);
-    if (r != NULL) {
-    return(r);
-    }
-
-    /* Here we can skip the use of cuddI, because the operands are known
-    ** to be non-constant.
-    */
-    F = Cudd_Regular(f);
-    topf = manager->perm[F->index];
-    G = Cudd_Regular(g);
-    topg = manager->perm[G->index];
-    top = ddMin(topf, topg);
-    topcube = manager->perm[cube->index];
-
-    if (topcube < top) {
-    return(cuddBddXorExistAbstractRecur(manager, f, g, cuddT(cube)));
-    }
-    /* Now, topcube >= top. */
-
-    if (topf == top) {
-    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 == top) {
-    gv = cuddT(G);
-    gnv = cuddE(G);
-    if (Cudd_IsComplement(g)) {
-        gv = Cudd_Not(gv);
-        gnv = Cudd_Not(gnv);
-    }
-    } else {
-    gv = gnv = g;
-    }
-
-    if (topcube == top) {
-    Cube = cuddT(cube);
-    } else {
-    Cube = cube;
-    }
-
-    t = cuddBddXorExistAbstractRecur(manager, fv, gv, Cube);
-    if (t == NULL) return(NULL);
-
-    /* Special case: 1 OR anything = 1. Hence, no need to compute
-    ** the else branch if t is 1.
-    */
-    if (t == one && topcube == top) {
-    cuddCacheInsert(manager, DD_BDD_XOR_EXIST_ABSTRACT_TAG, f, g, cube, one);
-    return(one);
-    }
-    cuddRef(t);
-
-    e = cuddBddXorExistAbstractRecur(manager, fnv, gnv, Cube);
-    if (e == NULL) {
-    Cudd_IterDerefBdd(manager, t);
-    return(NULL);
-    }
-    cuddRef(e);
-
-    if (topcube == top) {    /* abstract */
-    r = cuddBddAndRecur(manager, Cudd_Not(t), Cudd_Not(e));
-    if (r == NULL) {
-        Cudd_IterDerefBdd(manager, t);
-        Cudd_IterDerefBdd(manager, e);
-        return(NULL);
-    }
-    r = Cudd_Not(r);
-    cuddRef(r);
-    Cudd_IterDerefBdd(manager, t);
-    Cudd_IterDerefBdd(manager, e);
-    cuddDeref(r);
-    } else if (t == e) {
-    r = t;
-    cuddDeref(t);
-    cuddDeref(e);
-    } 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);
-    }
-    cuddCacheInsert(manager, DD_BDD_XOR_EXIST_ABSTRACT_TAG, f, g, cube, r);
-    return (r);
-
-} /* end of cuddBddXorExistAbstractRecur */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Performs the recursive steps of Cudd_bddBoleanDiff.]
-
-  Description [Performs the recursive steps of Cudd_bddBoleanDiff.
-  Returns the BDD obtained by XORing the cofactors of f with respect to
-  var if successful; NULL otherwise. Exploits the fact that dF/dx =
-  dF'/dx.]
-
-  SideEffects [None]
-
-  SeeAlso     []
-
-******************************************************************************/
-DdNode *
-cuddBddBooleanDiffRecur(
-  DdManager * manager,
-  DdNode * f,
-  DdNode * var)
-{
-    DdNode *T, *E, *res, *res1, *res2;
-
-    statLine(manager);
-    if (cuddI(manager,f->index) > manager->perm[var->index]) {
-    /* f does not depend on var. */
-    return(Cudd_Not(DD_ONE(manager)));
-    }
-
-    /* From now on, f is non-constant. */
-
-    /* If the two indices are the same, so are their levels. */
-    if (f->index == var->index) {
-    res = cuddBddXorRecur(manager, cuddT(f), cuddE(f));
-        return(res);
-    }
-
-    /* From now on, cuddI(manager,f->index) < cuddI(manager,cube->index). */
-
-    /* Check the cache. */
-    res = cuddCacheLookup2(manager, cuddBddBooleanDiffRecur, f, var);
-    if (res != NULL) {
-    return(res);
-    }
-
-    /* Compute the cofactors of f. */
-    T = cuddT(f); E = cuddE(f);
-
-    res1 = cuddBddBooleanDiffRecur(manager, T, var);
-    if (res1 == NULL) return(NULL);
-    cuddRef(res1);
-    res2 = cuddBddBooleanDiffRecur(manager, Cudd_Regular(E), var);
-    if (res2 == NULL) {
-    Cudd_IterDerefBdd(manager, res1);
-    return(NULL);
-    }
-    cuddRef(res2);
-    /* ITE takes care of possible complementation of res1 and of the
-    ** case in which res1 == res2. */
-    res = cuddBddIteRecur(manager, manager->vars[f->index], res1, res2);
-    if (res == NULL) {
-    Cudd_IterDerefBdd(manager, res1);
-    Cudd_IterDerefBdd(manager, res2);
-    return(NULL);
-    }
-    cuddDeref(res1);
-    cuddDeref(res2);
-    cuddCacheInsert2(manager, cuddBddBooleanDiffRecur, f, var, res);
-    return(res);
-
-} /* end of cuddBddBooleanDiffRecur */
-
-
-/*---------------------------------------------------------------------------*/
-/* Definition of static functions                                            */
-/*---------------------------------------------------------------------------*/
-
-/**Function********************************************************************
-
-  Synopsis [Checks whether cube is an BDD representing the product of
-  positive literals.]
-
-  Description [Returns 1 in case of success; 0 otherwise.]
-
-  SideEffects [None]
-
-******************************************************************************/
-static int
-bddCheckPositiveCube(
-  DdManager * manager,
-  DdNode * cube)
-{
-    if (Cudd_IsComplement(cube)) return(0);
-    if (cube == DD_ONE(manager)) return(1);
-    if (cuddIsConstant(cube)) return(0);
-    if (cuddE(cube) == Cudd_Not(DD_ONE(manager))) {
-        return(bddCheckPositiveCube(manager, cuddT(cube)));
-    }
-    return(0);
-
-} /* end of bddCheckPositiveCube */
-