diff options
Diffstat (limited to 'src/misc/extra/extraBddTime.c')
| -rw-r--r-- | src/misc/extra/extraBddTime.c | 660 |
1 files changed, 0 insertions, 660 deletions
diff --git a/src/misc/extra/extraBddTime.c b/src/misc/extra/extraBddTime.c deleted file mode 100644 index dc9ff147..00000000 --- a/src/misc/extra/extraBddTime.c +++ /dev/null @@ -1,660 +0,0 @@ -/**CFile**************************************************************** - - FileName [extraBddTime.c] - - PackageName [extra] - - Synopsis [Procedures to control runtime in BDD operators.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 2.0. Started - September 1, 2003.] - - Revision [$Id: extraBddTime.c,v 1.0 2003/05/21 18:03:50 alanmi Exp $] - -***********************************************************************/ - -#include "extraBdd.h" - -ABC_NAMESPACE_IMPL_START - - -/*---------------------------------------------------------------------------*/ -/* Constant declarations */ -/*---------------------------------------------------------------------------*/ - -#define CHECK_FACTOR 10 - -/*---------------------------------------------------------------------------*/ -/* Stucture declarations */ -/*---------------------------------------------------------------------------*/ - -/*---------------------------------------------------------------------------*/ -/* Type declarations */ -/*---------------------------------------------------------------------------*/ - - -/*---------------------------------------------------------------------------*/ -/* Variable declarations */ -/*---------------------------------------------------------------------------*/ - - - -/*---------------------------------------------------------------------------*/ -/* Macro declarations */ -/*---------------------------------------------------------------------------*/ - - -/**AutomaticStart*************************************************************/ - -/*---------------------------------------------------------------------------*/ -/* Static function prototypes */ -/*---------------------------------------------------------------------------*/ - -static DdNode * cuddBddAndRecurTime( DdManager * manager, DdNode * f, DdNode * g, int * pRecCalls, int TimeOut ); -static DdNode * cuddBddAndAbstractRecurTime( DdManager * manager, DdNode * f, DdNode * g, DdNode * cube, int * pRecCalls, int TimeOut ); -static DdNode * extraTransferPermuteTime( DdManager * ddS, DdManager * ddD, DdNode * f, int * Permute, int TimeOut ); -static DdNode * extraTransferPermuteRecurTime( DdManager * ddS, DdManager * ddD, DdNode * f, st__table * table, int * Permute, int TimeOut ); - -/**AutomaticEnd***************************************************************/ - - -/*---------------------------------------------------------------------------*/ -/* Definition of exported functions */ -/*---------------------------------------------------------------------------*/ - -/**Function******************************************************************** - - Synopsis [Computes the conjunction of two BDDs f and g.] - - Description [Computes the conjunction of two BDDs f and g. Returns a - pointer to the resulting BDD if successful; NULL if the intermediate - result blows up.] - - SideEffects [None] - - SeeAlso [Cudd_bddIte Cudd_addApply Cudd_bddAndAbstract Cudd_bddIntersect - Cudd_bddOr Cudd_bddNand Cudd_bddNor Cudd_bddXor Cudd_bddXnor] - -******************************************************************************/ -DdNode * -Extra_bddAndTime( - DdManager * dd, - DdNode * f, - DdNode * g, - int TimeOut) -{ - DdNode *res; - int Counter = 0; - - do { - dd->reordered = 0; - res = cuddBddAndRecurTime(dd,f,g, &Counter, TimeOut); - } while (dd->reordered == 1); - return(res); - -} /* end of Extra_bddAndTime */ - -/**Function******************************************************************** - - Synopsis [Takes the AND of two BDDs and simultaneously abstracts the - variables in cube.] - - Description [Takes the AND 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. - Cudd_bddAndAbstract implements the semiring matrix multiplication - algorithm for the boolean semiring.] - - SideEffects [None] - - SeeAlso [Cudd_addMatrixMultiply Cudd_addTriangle Cudd_bddAnd] - -******************************************************************************/ -DdNode * -Extra_bddAndAbstractTime( - DdManager * manager, - DdNode * f, - DdNode * g, - DdNode * cube, - int TimeOut) -{ - DdNode *res; - int Counter = 0; - - do { - manager->reordered = 0; - res = cuddBddAndAbstractRecurTime(manager, f, g, cube, &Counter, TimeOut); - } while (manager->reordered == 1); - return(res); - -} /* end of Extra_bddAndAbstractTime */ - -/**Function******************************************************************** - - Synopsis [Convert a {A,B}DD from a manager to another with variable remapping.] - - Description [Convert a {A,B}DD from a manager to another one. The orders of the - variables in the two managers may be different. Returns a - pointer to the {A,B}DD in the destination manager if successful; NULL - otherwise. The i-th entry in the array Permute tells what is the index - of the i-th variable from the old manager in the new manager.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -DdNode * Extra_TransferPermuteTime( DdManager * ddSource, DdManager * ddDestination, DdNode * f, int * Permute, int TimeOut ) -{ - DdNode * bRes; - do - { - ddDestination->reordered = 0; - bRes = extraTransferPermuteTime( ddSource, ddDestination, f, Permute, TimeOut ); - } - while ( ddDestination->reordered == 1 ); - return ( bRes ); - -} /* end of Extra_TransferPermuteTime */ - - -/*---------------------------------------------------------------------------*/ -/* Definition of internal functions */ -/*---------------------------------------------------------------------------*/ - -/**Function******************************************************************** - - Synopsis [Implements the recursive step of Cudd_bddAnd.] - - Description [Implements the recursive step of Cudd_bddAnd by taking - the conjunction of two BDDs. Returns a pointer to the result is - successful; NULL otherwise.] - - SideEffects [None] - - SeeAlso [Cudd_bddAnd] - -******************************************************************************/ -DdNode * -cuddBddAndRecurTime( - DdManager * manager, - DdNode * f, - DdNode * g, - int * pRecCalls, - int TimeOut) -{ - DdNode *F, *fv, *fnv, *G, *gv, *gnv; - DdNode *one, *r, *t, *e; - unsigned int topf, topg, index; - - statLine(manager); - one = DD_ONE(manager); - - /* Terminal cases. */ - F = Cudd_Regular(f); - G = Cudd_Regular(g); - if (F == G) { - if (f == g) return(f); - else return(Cudd_Not(one)); - } - if (F == one) { - if (f == one) return(g); - else return(f); - } - if (G == one) { - if (g == one) return(f); - else return(g); - } - - /* At this point f and g are not constant. */ - if (f > g) { /* Try to increase cache efficiency. */ - DdNode *tmp = f; - f = g; - g = tmp; - F = Cudd_Regular(f); - G = Cudd_Regular(g); - } - - /* Check cache. */ - if (F->ref != 1 || G->ref != 1) { - r = cuddCacheLookup2(manager, Cudd_bddAnd, f, g); - if (r != NULL) return(r); - } - -// if ( TimeOut && ((*pRecCalls)++ % CHECK_FACTOR) == 0 && TimeOut < Abc_Clock() ) - if ( TimeOut && Abc_Clock() > TimeOut ) - return NULL; - - /* Here we can skip the use of cuddI, because the operands are known - ** to be non-constant. - */ - topf = manager->perm[F->index]; - topg = manager->perm[G->index]; - - /* Compute cofactors. */ - if (topf <= topg) { - index = F->index; - fv = cuddT(F); - fnv = cuddE(F); - if (Cudd_IsComplement(f)) { - fv = Cudd_Not(fv); - fnv = Cudd_Not(fnv); - } - } else { - index = G->index; - fv = fnv = f; - } - - if (topg <= topf) { - gv = cuddT(G); - gnv = cuddE(G); - if (Cudd_IsComplement(g)) { - gv = Cudd_Not(gv); - gnv = Cudd_Not(gnv); - } - } else { - gv = gnv = g; - } - - t = cuddBddAndRecurTime(manager, fv, gv, pRecCalls, TimeOut); - if (t == NULL) return(NULL); - cuddRef(t); - - e = cuddBddAndRecurTime(manager, fnv, gnv, pRecCalls, TimeOut); - if (e == NULL) { - Cudd_IterDerefBdd(manager, t); - return(NULL); - } - cuddRef(e); - - if (t == e) { - r = t; - } else { - if (Cudd_IsComplement(t)) { - r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e)); - if (r == NULL) { - Cudd_IterDerefBdd(manager, t); - Cudd_IterDerefBdd(manager, e); - return(NULL); - } - r = Cudd_Not(r); - } else { - r = cuddUniqueInter(manager,(int)index,t,e); - if (r == NULL) { - Cudd_IterDerefBdd(manager, t); - Cudd_IterDerefBdd(manager, e); - return(NULL); - } - } - } - cuddDeref(e); - cuddDeref(t); - if (F->ref != 1 || G->ref != 1) - cuddCacheInsert2(manager, Cudd_bddAnd, f, g, r); - return(r); - -} /* end of cuddBddAndRecur */ - - -/**Function******************************************************************** - - Synopsis [Takes the AND of two BDDs and simultaneously abstracts the - variables in cube.] - - Description [Takes the AND 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 * -cuddBddAndAbstractRecurTime( - DdManager * manager, - DdNode * f, - DdNode * g, - DdNode * cube, - int * pRecCalls, - int TimeOut) -{ - DdNode *F, *ft, *fe, *G, *gt, *ge; - DdNode *one, *zero, *r, *t, *e; - unsigned int topf, topg, topcube, top, index; - - statLine(manager); - one = DD_ONE(manager); - zero = Cudd_Not(one); - - /* Terminal cases. */ - if (f == zero || g == zero || f == Cudd_Not(g)) return(zero); - if (f == one && g == one) return(one); - - if (cube == one) { - return(cuddBddAndRecurTime(manager, f, g, pRecCalls, TimeOut)); - } - if (f == one || f == g) { - return(cuddBddExistAbstractRecur(manager, g, cube)); - } - if (g == one) { - 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; - } - - /* Here we can skip the use of cuddI, because the operands are known - ** to be non-constant. - */ - F = Cudd_Regular(f); - G = Cudd_Regular(g); - topf = manager->perm[F->index]; - topg = manager->perm[G->index]; - top = ddMin(topf, topg); - topcube = manager->perm[cube->index]; - - while (topcube < top) { - cube = cuddT(cube); - if (cube == one) { - return(cuddBddAndRecurTime(manager, f, g, pRecCalls, TimeOut)); - } - topcube = manager->perm[cube->index]; - } - /* Now, topcube >= top. */ - - /* Check cache. */ - if (F->ref != 1 || G->ref != 1) { - r = cuddCacheLookup(manager, DD_BDD_AND_ABSTRACT_TAG, f, g, cube); - if (r != NULL) { - return(r); - } - } - -// if ( TimeOut && ((*pRecCalls)++ % CHECK_FACTOR) == 0 && TimeOut < Abc_Clock() ) - if ( TimeOut && Abc_Clock() > TimeOut ) - return NULL; - - if (topf == top) { - index = F->index; - ft = cuddT(F); - fe = cuddE(F); - if (Cudd_IsComplement(f)) { - ft = Cudd_Not(ft); - fe = Cudd_Not(fe); - } - } else { - index = G->index; - ft = fe = f; - } - - if (topg == top) { - gt = cuddT(G); - ge = cuddE(G); - if (Cudd_IsComplement(g)) { - gt = Cudd_Not(gt); - ge = Cudd_Not(ge); - } - } else { - gt = ge = g; - } - - if (topcube == top) { /* quantify */ - DdNode *Cube = cuddT(cube); - t = cuddBddAndAbstractRecurTime(manager, ft, gt, Cube, pRecCalls, TimeOut); - if (t == NULL) return(NULL); - /* Special case: 1 OR anything = 1. Hence, no need to compute - ** the else branch if t is 1. Likewise t + t * anything == t. - ** Notice that t == fe implies that fe does not depend on the - ** variables in Cube. Likewise for t == ge. - */ - if (t == one || t == fe || t == ge) { - if (F->ref != 1 || G->ref != 1) - cuddCacheInsert(manager, DD_BDD_AND_ABSTRACT_TAG, - f, g, cube, t); - return(t); - } - cuddRef(t); - /* Special case: t + !t * anything == t + anything. */ - if (t == Cudd_Not(fe)) { - e = cuddBddExistAbstractRecur(manager, ge, Cube); - } else if (t == Cudd_Not(ge)) { - e = cuddBddExistAbstractRecur(manager, fe, Cube); - } else { - e = cuddBddAndAbstractRecurTime(manager, fe, ge, Cube, pRecCalls, TimeOut); - } - if (e == NULL) { - Cudd_IterDerefBdd(manager, t); - return(NULL); - } - if (t == e) { - r = t; - cuddDeref(t); - } else { - cuddRef(e); - r = cuddBddAndRecurTime(manager, Cudd_Not(t), Cudd_Not(e), pRecCalls, TimeOut); - if (r == NULL) { - Cudd_IterDerefBdd(manager, t); - Cudd_IterDerefBdd(manager, e); - return(NULL); - } - r = Cudd_Not(r); - cuddRef(r); - Cudd_DelayedDerefBdd(manager, t); - Cudd_DelayedDerefBdd(manager, e); - cuddDeref(r); - } - } else { - t = cuddBddAndAbstractRecurTime(manager, ft, gt, cube, pRecCalls, TimeOut); - if (t == NULL) return(NULL); - cuddRef(t); - e = cuddBddAndAbstractRecurTime(manager, fe, ge, cube, pRecCalls, TimeOut); - if (e == NULL) { - Cudd_IterDerefBdd(manager, t); - return(NULL); - } - if (t == e) { - r = t; - cuddDeref(t); - } else { - cuddRef(e); - if (Cudd_IsComplement(t)) { - r = cuddUniqueInter(manager, (int) index, - Cudd_Not(t), Cudd_Not(e)); - if (r == NULL) { - Cudd_IterDerefBdd(manager, t); - Cudd_IterDerefBdd(manager, e); - return(NULL); - } - r = Cudd_Not(r); - } else { - r = cuddUniqueInter(manager,(int)index,t,e); - if (r == NULL) { - Cudd_IterDerefBdd(manager, t); - Cudd_IterDerefBdd(manager, e); - return(NULL); - } - } - cuddDeref(e); - cuddDeref(t); - } - } - - if (F->ref != 1 || G->ref != 1) - cuddCacheInsert(manager, DD_BDD_AND_ABSTRACT_TAG, f, g, cube, r); - return (r); - -} /* end of cuddBddAndAbstractRecur */ - -/*---------------------------------------------------------------------------*/ -/* Definition of static functions */ -/*---------------------------------------------------------------------------*/ - -/**Function******************************************************************** - - Synopsis [Convert a BDD from a manager to another one.] - - Description [Convert a BDD from a manager to another one. Returns a - pointer to the BDD in the destination manager if successful; NULL - otherwise.] - - SideEffects [None] - - SeeAlso [Extra_TransferPermute] - -******************************************************************************/ -DdNode * extraTransferPermuteTime( DdManager * ddS, DdManager * ddD, DdNode * f, int * Permute, int TimeOut ) -{ - DdNode *res; - st__table *table = NULL; - st__generator *gen = NULL; - DdNode *key, *value; - - table = st__init_table( st__ptrcmp, st__ptrhash ); - if ( table == NULL ) - goto failure; - res = extraTransferPermuteRecurTime( ddS, ddD, f, table, Permute, TimeOut ); - if ( res != NULL ) - cuddRef( res ); - - /* Dereference all elements in the table and dispose of the table. - ** This must be done also if res is NULL to avoid leaks in case of - ** reordering. */ - gen = st__init_gen( table ); - if ( gen == NULL ) - goto failure; - while ( st__gen( gen, ( const char ** ) &key, ( char ** ) &value ) ) - { - Cudd_RecursiveDeref( ddD, value ); - } - st__free_gen( gen ); - gen = NULL; - st__free_table( table ); - table = NULL; - - if ( res != NULL ) - cuddDeref( res ); - return ( res ); - - failure: - if ( table != NULL ) - st__free_table( table ); - if ( gen != NULL ) - st__free_gen( gen ); - return ( NULL ); - -} /* end of extraTransferPermuteTime */ - - -/**Function******************************************************************** - - Synopsis [Performs the recursive step of Extra_TransferPermute.] - - Description [Performs the recursive step of Extra_TransferPermute. - Returns a pointer to the result if successful; NULL otherwise.] - - SideEffects [None] - - SeeAlso [extraTransferPermuteTime] - -******************************************************************************/ -static DdNode * -extraTransferPermuteRecurTime( - DdManager * ddS, - DdManager * ddD, - DdNode * f, - st__table * table, - int * Permute, - int TimeOut ) -{ - DdNode *ft, *fe, *t, *e, *var, *res; - DdNode *one, *zero; - int index; - int comple = 0; - - statLine( ddD ); - one = DD_ONE( ddD ); - comple = Cudd_IsComplement( f ); - - /* Trivial cases. */ - if ( Cudd_IsConstant( f ) ) - return ( Cudd_NotCond( one, comple ) ); - - - /* Make canonical to increase the utilization of the cache. */ - f = Cudd_NotCond( f, comple ); - /* Now f is a regular pointer to a non-constant node. */ - - /* Check the cache. */ - if ( st__lookup( table, ( char * ) f, ( char ** ) &res ) ) - return ( Cudd_NotCond( res, comple ) ); - - if ( TimeOut && Abc_Clock() > TimeOut ) - return NULL; - - /* Recursive step. */ - if ( Permute ) - index = Permute[f->index]; - else - index = f->index; - - ft = cuddT( f ); - fe = cuddE( f ); - - t = extraTransferPermuteRecurTime( ddS, ddD, ft, table, Permute, TimeOut ); - if ( t == NULL ) - { - return ( NULL ); - } - cuddRef( t ); - - e = extraTransferPermuteRecurTime( ddS, ddD, fe, table, Permute, TimeOut ); - if ( e == NULL ) - { - Cudd_RecursiveDeref( ddD, t ); - return ( NULL ); - } - cuddRef( e ); - - zero = Cudd_Not(ddD->one); - var = cuddUniqueInter( ddD, index, one, zero ); - if ( var == NULL ) - { - Cudd_RecursiveDeref( ddD, t ); - Cudd_RecursiveDeref( ddD, e ); - return ( NULL ); - } - res = cuddBddIteRecur( ddD, var, t, e ); - - if ( res == NULL ) - { - Cudd_RecursiveDeref( ddD, t ); - Cudd_RecursiveDeref( ddD, e ); - return ( NULL ); - } - cuddRef( res ); - Cudd_RecursiveDeref( ddD, t ); - Cudd_RecursiveDeref( ddD, e ); - - if ( st__add_direct( table, ( char * ) f, ( char * ) res ) == - st__OUT_OF_MEM ) - { - Cudd_RecursiveDeref( ddD, res ); - return ( NULL ); - } - return ( Cudd_NotCond( res, comple ) ); - -} /* end of extraTransferPermuteRecurTime */ - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// -ABC_NAMESPACE_IMPL_END - |