From 24f2a120f2203acc8038ccce4e8dd141564a7a04 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 24 Aug 2015 21:09:50 -0700 Subject: Changes to be able to compile ABC without CUDD. --- src/bdd/extrab/extraBdd.h | 317 ++++++ src/bdd/extrab/extraBddAuto.c | 1563 +++++++++++++++++++++++++++ src/bdd/extrab/extraBddCas.c | 1235 +++++++++++++++++++++ src/bdd/extrab/extraBddImage.c | 1162 ++++++++++++++++++++ src/bdd/extrab/extraBddKmap.c | 876 +++++++++++++++ src/bdd/extrab/extraBddMisc.c | 2342 ++++++++++++++++++++++++++++++++++++++++ src/bdd/extrab/extraBddSymm.c | 1474 +++++++++++++++++++++++++ src/bdd/extrab/extraBddTime.c | 660 +++++++++++ src/bdd/extrab/extraBddUnate.c | 646 +++++++++++ src/bdd/extrab/module.make | 8 + 10 files changed, 10283 insertions(+) create mode 100644 src/bdd/extrab/extraBdd.h create mode 100644 src/bdd/extrab/extraBddAuto.c create mode 100644 src/bdd/extrab/extraBddCas.c create mode 100644 src/bdd/extrab/extraBddImage.c create mode 100644 src/bdd/extrab/extraBddKmap.c create mode 100644 src/bdd/extrab/extraBddMisc.c create mode 100644 src/bdd/extrab/extraBddSymm.c create mode 100644 src/bdd/extrab/extraBddTime.c create mode 100644 src/bdd/extrab/extraBddUnate.c create mode 100644 src/bdd/extrab/module.make (limited to 'src/bdd/extrab') diff --git a/src/bdd/extrab/extraBdd.h b/src/bdd/extrab/extraBdd.h new file mode 100644 index 00000000..3dbc6264 --- /dev/null +++ b/src/bdd/extrab/extraBdd.h @@ -0,0 +1,317 @@ +/**CFile**************************************************************** + + FileName [extraBdd.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [extra] + + Synopsis [Various reusable software utilities.] + + Description [This library contains a number of operators and + traversal routines developed to extend the functionality of + CUDD v.2.3.x, by Fabio Somenzi (http://vlsi.colorado.edu/~fabio/) + To compile your code with the library, #include "extra.h" + in your source files and link your project to CUDD and this + library. Use the library at your own risk and with caution. + Note that debugging of some operators still continues.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: extraBdd.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef ABC__misc__extra__extra_bdd_h +#define ABC__misc__extra__extra_bdd_h + + +#ifdef _WIN32 +#define inline __inline // compatible with MS VS 6.0 +#endif + +/*---------------------------------------------------------------------------*/ +/* Nested includes */ +/*---------------------------------------------------------------------------*/ + +#include +#include +#include +#include + +#include "misc/st/st.h" +#include "bdd/cudd/cuddInt.h" +#include "misc/extra/extra.h" + + +ABC_NAMESPACE_HEADER_START + + +/*---------------------------------------------------------------------------*/ +/* Constant declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Stucture declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Type declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Variable declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Macro declarations */ +/*---------------------------------------------------------------------------*/ + +/* constants of the manager */ +#define b0 Cudd_Not((dd)->one) +#define b1 (dd)->one +#define z0 (dd)->zero +#define z1 (dd)->one +#define a0 (dd)->zero +#define a1 (dd)->one + +// hash key macros +#define hashKey1(a,TSIZE) \ +((ABC_PTRUINT_T)(a) % TSIZE) + +#define hashKey2(a,b,TSIZE) \ +(((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b) * DD_P1) % TSIZE) + +#define hashKey3(a,b,c,TSIZE) \ +(((((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b)) * DD_P1 + (ABC_PTRUINT_T)(c)) * DD_P2 ) % TSIZE) + +#define hashKey4(a,b,c,d,TSIZE) \ +((((((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b)) * DD_P1 + (ABC_PTRUINT_T)(c)) * DD_P2 + \ + (ABC_PTRUINT_T)(d)) * DD_P3) % TSIZE) + +#define hashKey5(a,b,c,d,e,TSIZE) \ +(((((((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b)) * DD_P1 + (ABC_PTRUINT_T)(c)) * DD_P2 + \ + (ABC_PTRUINT_T)(d)) * DD_P3 + (ABC_PTRUINT_T)(e)) * DD_P1) % TSIZE) + +/*===========================================================================*/ +/* Various Utilities */ +/*===========================================================================*/ + +/*=== extraBddAuto.c ========================================================*/ + +extern DdNode * Extra_bddSpaceFromFunctionFast( DdManager * dd, DdNode * bFunc ); +extern DdNode * Extra_bddSpaceFromFunction( DdManager * dd, DdNode * bF, DdNode * bG ); +extern DdNode * extraBddSpaceFromFunction( DdManager * dd, DdNode * bF, DdNode * bG ); +extern DdNode * Extra_bddSpaceFromFunctionPos( DdManager * dd, DdNode * bFunc ); +extern DdNode * extraBddSpaceFromFunctionPos( DdManager * dd, DdNode * bFunc ); +extern DdNode * Extra_bddSpaceFromFunctionNeg( DdManager * dd, DdNode * bFunc ); +extern DdNode * extraBddSpaceFromFunctionNeg( DdManager * dd, DdNode * bFunc ); + +extern DdNode * Extra_bddSpaceCanonVars( DdManager * dd, DdNode * bSpace ); +extern DdNode * extraBddSpaceCanonVars( DdManager * dd, DdNode * bSpace ); + +extern DdNode * Extra_bddSpaceEquations( DdManager * dd, DdNode * bSpace ); +extern DdNode * Extra_bddSpaceEquationsNeg( DdManager * dd, DdNode * bSpace ); +extern DdNode * extraBddSpaceEquationsNeg( DdManager * dd, DdNode * bSpace ); +extern DdNode * Extra_bddSpaceEquationsPos( DdManager * dd, DdNode * bSpace ); +extern DdNode * extraBddSpaceEquationsPos( DdManager * dd, DdNode * bSpace ); + +extern DdNode * Extra_bddSpaceFromMatrixPos( DdManager * dd, DdNode * zA ); +extern DdNode * extraBddSpaceFromMatrixPos( DdManager * dd, DdNode * zA ); +extern DdNode * Extra_bddSpaceFromMatrixNeg( DdManager * dd, DdNode * zA ); +extern DdNode * extraBddSpaceFromMatrixNeg( DdManager * dd, DdNode * zA ); + +extern DdNode * Extra_bddSpaceReduce( DdManager * dd, DdNode * bFunc, DdNode * bCanonVars ); +extern DdNode ** Extra_bddSpaceExorGates( DdManager * dd, DdNode * bFuncRed, DdNode * zEquations ); + +/*=== extraBddCas.c =============================================================*/ + +/* performs the binary encoding of the set of function using the given vars */ +extern DdNode * Extra_bddEncodingBinary( DdManager * dd, DdNode ** pbFuncs, int nFuncs, DdNode ** pbVars, int nVars ); +/* solves the column encoding problem using a sophisticated method */ +extern DdNode * Extra_bddEncodingNonStrict( DdManager * dd, DdNode ** pbColumns, int nColumns, DdNode * bVarsCol, DdNode ** pCVars, int nMulti, int * pSimple ); +/* collects the nodes under the cut and, for each node, computes the sum of paths leading to it from the root */ +extern st__table * Extra_bddNodePathsUnderCut( DdManager * dd, DdNode * bFunc, int CutLevel ); +/* collects the nodes under the cut starting from the given set of ADD nodes */ +extern int Extra_bddNodePathsUnderCutArray( DdManager * dd, DdNode ** paNodes, DdNode ** pbCubes, int nNodes, DdNode ** paNodesRes, DdNode ** pbCubesRes, int CutLevel ); +/* find the profile of a DD (the number of edges crossing each level) */ +extern int Extra_ProfileWidth( DdManager * dd, DdNode * F, int * Profile, int CutLevel ); + +/*=== extraBddImage.c ================================================================*/ + +typedef struct Extra_ImageTree_t_ Extra_ImageTree_t; +extern Extra_ImageTree_t * Extra_bddImageStart( + DdManager * dd, DdNode * bCare, + int nParts, DdNode ** pbParts, + int nVars, DdNode ** pbVars, int fVerbose ); +extern DdNode * Extra_bddImageCompute( Extra_ImageTree_t * pTree, DdNode * bCare ); +extern void Extra_bddImageTreeDelete( Extra_ImageTree_t * pTree ); +extern DdNode * Extra_bddImageRead( Extra_ImageTree_t * pTree ); + +typedef struct Extra_ImageTree2_t_ Extra_ImageTree2_t; +extern Extra_ImageTree2_t * Extra_bddImageStart2( + DdManager * dd, DdNode * bCare, + int nParts, DdNode ** pbParts, + int nVars, DdNode ** pbVars, int fVerbose ); +extern DdNode * Extra_bddImageCompute2( Extra_ImageTree2_t * pTree, DdNode * bCare ); +extern void Extra_bddImageTreeDelete2( Extra_ImageTree2_t * pTree ); +extern DdNode * Extra_bddImageRead2( Extra_ImageTree2_t * pTree ); + +/*=== extraBddMisc.c ========================================================*/ + +extern DdNode * Extra_TransferPermute( DdManager * ddSource, DdManager * ddDestination, DdNode * f, int * Permute ); +extern DdNode * Extra_TransferLevelByLevel( DdManager * ddSource, DdManager * ddDestination, DdNode * f ); +extern DdNode * Extra_bddRemapUp( DdManager * dd, DdNode * bF ); +extern DdNode * Extra_bddMove( DdManager * dd, DdNode * bF, int nVars ); +extern DdNode * extraBddMove( DdManager * dd, DdNode * bF, DdNode * bFlag ); +extern void Extra_StopManager( DdManager * dd ); +extern void Extra_bddPrint( DdManager * dd, DdNode * F ); +extern void Extra_bddPrintSupport( DdManager * dd, DdNode * F ); +extern void extraDecomposeCover( DdManager* dd, DdNode* zC, DdNode** zC0, DdNode** zC1, DdNode** zC2 ); +extern int Extra_bddSuppSize( DdManager * dd, DdNode * bSupp ); +extern int Extra_bddSuppContainVar( DdManager * dd, DdNode * bS, DdNode * bVar ); +extern int Extra_bddSuppOverlapping( DdManager * dd, DdNode * S1, DdNode * S2 ); +extern int Extra_bddSuppDifferentVars( DdManager * dd, DdNode * S1, DdNode * S2, int DiffMax ); +extern int Extra_bddSuppCheckContainment( DdManager * dd, DdNode * bL, DdNode * bH, DdNode ** bLarge, DdNode ** bSmall ); +extern int * Extra_SupportArray( DdManager * dd, DdNode * F, int * support ); +extern int * Extra_VectorSupportArray( DdManager * dd, DdNode ** F, int n, int * support ); +extern DdNode * Extra_bddFindOneCube( DdManager * dd, DdNode * bF ); +extern DdNode * Extra_bddGetOneCube( DdManager * dd, DdNode * bFunc ); +extern DdNode * Extra_bddComputeRangeCube( DdManager * dd, int iStart, int iStop ); +extern DdNode * Extra_bddBitsToCube( DdManager * dd, int Code, int CodeWidth, DdNode ** pbVars, int fMsbFirst ); +extern DdNode * Extra_bddSupportNegativeCube( DdManager * dd, DdNode * f ); +extern int Extra_bddIsVar( DdNode * bFunc ); +extern DdNode * Extra_bddCreateAnd( DdManager * dd, int nVars ); +extern DdNode * Extra_bddCreateOr( DdManager * dd, int nVars ); +extern DdNode * Extra_bddCreateExor( DdManager * dd, int nVars ); +extern DdNode * Extra_zddPrimes( DdManager * dd, DdNode * F ); +extern void Extra_bddPermuteArray( DdManager * dd, DdNode ** bNodesIn, DdNode ** bNodesOut, int nNodes, int *permut ); +extern DdNode * Extra_bddComputeCube( DdManager * dd, DdNode ** bXVars, int nVars ); +extern DdNode * Extra_bddChangePolarity( DdManager * dd, DdNode * bFunc, DdNode * bVars ); +extern DdNode * extraBddChangePolarity( DdManager * dd, DdNode * bFunc, DdNode * bVars ); +extern int Extra_bddVarIsInCube( DdNode * bCube, int iVar ); +extern DdNode * Extra_bddAndPermute( DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode * bG, int * pPermute ); +extern int Extra_bddCountCubes( DdManager * dd, DdNode ** pFuncs, int nFuncs, int fMode, int nLimit, int * pGuide ); +extern void Extra_zddDumpPla( DdManager * dd, DdNode * zCover, int nVars, char * pFileName ); + +#ifndef ABC_PRB +#define ABC_PRB(dd,f) printf("%s = ", #f); Extra_bddPrint(dd,f); printf("\n") +#endif + +/*=== extraBddKmap.c ================================================================*/ + +/* displays the Karnaugh Map of a function */ +extern void Extra_PrintKMap( FILE * pFile, DdManager * dd, DdNode * OnSet, DdNode * OffSet, int nVars, DdNode ** XVars, int fSuppType, char ** pVarNames ); +/* displays the Karnaugh Map of a relation */ +extern void Extra_PrintKMapRelation( FILE * pFile, DdManager * dd, DdNode * OnSet, DdNode * OffSet, int nXVars, int nYVars, DdNode ** XVars, DdNode ** YVars ); + +/*=== extraBddSymm.c =================================================================*/ + +typedef struct Extra_SymmInfo_t_ Extra_SymmInfo_t; +struct Extra_SymmInfo_t_ { + int nVars; // the number of variables in the support + int nVarsMax; // the number of variables in the DD manager + int nSymms; // the number of pair-wise symmetries + int nNodes; // the number of nodes in a ZDD (if applicable) + int * pVars; // the list of all variables present in the support + char ** pSymms; // the symmetry information +}; + +/* computes the classical symmetry information for the function - recursive */ +extern Extra_SymmInfo_t * Extra_SymmPairsCompute( DdManager * dd, DdNode * bFunc ); +/* computes the classical symmetry information for the function - using naive approach */ +extern Extra_SymmInfo_t * Extra_SymmPairsComputeNaive( DdManager * dd, DdNode * bFunc ); +extern int Extra_bddCheckVarsSymmetricNaive( DdManager * dd, DdNode * bF, int iVar1, int iVar2 ); + +/* allocates the data structure */ +extern Extra_SymmInfo_t * Extra_SymmPairsAllocate( int nVars ); +/* deallocates the data structure */ +extern void Extra_SymmPairsDissolve( Extra_SymmInfo_t * ); +/* print the contents the data structure */ +extern void Extra_SymmPairsPrint( Extra_SymmInfo_t * ); +/* converts the ZDD into the Extra_SymmInfo_t structure */ +extern Extra_SymmInfo_t * Extra_SymmPairsCreateFromZdd( DdManager * dd, DdNode * zPairs, DdNode * bVars ); + +/* computes the classical symmetry information as a ZDD */ +extern DdNode * Extra_zddSymmPairsCompute( DdManager * dd, DdNode * bF, DdNode * bVars ); +extern DdNode * extraZddSymmPairsCompute( DdManager * dd, DdNode * bF, DdNode * bVars ); +/* returns a singleton-set ZDD containing all variables that are symmetric with the given one */ +extern DdNode * Extra_zddGetSymmetricVars( DdManager * dd, DdNode * bF, DdNode * bG, DdNode * bVars ); +extern DdNode * extraZddGetSymmetricVars( DdManager * dd, DdNode * bF, DdNode * bG, DdNode * bVars ); +/* converts a set of variables into a set of singleton subsets */ +extern DdNode * Extra_zddGetSingletons( DdManager * dd, DdNode * bVars ); +extern DdNode * extraZddGetSingletons( DdManager * dd, DdNode * bVars ); +/* filters the set of variables using the support of the function */ +extern DdNode * Extra_bddReduceVarSet( DdManager * dd, DdNode * bVars, DdNode * bF ); +extern DdNode * extraBddReduceVarSet( DdManager * dd, DdNode * bVars, DdNode * bF ); + +/* checks the possibility that the two vars are symmetric */ +extern int Extra_bddCheckVarsSymmetric( DdManager * dd, DdNode * bF, int iVar1, int iVar2 ); +extern DdNode * extraBddCheckVarsSymmetric( DdManager * dd, DdNode * bF, DdNode * bVars ); + +/* build the set of all tuples of K variables out of N from the BDD cube */ +extern DdNode * Extra_zddTuplesFromBdd( DdManager * dd, int K, DdNode * bVarsN ); +extern DdNode * extraZddTuplesFromBdd( DdManager * dd, DdNode * bVarsK, DdNode * bVarsN ); +/* selects one subset from a ZDD representing the set of subsets */ +extern DdNode * Extra_zddSelectOneSubset( DdManager * dd, DdNode * zS ); +extern DdNode * extraZddSelectOneSubset( DdManager * dd, DdNode * zS ); + +/*=== extraBddUnate.c =================================================================*/ + +extern DdNode * Extra_bddAndTime( DdManager * dd, DdNode * f, DdNode * g, int TimeOut ); +extern DdNode * Extra_bddAndAbstractTime( DdManager * manager, DdNode * f, DdNode * g, DdNode * cube, int TimeOut ); +extern DdNode * Extra_TransferPermuteTime( DdManager * ddSource, DdManager * ddDestination, DdNode * f, int * Permute, int TimeOut ); + +/*=== extraBddUnate.c =================================================================*/ + +typedef struct Extra_UnateVar_t_ Extra_UnateVar_t; +struct Extra_UnateVar_t_ { + unsigned iVar : 30; // index of the variable + unsigned Pos : 1; // 1 if positive unate + unsigned Neg : 1; // 1 if negative unate +}; + +typedef struct Extra_UnateInfo_t_ Extra_UnateInfo_t; +struct Extra_UnateInfo_t_ { + int nVars; // the number of variables in the support + int nVarsMax; // the number of variables in the DD manager + int nUnate; // the number of unate variables + Extra_UnateVar_t * pVars; // the array of variables present in the support +}; + +/* allocates the data structure */ +extern Extra_UnateInfo_t * Extra_UnateInfoAllocate( int nVars ); +/* deallocates the data structure */ +extern void Extra_UnateInfoDissolve( Extra_UnateInfo_t * ); +/* print the contents the data structure */ +extern void Extra_UnateInfoPrint( Extra_UnateInfo_t * ); +/* converts the ZDD into the Extra_SymmInfo_t structure */ +extern Extra_UnateInfo_t * Extra_UnateInfoCreateFromZdd( DdManager * dd, DdNode * zUnate, DdNode * bVars ); +/* naive check of unateness of one variable */ +extern int Extra_bddCheckUnateNaive( DdManager * dd, DdNode * bF, int iVar ); + +/* computes the unateness information for the function */ +extern Extra_UnateInfo_t * Extra_UnateComputeFast( DdManager * dd, DdNode * bFunc ); +extern Extra_UnateInfo_t * Extra_UnateComputeSlow( DdManager * dd, DdNode * bFunc ); + +/* computes the classical symmetry information as a ZDD */ +extern DdNode * Extra_zddUnateInfoCompute( DdManager * dd, DdNode * bF, DdNode * bVars ); +extern DdNode * extraZddUnateInfoCompute( DdManager * dd, DdNode * bF, DdNode * bVars ); + +/* converts a set of variables into a set of singleton subsets */ +extern DdNode * Extra_zddGetSingletonsBoth( DdManager * dd, DdNode * bVars ); +extern DdNode * extraZddGetSingletonsBoth( DdManager * dd, DdNode * bVars ); + +/**AutomaticEnd***************************************************************/ + + + +ABC_NAMESPACE_HEADER_END + + + +#endif /* __EXTRA_H__ */ diff --git a/src/bdd/extrab/extraBddAuto.c b/src/bdd/extrab/extraBddAuto.c new file mode 100644 index 00000000..5fb38aec --- /dev/null +++ b/src/bdd/extrab/extraBddAuto.c @@ -0,0 +1,1563 @@ +/**CFile**************************************************************** + + FileName [extraBddAuto.c] + + PackageName [extra] + + Synopsis [Computation of autosymmetries.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 2.0. Started - September 1, 2003.] + + Revision [$Id: extraBddAuto.c,v 1.0 2003/05/21 18:03:50 alanmi Exp $] + +***********************************************************************/ + +#include "extraBdd.h" + +ABC_NAMESPACE_IMPL_START + + +/*---------------------------------------------------------------------------*/ +/* Constant declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Stucture declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Type declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Variable declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Macro declarations */ +/*---------------------------------------------------------------------------*/ + + +/**AutomaticStart*************************************************************/ + +/*---------------------------------------------------------------------------*/ +/* Static function prototypes */ +/*---------------------------------------------------------------------------*/ + +/**AutomaticEnd***************************************************************/ + + +/* + LinearSpace(f) = Space(f,f) + + Space(f,g) + { + if ( f = const ) + { + if ( f = g ) return 1; + else return 0; + } + if ( g = const ) return 0; + return x' * Space(fx',gx') * Space(fx,gx) + x * Space(fx',gx) * Space(fx,gx'); + } + + Equations(s) = Pos(s) + Neg(s); + + Pos(s) + { + if ( s = 0 ) return 1; + if ( s = 1 ) return 0; + if ( sx'= 0 ) return Pos(sx) + x; + if ( sx = 0 ) return Pos(sx'); + return 1 * [Pos(sx') & Pos(sx)] + x * [Pos(sx') & Neg(sx)]; + } + + Neg(s) + { + if ( s = 0 ) return 1; + if ( s = 1 ) return 0; + if ( sx'= 0 ) return Neg(sx); + if ( sx = 0 ) return Neg(sx') + x; + return 1 * [Neg(sx') & Neg(sx)] + x * [Neg(sx') & Pos(sx)]; + } + + + SpaceP(A) + { + if ( A = 0 ) return 1; + if ( A = 1 ) return 1; + return x' * SpaceP(Ax') * SpaceP(Ax) + x * SpaceP(Ax') * SpaceN(Ax); + } + + SpaceN(A) + { + if ( A = 0 ) return 1; + if ( A = 1 ) return 0; + return x' * SpaceN(Ax') * SpaceN(Ax) + x * SpaceN(Ax') * SpaceP(Ax); + } + + + LinInd(A) + { + if ( A = const ) return 1; + if ( !LinInd(Ax') ) return 0; + if ( !LinInd(Ax) ) return 0; + if ( LinSumOdd(Ax') & LinSumEven(Ax) != 0 ) return 0; + if ( LinSumEven(Ax') & LinSumEven(Ax) != 0 ) return 0; + return 1; + } + + LinSumOdd(A) + { + if ( A = 0 ) return 0; // Odd0 ---e-- Odd1 + if ( A = 1 ) return 1; // \ o + Odd0 = LinSumOdd(Ax'); // x is absent // \ + Even0 = LinSumEven(Ax'); // x is absent // / o + Odd1 = LinSumOdd(Ax); // x is present // Even0 ---e-- Even1 + Even1 = LinSumEven(Ax); // x is absent + return 1 * [Odd0 + ExorP(Odd0, Even1)] + x * [Odd1 + ExorP(Odd1, Even0)]; + } + + LinSumEven(A) + { + if ( A = 0 ) return 0; + if ( A = 1 ) return 0; + Odd0 = LinSumOdd(Ax'); // x is absent + Even0 = LinSumEven(Ax'); // x is absent + Odd1 = LinSumOdd(Ax); // x is present + Even1 = LinSumEven(Ax); // x is absent + return 1 * [Even0 + Even1 + ExorP(Even0, Even1)] + x * [ExorP(Odd0, Odd1)]; + } + +*/ + +/*---------------------------------------------------------------------------*/ +/* Definition of exported functions */ +/*---------------------------------------------------------------------------*/ + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Extra_bddSpaceFromFunctionFast( DdManager * dd, DdNode * bFunc ) +{ + int * pSupport; + int * pPermute; + int * pPermuteBack; + DdNode ** pCompose; + DdNode * bCube, * bTemp; + DdNode * bSpace, * bFunc1, * bFunc2, * bSpaceShift; + int nSupp, Counter; + int i, lev; + + // get the support + pSupport = ABC_ALLOC( int, ddMax(dd->size,dd->sizeZ) ); + Extra_SupportArray( dd, bFunc, pSupport ); + nSupp = 0; + for ( i = 0; i < dd->size; i++ ) + if ( pSupport[i] ) + nSupp++; + + // make sure the manager has enough variables + if ( 2*nSupp > dd->size ) + { + printf( "Cannot derive linear space, because DD manager does not have enough variables.\n" ); + fflush( stdout ); + ABC_FREE( pSupport ); + return NULL; + } + + // create the permutation arrays + pPermute = ABC_ALLOC( int, dd->size ); + pPermuteBack = ABC_ALLOC( int, dd->size ); + pCompose = ABC_ALLOC( DdNode *, dd->size ); + for ( i = 0; i < dd->size; i++ ) + { + pPermute[i] = i; + pPermuteBack[i] = i; + pCompose[i] = dd->vars[i]; Cudd_Ref( pCompose[i] ); + } + + // remap the function in such a way that the variables are interleaved + Counter = 0; + bCube = b1; Cudd_Ref( bCube ); + for ( lev = 0; lev < dd->size; lev++ ) + if ( pSupport[ dd->invperm[lev] ] ) + { // var "dd->invperm[lev]" on level "lev" should go to level 2*Counter; + pPermute[ dd->invperm[lev] ] = dd->invperm[2*Counter]; + // var from level 2*Counter+1 should go back to the place of this var + pPermuteBack[ dd->invperm[2*Counter+1] ] = dd->invperm[lev]; + // the permutation should be defined in such a way that variable + // on level 2*Counter is replaced by an EXOR of itself and var on the next level + Cudd_Deref( pCompose[ dd->invperm[2*Counter] ] ); + pCompose[ dd->invperm[2*Counter] ] = + Cudd_bddXor( dd, dd->vars[ dd->invperm[2*Counter] ], dd->vars[ dd->invperm[2*Counter+1] ] ); + Cudd_Ref( pCompose[ dd->invperm[2*Counter] ] ); + // add this variable to the cube + bCube = Cudd_bddAnd( dd, bTemp = bCube, dd->vars[ dd->invperm[2*Counter] ] ); Cudd_Ref( bCube ); + Cudd_RecursiveDeref( dd, bTemp ); + // increment the counter + Counter ++; + } + + // permute the functions + bFunc1 = Cudd_bddPermute( dd, bFunc, pPermute ); Cudd_Ref( bFunc1 ); + // compose to gate the function depending on both vars + bFunc2 = Cudd_bddVectorCompose( dd, bFunc1, pCompose ); Cudd_Ref( bFunc2 ); + // gate the vector space + // L(a) = ForAll x [ F(x) = F(x+a) ] = Not( Exist x [ F(x) (+) F(x+a) ] ) + bSpaceShift = Cudd_bddXorExistAbstract( dd, bFunc1, bFunc2, bCube ); Cudd_Ref( bSpaceShift ); + bSpaceShift = Cudd_Not( bSpaceShift ); + // permute the space back into the original mapping + bSpace = Cudd_bddPermute( dd, bSpaceShift, pPermuteBack ); Cudd_Ref( bSpace ); + Cudd_RecursiveDeref( dd, bFunc1 ); + Cudd_RecursiveDeref( dd, bFunc2 ); + Cudd_RecursiveDeref( dd, bSpaceShift ); + Cudd_RecursiveDeref( dd, bCube ); + + for ( i = 0; i < dd->size; i++ ) + Cudd_RecursiveDeref( dd, pCompose[i] ); + ABC_FREE( pPermute ); + ABC_FREE( pPermuteBack ); + ABC_FREE( pCompose ); + ABC_FREE( pSupport ); + + Cudd_Deref( bSpace ); + return bSpace; +} + + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Extra_bddSpaceFromFunction( DdManager * dd, DdNode * bF, DdNode * bG ) +{ + DdNode * bRes; + do { + dd->reordered = 0; + bRes = extraBddSpaceFromFunction( dd, bF, bG ); + } while (dd->reordered == 1); + return bRes; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Extra_bddSpaceFromFunctionPos( DdManager * dd, DdNode * bFunc ) +{ + DdNode * bRes; + do { + dd->reordered = 0; + bRes = extraBddSpaceFromFunctionPos( dd, bFunc ); + } while (dd->reordered == 1); + return bRes; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Extra_bddSpaceFromFunctionNeg( DdManager * dd, DdNode * bFunc ) +{ + DdNode * bRes; + do { + dd->reordered = 0; + bRes = extraBddSpaceFromFunctionNeg( dd, bFunc ); + } while (dd->reordered == 1); + return bRes; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Extra_bddSpaceCanonVars( DdManager * dd, DdNode * bSpace ) +{ + DdNode * bRes; + do { + dd->reordered = 0; + bRes = extraBddSpaceCanonVars( dd, bSpace ); + } while (dd->reordered == 1); + return bRes; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Extra_bddSpaceReduce( DdManager * dd, DdNode * bFunc, DdNode * bCanonVars ) +{ + DdNode * bNegCube; + DdNode * bResult; + bNegCube = Extra_bddSupportNegativeCube( dd, bCanonVars ); Cudd_Ref( bNegCube ); + bResult = Cudd_Cofactor( dd, bFunc, bNegCube ); Cudd_Ref( bResult ); + Cudd_RecursiveDeref( dd, bNegCube ); + Cudd_Deref( bResult ); + return bResult; +} + + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Extra_bddSpaceEquations( DdManager * dd, DdNode * bSpace ) +{ + DdNode * zRes; + DdNode * zEquPos; + DdNode * zEquNeg; + zEquPos = Extra_bddSpaceEquationsPos( dd, bSpace ); Cudd_Ref( zEquPos ); + zEquNeg = Extra_bddSpaceEquationsNeg( dd, bSpace ); Cudd_Ref( zEquNeg ); + zRes = Cudd_zddUnion( dd, zEquPos, zEquNeg ); Cudd_Ref( zRes ); + Cudd_RecursiveDerefZdd( dd, zEquPos ); + Cudd_RecursiveDerefZdd( dd, zEquNeg ); + Cudd_Deref( zRes ); + return zRes; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Extra_bddSpaceEquationsPos( DdManager * dd, DdNode * bSpace ) +{ + DdNode * zRes; + do { + dd->reordered = 0; + zRes = extraBddSpaceEquationsPos( dd, bSpace ); + } while (dd->reordered == 1); + return zRes; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Extra_bddSpaceEquationsNeg( DdManager * dd, DdNode * bSpace ) +{ + DdNode * zRes; + do { + dd->reordered = 0; + zRes = extraBddSpaceEquationsNeg( dd, bSpace ); + } while (dd->reordered == 1); + return zRes; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Extra_bddSpaceFromMatrixPos( DdManager * dd, DdNode * zA ) +{ + DdNode * bRes; + do { + dd->reordered = 0; + bRes = extraBddSpaceFromMatrixPos( dd, zA ); + } while (dd->reordered == 1); + return bRes; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Extra_bddSpaceFromMatrixNeg( DdManager * dd, DdNode * zA ) +{ + DdNode * bRes; + do { + dd->reordered = 0; + bRes = extraBddSpaceFromMatrixNeg( dd, zA ); + } while (dd->reordered == 1); + return bRes; +} + +/**Function************************************************************* + + Synopsis [Counts the number of literals in one combination.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Extra_zddLitCountComb( DdManager * dd, DdNode * zComb ) +{ + int Counter; + if ( zComb == z0 ) + return 0; + Counter = 0; + for ( ; zComb != z1; zComb = cuddT(zComb) ) + Counter++; + return Counter; +} + +/**Function************************************************************* + + Synopsis [] + + Description [Returns the array of ZDDs with the number equal to the number of + vars in the DD manager. If the given var is non-canonical, this array contains + the referenced ZDD representing literals in the corresponding EXOR equation.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode ** Extra_bddSpaceExorGates( DdManager * dd, DdNode * bFuncRed, DdNode * zEquations ) +{ + DdNode ** pzRes; + int * pVarsNonCan; + DdNode * zEquRem; + int iVarNonCan; + DdNode * zExor, * zTemp; + + // get the set of non-canonical variables + pVarsNonCan = ABC_ALLOC( int, ddMax(dd->size,dd->sizeZ) ); + Extra_SupportArray( dd, bFuncRed, pVarsNonCan ); + + // allocate storage for the EXOR sets + pzRes = ABC_ALLOC( DdNode *, dd->size ); + memset( pzRes, 0, sizeof(DdNode *) * dd->size ); + + // go through all the equations + zEquRem = zEquations; Cudd_Ref( zEquRem ); + while ( zEquRem != z0 ) + { + // extract one product + zExor = Extra_zddSelectOneSubset( dd, zEquRem ); Cudd_Ref( zExor ); + // remove it from the set + zEquRem = Cudd_zddDiff( dd, zTemp = zEquRem, zExor ); Cudd_Ref( zEquRem ); + Cudd_RecursiveDerefZdd( dd, zTemp ); + + // locate the non-canonical variable + iVarNonCan = -1; + for ( zTemp = zExor; zTemp != z1; zTemp = cuddT(zTemp) ) + { + if ( pVarsNonCan[zTemp->index/2] == 1 ) + { + assert( iVarNonCan == -1 ); + iVarNonCan = zTemp->index/2; + } + } + assert( iVarNonCan != -1 ); + + if ( Extra_zddLitCountComb( dd, zExor ) > 1 ) + pzRes[ iVarNonCan ] = zExor; // takes ref + else + Cudd_RecursiveDerefZdd( dd, zExor ); + } + Cudd_RecursiveDerefZdd( dd, zEquRem ); + + ABC_FREE( pVarsNonCan ); + return pzRes; +} + + +/*---------------------------------------------------------------------------*/ +/* Definition of internal functions */ +/*---------------------------------------------------------------------------*/ + +/**Function******************************************************************** + + Synopsis [Performs the recursive steps of Extra_bddSpaceFromFunction.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * extraBddSpaceFromFunction( DdManager * dd, DdNode * bF, DdNode * bG ) +{ + DdNode * bRes; + DdNode * bFR, * bGR; + + bFR = Cudd_Regular( bF ); + bGR = Cudd_Regular( bG ); + if ( cuddIsConstant(bFR) ) + { + if ( bF == bG ) + return b1; + else + return b0; + } + if ( cuddIsConstant(bGR) ) + return b0; + // both bFunc and bCore are not constants + + // the operation is commutative - normalize the problem + if ( (unsigned)(ABC_PTRUINT_T)bF > (unsigned)(ABC_PTRUINT_T)bG ) + return extraBddSpaceFromFunction(dd, bG, bF); + + + if ( (bRes = cuddCacheLookup2(dd, extraBddSpaceFromFunction, bF, bG)) ) + return bRes; + else + { + DdNode * bF0, * bF1; + DdNode * bG0, * bG1; + DdNode * bTemp1, * bTemp2; + DdNode * bRes0, * bRes1; + int LevelF, LevelG; + int index; + + LevelF = dd->perm[bFR->index]; + LevelG = dd->perm[bGR->index]; + if ( LevelF <= LevelG ) + { + index = dd->invperm[LevelF]; + if ( bFR != bF ) + { + bF0 = Cudd_Not( cuddE(bFR) ); + bF1 = Cudd_Not( cuddT(bFR) ); + } + else + { + bF0 = cuddE(bFR); + bF1 = cuddT(bFR); + } + } + else + { + index = dd->invperm[LevelG]; + bF0 = bF1 = bF; + } + + if ( LevelG <= LevelF ) + { + if ( bGR != bG ) + { + bG0 = Cudd_Not( cuddE(bGR) ); + bG1 = Cudd_Not( cuddT(bGR) ); + } + else + { + bG0 = cuddE(bGR); + bG1 = cuddT(bGR); + } + } + else + bG0 = bG1 = bG; + + bTemp1 = extraBddSpaceFromFunction( dd, bF0, bG0 ); + if ( bTemp1 == NULL ) + return NULL; + cuddRef( bTemp1 ); + + bTemp2 = extraBddSpaceFromFunction( dd, bF1, bG1 ); + if ( bTemp2 == NULL ) + { + Cudd_RecursiveDeref( dd, bTemp1 ); + return NULL; + } + cuddRef( bTemp2 ); + + + bRes0 = cuddBddAndRecur( dd, bTemp1, bTemp2 ); + if ( bRes0 == NULL ) + { + Cudd_RecursiveDeref( dd, bTemp1 ); + Cudd_RecursiveDeref( dd, bTemp2 ); + return NULL; + } + cuddRef( bRes0 ); + Cudd_RecursiveDeref( dd, bTemp1 ); + Cudd_RecursiveDeref( dd, bTemp2 ); + + + bTemp1 = extraBddSpaceFromFunction( dd, bF0, bG1 ); + if ( bTemp1 == NULL ) + { + Cudd_RecursiveDeref( dd, bRes0 ); + return NULL; + } + cuddRef( bTemp1 ); + + bTemp2 = extraBddSpaceFromFunction( dd, bF1, bG0 ); + if ( bTemp2 == NULL ) + { + Cudd_RecursiveDeref( dd, bRes0 ); + Cudd_RecursiveDeref( dd, bTemp1 ); + return NULL; + } + cuddRef( bTemp2 ); + + bRes1 = cuddBddAndRecur( dd, bTemp1, bTemp2 ); + if ( bRes1 == NULL ) + { + Cudd_RecursiveDeref( dd, bRes0 ); + Cudd_RecursiveDeref( dd, bTemp1 ); + Cudd_RecursiveDeref( dd, bTemp2 ); + return NULL; + } + cuddRef( bRes1 ); + Cudd_RecursiveDeref( dd, bTemp1 ); + Cudd_RecursiveDeref( dd, bTemp2 ); + + + + // consider the case when Res0 and Res1 are the same node + if ( bRes0 == bRes1 ) + bRes = bRes1; + // consider the case when Res1 is complemented + else if ( Cudd_IsComplement(bRes1) ) + { + bRes = cuddUniqueInter(dd, index, Cudd_Not(bRes1), Cudd_Not(bRes0)); + if ( bRes == NULL ) + { + Cudd_RecursiveDeref(dd,bRes0); + Cudd_RecursiveDeref(dd,bRes1); + return NULL; + } + bRes = Cudd_Not(bRes); + } + else + { + bRes = cuddUniqueInter( dd, index, bRes1, bRes0 ); + if ( bRes == NULL ) + { + Cudd_RecursiveDeref(dd,bRes0); + Cudd_RecursiveDeref(dd,bRes1); + return NULL; + } + } + cuddDeref( bRes0 ); + cuddDeref( bRes1 ); + + // insert the result into cache + cuddCacheInsert2(dd, extraBddSpaceFromFunction, bF, bG, bRes); + return bRes; + } +} /* end of extraBddSpaceFromFunction */ + + + +/**Function************************************************************* + + Synopsis [Performs the recursive step of Extra_bddSpaceFromFunctionPos().] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * extraBddSpaceFromFunctionPos( DdManager * dd, DdNode * bF ) +{ + DdNode * bRes, * bFR; + statLine( dd ); + + bFR = Cudd_Regular(bF); + if ( cuddIsConstant(bFR) ) + return b1; + + if ( (bRes = cuddCacheLookup1(dd, extraBddSpaceFromFunctionPos, bF)) ) + return bRes; + else + { + DdNode * bF0, * bF1; + DdNode * bPos0, * bPos1; + DdNode * bNeg0, * bNeg1; + DdNode * bRes0, * bRes1; + + if ( bFR != bF ) // bF is complemented + { + bF0 = Cudd_Not( cuddE(bFR) ); + bF1 = Cudd_Not( cuddT(bFR) ); + } + else + { + bF0 = cuddE(bFR); + bF1 = cuddT(bFR); + } + + + bPos0 = extraBddSpaceFromFunctionPos( dd, bF0 ); + if ( bPos0 == NULL ) + return NULL; + cuddRef( bPos0 ); + + bPos1 = extraBddSpaceFromFunctionPos( dd, bF1 ); + if ( bPos1 == NULL ) + { + Cudd_RecursiveDeref( dd, bPos0 ); + return NULL; + } + cuddRef( bPos1 ); + + bRes0 = cuddBddAndRecur( dd, bPos0, bPos1 ); + if ( bRes0 == NULL ) + { + Cudd_RecursiveDeref( dd, bPos0 ); + Cudd_RecursiveDeref( dd, bPos1 ); + return NULL; + } + cuddRef( bRes0 ); + Cudd_RecursiveDeref( dd, bPos0 ); + Cudd_RecursiveDeref( dd, bPos1 ); + + + bNeg0 = extraBddSpaceFromFunctionNeg( dd, bF0 ); + if ( bNeg0 == NULL ) + { + Cudd_RecursiveDeref( dd, bRes0 ); + return NULL; + } + cuddRef( bNeg0 ); + + bNeg1 = extraBddSpaceFromFunctionNeg( dd, bF1 ); + if ( bNeg1 == NULL ) + { + Cudd_RecursiveDeref( dd, bRes0 ); + Cudd_RecursiveDeref( dd, bNeg0 ); + return NULL; + } + cuddRef( bNeg1 ); + + bRes1 = cuddBddAndRecur( dd, bNeg0, bNeg1 ); + if ( bRes1 == NULL ) + { + Cudd_RecursiveDeref( dd, bRes0 ); + Cudd_RecursiveDeref( dd, bNeg0 ); + Cudd_RecursiveDeref( dd, bNeg1 ); + return NULL; + } + cuddRef( bRes1 ); + Cudd_RecursiveDeref( dd, bNeg0 ); + Cudd_RecursiveDeref( dd, bNeg1 ); + + + // consider the case when Res0 and Res1 are the same node + if ( bRes0 == bRes1 ) + bRes = bRes1; + // consider the case when Res1 is complemented + else if ( Cudd_IsComplement(bRes1) ) + { + bRes = cuddUniqueInter( dd, bFR->index, Cudd_Not(bRes1), Cudd_Not(bRes0) ); + if ( bRes == NULL ) + { + Cudd_RecursiveDeref(dd,bRes0); + Cudd_RecursiveDeref(dd,bRes1); + return NULL; + } + bRes = Cudd_Not(bRes); + } + else + { + bRes = cuddUniqueInter( dd, bFR->index, bRes1, bRes0 ); + if ( bRes == NULL ) + { + Cudd_RecursiveDeref(dd,bRes0); + Cudd_RecursiveDeref(dd,bRes1); + return NULL; + } + } + cuddDeref( bRes0 ); + cuddDeref( bRes1 ); + + cuddCacheInsert1( dd, extraBddSpaceFromFunctionPos, bF, bRes ); + return bRes; + } +} + + + +/**Function************************************************************* + + Synopsis [Performs the recursive step of Extra_bddSpaceFromFunctionPos().] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * extraBddSpaceFromFunctionNeg( DdManager * dd, DdNode * bF ) +{ + DdNode * bRes, * bFR; + statLine( dd ); + + bFR = Cudd_Regular(bF); + if ( cuddIsConstant(bFR) ) + return b0; + + if ( (bRes = cuddCacheLookup1(dd, extraBddSpaceFromFunctionNeg, bF)) ) + return bRes; + else + { + DdNode * bF0, * bF1; + DdNode * bPos0, * bPos1; + DdNode * bNeg0, * bNeg1; + DdNode * bRes0, * bRes1; + + if ( bFR != bF ) // bF is complemented + { + bF0 = Cudd_Not( cuddE(bFR) ); + bF1 = Cudd_Not( cuddT(bFR) ); + } + else + { + bF0 = cuddE(bFR); + bF1 = cuddT(bFR); + } + + + bPos0 = extraBddSpaceFromFunctionNeg( dd, bF0 ); + if ( bPos0 == NULL ) + return NULL; + cuddRef( bPos0 ); + + bPos1 = extraBddSpaceFromFunctionNeg( dd, bF1 ); + if ( bPos1 == NULL ) + { + Cudd_RecursiveDeref( dd, bPos0 ); + return NULL; + } + cuddRef( bPos1 ); + + bRes0 = cuddBddAndRecur( dd, bPos0, bPos1 ); + if ( bRes0 == NULL ) + { + Cudd_RecursiveDeref( dd, bPos0 ); + Cudd_RecursiveDeref( dd, bPos1 ); + return NULL; + } + cuddRef( bRes0 ); + Cudd_RecursiveDeref( dd, bPos0 ); + Cudd_RecursiveDeref( dd, bPos1 ); + + + bNeg0 = extraBddSpaceFromFunctionPos( dd, bF0 ); + if ( bNeg0 == NULL ) + { + Cudd_RecursiveDeref( dd, bRes0 ); + return NULL; + } + cuddRef( bNeg0 ); + + bNeg1 = extraBddSpaceFromFunctionPos( dd, bF1 ); + if ( bNeg1 == NULL ) + { + Cudd_RecursiveDeref( dd, bRes0 ); + Cudd_RecursiveDeref( dd, bNeg0 ); + return NULL; + } + cuddRef( bNeg1 ); + + bRes1 = cuddBddAndRecur( dd, bNeg0, bNeg1 ); + if ( bRes1 == NULL ) + { + Cudd_RecursiveDeref( dd, bRes0 ); + Cudd_RecursiveDeref( dd, bNeg0 ); + Cudd_RecursiveDeref( dd, bNeg1 ); + return NULL; + } + cuddRef( bRes1 ); + Cudd_RecursiveDeref( dd, bNeg0 ); + Cudd_RecursiveDeref( dd, bNeg1 ); + + + // consider the case when Res0 and Res1 are the same node + if ( bRes0 == bRes1 ) + bRes = bRes1; + // consider the case when Res1 is complemented + else if ( Cudd_IsComplement(bRes1) ) + { + bRes = cuddUniqueInter( dd, bFR->index, Cudd_Not(bRes1), Cudd_Not(bRes0) ); + if ( bRes == NULL ) + { + Cudd_RecursiveDeref(dd,bRes0); + Cudd_RecursiveDeref(dd,bRes1); + return NULL; + } + bRes = Cudd_Not(bRes); + } + else + { + bRes = cuddUniqueInter( dd, bFR->index, bRes1, bRes0 ); + if ( bRes == NULL ) + { + Cudd_RecursiveDeref(dd,bRes0); + Cudd_RecursiveDeref(dd,bRes1); + return NULL; + } + } + cuddDeref( bRes0 ); + cuddDeref( bRes1 ); + + cuddCacheInsert1( dd, extraBddSpaceFromFunctionNeg, bF, bRes ); + return bRes; + } +} + + + +/**Function************************************************************* + + Synopsis [Performs the recursive step of Extra_bddSpaceCanonVars().] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * extraBddSpaceCanonVars( DdManager * dd, DdNode * bF ) +{ + DdNode * bRes, * bFR; + statLine( dd ); + + bFR = Cudd_Regular(bF); + if ( cuddIsConstant(bFR) ) + return bF; + + if ( (bRes = cuddCacheLookup1(dd, extraBddSpaceCanonVars, bF)) ) + return bRes; + else + { + DdNode * bF0, * bF1; + DdNode * bRes, * bRes0; + + if ( bFR != bF ) // bF is complemented + { + bF0 = Cudd_Not( cuddE(bFR) ); + bF1 = Cudd_Not( cuddT(bFR) ); + } + else + { + bF0 = cuddE(bFR); + bF1 = cuddT(bFR); + } + + if ( bF0 == b0 ) + { + bRes = extraBddSpaceCanonVars( dd, bF1 ); + if ( bRes == NULL ) + return NULL; + } + else if ( bF1 == b0 ) + { + bRes = extraBddSpaceCanonVars( dd, bF0 ); + if ( bRes == NULL ) + return NULL; + } + else + { + bRes0 = extraBddSpaceCanonVars( dd, bF0 ); + if ( bRes0 == NULL ) + return NULL; + cuddRef( bRes0 ); + + bRes = cuddUniqueInter( dd, bFR->index, bRes0, b0 ); + if ( bRes == NULL ) + { + Cudd_RecursiveDeref( dd,bRes0 ); + return NULL; + } + cuddDeref( bRes0 ); + } + + cuddCacheInsert1( dd, extraBddSpaceCanonVars, bF, bRes ); + return bRes; + } +} + +/**Function************************************************************* + + Synopsis [Performs the recursive step of Extra_bddSpaceEquationsPos().] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * extraBddSpaceEquationsPos( DdManager * dd, DdNode * bF ) +{ + DdNode * zRes; + statLine( dd ); + + if ( bF == b0 ) + return z1; + if ( bF == b1 ) + return z0; + + if ( (zRes = cuddCacheLookup1Zdd(dd, extraBddSpaceEquationsPos, bF)) ) + return zRes; + else + { + DdNode * bFR, * bF0, * bF1; + DdNode * zPos0, * zPos1, * zNeg1; + DdNode * zRes, * zRes0, * zRes1; + + bFR = Cudd_Regular(bF); + if ( bFR != bF ) // bF is complemented + { + bF0 = Cudd_Not( cuddE(bFR) ); + bF1 = Cudd_Not( cuddT(bFR) ); + } + else + { + bF0 = cuddE(bFR); + bF1 = cuddT(bFR); + } + + if ( bF0 == b0 ) + { + zRes1 = extraBddSpaceEquationsPos( dd, bF1 ); + if ( zRes1 == NULL ) + return NULL; + cuddRef( zRes1 ); + + // add the current element to the set + zRes = cuddZddGetNode( dd, 2*bFR->index, z1, zRes1 ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zRes1); + return NULL; + } + cuddDeref( zRes1 ); + } + else if ( bF1 == b0 ) + { + zRes = extraBddSpaceEquationsPos( dd, bF0 ); + if ( zRes == NULL ) + return NULL; + } + else + { + zPos0 = extraBddSpaceEquationsPos( dd, bF0 ); + if ( zPos0 == NULL ) + return NULL; + cuddRef( zPos0 ); + + zPos1 = extraBddSpaceEquationsPos( dd, bF1 ); + if ( zPos1 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zPos0); + return NULL; + } + cuddRef( zPos1 ); + + zNeg1 = extraBddSpaceEquationsNeg( dd, bF1 ); + if ( zNeg1 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zPos0); + Cudd_RecursiveDerefZdd(dd, zPos1); + return NULL; + } + cuddRef( zNeg1 ); + + + zRes0 = cuddZddIntersect( dd, zPos0, zPos1 ); + if ( zRes0 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zNeg1); + Cudd_RecursiveDerefZdd(dd, zPos0); + Cudd_RecursiveDerefZdd(dd, zPos1); + return NULL; + } + cuddRef( zRes0 ); + + zRes1 = cuddZddIntersect( dd, zPos0, zNeg1 ); + if ( zRes1 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zRes0); + Cudd_RecursiveDerefZdd(dd, zNeg1); + Cudd_RecursiveDerefZdd(dd, zPos0); + Cudd_RecursiveDerefZdd(dd, zPos1); + return NULL; + } + cuddRef( zRes1 ); + Cudd_RecursiveDerefZdd(dd, zNeg1); + Cudd_RecursiveDerefZdd(dd, zPos0); + Cudd_RecursiveDerefZdd(dd, zPos1); + // only zRes0 and zRes1 are refed at this point + + zRes = cuddZddGetNode( dd, 2*bFR->index, zRes1, zRes0 ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zRes0); + Cudd_RecursiveDerefZdd(dd, zRes1); + return NULL; + } + cuddDeref( zRes0 ); + cuddDeref( zRes1 ); + } + + cuddCacheInsert1( dd, extraBddSpaceEquationsPos, bF, zRes ); + return zRes; + } +} + + +/**Function************************************************************* + + Synopsis [Performs the recursive step of Extra_bddSpaceEquationsNev().] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * extraBddSpaceEquationsNeg( DdManager * dd, DdNode * bF ) +{ + DdNode * zRes; + statLine( dd ); + + if ( bF == b0 ) + return z1; + if ( bF == b1 ) + return z0; + + if ( (zRes = cuddCacheLookup1Zdd(dd, extraBddSpaceEquationsNeg, bF)) ) + return zRes; + else + { + DdNode * bFR, * bF0, * bF1; + DdNode * zPos0, * zPos1, * zNeg1; + DdNode * zRes, * zRes0, * zRes1; + + bFR = Cudd_Regular(bF); + if ( bFR != bF ) // bF is complemented + { + bF0 = Cudd_Not( cuddE(bFR) ); + bF1 = Cudd_Not( cuddT(bFR) ); + } + else + { + bF0 = cuddE(bFR); + bF1 = cuddT(bFR); + } + + if ( bF0 == b0 ) + { + zRes = extraBddSpaceEquationsNeg( dd, bF1 ); + if ( zRes == NULL ) + return NULL; + } + else if ( bF1 == b0 ) + { + zRes0 = extraBddSpaceEquationsNeg( dd, bF0 ); + if ( zRes0 == NULL ) + return NULL; + cuddRef( zRes0 ); + + // add the current element to the set + zRes = cuddZddGetNode( dd, 2*bFR->index, z1, zRes0 ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zRes0); + return NULL; + } + cuddDeref( zRes0 ); + } + else + { + zPos0 = extraBddSpaceEquationsNeg( dd, bF0 ); + if ( zPos0 == NULL ) + return NULL; + cuddRef( zPos0 ); + + zPos1 = extraBddSpaceEquationsNeg( dd, bF1 ); + if ( zPos1 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zPos0); + return NULL; + } + cuddRef( zPos1 ); + + zNeg1 = extraBddSpaceEquationsPos( dd, bF1 ); + if ( zNeg1 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zPos0); + Cudd_RecursiveDerefZdd(dd, zPos1); + return NULL; + } + cuddRef( zNeg1 ); + + + zRes0 = cuddZddIntersect( dd, zPos0, zPos1 ); + if ( zRes0 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zNeg1); + Cudd_RecursiveDerefZdd(dd, zPos0); + Cudd_RecursiveDerefZdd(dd, zPos1); + return NULL; + } + cuddRef( zRes0 ); + + zRes1 = cuddZddIntersect( dd, zPos0, zNeg1 ); + if ( zRes1 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zRes0); + Cudd_RecursiveDerefZdd(dd, zNeg1); + Cudd_RecursiveDerefZdd(dd, zPos0); + Cudd_RecursiveDerefZdd(dd, zPos1); + return NULL; + } + cuddRef( zRes1 ); + Cudd_RecursiveDerefZdd(dd, zNeg1); + Cudd_RecursiveDerefZdd(dd, zPos0); + Cudd_RecursiveDerefZdd(dd, zPos1); + // only zRes0 and zRes1 are refed at this point + + zRes = cuddZddGetNode( dd, 2*bFR->index, zRes1, zRes0 ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zRes0); + Cudd_RecursiveDerefZdd(dd, zRes1); + return NULL; + } + cuddDeref( zRes0 ); + cuddDeref( zRes1 ); + } + + cuddCacheInsert1( dd, extraBddSpaceEquationsNeg, bF, zRes ); + return zRes; + } +} + + + + +/**Function************************************************************* + + Synopsis [Performs the recursive step of Extra_bddSpaceFromFunctionPos().] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * extraBddSpaceFromMatrixPos( DdManager * dd, DdNode * zA ) +{ + DdNode * bRes; + statLine( dd ); + + if ( zA == z0 ) + return b1; + if ( zA == z1 ) + return b1; + + if ( (bRes = cuddCacheLookup1(dd, extraBddSpaceFromMatrixPos, zA)) ) + return bRes; + else + { + DdNode * bP0, * bP1; + DdNode * bN0, * bN1; + DdNode * bRes0, * bRes1; + + bP0 = extraBddSpaceFromMatrixPos( dd, cuddE(zA) ); + if ( bP0 == NULL ) + return NULL; + cuddRef( bP0 ); + + bP1 = extraBddSpaceFromMatrixPos( dd, cuddT(zA) ); + if ( bP1 == NULL ) + { + Cudd_RecursiveDeref( dd, bP0 ); + return NULL; + } + cuddRef( bP1 ); + + bRes0 = cuddBddAndRecur( dd, bP0, bP1 ); + if ( bRes0 == NULL ) + { + Cudd_RecursiveDeref( dd, bP0 ); + Cudd_RecursiveDeref( dd, bP1 ); + return NULL; + } + cuddRef( bRes0 ); + Cudd_RecursiveDeref( dd, bP0 ); + Cudd_RecursiveDeref( dd, bP1 ); + + + bN0 = extraBddSpaceFromMatrixPos( dd, cuddE(zA) ); + if ( bN0 == NULL ) + { + Cudd_RecursiveDeref( dd, bRes0 ); + return NULL; + } + cuddRef( bN0 ); + + bN1 = extraBddSpaceFromMatrixNeg( dd, cuddT(zA) ); + if ( bN1 == NULL ) + { + Cudd_RecursiveDeref( dd, bRes0 ); + Cudd_RecursiveDeref( dd, bN0 ); + return NULL; + } + cuddRef( bN1 ); + + bRes1 = cuddBddAndRecur( dd, bN0, bN1 ); + if ( bRes1 == NULL ) + { + Cudd_RecursiveDeref( dd, bRes0 ); + Cudd_RecursiveDeref( dd, bN0 ); + Cudd_RecursiveDeref( dd, bN1 ); + return NULL; + } + cuddRef( bRes1 ); + Cudd_RecursiveDeref( dd, bN0 ); + Cudd_RecursiveDeref( dd, bN1 ); + + + // consider the case when Res0 and Res1 are the same node + if ( bRes0 == bRes1 ) + bRes = bRes1; + // consider the case when Res1 is complemented + else if ( Cudd_IsComplement(bRes1) ) + { + bRes = cuddUniqueInter( dd, zA->index/2, Cudd_Not(bRes1), Cudd_Not(bRes0) ); + if ( bRes == NULL ) + { + Cudd_RecursiveDeref(dd,bRes0); + Cudd_RecursiveDeref(dd,bRes1); + return NULL; + } + bRes = Cudd_Not(bRes); + } + else + { + bRes = cuddUniqueInter( dd, zA->index/2, bRes1, bRes0 ); + if ( bRes == NULL ) + { + Cudd_RecursiveDeref(dd,bRes0); + Cudd_RecursiveDeref(dd,bRes1); + return NULL; + } + } + cuddDeref( bRes0 ); + cuddDeref( bRes1 ); + + cuddCacheInsert1( dd, extraBddSpaceFromMatrixPos, zA, bRes ); + return bRes; + } +} + + +/**Function************************************************************* + + Synopsis [Performs the recursive step of Extra_bddSpaceFromFunctionPos().] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * extraBddSpaceFromMatrixNeg( DdManager * dd, DdNode * zA ) +{ + DdNode * bRes; + statLine( dd ); + + if ( zA == z0 ) + return b1; + if ( zA == z1 ) + return b0; + + if ( (bRes = cuddCacheLookup1(dd, extraBddSpaceFromMatrixNeg, zA)) ) + return bRes; + else + { + DdNode * bP0, * bP1; + DdNode * bN0, * bN1; + DdNode * bRes0, * bRes1; + + bP0 = extraBddSpaceFromMatrixNeg( dd, cuddE(zA) ); + if ( bP0 == NULL ) + return NULL; + cuddRef( bP0 ); + + bP1 = extraBddSpaceFromMatrixNeg( dd, cuddT(zA) ); + if ( bP1 == NULL ) + { + Cudd_RecursiveDeref( dd, bP0 ); + return NULL; + } + cuddRef( bP1 ); + + bRes0 = cuddBddAndRecur( dd, bP0, bP1 ); + if ( bRes0 == NULL ) + { + Cudd_RecursiveDeref( dd, bP0 ); + Cudd_RecursiveDeref( dd, bP1 ); + return NULL; + } + cuddRef( bRes0 ); + Cudd_RecursiveDeref( dd, bP0 ); + Cudd_RecursiveDeref( dd, bP1 ); + + + bN0 = extraBddSpaceFromMatrixNeg( dd, cuddE(zA) ); + if ( bN0 == NULL ) + { + Cudd_RecursiveDeref( dd, bRes0 ); + return NULL; + } + cuddRef( bN0 ); + + bN1 = extraBddSpaceFromMatrixPos( dd, cuddT(zA) ); + if ( bN1 == NULL ) + { + Cudd_RecursiveDeref( dd, bRes0 ); + Cudd_RecursiveDeref( dd, bN0 ); + return NULL; + } + cuddRef( bN1 ); + + bRes1 = cuddBddAndRecur( dd, bN0, bN1 ); + if ( bRes1 == NULL ) + { + Cudd_RecursiveDeref( dd, bRes0 ); + Cudd_RecursiveDeref( dd, bN0 ); + Cudd_RecursiveDeref( dd, bN1 ); + return NULL; + } + cuddRef( bRes1 ); + Cudd_RecursiveDeref( dd, bN0 ); + Cudd_RecursiveDeref( dd, bN1 ); + + + // consider the case when Res0 and Res1 are the same node + if ( bRes0 == bRes1 ) + bRes = bRes1; + // consider the case when Res1 is complemented + else if ( Cudd_IsComplement(bRes1) ) + { + bRes = cuddUniqueInter( dd, zA->index/2, Cudd_Not(bRes1), Cudd_Not(bRes0) ); + if ( bRes == NULL ) + { + Cudd_RecursiveDeref(dd,bRes0); + Cudd_RecursiveDeref(dd,bRes1); + return NULL; + } + bRes = Cudd_Not(bRes); + } + else + { + bRes = cuddUniqueInter( dd, zA->index/2, bRes1, bRes0 ); + if ( bRes == NULL ) + { + Cudd_RecursiveDeref(dd,bRes0); + Cudd_RecursiveDeref(dd,bRes1); + return NULL; + } + } + cuddDeref( bRes0 ); + cuddDeref( bRes1 ); + + cuddCacheInsert1( dd, extraBddSpaceFromMatrixNeg, zA, bRes ); + return bRes; + } +} + + +/*---------------------------------------------------------------------------*/ +/* Definition of static functions */ +/*---------------------------------------------------------------------------*/ + +ABC_NAMESPACE_IMPL_END + diff --git a/src/bdd/extrab/extraBddCas.c b/src/bdd/extrab/extraBddCas.c new file mode 100644 index 00000000..024e4462 --- /dev/null +++ b/src/bdd/extrab/extraBddCas.c @@ -0,0 +1,1235 @@ +/**CFile**************************************************************** + + FileName [extraBddCas.c] + + PackageName [extra] + + Synopsis [Procedures related to LUT cascade synthesis.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 2.0. Started - September 1, 2003.] + + Revision [$Id: extraBddCas.c,v 1.0 2003/05/21 18:03:50 alanmi Exp $] + +***********************************************************************/ + +#include "extraBdd.h" + +ABC_NAMESPACE_IMPL_START + + +/*---------------------------------------------------------------------------*/ +/* Constant declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Stucture declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Type declarations */ +/*---------------------------------------------------------------------------*/ + +// the table to store cofactor operations +#define _TABLESIZE_COF 51113 +typedef struct +{ + unsigned Sign; + DdNode * Arg1; +} _HashEntry_cof; +_HashEntry_cof HHTable1[_TABLESIZE_COF]; + +// the table to store the result of computation of the number of minterms +#define _TABLESIZE_MINT 15113 +typedef struct +{ + DdNode * Arg1; + unsigned Arg2; + unsigned Res; +} _HashEntry_mint; +_HashEntry_mint HHTable2[_TABLESIZE_MINT]; + +typedef struct +{ + int nEdges; // the number of in-coming edges of the node + DdNode * bSum; // the sum of paths of the incoming edges +} traventry; + +// the signature used for hashing +static unsigned s_Signature = 1; + +static int s_CutLevel = 0; + +/*---------------------------------------------------------------------------*/ +/* Variable declarations */ +/*---------------------------------------------------------------------------*/ + +// because the proposed solution to the optimal encoding problem has exponential complexity +// we limit the depth of the branch and bound procedure to 5 levels +static int s_MaxDepth = 5; + +static int s_nVarsBest; // the number of vars in the best ordering +static int s_VarOrderBest[32]; // storing the best ordering of vars in the "simple encoding" +static int s_VarOrderCur[32]; // storing the current ordering of vars + +// the place to store the supports of the encoded function +static DdNode * s_Field[8][256]; // the size should be K, 2^K, where K is no less than MaxDepth +static DdNode * s_Encoded; // this is the original function +static DdNode * s_VarAll; // the set of all column variables +static int s_MultiStart; // the total number of encoding variables used +// the array field now stores the supports + +static DdNode ** s_pbTemp; // the temporary storage for the columns + +static int s_BackTracks; +static int s_BackTrackLimit = 100; + +static DdNode * s_Terminal; // the terminal value for counting minterms + + +static int s_EncodingVarsLevel; + + +/*---------------------------------------------------------------------------*/ +/* Macro declarations */ +/*---------------------------------------------------------------------------*/ + + +/**AutomaticStart*************************************************************/ + +/*---------------------------------------------------------------------------*/ +/* Static function prototypes */ +/*---------------------------------------------------------------------------*/ + +static DdNode * CreateTheCodes_rec( DdManager * dd, DdNode * bEncoded, int Level, DdNode ** pCVars ); +static void EvaluateEncodings_rec( DdManager * dd, DdNode * bVarsCol, int nVarsCol, int nMulti, int Level ); +// functions called from EvaluateEncodings_rec() +static DdNode * ComputeVarSetAndCountMinterms( DdManager * dd, DdNode * bVars, DdNode * bVarTop, unsigned * Cost ); +static DdNode * ComputeVarSetAndCountMinterms2( DdManager * dd, DdNode * bVars, DdNode * bVarTop, unsigned * Cost ); +unsigned Extra_CountCofactorMinterms( DdManager * dd, DdNode * bFunc, DdNode * bVarsCof, DdNode * bVarsAll ); +static unsigned Extra_CountMintermsSimple( DdNode * bFunc, unsigned max ); + +static void CountNodeVisits_rec( DdManager * dd, DdNode * aFunc, st__table * Visited ); +static void CollectNodesAndComputePaths_rec( DdManager * dd, DdNode * aFunc, DdNode * bCube, st__table * Visited, st__table * CutNodes ); + +/**AutomaticEnd***************************************************************/ + + +/*---------------------------------------------------------------------------*/ +/* Definition of exported functions */ +/*---------------------------------------------------------------------------*/ + +/**Function******************************************************************** + + Synopsis [Performs the binary encoding of the set of function using the given vars.] + + Description [Performs a straight binary encoding of the set of functions using + the variable cubes formed from the given set of variables. ] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * +Extra_bddEncodingBinary( + DdManager * dd, + DdNode ** pbFuncs, // pbFuncs is the array of columns to be encoded + int nFuncs, // nFuncs is the number of columns in the array + DdNode ** pbVars, // pbVars is the array of variables to use for the codes + int nVars ) // nVars is the column multiplicity, [log2(nFuncs)] +{ + int i; + DdNode * bResult; + DdNode * bCube, * bTemp, * bProd; + + assert( nVars >= Abc_Base2Log(nFuncs) ); + + bResult = b0; Cudd_Ref( bResult ); + for ( i = 0; i < nFuncs; i++ ) + { + bCube = Extra_bddBitsToCube( dd, i, nVars, pbVars, 1 ); Cudd_Ref( bCube ); + bProd = Cudd_bddAnd( dd, bCube, pbFuncs[i] ); Cudd_Ref( bProd ); + Cudd_RecursiveDeref( dd, bCube ); + + bResult = Cudd_bddOr( dd, bProd, bTemp = bResult ); Cudd_Ref( bResult ); + Cudd_RecursiveDeref( dd, bTemp ); + Cudd_RecursiveDeref( dd, bProd ); + } + + Cudd_Deref( bResult ); + return bResult; +} /* end of Extra_bddEncodingBinary */ + + +/**Function******************************************************************** + + Synopsis [Solves the column encoding problem using a sophisticated method.] + + Description [The encoding is based on the idea of deriving functions which + depend on only one variable, which corresponds to the case of non-disjoint + decompostion. It is assumed that the variables pCVars are ordered below the variables + representing the solumns, and the first variable pCVars[0] is the topmost one.] + + SideEffects [] + + SeeAlso [Extra_bddEncodingBinary] + +******************************************************************************/ + +DdNode * +Extra_bddEncodingNonStrict( + DdManager * dd, + DdNode ** pbColumns, // pbColumns is the array of columns to be encoded; + int nColumns, // nColumns is the number of columns in the array + DdNode * bVarsCol, // bVarsCol is the cube of variables on which the columns depend + DdNode ** pCVars, // pCVars is the array of variables to use for the codes + int nMulti, // nMulti is the column multiplicity, [log2(nColumns)] + int * pSimple ) // pSimple gets the number of code variables taken from the input varibles without change +{ + DdNode * bEncoded, * bResult; + int nVarsCol = Cudd_SupportSize(dd,bVarsCol); + abctime clk; + + // cannot work with more that 32-bit codes + assert( nMulti < 32 ); + + // perform the preliminary encoding using the straight binary code + bEncoded = Extra_bddEncodingBinary( dd, pbColumns, nColumns, pCVars, nMulti ); Cudd_Ref( bEncoded ); + //printf( "Node count = %d", Cudd_DagSize(bEncoded) ); + + // set the backgroup value for counting minterms + s_Terminal = b0; + // set the level of the encoding variables + s_EncodingVarsLevel = dd->invperm[pCVars[0]->index]; + + // the current number of backtracks + s_BackTracks = 0; + // the variables that are cofactored on the topmost level where everything starts (no vars) + s_Field[0][0] = b1; + // the size of the best set of "simple" encoding variables found so far + s_nVarsBest = 0; + + // set the relation to be accessible to traversal procedures + s_Encoded = bEncoded; + // the set of all vars to be accessible to traversal procedures + s_VarAll = bVarsCol; + // the column multiplicity + s_MultiStart = nMulti; + + + clk = Abc_Clock(); + // find the simplest encoding + if ( nColumns > 2 ) + EvaluateEncodings_rec( dd, bVarsCol, nVarsCol, nMulti, 1 ); +// printf( "The number of backtracks = %d\n", s_BackTracks ); +// s_EncSearchTime += Abc_Clock() - clk; + + // allocate the temporary storage for the columns + s_pbTemp = (DdNode **)ABC_ALLOC( char, nColumns * sizeof(DdNode *) ); + +// clk = Abc_Clock(); + bResult = CreateTheCodes_rec( dd, bEncoded, 0, pCVars ); Cudd_Ref( bResult ); +// s_EncComputeTime += Abc_Clock() - clk; + + // delocate the preliminarily encoded set + Cudd_RecursiveDeref( dd, bEncoded ); +// Cudd_RecursiveDeref( dd, aEncoded ); + + ABC_FREE( s_pbTemp ); + + *pSimple = s_nVarsBest; + Cudd_Deref( bResult ); + return bResult; +} + +/**Function******************************************************************** + + Synopsis [Collects the nodes under the cut and, for each node, computes the sum of paths leading to it from the root.] + + Description [The table returned contains the set of BDD nodes pointed to under the cut + and, for each node, the BDD of the sum of paths leading to this node from the root + The sums of paths in the table are referenced. CutLevel is the first DD level + considered to be under the cut.] + + SideEffects [] + + SeeAlso [Extra_bddNodePaths] + +******************************************************************************/ + st__table * Extra_bddNodePathsUnderCut( DdManager * dd, DdNode * bFunc, int CutLevel ) +{ + st__table * Visited; // temporary table to remember the visited nodes + st__table * CutNodes; // the result goes here + st__table * Result; // the result goes here + DdNode * aFunc; + + s_CutLevel = CutLevel; + + Result = st__init_table( st__ptrcmp, st__ptrhash);; + // the terminal cases + if ( Cudd_IsConstant( bFunc ) ) + { + if ( bFunc == b1 ) + { + st__insert( Result, (char*)b1, (char*)b1 ); + Cudd_Ref( b1 ); + Cudd_Ref( b1 ); + } + else + { + st__insert( Result, (char*)b0, (char*)b0 ); + Cudd_Ref( b0 ); + Cudd_Ref( b0 ); + } + return Result; + } + + // create the ADD to simplify processing (no complemented edges) + aFunc = Cudd_BddToAdd( dd, bFunc ); Cudd_Ref( aFunc ); + + // Step 1: Start the tables and collect information about the nodes above the cut + // this information tells how many edges point to each node + Visited = st__init_table( st__ptrcmp, st__ptrhash);; + CutNodes = st__init_table( st__ptrcmp, st__ptrhash);; + + CountNodeVisits_rec( dd, aFunc, Visited ); + + // Step 2: Traverse the BDD using the visited table and compute the sum of paths + CollectNodesAndComputePaths_rec( dd, aFunc, b1, Visited, CutNodes ); + + // at this point the table of cut nodes is ready and the table of visited is useless + { + st__generator * gen; + DdNode * aNode; + traventry * p; + st__foreach_item( Visited, gen, (const char**)&aNode, (char**)&p ) + { + Cudd_RecursiveDeref( dd, p->bSum ); + ABC_FREE( p ); + } + st__free_table( Visited ); + } + + // go through the table CutNodes and create the BDD and the path to be returned + { + st__generator * gen; + DdNode * aNode, * bNode, * bSum; + st__foreach_item( CutNodes, gen, (const char**)&aNode, (char**)&bSum) + { + // aNode is not referenced, because aFunc is holding it + bNode = Cudd_addBddPattern( dd, aNode ); Cudd_Ref( bNode ); + st__insert( Result, (char*)bNode, (char*)bSum ); + // the new table takes both refs + } + st__free_table( CutNodes ); + } + + // dereference the ADD + Cudd_RecursiveDeref( dd, aFunc ); + + // return the table + return Result; + +} /* end of Extra_bddNodePathsUnderCut */ + +/**Function******************************************************************** + + Synopsis [Collects the nodes under the cut in the ADD starting from the given set of ADD nodes.] + + Description [Takes the array, paNodes, of ADD nodes to start the traversal, + the array, pbCubes, of BDD cubes to start the traversal with in each node, + and the number, nNodes, of ADD nodes and BDD cubes in paNodes and pbCubes. + Returns the number of columns found. Fills in paNodesRes (pbCubesRes) + with the set of ADD columns (BDD paths). These arrays should be allocated + by the user.] + + SideEffects [] + + SeeAlso [Extra_bddNodePaths] + +******************************************************************************/ +int Extra_bddNodePathsUnderCutArray( DdManager * dd, DdNode ** paNodes, DdNode ** pbCubes, int nNodes, DdNode ** paNodesRes, DdNode ** pbCubesRes, int CutLevel ) +{ + st__table * Visited; // temporary table to remember the visited nodes + st__table * CutNodes; // the nodes under the cut go here + int i, Counter; + + s_CutLevel = CutLevel; + + // there should be some nodes + assert( nNodes > 0 ); + if ( nNodes == 1 && Cudd_IsConstant( paNodes[0] ) ) + { + if ( paNodes[0] == a1 ) + { + paNodesRes[0] = a1; Cudd_Ref( a1 ); + pbCubesRes[0] = pbCubes[0]; Cudd_Ref( pbCubes[0] ); + } + else + { + paNodesRes[0] = a0; Cudd_Ref( a0 ); + pbCubesRes[0] = pbCubes[0]; Cudd_Ref( pbCubes[0] ); + } + return 1; + } + + // Step 1: Start the table and collect information about the nodes above the cut + // this information tells how many edges point to each node + CutNodes = st__init_table( st__ptrcmp, st__ptrhash);; + Visited = st__init_table( st__ptrcmp, st__ptrhash);; + + for ( i = 0; i < nNodes; i++ ) + CountNodeVisits_rec( dd, paNodes[i], Visited ); + + // Step 2: Traverse the BDD using the visited table and compute the sum of paths + for ( i = 0; i < nNodes; i++ ) + CollectNodesAndComputePaths_rec( dd, paNodes[i], pbCubes[i], Visited, CutNodes ); + + // at this point, the table of cut nodes is ready and the table of visited is useless + { + st__generator * gen; + DdNode * aNode; + traventry * p; + st__foreach_item( Visited, gen, (const char**)&aNode, (char**)&p ) + { + Cudd_RecursiveDeref( dd, p->bSum ); + ABC_FREE( p ); + } + st__free_table( Visited ); + } + + // go through the table CutNodes and create the BDD and the path to be returned + { + st__generator * gen; + DdNode * aNode, * bSum; + Counter = 0; + st__foreach_item( CutNodes, gen, (const char**)&aNode, (char**)&bSum) + { + paNodesRes[Counter] = aNode; Cudd_Ref( aNode ); + pbCubesRes[Counter] = bSum; + Counter++; + } + st__free_table( CutNodes ); + } + + // return the number of cofactors found + return Counter; + +} /* end of Extra_bddNodePathsUnderCutArray */ + +/**Function************************************************************* + + Synopsis [Collects all the BDD nodes into the table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void extraCollectNodes( DdNode * Func, st__table * tNodes ) +{ + DdNode * FuncR; + FuncR = Cudd_Regular(Func); + if ( st__find_or_add( tNodes, (char*)FuncR, NULL ) ) + return; + if ( cuddIsConstant(FuncR) ) + return; + extraCollectNodes( cuddE(FuncR), tNodes ); + extraCollectNodes( cuddT(FuncR), tNodes ); +} + +/**Function************************************************************* + + Synopsis [Collects all the nodes of one DD into the table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + st__table * Extra_CollectNodes( DdNode * Func ) +{ + st__table * tNodes; + tNodes = st__init_table( st__ptrcmp, st__ptrhash ); + extraCollectNodes( Func, tNodes ); + return tNodes; +} + +/**Function************************************************************* + + Synopsis [Updates the topmost level from which the given node is referenced.] + + Description [Takes the table which maps each BDD nodes (including the constants) + into the topmost level on which this node counts as a cofactor. Takes the topmost + level, on which this node counts as a cofactor (see Extra_ProfileWidthFast(). + Takes the node, for which the table entry should be updated.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void extraProfileUpdateTopLevel( st__table * tNodeTopRef, int TopLevelNew, DdNode * node ) +{ + int * pTopLevel; + + if ( st__find_or_add( tNodeTopRef, (char*)node, (char***)&pTopLevel ) ) + { // the node is already referenced + // the current top level should be updated if it is larger than the new level + if ( *pTopLevel > TopLevelNew ) + *pTopLevel = TopLevelNew; + } + else + { // the node is not referenced + // its level should be set to the current new level + *pTopLevel = TopLevelNew; + } +} +/**Function************************************************************* + + Synopsis [Fast computation of the BDD profile.] + + Description [The array to store the profile is given by the user and should + contain at least as many entries as there is the maximum of the BDD/ZDD + size of the manager PLUS ONE. + When we say that the widths of the DD on level L is W, we mean the following. + Let us create the cut between the level L-1 and the level L and count the number + of different DD nodes pointed to across the cut. This number is the width W. + From this it follows the on level 0, the width is equal to the number of external + pointers to the considered DDs. If there is only one DD, then the profile on + level 0 is always 1. If this DD is rooted in the topmost variable, then the width + on level 1 is always 2, etc. The width at the level equal to dd->size is the + number of terminal nodes in the DD. (Because we consider the first level #0 + and the last level #dd->size, the profile array should contain dd->size+1 entries.) + ] + + SideEffects [This procedure will not work for BDDs w/ complement edges, only for ADDs and ZDDs] + + SeeAlso [] + +***********************************************************************/ +int Extra_ProfileWidth( DdManager * dd, DdNode * Func, int * pProfile, int CutLevel ) +{ + st__generator * gen; + st__table * tNodeTopRef; // this table stores the top level from which this node is pointed to + st__table * tNodes; + DdNode * node; + DdNode * nodeR; + int LevelStart, Limit; + int i, size; + int WidthMax; + + // start the mapping table + tNodeTopRef = st__init_table( st__ptrcmp, st__ptrhash);; + // add the topmost node to the profile + extraProfileUpdateTopLevel( tNodeTopRef, 0, Func ); + + // collect all nodes + tNodes = Extra_CollectNodes( Func ); + // go though all the nodes and set the top level the cofactors are pointed from +// Cudd_ForeachNode( dd, Func, genDD, node ) + st__foreach_item( tNodes, gen, (const char**)&node, NULL ) + { +// assert( Cudd_Regular(node) ); // this procedure works only with ADD/ZDD (not BDD w/ compl.edges) + nodeR = Cudd_Regular(node); + if ( cuddIsConstant(nodeR) ) + continue; + // this node is not a constant - consider its cofactors + extraProfileUpdateTopLevel( tNodeTopRef, dd->perm[node->index]+1, cuddE(nodeR) ); + extraProfileUpdateTopLevel( tNodeTopRef, dd->perm[node->index]+1, cuddT(nodeR) ); + } + st__free_table( tNodes ); + + // clean the profile + size = ddMax(dd->size, dd->sizeZ) + 1; + for ( i = 0; i < size; i++ ) + pProfile[i] = 0; + + // create the profile + st__foreach_item( tNodeTopRef, gen, (const char**)&node, (char**)&LevelStart ) + { + nodeR = Cudd_Regular(node); + Limit = (cuddIsConstant(nodeR))? dd->size: dd->perm[nodeR->index]; + for ( i = LevelStart; i <= Limit; i++ ) + pProfile[i]++; + } + + if ( CutLevel != -1 && CutLevel != 0 ) + size = CutLevel; + + // get the max width + WidthMax = 0; + for ( i = 0; i < size; i++ ) + if ( WidthMax < pProfile[i] ) + WidthMax = pProfile[i]; + + // deref the table + st__free_table( tNodeTopRef ); + + return WidthMax; +} /* end of Extra_ProfileWidth */ + + +/*---------------------------------------------------------------------------*/ +/* Definition of internal functions */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Definition of static functions */ +/*---------------------------------------------------------------------------*/ + +/**Function******************************************************************** + + Synopsis [Computes the non-strict codes when evaluation is finished.] + + Description [The information about the best code is stored in s_VarOrderBest, + which has s_nVarsBest entries.] + + SideEffects [None] + +******************************************************************************/ +DdNode * CreateTheCodes_rec( DdManager * dd, DdNode * bEncoded, int Level, DdNode ** pCVars ) +// bEncoded is the preliminarily encoded set of columns +// Level is the current level in the recursion +// pCVars are the variables to be used for encoding +{ + DdNode * bRes; + if ( Level == s_nVarsBest ) + { // the terminal case, when we need to remap the encoded function + // from the preliminary encoded variables to the new ones + st__table * CutNodes; + int nCols; +// double nMints; +/* +#ifdef _DEBUG + + { + DdNode * bTemp; + // make sure that the given number of variables is enough + bTemp = Cudd_bddExistAbstract( dd, bEncoded, s_VarAll ); Cudd_Ref( bTemp ); +// nMints = Cudd_CountMinterm( dd, bTemp, s_MultiStart ); + nMints = Extra_CountMintermsSimple( bTemp, (1< Extra_Power2( s_MultiStart-Level ) ) + { // the number of minterms is too large to encode the columns + // using the given minimum number of encoding variables + assert( 0 ); + } + Cudd_RecursiveDeref( dd, bTemp ); + } +#endif +*/ + // get the columns to be re-encoded + CutNodes = Extra_bddNodePathsUnderCut( dd, bEncoded, s_EncodingVarsLevel ); + // LUT size is the cut level because because the temporary encoding variables + // are above the functional variables - this is not true!!! + // the temporary variables are below! + + // put the entries from the table into the temporary array + { + st__generator * gen; + DdNode * bColumn, * bCode; + nCols = 0; + st__foreach_item( CutNodes, gen, (const char**)&bCode, (char**)&bColumn ) + { + if ( bCode == b0 ) + { // the unused part of the columns + Cudd_RecursiveDeref( dd, bColumn ); + Cudd_RecursiveDeref( dd, bCode ); + continue; + } + else + { + s_pbTemp[ nCols ] = bColumn; // takes ref + Cudd_RecursiveDeref( dd, bCode ); + nCols++; + } + } + st__free_table( CutNodes ); +// assert( nCols == (int)nMints ); + } + + // encode the columns + if ( s_MultiStart-Level == 0 ) // we reached the bottom level of recursion + { + assert( nCols == 1 ); +// assert( (int)nMints == 1 ); + bRes = s_pbTemp[0]; Cudd_Ref( bRes ); + } + else + { + bRes = Extra_bddEncodingBinary( dd, s_pbTemp, nCols, pCVars+Level, s_MultiStart-Level ); Cudd_Ref( bRes ); + } + + // deref the columns + { + int i; + for ( i = 0; i < nCols; i++ ) + Cudd_RecursiveDeref( dd, s_pbTemp[i] ); + } + } + else + { + // cofactor the problem as specified in the best solution + DdNode * bCof0, * bCof1; + DdNode * bRes0, * bRes1; + DdNode * bProd0, * bProd1; + DdNode * bTemp; + DdNode * bVarNext = dd->vars[ s_VarOrderBest[Level] ]; + + bCof0 = Cudd_Cofactor( dd, bEncoded, Cudd_Not( bVarNext ) ); Cudd_Ref( bCof0 ); + bCof1 = Cudd_Cofactor( dd, bEncoded, bVarNext ); Cudd_Ref( bCof1 ); + + // call recursively + bRes0 = CreateTheCodes_rec( dd, bCof0, Level+1, pCVars ); Cudd_Ref( bRes0 ); + bRes1 = CreateTheCodes_rec( dd, bCof1, Level+1, pCVars ); Cudd_Ref( bRes1 ); + + Cudd_RecursiveDeref( dd, bCof0 ); + Cudd_RecursiveDeref( dd, bCof1 ); + + // compose the result using the identity (bVarNext <=> pCVars[Level]) - this is wrong! + // compose the result as follows: x'y'F0 + xyF1 + bProd0 = Cudd_bddAnd( dd, Cudd_Not(bVarNext), Cudd_Not(pCVars[Level]) ); Cudd_Ref( bProd0 ); + bProd1 = Cudd_bddAnd( dd, bVarNext , pCVars[Level] ); Cudd_Ref( bProd1 ); + + bProd0 = Cudd_bddAnd( dd, bTemp = bProd0, bRes0 ); Cudd_Ref( bProd0 ); + Cudd_RecursiveDeref( dd, bTemp ); + Cudd_RecursiveDeref( dd, bRes0 ); + + bProd1 = Cudd_bddAnd( dd, bTemp = bProd1, bRes1 ); Cudd_Ref( bProd1 ); + Cudd_RecursiveDeref( dd, bTemp ); + Cudd_RecursiveDeref( dd, bRes1 ); + + bRes = Cudd_bddOr( dd, bProd0, bProd1 ); Cudd_Ref( bRes ); + + Cudd_RecursiveDeref( dd, bProd0 ); + Cudd_RecursiveDeref( dd, bProd1 ); + } + Cudd_Deref( bRes ); + return bRes; +} + +/**Function******************************************************************** + + Synopsis [Computes the current set of variables and counts the number of minterms.] + + Description [Old implementation.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +void EvaluateEncodings_rec( DdManager * dd, DdNode * bVarsCol, int nVarsCol, int nMulti, int Level ) +// bVarsCol is the set of remaining variables +// nVarsCol is the number of remaining variables +// nMulti is the number of encoding variables to be used +// Level is the level of recursion, from which this function is called +// if we successfully finish this procedure, Level also stands for how many encoding variabled we saved +{ + int i, k; + int nEntries = (1<<(Level-1)); // the number of entries in the field of the previous level + DdNode * bVars0, * bVars1; // the cofactors + unsigned nMint0, nMint1; // the number of minterms + DdNode * bTempV; + DdNode * bVarTop; + int fBreak; + + + // there is no need to search above this level + if ( Level > s_MaxDepth ) + return; + + // if there are no variables left, quit the research + if ( bVarsCol == b1 ) + return; + + if ( s_BackTracks > s_BackTrackLimit ) + return; + + s_BackTracks++; + + // otherwise, go through the remaining variables + for ( bTempV = bVarsCol; bTempV != b1; bTempV = cuddT(bTempV) ) + { + // the currently tested variable + bVarTop = dd->vars[bTempV->index]; + + // put it into the array + s_VarOrderCur[Level-1] = bTempV->index; + + // go through the entries and fill them out by cofactoring + fBreak = 0; + for ( i = 0; i < nEntries; i++ ) + { + bVars0 = ComputeVarSetAndCountMinterms( dd, s_Field[Level-1][i], Cudd_Not(bVarTop), &nMint0 ); + Cudd_Ref( bVars0 ); + + if ( nMint0 > Extra_Power2( nMulti-1 ) ) + { + // there is no way to encode - dereference and return + Cudd_RecursiveDeref( dd, bVars0 ); + fBreak = 1; + break; + } + + bVars1 = ComputeVarSetAndCountMinterms( dd, s_Field[Level-1][i], bVarTop, &nMint1 ); + Cudd_Ref( bVars1 ); + + if ( nMint1 > Extra_Power2( nMulti-1 ) ) + { + // there is no way to encode - dereference and return + Cudd_RecursiveDeref( dd, bVars0 ); + Cudd_RecursiveDeref( dd, bVars1 ); + fBreak = 1; + break; + } + + // otherwise, add these two cofactors + s_Field[Level][2*i + 0] = bVars0; // takes ref + s_Field[Level][2*i + 1] = bVars1; // takes ref + } + + if ( !fBreak ) + { + DdNode * bVarsRem; + // if we ended up here, it means that the cofactors w.r.t. variable bVarTop satisfy the condition + // save this situation + if ( s_nVarsBest < Level ) + { + s_nVarsBest = Level; + // copy the variable assignment + for ( k = 0; k < Level; k++ ) + s_VarOrderBest[k] = s_VarOrderCur[k]; + } + + // call recursively + // get the new variable set + if ( nMulti-1 > 0 ) + { + bVarsRem = Cudd_bddExistAbstract( dd, bVarsCol, bVarTop ); Cudd_Ref( bVarsRem ); + EvaluateEncodings_rec( dd, bVarsRem, nVarsCol-1, nMulti-1, Level+1 ); + Cudd_RecursiveDeref( dd, bVarsRem ); + } + } + + // deref the contents of the array + for ( k = 0; k < i; k++ ) + { + Cudd_RecursiveDeref( dd, s_Field[Level][2*k + 0] ); + Cudd_RecursiveDeref( dd, s_Field[Level][2*k + 1] ); + } + + // if the solution is found, there is no need to continue + if ( s_nVarsBest == s_MaxDepth ) + return; + + // if the solution is found, there is no need to continue + if ( s_nVarsBest == s_MultiStart ) + return; + } + // at this point, we have tried all possible directions in the space of variables +} + +/**Function******************************************************************** + + Synopsis [Computes the current set of variables and counts the number of minterms.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * ComputeVarSetAndCountMinterms( DdManager * dd, DdNode * bVars, DdNode * bVarTop, unsigned * Cost ) +// takes bVars - the variables cofactored so far (some of them may be in negative polarity) +// bVarTop - the topmost variable w.r.t. which to cofactor (may be in negative polarity) +// returns the cost and the new set of variables (bVars & bVarTop) +{ + DdNode * bVarsRes; + + // get the resulting set of variables + bVarsRes = Cudd_bddAnd( dd, bVars, bVarTop ); Cudd_Ref( bVarsRes ); + + // increment signature before calling Cudd_CountCofactorMinterms() + s_Signature++; + *Cost = Extra_CountCofactorMinterms( dd, s_Encoded, bVarsRes, s_VarAll ); + + Cudd_Deref( bVarsRes ); +// s_CountCalls++; + return bVarsRes; +} + +/**Function******************************************************************** + + Synopsis [Computes the current set of variables and counts the number of minterms.] + + Description [The old implementation, which is approximately 4 times slower.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * ComputeVarSetAndCountMinterms2( DdManager * dd, DdNode * bVars, DdNode * bVarTop, unsigned * Cost ) +{ + DdNode * bVarsRes; + DdNode * bCof, * bFun; + + bVarsRes = Cudd_bddAnd( dd, bVars, bVarTop ); Cudd_Ref( bVarsRes ); + + bCof = Cudd_Cofactor( dd, s_Encoded, bVarsRes ); Cudd_Ref( bCof ); + bFun = Cudd_bddExistAbstract( dd, bCof, s_VarAll ); Cudd_Ref( bFun ); + *Cost = (unsigned)Cudd_CountMinterm( dd, bFun, s_MultiStart ); + Cudd_RecursiveDeref( dd, bFun ); + Cudd_RecursiveDeref( dd, bCof ); + + Cudd_Deref( bVarsRes ); +// s_CountCalls++; + return bVarsRes; +} + + +/**Function******************************************************************** + + Synopsis [Counts the number of encoding minterms pointed to by the cofactor of the function.] + + Description [] + + SideEffects [None] + +******************************************************************************/ +unsigned Extra_CountCofactorMinterms( DdManager * dd, DdNode * bFunc, DdNode * bVarsCof, DdNode * bVarsAll ) +// this function computes how many minterms depending on the encoding variables +// are there in the cofactor of bFunc w.r.t. variables bVarsCof +// bFunc is assumed to depend on variables s_VarsAll +// the variables s_VarsAll should be ordered above the encoding variables +{ + unsigned HKey; + DdNode * bFuncR; + + // if the function is zero, there are no minterms +// if ( bFunc == b0 ) +// return 0; + +// if ( st__lookup(Visited, (char*)bFunc, NULL) ) +// return 0; + +// HKey = hashKey2c( s_Signature, bFuncR ); +// if ( HHTable1[HKey].Sign == s_Signature && HHTable1[HKey].Arg1 == bFuncR ) // this node is visited +// return 0; + + + // check the hash-table + bFuncR = Cudd_Regular(bFunc); +// HKey = hashKey2( s_Signature, bFuncR, _TABLESIZE_COF ); + HKey = hashKey2( s_Signature, bFunc, _TABLESIZE_COF ); + for ( ; HHTable1[HKey].Sign == s_Signature; HKey = (HKey+1) % _TABLESIZE_COF ) +// if ( HHTable1[HKey].Arg1 == bFuncR ) // this node is visited + if ( HHTable1[HKey].Arg1 == bFunc ) // this node is visited + return 0; + + + // if the function is already the code + if ( dd->perm[bFuncR->index] >= s_EncodingVarsLevel ) + { +// st__insert(Visited, (char*)bFunc, NULL); + +// HHTable1[HKey].Sign = s_Signature; +// HHTable1[HKey].Arg1 = bFuncR; + + assert( HHTable1[HKey].Sign != s_Signature ); + HHTable1[HKey].Sign = s_Signature; +// HHTable1[HKey].Arg1 = bFuncR; + HHTable1[HKey].Arg1 = bFunc; + + return Extra_CountMintermsSimple( bFunc, (1<perm[bFuncR->index]; + int LevelC = cuddI(dd,bVarsCofR->index); + int LevelA = dd->perm[bVarsAll->index]; + + int LevelTop = LevelF; + + if ( LevelTop > LevelC ) + LevelTop = LevelC; + + if ( LevelTop > LevelA ) + LevelTop = LevelA; + + // the top var in the function or in cofactoring vars always belongs to the set of all vars + assert( !( LevelTop == LevelF || LevelTop == LevelC ) || LevelTop == LevelA ); + + // cofactor the function + if ( LevelTop == LevelF ) + { + if ( bFuncR != bFunc ) // bFunc is complemented + { + bFunc0 = Cudd_Not( cuddE(bFuncR) ); + bFunc1 = Cudd_Not( cuddT(bFuncR) ); + } + else + { + bFunc0 = cuddE(bFuncR); + bFunc1 = cuddT(bFuncR); + } + } + else // bVars is higher in the variable order + bFunc0 = bFunc1 = bFunc; + + // cofactor the cube + if ( LevelTop == LevelC ) + { + if ( bVarsCofR != bVarsCof ) // bFunc is complemented + { + bVarsCof0 = Cudd_Not( cuddE(bVarsCofR) ); + bVarsCof1 = Cudd_Not( cuddT(bVarsCofR) ); + } + else + { + bVarsCof0 = cuddE(bVarsCofR); + bVarsCof1 = cuddT(bVarsCofR); + } + } + else // bVars is higher in the variable order + bVarsCof0 = bVarsCof1 = bVarsCof; + + // there are two cases: + // (1) the top variable belongs to the cofactoring variables + // (2) the top variable does not belong to the cofactoring variables + + // (1) the top variable belongs to the cofactoring variables + Res = 0; + if ( LevelTop == LevelC ) + { + if ( bVarsCof1 == b0 ) // this is a negative cofactor + { + if ( bFunc0 != b0 ) + Res = Extra_CountCofactorMinterms( dd, bFunc0, bVarsCof0, cuddT(bVarsAll) ); + } + else // this is a positive cofactor + { + if ( bFunc1 != b0 ) + Res = Extra_CountCofactorMinterms( dd, bFunc1, bVarsCof1, cuddT(bVarsAll) ); + } + } + else + { + if ( bFunc0 != b0 ) + Res += Extra_CountCofactorMinterms( dd, bFunc0, bVarsCof0, cuddT(bVarsAll) ); + + if ( bFunc1 != b0 ) + Res += Extra_CountCofactorMinterms( dd, bFunc1, bVarsCof1, cuddT(bVarsAll) ); + } + +// st__insert(Visited, (char*)bFunc, NULL); + +// HHTable1[HKey].Sign = s_Signature; +// HHTable1[HKey].Arg1 = bFuncR; + + // skip through the entries with the same signatures + // (these might have been created at the time of recursive calls) + for ( ; HHTable1[HKey].Sign == s_Signature; HKey = (HKey+1) % _TABLESIZE_COF ); + assert( HHTable1[HKey].Sign != s_Signature ); + HHTable1[HKey].Sign = s_Signature; +// HHTable1[HKey].Arg1 = bFuncR; + HHTable1[HKey].Arg1 = bFunc; + + return Res; + } +} + +/**Function******************************************************************** + + Synopsis [Counts the number of minterms.] + + Description [This function counts minterms for functions up to 32 variables + using a local cache. The terminal value (s_Termina) should be adjusted for + BDDs and ADDs.] + + SideEffects [None] + +******************************************************************************/ +unsigned Extra_CountMintermsSimple( DdNode * bFunc, unsigned max ) +{ + unsigned HKey; + + // normalize + if ( Cudd_IsComplement(bFunc) ) + return max - Extra_CountMintermsSimple( Cudd_Not(bFunc), max ); + + // now it is known that the function is not complemented + if ( cuddIsConstant(bFunc) ) + return ((bFunc==s_Terminal)? 0: max); + + // check cache + HKey = hashKey2( bFunc, max, _TABLESIZE_MINT ); + if ( HHTable2[HKey].Arg1 == bFunc && HHTable2[HKey].Arg2 == max ) + return HHTable2[HKey].Res; + else + { + // min = min0/2 + min1/2; + unsigned min = (Extra_CountMintermsSimple( cuddE(bFunc), max ) >> 1) + + (Extra_CountMintermsSimple( cuddT(bFunc), max ) >> 1); + + HHTable2[HKey].Arg1 = bFunc; + HHTable2[HKey].Arg2 = max; + HHTable2[HKey].Res = min; + + return min; + } +} /* end of Extra_CountMintermsSimple */ + + +/**Function******************************************************************** + + Synopsis [Visits the nodes.] + + Description [Visits the nodes above the cut and the nodes pointed to below the cut; + collects the visited nodes, counts how many times each node is visited, and sets + the path-sum to be the constant zero BDD.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +void CountNodeVisits_rec( DdManager * dd, DdNode * aFunc, st__table * Visited ) + +{ + traventry * p; + char **slot; + if ( st__find_or_add(Visited, (char*)aFunc, &slot) ) + { // the entry already exists + p = (traventry*) *slot; + // increment the counter of incoming edges + p->nEdges++; + return; + } + // this node has not been visited + assert( !Cudd_IsComplement(aFunc) ); + + // create the new traversal entry + p = (traventry *) ABC_ALLOC( char, sizeof(traventry) ); + // set the initial sum of edges to zero BDD + p->bSum = b0; Cudd_Ref( b0 ); + // set the starting number of incoming edges + p->nEdges = 1; + // set this entry into the slot + *slot = (char*)p; + + // recur if the node is above the cut + if ( cuddI(dd,aFunc->index) < s_CutLevel ) + { + CountNodeVisits_rec( dd, cuddE(aFunc), Visited ); + CountNodeVisits_rec( dd, cuddT(aFunc), Visited ); + } +} /* end of CountNodeVisits_rec */ + + +/**Function******************************************************************** + + Synopsis [Revisits the nodes and computes the paths.] + + Description [This function visits the nodes above the cut having the goal of + summing all the incomming BDD edges; when this function comes across the node + below the cut, it saves this node in the CutNode table.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +void CollectNodesAndComputePaths_rec( DdManager * dd, DdNode * aFunc, DdNode * bCube, st__table * Visited, st__table * CutNodes ) +{ + // find the node in the visited table + DdNode * bTemp; + traventry * p; + char **slot; + if ( st__find_or_add(Visited, (char*)aFunc, &slot) ) + { // the node is found + // get the pointer to the traversal entry + p = (traventry*) *slot; + + // make sure that the counter of incoming edges is positive + assert( p->nEdges > 0 ); + + // add the cube to the currently accumulated cubes + p->bSum = Cudd_bddOr( dd, bTemp = p->bSum, bCube ); Cudd_Ref( p->bSum ); + Cudd_RecursiveDeref( dd, bTemp ); + + // decrement the number of visits + p->nEdges--; + + // if more visits to this node are expected, return + if ( p->nEdges ) + return; + else // if ( p->nEdges == 0 ) + { // this is the last visit - propagate the cube + + // check where this node is + if ( cuddI(dd,aFunc->index) < s_CutLevel ) + { // the node is above the cut + DdNode * bCube0, * bCube1; + + // get the top-most variable + DdNode * bVarTop = dd->vars[aFunc->index]; + + // compute the propagated cubes + bCube0 = Cudd_bddAnd( dd, p->bSum, Cudd_Not( bVarTop ) ); Cudd_Ref( bCube0 ); + bCube1 = Cudd_bddAnd( dd, p->bSum, bVarTop ); Cudd_Ref( bCube1 ); + + // call recursively + CollectNodesAndComputePaths_rec( dd, cuddE(aFunc), bCube0, Visited, CutNodes ); + CollectNodesAndComputePaths_rec( dd, cuddT(aFunc), bCube1, Visited, CutNodes ); + + // dereference the cubes + Cudd_RecursiveDeref( dd, bCube0 ); + Cudd_RecursiveDeref( dd, bCube1 ); + return; + } + else + { // the node is below the cut + // add this node to the cut node table, if it is not yet there + +// DdNode * bNode; +// bNode = Cudd_addBddPattern( dd, aFunc ); Cudd_Ref( bNode ); + if ( st__find_or_add(CutNodes, (char*)aFunc, &slot) ) + { // the node exists - should never happen + assert( 0 ); + } + *slot = (char*) p->bSum; Cudd_Ref( p->bSum ); + // the table takes the reference of bNode + return; + } + } + } + + // the node does not exist in the visited table - should never happen + assert(0); + +} /* end of CollectNodesAndComputePaths_rec */ + + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/bdd/extrab/extraBddImage.c b/src/bdd/extrab/extraBddImage.c new file mode 100644 index 00000000..46afb4f2 --- /dev/null +++ b/src/bdd/extrab/extraBddImage.c @@ -0,0 +1,1162 @@ +/**CFile**************************************************************** + + FileName [extraBddImage.c] + + PackageName [extra] + + Synopsis [Various reusable software utilities.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - September 1, 2003.] + + Revision [$Id: extraBddImage.c,v 1.0 2003/09/01 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "extraBdd.h" + +ABC_NAMESPACE_IMPL_START + + +/* + The ideas implemented in this file are inspired by the paper: + Pankaj Chauhan, Edmund Clarke, Somesh Jha, Jim Kukula, Tom Shiple, + Helmut Veith, Dong Wang. Non-linear Quantification Scheduling in + Image Computation. ICCAD, 2001. +*/ + +/*---------------------------------------------------------------------------*/ +/* Constant declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Stucture declarations */ +/*---------------------------------------------------------------------------*/ + +typedef struct Extra_ImageNode_t_ Extra_ImageNode_t; +typedef struct Extra_ImagePart_t_ Extra_ImagePart_t; +typedef struct Extra_ImageVar_t_ Extra_ImageVar_t; + +struct Extra_ImageTree_t_ +{ + Extra_ImageNode_t * pRoot; // the root of quantification tree + Extra_ImageNode_t * pCare; // the leaf node with the care set + DdNode * bCareSupp; // the cube to quantify from the care + int fVerbose; // the verbosity flag + int nNodesMax; // the max number of nodes in one iter + int nNodesMaxT; // the overall max number of nodes + int nIter; // the number of iterations with this tree +}; + +struct Extra_ImageNode_t_ +{ + DdManager * dd; // the manager + DdNode * bCube; // the cube to quantify + DdNode * bImage; // the partial image + Extra_ImageNode_t * pNode1; // the first branch + Extra_ImageNode_t * pNode2; // the second branch + Extra_ImagePart_t * pPart; // the partition (temporary) +}; + +struct Extra_ImagePart_t_ +{ + DdNode * bFunc; // the partition + DdNode * bSupp; // the support of this partition + int nNodes; // the number of BDD nodes + short nSupp; // the number of support variables + short iPart; // the number of this partition +}; + +struct Extra_ImageVar_t_ +{ + int iNum; // the BDD index of this variable + DdNode * bParts; // the partition numbers + int nParts; // the number of partitions +}; + +/*---------------------------------------------------------------------------*/ +/* Type declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Variable declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Macro declarations */ +/*---------------------------------------------------------------------------*/ + +/**AutomaticStart*************************************************************/ + + +/*---------------------------------------------------------------------------*/ +/* Static function prototypes */ +/*---------------------------------------------------------------------------*/ + +static Extra_ImagePart_t ** Extra_CreateParts( DdManager * dd, + int nParts, DdNode ** pbParts, DdNode * bCare ); +static Extra_ImageVar_t ** Extra_CreateVars( DdManager * dd, + int nParts, Extra_ImagePart_t ** pParts, + int nVars, DdNode ** pbVarsNs ); +static Extra_ImageNode_t ** Extra_CreateNodes( DdManager * dd, + int nParts, Extra_ImagePart_t ** pParts, + int nVars, Extra_ImageVar_t ** pVars ); +static void Extra_DeleteParts_rec( Extra_ImageNode_t * pNode ); +static int Extra_BuildTreeNode( DdManager * dd, + int nNodes, Extra_ImageNode_t ** pNodes, + int nVars, Extra_ImageVar_t ** pVars ); +static Extra_ImageNode_t * Extra_MergeTopNodes( DdManager * dd, + int nNodes, Extra_ImageNode_t ** pNodes ); +static void Extra_bddImageTreeDelete_rec( Extra_ImageNode_t * pNode ); +static void Extra_bddImageCompute_rec( Extra_ImageTree_t * pTree, Extra_ImageNode_t * pNode ); +static int Extra_FindBestVariable( DdManager * dd, + int nNodes, Extra_ImageNode_t ** pNodes, + int nVars, Extra_ImageVar_t ** pVars ); +static void Extra_FindBestPartitions( DdManager * dd, DdNode * bParts, + int nNodes, Extra_ImageNode_t ** pNodes, + int * piNode1, int * piNode2 ); +static Extra_ImageNode_t * Extra_CombineTwoNodes( DdManager * dd, DdNode * bCube, + Extra_ImageNode_t * pNode1, Extra_ImageNode_t * pNode2 ); + +static void Extra_bddImagePrintLatchDependency( DdManager * dd, DdNode * bCare, + int nParts, DdNode ** pbParts, + int nVars, DdNode ** pbVars ); +static void Extra_bddImagePrintLatchDependencyOne( DdManager * dd, DdNode * bFunc, + DdNode * bVarsCs, DdNode * bVarsNs, int iPart ); + +static void Extra_bddImagePrintTree( Extra_ImageTree_t * pTree ); +static void Extra_bddImagePrintTree_rec( Extra_ImageNode_t * pNode, int nOffset ); + + +/**AutomaticEnd***************************************************************/ + + +/*---------------------------------------------------------------------------*/ +/* Definition of exported functions */ +/*---------------------------------------------------------------------------*/ + +/**Function************************************************************* + + Synopsis [Starts the image computation using tree-based scheduling.] + + Description [This procedure starts the image computation. It uses + the given care set to test-run the image computation and creates the + quantification tree by scheduling variable quantifications. The tree can + be used to compute images for other care sets without rescheduling. + In this case, Extra_bddImageCompute() should be called.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Extra_ImageTree_t * Extra_bddImageStart( + DdManager * dd, DdNode * bCare, // the care set + int nParts, DdNode ** pbParts, // the partitions for image computation + int nVars, DdNode ** pbVars, int fVerbose ) // the NS and parameter variables (not quantified!) +{ + Extra_ImageTree_t * pTree; + Extra_ImagePart_t ** pParts; + Extra_ImageVar_t ** pVars; + Extra_ImageNode_t ** pNodes; + int v; + + if ( fVerbose && dd->size <= 80 ) + Extra_bddImagePrintLatchDependency( dd, bCare, nParts, pbParts, nVars, pbVars ); + + // create variables, partitions and leaf nodes + pParts = Extra_CreateParts( dd, nParts, pbParts, bCare ); + pVars = Extra_CreateVars( dd, nParts + 1, pParts, nVars, pbVars ); + pNodes = Extra_CreateNodes( dd, nParts + 1, pParts, dd->size, pVars ); + + // create the tree + pTree = ABC_ALLOC( Extra_ImageTree_t, 1 ); + memset( pTree, 0, sizeof(Extra_ImageTree_t) ); + pTree->pCare = pNodes[nParts]; + pTree->fVerbose = fVerbose; + + // process the nodes + while ( Extra_BuildTreeNode( dd, nParts + 1, pNodes, dd->size, pVars ) ); + + // make sure the variables are gone + for ( v = 0; v < dd->size; v++ ) + assert( pVars[v] == NULL ); + ABC_FREE( pVars ); + + // merge the topmost nodes + while ( (pTree->pRoot = Extra_MergeTopNodes( dd, nParts + 1, pNodes )) == NULL ); + + // make sure the nodes are gone + for ( v = 0; v < nParts + 1; v++ ) + assert( pNodes[v] == NULL ); + ABC_FREE( pNodes ); + +// if ( fVerbose ) +// Extra_bddImagePrintTree( pTree ); + + // set the support of the care set + pTree->bCareSupp = Cudd_Support( dd, bCare ); Cudd_Ref( pTree->bCareSupp ); + + // clean the partitions + Extra_DeleteParts_rec( pTree->pRoot ); + ABC_FREE( pParts ); + return pTree; +} + +/**Function************************************************************* + + Synopsis [Compute the image.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Extra_bddImageCompute( Extra_ImageTree_t * pTree, DdNode * bCare ) +{ + DdManager * dd = pTree->pCare->dd; + DdNode * bSupp, * bRem; + + pTree->nIter++; + + // make sure the supports are okay + bSupp = Cudd_Support( dd, bCare ); Cudd_Ref( bSupp ); + if ( bSupp != pTree->bCareSupp ) + { + bRem = Cudd_bddExistAbstract( dd, bSupp, pTree->bCareSupp ); Cudd_Ref( bRem ); + if ( bRem != b1 ) + { +printf( "Original care set support: " ); +ABC_PRB( dd, pTree->bCareSupp ); +printf( "Current care set support: " ); +ABC_PRB( dd, bSupp ); + Cudd_RecursiveDeref( dd, bSupp ); + Cudd_RecursiveDeref( dd, bRem ); + printf( "The care set depends on some vars that were not in the care set during scheduling.\n" ); + return NULL; + } + Cudd_RecursiveDeref( dd, bRem ); + } + Cudd_RecursiveDeref( dd, bSupp ); + + // remove the previous image + Cudd_RecursiveDeref( dd, pTree->pCare->bImage ); + pTree->pCare->bImage = bCare; Cudd_Ref( bCare ); + + // compute the image + pTree->nNodesMax = 0; + Extra_bddImageCompute_rec( pTree, pTree->pRoot ); + if ( pTree->nNodesMaxT < pTree->nNodesMax ) + pTree->nNodesMaxT = pTree->nNodesMax; + +// if ( pTree->fVerbose ) +// printf( "Iter %2d : Max nodes = %5d.\n", pTree->nIter, pTree->nNodesMax ); + return pTree->pRoot->bImage; +} + +/**Function************************************************************* + + Synopsis [Delete the tree.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Extra_bddImageTreeDelete( Extra_ImageTree_t * pTree ) +{ + if ( pTree->bCareSupp ) + Cudd_RecursiveDeref( pTree->pRoot->dd, pTree->bCareSupp ); + Extra_bddImageTreeDelete_rec( pTree->pRoot ); + ABC_FREE( pTree ); +} + +/**Function************************************************************* + + Synopsis [Reads the image from the tree.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Extra_bddImageRead( Extra_ImageTree_t * pTree ) +{ + return pTree->pRoot->bImage; +} + +/*---------------------------------------------------------------------------*/ +/* Definition of internal functions */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Definition of static Functions */ +/*---------------------------------------------------------------------------*/ + +/**Function************************************************************* + + Synopsis [Creates partitions.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Extra_ImagePart_t ** Extra_CreateParts( DdManager * dd, + int nParts, DdNode ** pbParts, DdNode * bCare ) +{ + Extra_ImagePart_t ** pParts; + int i; + + // start the partitions + pParts = ABC_ALLOC( Extra_ImagePart_t *, nParts + 1 ); + // create structures for each variable + for ( i = 0; i < nParts; i++ ) + { + pParts[i] = ABC_ALLOC( Extra_ImagePart_t, 1 ); + pParts[i]->bFunc = pbParts[i]; Cudd_Ref( pParts[i]->bFunc ); + pParts[i]->bSupp = Cudd_Support( dd, pParts[i]->bFunc ); Cudd_Ref( pParts[i]->bSupp ); + pParts[i]->nSupp = Extra_bddSuppSize( dd, pParts[i]->bSupp ); + pParts[i]->nNodes = Cudd_DagSize( pParts[i]->bFunc ); + pParts[i]->iPart = i; + } + // add the care set as the last partition + pParts[nParts] = ABC_ALLOC( Extra_ImagePart_t, 1 ); + pParts[nParts]->bFunc = bCare; Cudd_Ref( pParts[nParts]->bFunc ); + pParts[nParts]->bSupp = Cudd_Support( dd, pParts[nParts]->bFunc ); Cudd_Ref( pParts[nParts]->bSupp ); + pParts[nParts]->nSupp = Extra_bddSuppSize( dd, pParts[nParts]->bSupp ); + pParts[nParts]->nNodes = Cudd_DagSize( pParts[nParts]->bFunc ); + pParts[nParts]->iPart = nParts; + return pParts; +} + +/**Function************************************************************* + + Synopsis [Creates variables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Extra_ImageVar_t ** Extra_CreateVars( DdManager * dd, + int nParts, Extra_ImagePart_t ** pParts, + int nVars, DdNode ** pbVars ) +{ + Extra_ImageVar_t ** pVars; + DdNode ** pbFuncs; + DdNode * bCubeNs, * bSupp, * bParts, * bTemp, * bSuppTemp; + int nVarsTotal, iVar, p, Counter; + + // put all the functions into one array + pbFuncs = ABC_ALLOC( DdNode *, nParts ); + for ( p = 0; p < nParts; p++ ) + pbFuncs[p] = pParts[p]->bSupp; + bSupp = Cudd_VectorSupport( dd, pbFuncs, nParts ); Cudd_Ref( bSupp ); + ABC_FREE( pbFuncs ); + + // remove the NS vars + bCubeNs = Cudd_bddComputeCube( dd, pbVars, NULL, nVars ); Cudd_Ref( bCubeNs ); + bSupp = Cudd_bddExistAbstract( dd, bTemp = bSupp, bCubeNs ); Cudd_Ref( bSupp ); + Cudd_RecursiveDeref( dd, bTemp ); + Cudd_RecursiveDeref( dd, bCubeNs ); + + // get the number of I and CS variables to be quantified + nVarsTotal = Extra_bddSuppSize( dd, bSupp ); + + // start the variables + pVars = ABC_ALLOC( Extra_ImageVar_t *, dd->size ); + memset( pVars, 0, sizeof(Extra_ImageVar_t *) * dd->size ); + // create structures for each variable + for ( bSuppTemp = bSupp; bSuppTemp != b1; bSuppTemp = cuddT(bSuppTemp) ) + { + iVar = bSuppTemp->index; + pVars[iVar] = ABC_ALLOC( Extra_ImageVar_t, 1 ); + pVars[iVar]->iNum = iVar; + // collect all the parts this var belongs to + Counter = 0; + bParts = b1; Cudd_Ref( bParts ); + for ( p = 0; p < nParts; p++ ) + if ( Cudd_bddLeq( dd, pParts[p]->bSupp, dd->vars[bSuppTemp->index] ) ) + { + bParts = Cudd_bddAnd( dd, bTemp = bParts, dd->vars[p] ); Cudd_Ref( bParts ); + Cudd_RecursiveDeref( dd, bTemp ); + Counter++; + } + pVars[iVar]->bParts = bParts; // takes ref + pVars[iVar]->nParts = Counter; + } + Cudd_RecursiveDeref( dd, bSupp ); + return pVars; +} + +/**Function************************************************************* + + Synopsis [Creates variables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Extra_ImageNode_t ** Extra_CreateNodes( DdManager * dd, + int nParts, Extra_ImagePart_t ** pParts, + int nVars, Extra_ImageVar_t ** pVars ) +{ + Extra_ImageNode_t ** pNodes; + Extra_ImageNode_t * pNode; + DdNode * bTemp; + int i, v, iPart; +/* + DdManager * dd; // the manager + DdNode * bCube; // the cube to quantify + DdNode * bImage; // the partial image + Extra_ImageNode_t * pNode1; // the first branch + Extra_ImageNode_t * pNode2; // the second branch + Extra_ImagePart_t * pPart; // the partition (temporary) +*/ + // start the partitions + pNodes = ABC_ALLOC( Extra_ImageNode_t *, nParts ); + // create structures for each leaf nodes + for ( i = 0; i < nParts; i++ ) + { + pNodes[i] = ABC_ALLOC( Extra_ImageNode_t, 1 ); + memset( pNodes[i], 0, sizeof(Extra_ImageNode_t) ); + pNodes[i]->dd = dd; + pNodes[i]->pPart = pParts[i]; + } + // find the quantification cubes for each leaf node + for ( v = 0; v < nVars; v++ ) + { + if ( pVars[v] == NULL ) + continue; + assert( pVars[v]->nParts > 0 ); + if ( pVars[v]->nParts > 1 ) + continue; + iPart = pVars[v]->bParts->index; + if ( pNodes[iPart]->bCube == NULL ) + { + pNodes[iPart]->bCube = dd->vars[v]; + Cudd_Ref( dd->vars[v] ); + } + else + { + pNodes[iPart]->bCube = Cudd_bddAnd( dd, bTemp = pNodes[iPart]->bCube, dd->vars[v] ); + Cudd_Ref( pNodes[iPart]->bCube ); + Cudd_RecursiveDeref( dd, bTemp ); + } + // remove these variables + Cudd_RecursiveDeref( dd, pVars[v]->bParts ); + ABC_FREE( pVars[v] ); + } + + // assign the leaf node images + for ( i = 0; i < nParts; i++ ) + { + pNode = pNodes[i]; + if ( pNode->bCube ) + { + // update the partition + pParts[i]->bFunc = Cudd_bddExistAbstract( dd, bTemp = pParts[i]->bFunc, pNode->bCube ); + Cudd_Ref( pParts[i]->bFunc ); + Cudd_RecursiveDeref( dd, bTemp ); + // update the support the partition + pParts[i]->bSupp = Cudd_bddExistAbstract( dd, bTemp = pParts[i]->bSupp, pNode->bCube ); + Cudd_Ref( pParts[i]->bSupp ); + Cudd_RecursiveDeref( dd, bTemp ); + // update the numbers + pParts[i]->nSupp = Extra_bddSuppSize( dd, pParts[i]->bSupp ); + pParts[i]->nNodes = Cudd_DagSize( pParts[i]->bFunc ); + // get rid of the cube + // save the last (care set) quantification cube + if ( i < nParts - 1 ) + { + Cudd_RecursiveDeref( dd, pNode->bCube ); + pNode->bCube = NULL; + } + } + // copy the function + pNode->bImage = pParts[i]->bFunc; Cudd_Ref( pNode->bImage ); + } +/* + for ( i = 0; i < nParts; i++ ) + { + pNode = pNodes[i]; +ABC_PRB( dd, pNode->bCube ); +ABC_PRB( dd, pNode->pPart->bFunc ); +ABC_PRB( dd, pNode->pPart->bSupp ); +printf( "\n" ); + } +*/ + return pNodes; +} + + +/**Function************************************************************* + + Synopsis [Delete the partitions from the nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Extra_DeleteParts_rec( Extra_ImageNode_t * pNode ) +{ + Extra_ImagePart_t * pPart; + if ( pNode->pNode1 ) + Extra_DeleteParts_rec( pNode->pNode1 ); + if ( pNode->pNode2 ) + Extra_DeleteParts_rec( pNode->pNode2 ); + pPart = pNode->pPart; + Cudd_RecursiveDeref( pNode->dd, pPart->bFunc ); + Cudd_RecursiveDeref( pNode->dd, pPart->bSupp ); + ABC_FREE( pNode->pPart ); +} + +/**Function************************************************************* + + Synopsis [Delete the partitions from the nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Extra_bddImageTreeDelete_rec( Extra_ImageNode_t * pNode ) +{ + if ( pNode->pNode1 ) + Extra_bddImageTreeDelete_rec( pNode->pNode1 ); + if ( pNode->pNode2 ) + Extra_bddImageTreeDelete_rec( pNode->pNode2 ); + if ( pNode->bCube ) + Cudd_RecursiveDeref( pNode->dd, pNode->bCube ); + if ( pNode->bImage ) + Cudd_RecursiveDeref( pNode->dd, pNode->bImage ); + assert( pNode->pPart == NULL ); + ABC_FREE( pNode ); +} + +/**Function************************************************************* + + Synopsis [Recompute the image.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Extra_bddImageCompute_rec( Extra_ImageTree_t * pTree, Extra_ImageNode_t * pNode ) +{ + DdManager * dd = pNode->dd; + DdNode * bTemp; + int nNodes; + + // trivial case + if ( pNode->pNode1 == NULL ) + { + if ( pNode->bCube ) + { + pNode->bImage = Cudd_bddExistAbstract( dd, bTemp = pNode->bImage, pNode->bCube ); + Cudd_Ref( pNode->bImage ); + Cudd_RecursiveDeref( dd, bTemp ); + } + return; + } + + // compute the children + if ( pNode->pNode1 ) + Extra_bddImageCompute_rec( pTree, pNode->pNode1 ); + if ( pNode->pNode2 ) + Extra_bddImageCompute_rec( pTree, pNode->pNode2 ); + + // clean the old image + if ( pNode->bImage ) + Cudd_RecursiveDeref( dd, pNode->bImage ); + pNode->bImage = NULL; + + // compute the new image + if ( pNode->bCube ) + pNode->bImage = Cudd_bddAndAbstract( dd, + pNode->pNode1->bImage, pNode->pNode2->bImage, pNode->bCube ); + else + pNode->bImage = Cudd_bddAnd( dd, pNode->pNode1->bImage, pNode->pNode2->bImage ); + Cudd_Ref( pNode->bImage ); + + if ( pTree->fVerbose ) + { + nNodes = Cudd_DagSize( pNode->bImage ); + if ( pTree->nNodesMax < nNodes ) + pTree->nNodesMax = nNodes; + } +} + +/**Function************************************************************* + + Synopsis [Builds the tree.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Extra_BuildTreeNode( DdManager * dd, + int nNodes, Extra_ImageNode_t ** pNodes, + int nVars, Extra_ImageVar_t ** pVars ) +{ + Extra_ImageNode_t * pNode1, * pNode2; + Extra_ImageVar_t * pVar; + Extra_ImageNode_t * pNode; + DdNode * bCube, * bTemp, * bSuppTemp, * bParts; + int iNode1, iNode2; + int iVarBest, nSupp, v; + + // find the best variable + iVarBest = Extra_FindBestVariable( dd, nNodes, pNodes, nVars, pVars ); + if ( iVarBest == -1 ) + return 0; + + pVar = pVars[iVarBest]; + + // this var cannot appear in one partition only + nSupp = Extra_bddSuppSize( dd, pVar->bParts ); + assert( nSupp == pVar->nParts ); + assert( nSupp != 1 ); + + // if it appears in only two partitions, quantify it + if ( pVar->nParts == 2 ) + { + // get the nodes + iNode1 = pVar->bParts->index; + iNode2 = cuddT(pVar->bParts)->index; + pNode1 = pNodes[iNode1]; + pNode2 = pNodes[iNode2]; + + // get the quantification cube + bCube = dd->vars[pVar->iNum]; Cudd_Ref( bCube ); + // add the variables that appear only in these partitions + for ( v = 0; v < nVars; v++ ) + if ( pVars[v] && v != iVarBest && pVars[v]->bParts == pVars[iVarBest]->bParts ) + { + // add this var + bCube = Cudd_bddAnd( dd, bTemp = bCube, dd->vars[pVars[v]->iNum] ); Cudd_Ref( bCube ); + Cudd_RecursiveDeref( dd, bTemp ); + // clean this var + Cudd_RecursiveDeref( dd, pVars[v]->bParts ); + ABC_FREE( pVars[v] ); + } + // clean the best var + Cudd_RecursiveDeref( dd, pVars[iVarBest]->bParts ); + ABC_FREE( pVars[iVarBest] ); + + // combines two nodes + pNode = Extra_CombineTwoNodes( dd, bCube, pNode1, pNode2 ); + Cudd_RecursiveDeref( dd, bCube ); + } + else // if ( pVar->nParts > 2 ) + { + // find two smallest BDDs that have this var + Extra_FindBestPartitions( dd, pVar->bParts, nNodes, pNodes, &iNode1, &iNode2 ); + pNode1 = pNodes[iNode1]; + pNode2 = pNodes[iNode2]; + + // it is not possible that a var appears only in these two + // otherwise, it would have a different cost + bParts = Cudd_bddAnd( dd, dd->vars[iNode1], dd->vars[iNode2] ); Cudd_Ref( bParts ); + for ( v = 0; v < nVars; v++ ) + if ( pVars[v] && pVars[v]->bParts == bParts ) + assert( 0 ); + Cudd_RecursiveDeref( dd, bParts ); + + // combines two nodes + pNode = Extra_CombineTwoNodes( dd, b1, pNode1, pNode2 ); + } + + // clean the old nodes + pNodes[iNode1] = pNode; + pNodes[iNode2] = NULL; + + // update the variables that appear in pNode[iNode2] + for ( bSuppTemp = pNode2->pPart->bSupp; bSuppTemp != b1; bSuppTemp = cuddT(bSuppTemp) ) + { + pVar = pVars[bSuppTemp->index]; + if ( pVar == NULL ) // this variable is not be quantified + continue; + // quantify this var + assert( Cudd_bddLeq( dd, pVar->bParts, dd->vars[iNode2] ) ); + pVar->bParts = Cudd_bddExistAbstract( dd, bTemp = pVar->bParts, dd->vars[iNode2] ); Cudd_Ref( pVar->bParts ); + Cudd_RecursiveDeref( dd, bTemp ); + // add the new var + pVar->bParts = Cudd_bddAnd( dd, bTemp = pVar->bParts, dd->vars[iNode1] ); Cudd_Ref( pVar->bParts ); + Cudd_RecursiveDeref( dd, bTemp ); + // update the score + pVar->nParts = Extra_bddSuppSize( dd, pVar->bParts ); + } + return 1; +} + + +/**Function************************************************************* + + Synopsis [Merges the nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Extra_ImageNode_t * Extra_MergeTopNodes( + DdManager * dd, int nNodes, Extra_ImageNode_t ** pNodes ) +{ + Extra_ImageNode_t * pNode; + int n1 = -1, n2 = -1, n; + + // find the first and the second non-empty spots + for ( n = 0; n < nNodes; n++ ) + if ( pNodes[n] ) + { + if ( n1 == -1 ) + n1 = n; + else if ( n2 == -1 ) + { + n2 = n; + break; + } + } + assert( n1 != -1 ); + // check the situation when only one such node is detected + if ( n2 == -1 ) + { + // save the node + pNode = pNodes[n1]; + // clean the node + pNodes[n1] = NULL; + return pNode; + } + + // combines two nodes + pNode = Extra_CombineTwoNodes( dd, b1, pNodes[n1], pNodes[n2] ); + + // clean the old nodes + pNodes[n1] = pNode; + pNodes[n2] = NULL; + return NULL; +} + +/**Function************************************************************* + + Synopsis [Merges two nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Extra_ImageNode_t * Extra_CombineTwoNodes( DdManager * dd, DdNode * bCube, + Extra_ImageNode_t * pNode1, Extra_ImageNode_t * pNode2 ) +{ + Extra_ImageNode_t * pNode; + Extra_ImagePart_t * pPart; + + // create a new partition + pPart = ABC_ALLOC( Extra_ImagePart_t, 1 ); + memset( pPart, 0, sizeof(Extra_ImagePart_t) ); + // create the function + pPart->bFunc = Cudd_bddAndAbstract( dd, pNode1->pPart->bFunc, pNode2->pPart->bFunc, bCube ); + Cudd_Ref( pPart->bFunc ); + // update the support the partition + pPart->bSupp = Cudd_bddAndAbstract( dd, pNode1->pPart->bSupp, pNode2->pPart->bSupp, bCube ); + Cudd_Ref( pPart->bSupp ); + // update the numbers + pPart->nSupp = Extra_bddSuppSize( dd, pPart->bSupp ); + pPart->nNodes = Cudd_DagSize( pPart->bFunc ); + pPart->iPart = -1; +/* +ABC_PRB( dd, pNode1->pPart->bSupp ); +ABC_PRB( dd, pNode2->pPart->bSupp ); +ABC_PRB( dd, pPart->bSupp ); +*/ + // create a new node + pNode = ABC_ALLOC( Extra_ImageNode_t, 1 ); + memset( pNode, 0, sizeof(Extra_ImageNode_t) ); + pNode->dd = dd; + pNode->pPart = pPart; + pNode->pNode1 = pNode1; + pNode->pNode2 = pNode2; + // compute the image + pNode->bImage = Cudd_bddAndAbstract( dd, pNode1->bImage, pNode2->bImage, bCube ); + Cudd_Ref( pNode->bImage ); + // save the cube + if ( bCube != b1 ) + { + pNode->bCube = bCube; Cudd_Ref( bCube ); + } + return pNode; +} + +/**Function************************************************************* + + Synopsis [Computes the best variable.] + + Description [The variables is the best if the sum of squares of the + BDD sizes of the partitions, in which it participates, is the minimum.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Extra_FindBestVariable( DdManager * dd, + int nNodes, Extra_ImageNode_t ** pNodes, + int nVars, Extra_ImageVar_t ** pVars ) +{ + DdNode * bTemp; + int iVarBest, v; + double CostBest, CostCur; + + CostBest = 100000000000000.0; + iVarBest = -1; + for ( v = 0; v < nVars; v++ ) + if ( pVars[v] ) + { + CostCur = 0; + for ( bTemp = pVars[v]->bParts; bTemp != b1; bTemp = cuddT(bTemp) ) + CostCur += pNodes[bTemp->index]->pPart->nNodes * + pNodes[bTemp->index]->pPart->nNodes; + if ( CostBest > CostCur ) + { + CostBest = CostCur; + iVarBest = v; + } + } + return iVarBest; +} + +/**Function************************************************************* + + Synopsis [Computes two smallest partions that have this var.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Extra_FindBestPartitions( DdManager * dd, DdNode * bParts, + int nNodes, Extra_ImageNode_t ** pNodes, + int * piNode1, int * piNode2 ) +{ + DdNode * bTemp; + int iPart1, iPart2; + int CostMin1, CostMin2, Cost; + + // go through the partitions + iPart1 = iPart2 = -1; + CostMin1 = CostMin2 = 1000000; + for ( bTemp = bParts; bTemp != b1; bTemp = cuddT(bTemp) ) + { + Cost = pNodes[bTemp->index]->pPart->nNodes; + if ( CostMin1 > Cost ) + { + CostMin2 = CostMin1; iPart2 = iPart1; + CostMin1 = Cost; iPart1 = bTemp->index; + } + else if ( CostMin2 > Cost ) + { + CostMin2 = Cost; iPart2 = bTemp->index; + } + } + + *piNode1 = iPart1; + *piNode2 = iPart2; +} + +/**Function************************************************************* + + Synopsis [Prints the latch dependency matrix.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Extra_bddImagePrintLatchDependency( + DdManager * dd, DdNode * bCare, // the care set + int nParts, DdNode ** pbParts, // the partitions for image computation + int nVars, DdNode ** pbVars ) // the NS and parameter variables (not quantified!) +{ + int i; + DdNode * bVarsCs, * bVarsNs; + + bVarsCs = Cudd_Support( dd, bCare ); Cudd_Ref( bVarsCs ); + bVarsNs = Cudd_bddComputeCube( dd, pbVars, NULL, nVars ); Cudd_Ref( bVarsNs ); + + printf( "The latch dependency matrix:\n" ); + printf( "Partitions = %d Variables: total = %d non-quantifiable = %d\n", + nParts, dd->size, nVars ); + printf( " : " ); + for ( i = 0; i < dd->size; i++ ) + printf( "%d", i % 10 ); + printf( "\n" ); + + for ( i = 0; i < nParts; i++ ) + Extra_bddImagePrintLatchDependencyOne( dd, pbParts[i], bVarsCs, bVarsNs, i ); + Extra_bddImagePrintLatchDependencyOne( dd, bCare, bVarsCs, bVarsNs, nParts ); + + Cudd_RecursiveDeref( dd, bVarsCs ); + Cudd_RecursiveDeref( dd, bVarsNs ); +} + +/**Function************************************************************* + + Synopsis [Prints one row of the latch dependency matrix.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Extra_bddImagePrintLatchDependencyOne( + DdManager * dd, DdNode * bFunc, // the function + DdNode * bVarsCs, DdNode * bVarsNs, // the current/next state vars + int iPart ) +{ + DdNode * bSupport; + int v; + bSupport = Cudd_Support( dd, bFunc ); Cudd_Ref( bSupport ); + printf( " %3d : ", iPart ); + for ( v = 0; v < dd->size; v++ ) + { + if ( Cudd_bddLeq( dd, bSupport, dd->vars[v] ) ) + { + if ( Cudd_bddLeq( dd, bVarsCs, dd->vars[v] ) ) + printf( "c" ); + else if ( Cudd_bddLeq( dd, bVarsNs, dd->vars[v] ) ) + printf( "n" ); + else + printf( "i" ); + } + else + printf( "." ); + } + printf( "\n" ); + Cudd_RecursiveDeref( dd, bSupport ); +} + + +/**Function************************************************************* + + Synopsis [Prints the tree for quenstification scheduling.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Extra_bddImagePrintTree( Extra_ImageTree_t * pTree ) +{ + printf( "The quantification scheduling tree:\n" ); + Extra_bddImagePrintTree_rec( pTree->pRoot, 1 ); +} + +/**Function************************************************************* + + Synopsis [Prints the tree for quenstification scheduling.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Extra_bddImagePrintTree_rec( Extra_ImageNode_t * pNode, int Offset ) +{ + DdNode * Cube; + int i; + + Cube = pNode->bCube; + + if ( pNode->pNode1 == NULL ) + { + printf( "<%d> ", pNode->pPart->iPart ); + if ( Cube != NULL ) + { + ABC_PRB( pNode->dd, Cube ); + } + else + printf( "\n" ); + return; + } + + printf( "<*> " ); + if ( Cube != NULL ) + { + ABC_PRB( pNode->dd, Cube ); + } + else + printf( "\n" ); + + for ( i = 0; i < Offset; i++ ) + printf( " " ); + Extra_bddImagePrintTree_rec( pNode->pNode1, Offset + 1 ); + + for ( i = 0; i < Offset; i++ ) + printf( " " ); + Extra_bddImagePrintTree_rec( pNode->pNode2, Offset + 1 ); +} + + + + + +struct Extra_ImageTree2_t_ +{ + DdManager * dd; + DdNode * bRel; + DdNode * bCube; + DdNode * bImage; +}; + +/**Function************************************************************* + + Synopsis [Starts the monolithic image computation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Extra_ImageTree2_t * Extra_bddImageStart2( + DdManager * dd, DdNode * bCare, + int nParts, DdNode ** pbParts, + int nVars, DdNode ** pbVars, int fVerbose ) +{ + Extra_ImageTree2_t * pTree; + DdNode * bCubeAll, * bCubeNot, * bTemp; + int i; + + pTree = ABC_ALLOC( Extra_ImageTree2_t, 1 ); + pTree->dd = dd; + pTree->bImage = NULL; + + bCubeAll = Extra_bddComputeCube( dd, dd->vars, dd->size ); Cudd_Ref( bCubeAll ); + bCubeNot = Extra_bddComputeCube( dd, pbVars, nVars ); Cudd_Ref( bCubeNot ); + pTree->bCube = Cudd_bddExistAbstract( dd, bCubeAll, bCubeNot ); Cudd_Ref( pTree->bCube ); + Cudd_RecursiveDeref( dd, bCubeAll ); + Cudd_RecursiveDeref( dd, bCubeNot ); + + // derive the monolithic relation + pTree->bRel = b1; Cudd_Ref( pTree->bRel ); + for ( i = 0; i < nParts; i++ ) + { + pTree->bRel = Cudd_bddAnd( dd, bTemp = pTree->bRel, pbParts[i] ); Cudd_Ref( pTree->bRel ); + Cudd_RecursiveDeref( dd, bTemp ); + } + Extra_bddImageCompute2( pTree, bCare ); + return pTree; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Extra_bddImageCompute2( Extra_ImageTree2_t * pTree, DdNode * bCare ) +{ + if ( pTree->bImage ) + Cudd_RecursiveDeref( pTree->dd, pTree->bImage ); + pTree->bImage = Cudd_bddAndAbstract( pTree->dd, pTree->bRel, bCare, pTree->bCube ); + Cudd_Ref( pTree->bImage ); + return pTree->bImage; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Extra_bddImageTreeDelete2( Extra_ImageTree2_t * pTree ) +{ + if ( pTree->bRel ) + Cudd_RecursiveDeref( pTree->dd, pTree->bRel ); + if ( pTree->bCube ) + Cudd_RecursiveDeref( pTree->dd, pTree->bCube ); + if ( pTree->bImage ) + Cudd_RecursiveDeref( pTree->dd, pTree->bImage ); + ABC_FREE( pTree ); +} + +/**Function************************************************************* + + Synopsis [Returns the previously computed image.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Extra_bddImageRead2( Extra_ImageTree2_t * pTree ) +{ + return pTree->bImage; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/bdd/extrab/extraBddKmap.c b/src/bdd/extrab/extraBddKmap.c new file mode 100644 index 00000000..aa5efe75 --- /dev/null +++ b/src/bdd/extrab/extraBddKmap.c @@ -0,0 +1,876 @@ +/**CFile**************************************************************** + + FileName [extraBddKmap.c] + + PackageName [extra] + + Synopsis [Visualizing the K-map.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 2.0. Started - September 1, 2003.] + + Revision [$Id: extraBddKmap.c,v 1.0 2003/05/21 18:03:50 alanmi Exp $] + +***********************************************************************/ + +/// K-map visualization using pseudo graphics /// +/// Version 1.0. Started - August 20, 2000 /// +/// Version 2.0. Added to EXTRA - July 17, 2001 /// + +#include "extraBdd.h" + +#ifdef WIN32 +#include +#endif + +ABC_NAMESPACE_IMPL_START + + +/*---------------------------------------------------------------------------*/ +/* Constant declarations */ +/*---------------------------------------------------------------------------*/ + +// the maximum number of variables in the Karnaugh Map +#define MAXVARS 20 + +/* +// single line +#define SINGLE_VERTICAL (char)179 +#define SINGLE_HORIZONTAL (char)196 +#define SINGLE_TOP_LEFT (char)218 +#define SINGLE_TOP_RIGHT (char)191 +#define SINGLE_BOT_LEFT (char)192 +#define SINGLE_BOT_RIGHT (char)217 + +// double line +#define DOUBLE_VERTICAL (char)186 +#define DOUBLE_HORIZONTAL (char)205 +#define DOUBLE_TOP_LEFT (char)201 +#define DOUBLE_TOP_RIGHT (char)187 +#define DOUBLE_BOT_LEFT (char)200 +#define DOUBLE_BOT_RIGHT (char)188 + +// line intersections +#define SINGLES_CROSS (char)197 +#define DOUBLES_CROSS (char)206 +#define S_HOR_CROSS_D_VER (char)215 +#define S_VER_CROSS_D_HOR (char)216 + +// single line joining +#define S_JOINS_S_VER_LEFT (char)180 +#define S_JOINS_S_VER_RIGHT (char)195 +#define S_JOINS_S_HOR_TOP (char)193 +#define S_JOINS_S_HOR_BOT (char)194 + +// double line joining +#define D_JOINS_D_VER_LEFT (char)185 +#define D_JOINS_D_VER_RIGHT (char)204 +#define D_JOINS_D_HOR_TOP (char)202 +#define D_JOINS_D_HOR_BOT (char)203 + +// single line joining double line +#define S_JOINS_D_VER_LEFT (char)182 +#define S_JOINS_D_VER_RIGHT (char)199 +#define S_JOINS_D_HOR_TOP (char)207 +#define S_JOINS_D_HOR_BOT (char)209 +*/ + +// single line +#define SINGLE_VERTICAL (char)'|' +#define SINGLE_HORIZONTAL (char)'-' +#define SINGLE_TOP_LEFT (char)'+' +#define SINGLE_TOP_RIGHT (char)'+' +#define SINGLE_BOT_LEFT (char)'+' +#define SINGLE_BOT_RIGHT (char)'+' + +// double line +#define DOUBLE_VERTICAL (char)'|' +#define DOUBLE_HORIZONTAL (char)'-' +#define DOUBLE_TOP_LEFT (char)'+' +#define DOUBLE_TOP_RIGHT (char)'+' +#define DOUBLE_BOT_LEFT (char)'+' +#define DOUBLE_BOT_RIGHT (char)'+' + +// line intersections +#define SINGLES_CROSS (char)'+' +#define DOUBLES_CROSS (char)'+' +#define S_HOR_CROSS_D_VER (char)'+' +#define S_VER_CROSS_D_HOR (char)'+' + +// single line joining +#define S_JOINS_S_VER_LEFT (char)'+' +#define S_JOINS_S_VER_RIGHT (char)'+' +#define S_JOINS_S_HOR_TOP (char)'+' +#define S_JOINS_S_HOR_BOT (char)'+' + +// double line joining +#define D_JOINS_D_VER_LEFT (char)'+' +#define D_JOINS_D_VER_RIGHT (char)'+' +#define D_JOINS_D_HOR_TOP (char)'+' +#define D_JOINS_D_HOR_BOT (char)'+' + +// single line joining double line +#define S_JOINS_D_VER_LEFT (char)'+' +#define S_JOINS_D_VER_RIGHT (char)'+' +#define S_JOINS_D_HOR_TOP (char)'+' +#define S_JOINS_D_HOR_BOT (char)'+' + + +// other symbols +#define UNDERSCORE (char)95 +//#define SYMBOL_ZERO (char)248 // degree sign +//#define SYMBOL_ZERO (char)'o' +#ifdef WIN32 +#define SYMBOL_ZERO (char)'0' +#else +#define SYMBOL_ZERO (char)' ' +#endif +#define SYMBOL_ONE (char)'1' +#define SYMBOL_DC (char)'-' +#define SYMBOL_OVERLAP (char)'?' + +// full cells and half cells +#define CELL_FREE (char)32 +#define CELL_FULL (char)219 +#define HALF_UPPER (char)223 +#define HALF_LOWER (char)220 +#define HALF_LEFT (char)221 +#define HALF_RIGHT (char)222 + + +/*---------------------------------------------------------------------------*/ +/* Structure declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Type declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Variable declarations */ +/*---------------------------------------------------------------------------*/ + +// the array of BDD variables used internally +static DdNode * s_XVars[MAXVARS]; + +// flag which determines where the horizontal variable names are printed +static int fHorizontalVarNamesPrintedAbove = 1; + +/*---------------------------------------------------------------------------*/ +/* Macro declarations */ +/*---------------------------------------------------------------------------*/ + + +/**AutomaticStart*************************************************************/ + +/*---------------------------------------------------------------------------*/ +/* Static function prototypes */ +/*---------------------------------------------------------------------------*/ + +// Oleg's way of generating the gray code +static int GrayCode( int BinCode ); +static int BinCode ( int GrayCode ); + +/**AutomaticEnd***************************************************************/ + + +/*---------------------------------------------------------------------------*/ +/* Definition of exported functions */ +/*---------------------------------------------------------------------------*/ + + +/**Function******************************************************************** + + Synopsis [Prints the K-map of the function.] + + Description [If the pointer to the array of variables XVars is NULL, + fSuppType determines how the support will be determined. + fSuppType == 0 -- takes the first nVars of the manager + fSuppType == 1 -- takes the topmost nVars of the manager + fSuppType == 2 -- determines support from the on-set and the offset + ] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +void Extra_PrintKMap( + FILE * Output, /* the output stream */ + DdManager * dd, + DdNode * OnSet, + DdNode * OffSet, + int nVars, + DdNode ** XVars, + int fSuppType, /* the flag which determines how support is computed */ + char ** pVarNames ) +{ + int fPrintTruth = 1; + int d, p, n, s, v, h, w; + int nVarsVer; + int nVarsHor; + int nCellsVer; + int nCellsHor; + int nSkipSpaces; + + // make sure that on-set and off-set do not overlap + if ( !Cudd_bddLeq( dd, OnSet, Cudd_Not(OffSet) ) ) + { + fprintf( Output, "PrintKMap(): The on-set and the off-set overlap\n" ); + return; + } + if ( nVars == 0 ) + { printf( "Function is constant %d.\n", !Cudd_IsComplement(OnSet) ); return; } + + // print truth table for debugging + if ( fPrintTruth ) + { + DdNode * bCube, * bPart; + printf( "Truth table: " ); + if ( nVars == 0 ) + printf( "Constant" ); + else if ( nVars == 1 ) + printf( "1-var function" ); + else + { +// printf( "0x" ); + for ( d = (1<<(nVars-2)) - 1; d >= 0; d-- ) + { + int Value = 0; + for ( s = 0; s < 4; s++ ) + { + bCube = Extra_bddBitsToCube( dd, 4*d+s, nVars, dd->vars, 0 ); Cudd_Ref( bCube ); + bPart = Cudd_Cofactor( dd, OnSet, bCube ); Cudd_Ref( bPart ); + Value |= ((int)(bPart == b1) << s); + Cudd_RecursiveDeref( dd, bPart ); + Cudd_RecursiveDeref( dd, bCube ); + } + if ( Value < 10 ) + fprintf( stdout, "%d", Value ); + else + fprintf( stdout, "%c", 'a' + Value-10 ); + } + } + printf( "\n" ); + } + + +/* + if ( OnSet == b1 ) + { + fprintf( Output, "PrintKMap(): Constant 1\n" ); + return; + } + if ( OffSet == b1 ) + { + fprintf( Output, "PrintKMap(): Constant 0\n" ); + return; + } +*/ + if ( nVars < 0 || nVars > MAXVARS ) + { + fprintf( Output, "PrintKMap(): The number of variables is less than zero or more than %d\n", MAXVARS ); + return; + } + + // determine the support if it is not given + if ( XVars == NULL ) + { + if ( fSuppType == 0 ) + { // assume that the support includes the first nVars of the manager + assert( nVars ); + for ( v = 0; v < nVars; v++ ) + s_XVars[v] = Cudd_bddIthVar( dd, v ); + } + else if ( fSuppType == 1 ) + { // assume that the support includes the topmost nVars of the manager + assert( nVars ); + for ( v = 0; v < nVars; v++ ) + s_XVars[v] = Cudd_bddIthVar( dd, dd->invperm[v] ); + } + else // determine the support + { + DdNode * SuppOn, * SuppOff, * Supp; + int cVars = 0; + DdNode * TempSupp; + + // determine support + SuppOn = Cudd_Support( dd, OnSet ); Cudd_Ref( SuppOn ); + SuppOff = Cudd_Support( dd, OffSet ); Cudd_Ref( SuppOff ); + Supp = Cudd_bddAnd( dd, SuppOn, SuppOff ); Cudd_Ref( Supp ); + Cudd_RecursiveDeref( dd, SuppOn ); + Cudd_RecursiveDeref( dd, SuppOff ); + + nVars = Cudd_SupportSize( dd, Supp ); + if ( nVars > MAXVARS ) + { + fprintf( Output, "PrintKMap(): The number of variables is more than %d\n", MAXVARS ); + Cudd_RecursiveDeref( dd, Supp ); + return; + } + + // assign variables + for ( TempSupp = Supp; TempSupp != dd->one; TempSupp = Cudd_T(TempSupp), cVars++ ) + s_XVars[cVars] = Cudd_bddIthVar( dd, TempSupp->index ); + + Cudd_RecursiveDeref( dd, TempSupp ); + } + } + else + { + // copy variables + assert( XVars ); + for ( v = 0; v < nVars; v++ ) + s_XVars[v] = XVars[v]; + } + + //////////////////////////////////////////////////////////////////// + // determine the Karnaugh map parameters + nVarsVer = nVars/2; + nVarsHor = nVars - nVarsVer; + + nCellsVer = (1< MAXVARS ) + { + fprintf( Output, "PrintKMap(): The number of variables is less than zero or more than %d\n", MAXVARS ); + return; + } + + + //////////////////////////////////////////////////////////////////// + // determine the Karnaugh map parameters + nVarsVer = nXVars; + nVarsHor = nYVars; + nCellsVer = (1<> 1 ); +} + +/**Function******************************************************************** + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int BinCode ( int GrayCode ) +{ + int bc = GrayCode; + while( GrayCode >>= 1 ) bc ^= GrayCode; + return bc; +} + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/bdd/extrab/extraBddMisc.c b/src/bdd/extrab/extraBddMisc.c new file mode 100644 index 00000000..a2ba4036 --- /dev/null +++ b/src/bdd/extrab/extraBddMisc.c @@ -0,0 +1,2342 @@ +/**CFile**************************************************************** + + FileName [extraBddMisc.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [extra] + + Synopsis [DD-based utilities.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: extraBddMisc.c,v 1.4 2005/10/04 00:19:54 alanmi Exp $] + +***********************************************************************/ + +#include "extraBdd.h" + +ABC_NAMESPACE_IMPL_START + + +/*---------------------------------------------------------------------------*/ +/* Constant declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Stucture declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Type declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Variable declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Macro declarations */ +/*---------------------------------------------------------------------------*/ + + +/**AutomaticStart*************************************************************/ + +/*---------------------------------------------------------------------------*/ +/* Static function prototypes */ +/*---------------------------------------------------------------------------*/ + +// file "extraDdTransfer.c" +static DdNode * extraTransferPermuteRecur( DdManager * ddS, DdManager * ddD, DdNode * f, st__table * table, int * Permute ); +static DdNode * extraTransferPermute( DdManager * ddS, DdManager * ddD, DdNode * f, int * Permute ); +static DdNode * cuddBddPermuteRecur ARGS( ( DdManager * manager, DdHashTable * table, DdNode * node, int *permut ) ); + +static DdNode * extraBddAndPermute( DdHashTable * table, DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode * bG, int * pPermute ); + +// file "cuddUtils.c" +static void ddSupportStep(DdNode *f, int *support); +static void ddClearFlag(DdNode *f); + +static DdNode* extraZddPrimes( DdManager *dd, DdNode* F ); + +/**AutomaticEnd***************************************************************/ + +/*---------------------------------------------------------------------------*/ +/* Definition of exported functions */ +/*---------------------------------------------------------------------------*/ + +/**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_TransferPermute( DdManager * ddSource, DdManager * ddDestination, DdNode * f, int * Permute ) +{ + DdNode * bRes; + do + { + ddDestination->reordered = 0; + bRes = extraTransferPermute( ddSource, ddDestination, f, Permute ); + } + while ( ddDestination->reordered == 1 ); + return ( bRes ); + +} /* end of Extra_TransferPermute */ + +/**Function******************************************************************** + + Synopsis [Transfers the BDD from one manager into another level by level.] + + Description [Transfers the BDD from one manager into another while + preserving the correspondence between variables level by level.] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +DdNode * Extra_TransferLevelByLevel( DdManager * ddSource, DdManager * ddDestination, DdNode * f ) +{ + DdNode * bRes; + int * pPermute; + int nMin, nMax, i; + + nMin = ddMin(ddSource->size, ddDestination->size); + nMax = ddMax(ddSource->size, ddDestination->size); + pPermute = ABC_ALLOC( int, nMax ); + // set up the variable permutation + for ( i = 0; i < nMin; i++ ) + pPermute[ ddSource->invperm[i] ] = ddDestination->invperm[i]; + if ( ddSource->size > ddDestination->size ) + { + for ( ; i < nMax; i++ ) + pPermute[ ddSource->invperm[i] ] = -1; + } + bRes = Extra_TransferPermute( ddSource, ddDestination, f, pPermute ); + ABC_FREE( pPermute ); + return bRes; +} + +/**Function******************************************************************** + + Synopsis [Remaps the function to depend on the topmost variables on the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * Extra_bddRemapUp( + DdManager * dd, + DdNode * bF ) +{ + int * pPermute; + DdNode * bSupp, * bTemp, * bRes; + int Counter; + + pPermute = ABC_ALLOC( int, dd->size ); + + // get support + bSupp = Cudd_Support( dd, bF ); Cudd_Ref( bSupp ); + + // create the variable map + // to remap the DD into the upper part of the manager + Counter = 0; + for ( bTemp = bSupp; bTemp != dd->one; bTemp = cuddT(bTemp) ) + pPermute[bTemp->index] = dd->invperm[Counter++]; + + // transfer the BDD and remap it + bRes = Cudd_bddPermute( dd, bF, pPermute ); Cudd_Ref( bRes ); + + // remove support + Cudd_RecursiveDeref( dd, bSupp ); + + // return + Cudd_Deref( bRes ); + ABC_FREE( pPermute ); + return bRes; +} + +/**Function******************************************************************** + + Synopsis [Moves the BDD by the given number of variables up or down.] + + Description [] + + SideEffects [] + + SeeAlso [Extra_bddShift] + +******************************************************************************/ +DdNode * Extra_bddMove( + DdManager * dd, /* the DD manager */ + DdNode * bF, + int nVars) +{ + DdNode * res; + DdNode * bVars; + if ( nVars == 0 ) + return bF; + if ( Cudd_IsConstant(bF) ) + return bF; + assert( nVars <= dd->size ); + if ( nVars > 0 ) + bVars = dd->vars[nVars]; + else + bVars = Cudd_Not(dd->vars[-nVars]); + + do { + dd->reordered = 0; + res = extraBddMove( dd, bF, bVars ); + } while (dd->reordered == 1); + return(res); + +} /* end of Extra_bddMove */ + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Extra_StopManager( DdManager * dd ) +{ + int RetValue; + // check for remaining references in the package + RetValue = Cudd_CheckZeroRef( dd ); + if ( RetValue > 10 ) +// if ( RetValue ) + printf( "\nThe number of referenced nodes = %d\n\n", RetValue ); +// Cudd_PrintInfo( dd, stdout ); + Cudd_Quit( dd ); +} + +/**Function******************************************************************** + + Synopsis [Outputs the BDD in a readable format.] + + Description [] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +void Extra_bddPrint( DdManager * dd, DdNode * F ) +{ + DdGen * Gen; + int * Cube; + CUDD_VALUE_TYPE Value; + int nVars = dd->size; + int fFirstCube = 1; + int i; + + if ( F == NULL ) + { + printf("NULL"); + return; + } + if ( F == b0 ) + { + printf("Constant 0"); + return; + } + if ( F == b1 ) + { + printf("Constant 1"); + return; + } + + Cudd_ForeachCube( dd, F, Gen, Cube, Value ) + { + if ( fFirstCube ) + fFirstCube = 0; + else +// Output << " + "; + printf( " + " ); + + for ( i = 0; i < nVars; i++ ) + if ( Cube[i] == 0 ) + printf( "[%d]'", i ); +// printf( "%c'", (char)('a'+i) ); + else if ( Cube[i] == 1 ) + printf( "[%d]", i ); +// printf( "%c", (char)('a'+i) ); + } + +// printf("\n"); +} + +/**Function******************************************************************** + + Synopsis [Outputs the BDD in a readable format.] + + Description [] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +void Extra_bddPrintSupport( DdManager * dd, DdNode * F ) +{ + DdNode * bSupp; + bSupp = Cudd_Support( dd, F ); Cudd_Ref( bSupp ); + Extra_bddPrint( dd, bSupp ); + Cudd_RecursiveDeref( dd, bSupp ); +} + +/**Function******************************************************************** + + Synopsis [Returns the size of the support.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Extra_bddSuppSize( DdManager * dd, DdNode * bSupp ) +{ + int Counter = 0; + while ( bSupp != b1 ) + { + assert( !Cudd_IsComplement(bSupp) ); + assert( cuddE(bSupp) == b0 ); + + bSupp = cuddT(bSupp); + Counter++; + } + return Counter; +} + +/**Function******************************************************************** + + Synopsis [Returns 1 if the support contains the given BDD variable.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Extra_bddSuppContainVar( DdManager * dd, DdNode * bS, DdNode * bVar ) +{ + for( ; bS != b1; bS = cuddT(bS) ) + if ( bS->index == bVar->index ) + return 1; + return 0; +} + +/**Function******************************************************************** + + Synopsis [Returns 1 if two supports represented as BDD cubes are overlapping.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Extra_bddSuppOverlapping( DdManager * dd, DdNode * S1, DdNode * S2 ) +{ + while ( S1->index != CUDD_CONST_INDEX && S2->index != CUDD_CONST_INDEX ) + { + // if the top vars are the same, they intersect + if ( S1->index == S2->index ) + return 1; + // if the top vars are different, skip the one, which is higher + if ( dd->perm[S1->index] < dd->perm[S2->index] ) + S1 = cuddT(S1); + else + S2 = cuddT(S2); + } + return 0; +} + +/**Function******************************************************************** + + Synopsis [Returns the number of different vars in two supports.] + + Description [Counts the number of variables that appear in one support and + does not appear in other support. If the number exceeds DiffMax, returns DiffMax.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Extra_bddSuppDifferentVars( DdManager * dd, DdNode * S1, DdNode * S2, int DiffMax ) +{ + int Result = 0; + while ( S1->index != CUDD_CONST_INDEX && S2->index != CUDD_CONST_INDEX ) + { + // if the top vars are the same, this var is the same + if ( S1->index == S2->index ) + { + S1 = cuddT(S1); + S2 = cuddT(S2); + continue; + } + // the top var is different + Result++; + + if ( Result >= DiffMax ) + return DiffMax; + + // if the top vars are different, skip the one, which is higher + if ( dd->perm[S1->index] < dd->perm[S2->index] ) + S1 = cuddT(S1); + else + S2 = cuddT(S2); + } + + // consider the remaining variables + if ( S1->index != CUDD_CONST_INDEX ) + Result += Extra_bddSuppSize(dd,S1); + else if ( S2->index != CUDD_CONST_INDEX ) + Result += Extra_bddSuppSize(dd,S2); + + if ( Result >= DiffMax ) + return DiffMax; + return Result; +} + + +/**Function******************************************************************** + + Synopsis [Checks the support containment.] + + Description [This function returns 1 if one support is contained in another. + In this case, bLarge (bSmall) is assigned to point to the larger (smaller) support. + If the supports are identical, return 0 and does not assign the supports!] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Extra_bddSuppCheckContainment( DdManager * dd, DdNode * bL, DdNode * bH, DdNode ** bLarge, DdNode ** bSmall ) +{ + DdNode * bSL = bL; + DdNode * bSH = bH; + int fLcontainsH = 1; + int fHcontainsL = 1; + int TopVar; + + if ( bSL == bSH ) + return 0; + + while ( bSL != b1 || bSH != b1 ) + { + if ( bSL == b1 ) + { // Low component has no vars; High components has some vars + fLcontainsH = 0; + if ( fHcontainsL == 0 ) + return 0; + else + break; + } + + if ( bSH == b1 ) + { // similarly + fHcontainsL = 0; + if ( fLcontainsH == 0 ) + return 0; + else + break; + } + + // determine the topmost var of the supports by comparing their levels + if ( dd->perm[bSL->index] < dd->perm[bSH->index] ) + TopVar = bSL->index; + else + TopVar = bSH->index; + + if ( TopVar == bSL->index && TopVar == bSH->index ) + { // they are on the same level + // it does not tell us anything about their containment + // skip this var + bSL = cuddT(bSL); + bSH = cuddT(bSH); + } + else if ( TopVar == bSL->index ) // and TopVar != bSH->index + { // Low components is higher and contains more vars + // it is not possible that High component contains Low + fHcontainsL = 0; + // skip this var + bSL = cuddT(bSL); + } + else // if ( TopVar == bSH->index ) // and TopVar != bSL->index + { // similarly + fLcontainsH = 0; + // skip this var + bSH = cuddT(bSH); + } + + // check the stopping condition + if ( !fHcontainsL && !fLcontainsH ) + return 0; + } + // only one of them can be true at the same time + assert( !fHcontainsL || !fLcontainsH ); + if ( fHcontainsL ) + { + *bLarge = bH; + *bSmall = bL; + } + else // fLcontainsH + { + *bLarge = bL; + *bSmall = bH; + } + return 1; +} + + +/**Function******************************************************************** + + Synopsis [Finds variables on which the DD depends and returns them as am array.] + + Description [Finds the variables on which the DD depends. Returns an array + with entries set to 1 for those variables that belong to the support; + NULL otherwise. The array is allocated by the user and should have at least + as many entries as the maximum number of variables in BDD and ZDD parts of + the manager.] + + SideEffects [None] + + SeeAlso [Cudd_Support Cudd_VectorSupport Cudd_ClassifySupport] + +******************************************************************************/ +int * +Extra_SupportArray( + DdManager * dd, /* manager */ + DdNode * f, /* DD whose support is sought */ + int * support ) /* array allocated by the user */ +{ + int i, size; + + /* Initialize support array for ddSupportStep. */ + size = ddMax(dd->size, dd->sizeZ); + for (i = 0; i < size; i++) + support[i] = 0; + + /* Compute support and clean up markers. */ + ddSupportStep(Cudd_Regular(f),support); + ddClearFlag(Cudd_Regular(f)); + + return(support); + +} /* end of Extra_SupportArray */ + +/**Function******************************************************************** + + Synopsis [Finds the variables on which a set of DDs depends.] + + Description [Finds the variables on which a set of DDs depends. + The set must contain either BDDs and ADDs, or ZDDs. + Returns a BDD consisting of the product of the variables if + successful; NULL otherwise.] + + SideEffects [None] + + SeeAlso [Cudd_Support Cudd_ClassifySupport] + +******************************************************************************/ +int * +Extra_VectorSupportArray( + DdManager * dd, /* manager */ + DdNode ** F, /* array of DDs whose support is sought */ + int n, /* size of the array */ + int * support ) /* array allocated by the user */ +{ + int i, size; + + /* Allocate and initialize support array for ddSupportStep. */ + size = ddMax( dd->size, dd->sizeZ ); + for ( i = 0; i < size; i++ ) + support[i] = 0; + + /* Compute support and clean up markers. */ + for ( i = 0; i < n; i++ ) + ddSupportStep( Cudd_Regular(F[i]), support ); + for ( i = 0; i < n; i++ ) + ddClearFlag( Cudd_Regular(F[i]) ); + + return support; +} + +/**Function******************************************************************** + + Synopsis [Find any cube belonging to the on-set of the function.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * Extra_bddFindOneCube( DdManager * dd, DdNode * bF ) +{ + char * s_Temp; + DdNode * bCube, * bTemp; + int v; + + // get the vector of variables in the cube + s_Temp = ABC_ALLOC( char, dd->size ); + Cudd_bddPickOneCube( dd, bF, s_Temp ); + + // start the cube + bCube = b1; Cudd_Ref( bCube ); + for ( v = 0; v < dd->size; v++ ) + if ( s_Temp[v] == 0 ) + { +// Cube &= !s_XVars[v]; + bCube = Cudd_bddAnd( dd, bTemp = bCube, Cudd_Not(dd->vars[v]) ); Cudd_Ref( bCube ); + Cudd_RecursiveDeref( dd, bTemp ); + } + else if ( s_Temp[v] == 1 ) + { +// Cube &= s_XVars[v]; + bCube = Cudd_bddAnd( dd, bTemp = bCube, dd->vars[v] ); Cudd_Ref( bCube ); + Cudd_RecursiveDeref( dd, bTemp ); + } + Cudd_Deref(bCube); + ABC_FREE( s_Temp ); + return bCube; +} + +/**Function******************************************************************** + + Synopsis [Returns one cube contained in the given BDD.] + + Description [This function returns the cube with the smallest + bits-to-integer value.] + + SideEffects [] + +******************************************************************************/ +DdNode * Extra_bddGetOneCube( DdManager * dd, DdNode * bFunc ) +{ + DdNode * bFuncR, * bFunc0, * bFunc1; + DdNode * bRes0, * bRes1, * bRes; + + bFuncR = Cudd_Regular(bFunc); + if ( cuddIsConstant(bFuncR) ) + return bFunc; + + // cofactor + if ( Cudd_IsComplement(bFunc) ) + { + bFunc0 = Cudd_Not( cuddE(bFuncR) ); + bFunc1 = Cudd_Not( cuddT(bFuncR) ); + } + else + { + bFunc0 = cuddE(bFuncR); + bFunc1 = cuddT(bFuncR); + } + + // try to find the cube with the negative literal + bRes0 = Extra_bddGetOneCube( dd, bFunc0 ); Cudd_Ref( bRes0 ); + + if ( bRes0 != b0 ) + { + bRes = Cudd_bddAnd( dd, bRes0, Cudd_Not(dd->vars[bFuncR->index]) ); Cudd_Ref( bRes ); + Cudd_RecursiveDeref( dd, bRes0 ); + } + else + { + Cudd_RecursiveDeref( dd, bRes0 ); + // try to find the cube with the positive literal + bRes1 = Extra_bddGetOneCube( dd, bFunc1 ); Cudd_Ref( bRes1 ); + assert( bRes1 != b0 ); + bRes = Cudd_bddAnd( dd, bRes1, dd->vars[bFuncR->index] ); Cudd_Ref( bRes ); + Cudd_RecursiveDeref( dd, bRes1 ); + } + + Cudd_Deref( bRes ); + return bRes; +} + +/**Function******************************************************************** + + Synopsis [Performs the reordering-sensitive step of Extra_bddMove().] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * Extra_bddComputeRangeCube( DdManager * dd, int iStart, int iStop ) +{ + DdNode * bTemp, * bProd; + int i; + assert( iStart <= iStop ); + assert( iStart >= 0 && iStart <= dd->size ); + assert( iStop >= 0 && iStop <= dd->size ); + bProd = b1; Cudd_Ref( bProd ); + for ( i = iStart; i < iStop; i++ ) + { + bProd = Cudd_bddAnd( dd, bTemp = bProd, dd->vars[i] ); Cudd_Ref( bProd ); + Cudd_RecursiveDeref( dd, bTemp ); + } + Cudd_Deref( bProd ); + return bProd; +} + +/**Function******************************************************************** + + Synopsis [Computes the cube of BDD variables corresponding to bits it the bit-code] + + Description [Returns a bdd composed of elementary bdds found in array BddVars[] such + that the bdd vars encode the number Value of bit length CodeWidth (if fMsbFirst is 1, + the most significant bit is encoded with the first bdd variable). If the variables + BddVars are not specified, takes the first CodeWidth variables of the manager] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * Extra_bddBitsToCube( DdManager * dd, int Code, int CodeWidth, DdNode ** pbVars, int fMsbFirst ) +{ + int z; + DdNode * bTemp, * bVar, * bVarBdd, * bResult; + + bResult = b1; Cudd_Ref( bResult ); + for ( z = 0; z < CodeWidth; z++ ) + { + bVarBdd = (pbVars)? pbVars[z]: dd->vars[z]; + if ( fMsbFirst ) + bVar = Cudd_NotCond( bVarBdd, (Code & (1 << (CodeWidth-1-z)))==0 ); + else + bVar = Cudd_NotCond( bVarBdd, (Code & (1 << (z)))==0 ); + bResult = Cudd_bddAnd( dd, bTemp = bResult, bVar ); Cudd_Ref( bResult ); + Cudd_RecursiveDeref( dd, bTemp ); + } + Cudd_Deref( bResult ); + + return bResult; +} /* end of Extra_bddBitsToCube */ + +/**Function******************************************************************** + + Synopsis [Finds the support as a negative polarity cube.] + + Description [Finds the variables on which a DD depends. Returns a BDD + consisting of the product of the variables in the negative polarity + if successful; NULL otherwise.] + + SideEffects [None] + + SeeAlso [Cudd_VectorSupport Cudd_Support] + +******************************************************************************/ +DdNode * Extra_bddSupportNegativeCube( DdManager * dd, DdNode * f ) +{ + int *support; + DdNode *res, *tmp, *var; + int i, j; + int size; + + /* Allocate and initialize support array for ddSupportStep. */ + size = ddMax( dd->size, dd->sizeZ ); + support = ABC_ALLOC( int, size ); + if ( support == NULL ) + { + dd->errorCode = CUDD_MEMORY_OUT; + return ( NULL ); + } + for ( i = 0; i < size; i++ ) + { + support[i] = 0; + } + + /* Compute support and clean up markers. */ + ddSupportStep( Cudd_Regular( f ), support ); + ddClearFlag( Cudd_Regular( f ) ); + + /* Transform support from array to cube. */ + do + { + dd->reordered = 0; + res = DD_ONE( dd ); + cuddRef( res ); + for ( j = size - 1; j >= 0; j-- ) + { /* for each level bottom-up */ + i = ( j >= dd->size ) ? j : dd->invperm[j]; + if ( support[i] == 1 ) + { + var = cuddUniqueInter( dd, i, dd->one, Cudd_Not( dd->one ) ); + ////////////////////////////////////////////////////////////////// + var = Cudd_Not(var); + ////////////////////////////////////////////////////////////////// + cuddRef( var ); + tmp = cuddBddAndRecur( dd, res, var ); + if ( tmp == NULL ) + { + Cudd_RecursiveDeref( dd, res ); + Cudd_RecursiveDeref( dd, var ); + res = NULL; + break; + } + cuddRef( tmp ); + Cudd_RecursiveDeref( dd, res ); + Cudd_RecursiveDeref( dd, var ); + res = tmp; + } + } + } + while ( dd->reordered == 1 ); + + ABC_FREE( support ); + if ( res != NULL ) + cuddDeref( res ); + return ( res ); + +} /* end of Extra_SupportNeg */ + +/**Function******************************************************************** + + Synopsis [Returns 1 if the BDD is the BDD of elementary variable.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Extra_bddIsVar( DdNode * bFunc ) +{ + bFunc = Cudd_Regular( bFunc ); + if ( cuddIsConstant(bFunc) ) + return 0; + return cuddIsConstant( cuddT(bFunc) ) && cuddIsConstant( Cudd_Regular(cuddE(bFunc)) ); +} + +/**Function******************************************************************** + + Synopsis [Creates AND composed of the first nVars of the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * Extra_bddCreateAnd( DdManager * dd, int nVars ) +{ + DdNode * bFunc, * bTemp; + int i; + bFunc = Cudd_ReadOne(dd); Cudd_Ref( bFunc ); + for ( i = 0; i < nVars; i++ ) + { + bFunc = Cudd_bddAnd( dd, bTemp = bFunc, Cudd_bddIthVar(dd,i) ); Cudd_Ref( bFunc ); + Cudd_RecursiveDeref( dd, bTemp ); + } + Cudd_Deref( bFunc ); + return bFunc; +} + +/**Function******************************************************************** + + Synopsis [Creates OR composed of the first nVars of the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * Extra_bddCreateOr( DdManager * dd, int nVars ) +{ + DdNode * bFunc, * bTemp; + int i; + bFunc = Cudd_ReadLogicZero(dd); Cudd_Ref( bFunc ); + for ( i = 0; i < nVars; i++ ) + { + bFunc = Cudd_bddOr( dd, bTemp = bFunc, Cudd_bddIthVar(dd,i) ); Cudd_Ref( bFunc ); + Cudd_RecursiveDeref( dd, bTemp ); + } + Cudd_Deref( bFunc ); + return bFunc; +} + +/**Function******************************************************************** + + Synopsis [Creates EXOR composed of the first nVars of the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * Extra_bddCreateExor( DdManager * dd, int nVars ) +{ + DdNode * bFunc, * bTemp; + int i; + bFunc = Cudd_ReadLogicZero(dd); Cudd_Ref( bFunc ); + for ( i = 0; i < nVars; i++ ) + { + bFunc = Cudd_bddXor( dd, bTemp = bFunc, Cudd_bddIthVar(dd,i) ); Cudd_Ref( bFunc ); + Cudd_RecursiveDeref( dd, bTemp ); + } + Cudd_Deref( bFunc ); + return bFunc; +} + +/**Function******************************************************************** + + Synopsis [Computes the set of primes as a ZDD.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * Extra_zddPrimes( DdManager * dd, DdNode * F ) +{ + DdNode *res; + do { + dd->reordered = 0; + res = extraZddPrimes(dd, F); + if ( dd->reordered == 1 ) + printf("\nReordering in Extra_zddPrimes()\n"); + } while (dd->reordered == 1); + return(res); + +} /* end of Extra_zddPrimes */ + +/**Function******************************************************************** + + Synopsis [Permutes the variables of the array of BDDs.] + + Description [Given a permutation in array permut, creates a new BDD + with permuted variables. There should be an entry in array permut + for each variable in the manager. The i-th entry of permut holds the + index of the variable that is to substitute the i-th variable. + The DDs in the resulting array are already referenced.] + + SideEffects [None] + + SeeAlso [Cudd_addPermute Cudd_bddSwapVariables] + +******************************************************************************/ +void Extra_bddPermuteArray( DdManager * manager, DdNode ** bNodesIn, DdNode ** bNodesOut, int nNodes, int *permut ) +{ + DdHashTable *table; + int i, k; + do + { + manager->reordered = 0; + table = cuddHashTableInit( manager, 1, 2 ); + + /* permute the output functions one-by-one */ + for ( i = 0; i < nNodes; i++ ) + { + bNodesOut[i] = cuddBddPermuteRecur( manager, table, bNodesIn[i], permut ); + if ( bNodesOut[i] == NULL ) + { + /* deref the array of the already computed outputs */ + for ( k = 0; k < i; k++ ) + Cudd_RecursiveDeref( manager, bNodesOut[k] ); + break; + } + cuddRef( bNodesOut[i] ); + } + /* Dispose of local cache. */ + cuddHashTableQuit( table ); + } + while ( manager->reordered == 1 ); +} /* end of Extra_bddPermuteArray */ + + +/**Function******************************************************************** + + Synopsis [Computes the positive polarty cube composed of the first vars in the array.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * Extra_bddComputeCube( DdManager * dd, DdNode ** bXVars, int nVars ) +{ + DdNode * bRes; + DdNode * bTemp; + int i; + + bRes = b1; Cudd_Ref( bRes ); + for ( i = 0; i < nVars; i++ ) + { + bRes = Cudd_bddAnd( dd, bTemp = bRes, bXVars[i] ); Cudd_Ref( bRes ); + Cudd_RecursiveDeref( dd, bTemp ); + } + + Cudd_Deref( bRes ); + return bRes; +} + +/**Function******************************************************************** + + Synopsis [Changes the polarity of vars listed in the cube.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * Extra_bddChangePolarity( + DdManager * dd, /* the DD manager */ + DdNode * bFunc, + DdNode * bVars) +{ + DdNode *res; + do { + dd->reordered = 0; + res = extraBddChangePolarity( dd, bFunc, bVars ); + } while (dd->reordered == 1); + return(res); + +} /* end of Extra_bddChangePolarity */ + + +/**Function************************************************************* + + Synopsis [Checks if the given variable belongs to the cube.] + + Description [Return -1 if the var does not appear in the cube. + Otherwise, returns polarity (0 or 1) of the var in the cube.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Extra_bddVarIsInCube( DdNode * bCube, int iVar ) +{ + DdNode * bCube0, * bCube1; + while ( Cudd_Regular(bCube)->index != CUDD_CONST_INDEX ) + { + bCube0 = Cudd_NotCond( cuddE(Cudd_Regular(bCube)), Cudd_IsComplement(bCube) ); + bCube1 = Cudd_NotCond( cuddT(Cudd_Regular(bCube)), Cudd_IsComplement(bCube) ); + // make sure it is a cube + assert( (Cudd_IsComplement(bCube0) && Cudd_Regular(bCube0)->index == CUDD_CONST_INDEX) || // bCube0 == 0 + (Cudd_IsComplement(bCube1) && Cudd_Regular(bCube1)->index == CUDD_CONST_INDEX) ); // bCube1 == 0 + // quit if it is the last one + if ( Cudd_Regular(bCube)->index == iVar ) + return (int)(Cudd_IsComplement(bCube0) && Cudd_Regular(bCube0)->index == CUDD_CONST_INDEX); + // get the next cube + if ( (Cudd_IsComplement(bCube0) && Cudd_Regular(bCube0)->index == CUDD_CONST_INDEX) ) + bCube = bCube1; + else + bCube = bCube0; + } + return -1; +} + +/**Function************************************************************* + + Synopsis [Computes the AND of two BDD with different orders.] + + Description [Derives the result of Boolean AND of bF and bG in ddF. + The array pPermute gives the mapping of variables of ddG into that of ddF.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Extra_bddAndPermute( DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode * bG, int * pPermute ) +{ + DdHashTable * table; + DdNode * bRes; + do + { + ddF->reordered = 0; + table = cuddHashTableInit( ddF, 2, 256 ); + if (table == NULL) return NULL; + bRes = extraBddAndPermute( table, ddF, bF, ddG, bG, pPermute ); + if ( bRes ) cuddRef( bRes ); + cuddHashTableQuit( table ); + if ( bRes ) cuddDeref( bRes ); +//if ( ddF->reordered == 1 ) +//printf( "Reordering happened\n" ); + } + while ( ddF->reordered == 1 ); +//printf( "|F| =%6d |G| =%6d |H| =%6d |F|*|G| =%9d\n", +// Cudd_DagSize(bF), Cudd_DagSize(bG), Cudd_DagSize(bRes), +// Cudd_DagSize(bF) * Cudd_DagSize(bG) ); + return ( bRes ); +} + +/*---------------------------------------------------------------------------*/ +/* Definition of internal functions */ +/*---------------------------------------------------------------------------*/ + +/**Function******************************************************************** + + Synopsis [Performs the reordering-sensitive step of Extra_bddMove().] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * extraBddMove( + DdManager * dd, /* the DD manager */ + DdNode * bF, + DdNode * bDist) +{ + DdNode * bRes; + + if ( Cudd_IsConstant(bF) ) + return bF; + + if ( (bRes = cuddCacheLookup2(dd, extraBddMove, bF, bDist)) ) + return bRes; + else + { + DdNode * bRes0, * bRes1; + DdNode * bF0, * bF1; + DdNode * bFR = Cudd_Regular(bF); + int VarNew; + + if ( Cudd_IsComplement(bDist) ) + VarNew = bFR->index - Cudd_Not(bDist)->index; + else + VarNew = bFR->index + bDist->index; + assert( VarNew < dd->size ); + + // cofactor the functions + if ( bFR != bF ) // bFunc is complemented + { + bF0 = Cudd_Not( cuddE(bFR) ); + bF1 = Cudd_Not( cuddT(bFR) ); + } + else + { + bF0 = cuddE(bFR); + bF1 = cuddT(bFR); + } + + bRes0 = extraBddMove( dd, bF0, bDist ); + if ( bRes0 == NULL ) + return NULL; + cuddRef( bRes0 ); + + bRes1 = extraBddMove( dd, bF1, bDist ); + if ( bRes1 == NULL ) + { + Cudd_RecursiveDeref( dd, bRes0 ); + return NULL; + } + cuddRef( bRes1 ); + + /* only bRes0 and bRes1 are referenced at this point */ + bRes = cuddBddIteRecur( dd, dd->vars[VarNew], bRes1, bRes0 ); + if ( bRes == NULL ) + { + Cudd_RecursiveDeref( dd, bRes0 ); + Cudd_RecursiveDeref( dd, bRes1 ); + return NULL; + } + cuddRef( bRes ); + Cudd_RecursiveDeref( dd, bRes0 ); + Cudd_RecursiveDeref( dd, bRes1 ); + + /* insert the result into cache */ + cuddCacheInsert2( dd, extraBddMove, bF, bDist, bRes ); + cuddDeref( bRes ); + return bRes; + } +} /* end of extraBddMove */ + + +/**Function******************************************************************** + + Synopsis [Finds three cofactors of the cover w.r.t. to the topmost variable.] + + Description [Finds three cofactors of the cover w.r.t. to the topmost variable. + Does not check the cover for being a constant. Assumes that ZDD variables encoding + positive and negative polarities are adjacent in the variable order. Is different + from cuddZddGetCofactors3() in that it does not compute the cofactors w.r.t. the + given variable but takes the cofactors with respent to the topmost variable. + This function is more efficient when used in recursive procedures because it does + not require referencing of the resulting cofactors (compare cuddZddProduct() + and extraZddPrimeProduct()).] + + SideEffects [None] + + SeeAlso [cuddZddGetCofactors3] + +******************************************************************************/ +void +extraDecomposeCover( + DdManager* dd, /* the manager */ + DdNode* zC, /* the cover */ + DdNode** zC0, /* the pointer to the negative var cofactor */ + DdNode** zC1, /* the pointer to the positive var cofactor */ + DdNode** zC2 ) /* the pointer to the cofactor without var */ +{ + if ( (zC->index & 1) == 0 ) + { /* the top variable is present in positive polarity and maybe in negative */ + + DdNode *Temp = cuddE( zC ); + *zC1 = cuddT( zC ); + if ( cuddIZ(dd,Temp->index) == cuddIZ(dd,zC->index) + 1 ) + { /* Temp is not a terminal node + * top var is present in negative polarity */ + *zC2 = cuddE( Temp ); + *zC0 = cuddT( Temp ); + } + else + { /* top var is not present in negative polarity */ + *zC2 = Temp; + *zC0 = dd->zero; + } + } + else + { /* the top variable is present only in negative */ + *zC1 = dd->zero; + *zC2 = cuddE( zC ); + *zC0 = cuddT( zC ); + } +} /* extraDecomposeCover */ + + + +/**Function******************************************************************** + + Synopsis [Counts the total number of cubes in the ISOPs of the functions.] + + Description [Returns -1 if the number of cubes exceeds the limit.] + + SideEffects [None] + + SeeAlso [Extra_TransferPermute] + +******************************************************************************/ +static DdNode * extraBddCountCubes( DdManager * dd, DdNode * L, DdNode * U, st__table *table, int * pnCubes, int Limit ) +{ + DdNode *one = DD_ONE(dd); + DdNode *zero = Cudd_Not(one); + int v, top_l, top_u; + DdNode *Lsub0, *Usub0, *Lsub1, *Usub1, *Ld, *Ud; + DdNode *Lsuper0, *Usuper0, *Lsuper1, *Usuper1; + DdNode *Isub0, *Isub1, *Id; + DdNode *x; + DdNode *term0, *term1, *sum; + DdNode *Lv, *Uv, *Lnv, *Unv; + DdNode *r; + int index; + int Count0 = 0, Count1 = 0, Count2 = 0; + + statLine(dd); + if (L == zero) + { + *pnCubes = 0; + return(zero); + } + if (U == one) + { + *pnCubes = 1; + return(one); + } + + /* Check cache */ + r = cuddCacheLookup2(dd, cuddBddIsop, L, U); + if (r) + { + int nCubes = 0; + if ( st__lookup( table, (char *)r, (char **)&nCubes ) ) + *pnCubes = nCubes; + else assert( 0 ); + return r; + } + + top_l = dd->perm[Cudd_Regular(L)->index]; + top_u = dd->perm[Cudd_Regular(U)->index]; + v = ddMin(top_l, top_u); + + /* Compute cofactors */ + if (top_l == v) { + index = Cudd_Regular(L)->index; + Lv = Cudd_T(L); + Lnv = Cudd_E(L); + if (Cudd_IsComplement(L)) { + Lv = Cudd_Not(Lv); + Lnv = Cudd_Not(Lnv); + } + } + else { + index = Cudd_Regular(U)->index; + Lv = Lnv = L; + } + + if (top_u == v) { + Uv = Cudd_T(U); + Unv = Cudd_E(U); + if (Cudd_IsComplement(U)) { + Uv = Cudd_Not(Uv); + Unv = Cudd_Not(Unv); + } + } + else { + Uv = Unv = U; + } + + Lsub0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Uv)); + if (Lsub0 == NULL) + return(NULL); + Cudd_Ref(Lsub0); + Usub0 = Unv; + Lsub1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Unv)); + if (Lsub1 == NULL) { + Cudd_RecursiveDeref(dd, Lsub0); + return(NULL); + } + Cudd_Ref(Lsub1); + Usub1 = Uv; + + Isub0 = extraBddCountCubes(dd, Lsub0, Usub0, table, &Count0, Limit); + if (Isub0 == NULL) { + Cudd_RecursiveDeref(dd, Lsub0); + Cudd_RecursiveDeref(dd, Lsub1); + return(NULL); + } + Cudd_Ref(Isub0); + Isub1 = extraBddCountCubes(dd, Lsub1, Usub1, table, &Count1, Limit); + if (Isub1 == NULL) { + Cudd_RecursiveDeref(dd, Lsub0); + Cudd_RecursiveDeref(dd, Lsub1); + Cudd_RecursiveDeref(dd, Isub0); + return(NULL); + } + Cudd_Ref(Isub1); + Cudd_RecursiveDeref(dd, Lsub0); + Cudd_RecursiveDeref(dd, Lsub1); + + Lsuper0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Isub0)); + if (Lsuper0 == NULL) { + Cudd_RecursiveDeref(dd, Isub0); + Cudd_RecursiveDeref(dd, Isub1); + return(NULL); + } + Cudd_Ref(Lsuper0); + Lsuper1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Isub1)); + if (Lsuper1 == NULL) { + Cudd_RecursiveDeref(dd, Isub0); + Cudd_RecursiveDeref(dd, Isub1); + Cudd_RecursiveDeref(dd, Lsuper0); + return(NULL); + } + Cudd_Ref(Lsuper1); + Usuper0 = Unv; + Usuper1 = Uv; + + /* Ld = Lsuper0 + Lsuper1 */ + Ld = cuddBddAndRecur(dd, Cudd_Not(Lsuper0), Cudd_Not(Lsuper1)); + Ld = Cudd_NotCond(Ld, Ld != NULL); + if (Ld == NULL) { + Cudd_RecursiveDeref(dd, Isub0); + Cudd_RecursiveDeref(dd, Isub1); + Cudd_RecursiveDeref(dd, Lsuper0); + Cudd_RecursiveDeref(dd, Lsuper1); + return(NULL); + } + Cudd_Ref(Ld); + Ud = cuddBddAndRecur(dd, Usuper0, Usuper1); + if (Ud == NULL) { + Cudd_RecursiveDeref(dd, Isub0); + Cudd_RecursiveDeref(dd, Isub1); + Cudd_RecursiveDeref(dd, Lsuper0); + Cudd_RecursiveDeref(dd, Lsuper1); + Cudd_RecursiveDeref(dd, Ld); + return(NULL); + } + Cudd_Ref(Ud); + Cudd_RecursiveDeref(dd, Lsuper0); + Cudd_RecursiveDeref(dd, Lsuper1); + + Id = extraBddCountCubes(dd, Ld, Ud, table, &Count2, Limit); + if (Id == NULL) { + Cudd_RecursiveDeref(dd, Isub0); + Cudd_RecursiveDeref(dd, Isub1); + Cudd_RecursiveDeref(dd, Ld); + Cudd_RecursiveDeref(dd, Ud); + return(NULL); + } + Cudd_Ref(Id); + Cudd_RecursiveDeref(dd, Ld); + Cudd_RecursiveDeref(dd, Ud); + + x = cuddUniqueInter(dd, index, one, zero); + if (x == NULL) { + Cudd_RecursiveDeref(dd, Isub0); + Cudd_RecursiveDeref(dd, Isub1); + Cudd_RecursiveDeref(dd, Id); + return(NULL); + } + Cudd_Ref(x); + term0 = cuddBddAndRecur(dd, Cudd_Not(x), Isub0); + if (term0 == NULL) { + Cudd_RecursiveDeref(dd, Isub0); + Cudd_RecursiveDeref(dd, Isub1); + Cudd_RecursiveDeref(dd, Id); + Cudd_RecursiveDeref(dd, x); + return(NULL); + } + Cudd_Ref(term0); + Cudd_RecursiveDeref(dd, Isub0); + term1 = cuddBddAndRecur(dd, x, Isub1); + if (term1 == NULL) { + Cudd_RecursiveDeref(dd, Isub1); + Cudd_RecursiveDeref(dd, Id); + Cudd_RecursiveDeref(dd, x); + Cudd_RecursiveDeref(dd, term0); + return(NULL); + } + Cudd_Ref(term1); + Cudd_RecursiveDeref(dd, x); + Cudd_RecursiveDeref(dd, Isub1); + /* sum = term0 + term1 */ + sum = cuddBddAndRecur(dd, Cudd_Not(term0), Cudd_Not(term1)); + sum = Cudd_NotCond(sum, sum != NULL); + if (sum == NULL) { + Cudd_RecursiveDeref(dd, Id); + Cudd_RecursiveDeref(dd, term0); + Cudd_RecursiveDeref(dd, term1); + return(NULL); + } + Cudd_Ref(sum); + Cudd_RecursiveDeref(dd, term0); + Cudd_RecursiveDeref(dd, term1); + /* r = sum + Id */ + r = cuddBddAndRecur(dd, Cudd_Not(sum), Cudd_Not(Id)); + r = Cudd_NotCond(r, r != NULL); + if (r == NULL) { + Cudd_RecursiveDeref(dd, Id); + Cudd_RecursiveDeref(dd, sum); + return(NULL); + } + Cudd_Ref(r); + Cudd_RecursiveDeref(dd, sum); + Cudd_RecursiveDeref(dd, Id); + + cuddCacheInsert2(dd, cuddBddIsop, L, U, r); + *pnCubes = Count0 + Count1 + Count2; + if ( st__add_direct( table, (char *)r, (char *)(ABC_PTRINT_T)*pnCubes ) == st__OUT_OF_MEM ) + { + Cudd_RecursiveDeref( dd, r ); + return NULL; + } + if ( *pnCubes > Limit ) + { + Cudd_RecursiveDeref( dd, r ); + return NULL; + } + //printf( "%d ", *pnCubes ); + Cudd_Deref(r); + return r; +} +int Extra_bddCountCubes( DdManager * dd, DdNode ** pFuncs, int nFuncs, int fMode, int nLimit, int * pGuide ) +{ + DdNode * pF0, * pF1; + int i, Count, Count0, Count1, CounterAll = 0; + st__table *table = st__init_table( st__ptrcmp, st__ptrhash ); + unsigned int saveLimit = dd->maxLive; + dd->maxLive = dd->keys - dd->dead + 1000000; // limit on intermediate BDD nodes + for ( i = 0; i < nFuncs; i++ ) + { + if ( !pFuncs[i] ) + continue; + pF1 = pF0 = NULL; + Count0 = Count1 = nLimit; + if ( fMode == -1 || fMode == 1 ) // both or pos + pF1 = extraBddCountCubes( dd, pFuncs[i], pFuncs[i], table, &Count1, nLimit ); + pFuncs[i] = Cudd_Not( pFuncs[i] ); + if ( fMode == -1 || fMode == 0 ) // both or neg + pF0 = extraBddCountCubes( dd, pFuncs[i], pFuncs[i], table, &Count0, Count1 ); + pFuncs[i] = Cudd_Not( pFuncs[i] ); + if ( !pF1 && !pF0 ) + break; + if ( !pF0 ) pGuide[i] = 1, Count = Count1; // use pos + else if ( !pF1 ) pGuide[i] = 0, Count = Count0; // use neg + else if ( Count1 <= Count0 ) pGuide[i] = 1, Count = Count1; // use pos + else pGuide[i] = 0, Count = Count0; // use neg + CounterAll += Count; + //printf( "Output %5d has %5d cubes (%d) (%5d and %5d)\n", nOuts++, Count, pGuide[i], Count1, Count0 ); + } + dd->maxLive = saveLimit; + st__free_table( table ); + return i == nFuncs ? CounterAll : -1; +} /* end of Extra_bddCountCubes */ + +/*---------------------------------------------------------------------------*/ +/* 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 * extraTransferPermute( DdManager * ddS, DdManager * ddD, DdNode * f, int * Permute ) +{ + 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 = extraTransferPermuteRecur( ddS, ddD, f, table, Permute ); + 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 extraTransferPermute */ + + +/**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 [extraTransferPermute] + +******************************************************************************/ +static DdNode * +extraTransferPermuteRecur( + DdManager * ddS, + DdManager * ddD, + DdNode * f, + st__table * table, + int * Permute ) +{ + 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 ( ddS->TimeStop && Abc_Clock() > ddS->TimeStop ) + return NULL; + if ( ddD->TimeStop && Abc_Clock() > ddD->TimeStop ) + return NULL; + + /* Recursive step. */ + if ( Permute ) + index = Permute[f->index]; + else + index = f->index; + + ft = cuddT( f ); + fe = cuddE( f ); + + t = extraTransferPermuteRecur( ddS, ddD, ft, table, Permute ); + if ( t == NULL ) + { + return ( NULL ); + } + cuddRef( t ); + + e = extraTransferPermuteRecur( ddS, ddD, fe, table, Permute ); + 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 extraTransferPermuteRecur */ + +/**Function******************************************************************** + + Synopsis [Performs the recursive step of Cudd_Support.] + + Description [Performs the recursive step of Cudd_Support. Performs a + DFS from f. The support is accumulated in supp as a side effect. Uses + the LSB of the then pointer as visited flag.] + + SideEffects [None] + + SeeAlso [ddClearFlag] + +******************************************************************************/ +static void +ddSupportStep( + DdNode * f, + int * support) +{ + if (cuddIsConstant(f) || Cudd_IsComplement(f->next)) { + return; + } + + support[f->index] = 1; + ddSupportStep(cuddT(f),support); + ddSupportStep(Cudd_Regular(cuddE(f)),support); + /* Mark as visited. */ + f->next = Cudd_Not(f->next); + return; + +} /* end of ddSupportStep */ + + +/**Function******************************************************************** + + Synopsis [Performs a DFS from f, clearing the LSB of the next + pointers.] + + Description [] + + SideEffects [None] + + SeeAlso [ddSupportStep ddDagInt] + +******************************************************************************/ +static void +ddClearFlag( + DdNode * f) +{ + if (!Cudd_IsComplement(f->next)) { + return; + } + /* Clear visited flag. */ + f->next = Cudd_Regular(f->next); + if (cuddIsConstant(f)) { + return; + } + ddClearFlag(cuddT(f)); + ddClearFlag(Cudd_Regular(cuddE(f))); + return; + +} /* end of ddClearFlag */ + + +/**Function******************************************************************** + + Synopsis [Composed three subcovers into one ZDD.] + + Description [] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +DdNode * +extraComposeCover( + DdManager* dd, /* the manager */ + DdNode* zC0, /* the pointer to the negative var cofactor */ + DdNode* zC1, /* the pointer to the positive var cofactor */ + DdNode* zC2, /* the pointer to the cofactor without var */ + int TopVar) /* the index of the positive ZDD var */ +{ + DdNode * zRes, * zTemp; + /* compose with-neg-var and without-var using the neg ZDD var */ + zTemp = cuddZddGetNode( dd, 2*TopVar + 1, zC0, zC2 ); + if ( zTemp == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zC0); + Cudd_RecursiveDerefZdd(dd, zC1); + Cudd_RecursiveDerefZdd(dd, zC2); + return NULL; + } + cuddRef( zTemp ); + cuddDeref( zC0 ); + cuddDeref( zC2 ); + + /* compose with-pos-var and previous result using the pos ZDD var */ + zRes = cuddZddGetNode( dd, 2*TopVar, zC1, zTemp ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zC1); + Cudd_RecursiveDerefZdd(dd, zTemp); + return NULL; + } + cuddDeref( zC1 ); + cuddDeref( zTemp ); + return zRes; +} /* extraComposeCover */ + +/**Function******************************************************************** + + Synopsis [Performs the recursive step of prime computation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode* extraZddPrimes( DdManager *dd, DdNode* F ) +{ + DdNode *zRes; + + if ( F == Cudd_Not( dd->one ) ) + return dd->zero; + if ( F == dd->one ) + return dd->one; + + /* check cache */ + zRes = cuddCacheLookup1Zdd(dd, extraZddPrimes, F); + if (zRes) + return(zRes); + { + /* temporary variables */ + DdNode *bF01, *zP0, *zP1; + /* three components of the prime set */ + DdNode *zResE, *zResP, *zResN; + int fIsComp = Cudd_IsComplement( F ); + + /* find cofactors of F */ + DdNode * bF0 = Cudd_NotCond( Cudd_E( F ), fIsComp ); + DdNode * bF1 = Cudd_NotCond( Cudd_T( F ), fIsComp ); + + /* find the intersection of cofactors */ + bF01 = cuddBddAndRecur( dd, bF0, bF1 ); + if ( bF01 == NULL ) return NULL; + cuddRef( bF01 ); + + /* solve the problems for cofactors */ + zP0 = extraZddPrimes( dd, bF0 ); + if ( zP0 == NULL ) + { + Cudd_RecursiveDeref( dd, bF01 ); + return NULL; + } + cuddRef( zP0 ); + + zP1 = extraZddPrimes( dd, bF1 ); + if ( zP1 == NULL ) + { + Cudd_RecursiveDeref( dd, bF01 ); + Cudd_RecursiveDerefZdd( dd, zP0 ); + return NULL; + } + cuddRef( zP1 ); + + /* check for local unateness */ + if ( bF01 == bF0 ) /* unate increasing */ + { + /* intersection is useless */ + cuddDeref( bF01 ); + /* the primes of intersection are the primes of F0 */ + zResE = zP0; + /* there are no primes with negative var */ + zResN = dd->zero; + cuddRef( zResN ); + /* primes with positive var are primes of F1 that are not primes of F01 */ + zResP = cuddZddDiff( dd, zP1, zP0 ); + if ( zResP == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zResE ); + Cudd_RecursiveDerefZdd( dd, zResN ); + Cudd_RecursiveDerefZdd( dd, zP1 ); + return NULL; + } + cuddRef( zResP ); + Cudd_RecursiveDerefZdd( dd, zP1 ); + } + else if ( bF01 == bF1 ) /* unate decreasing */ + { + /* intersection is useless */ + cuddDeref( bF01 ); + /* the primes of intersection are the primes of F1 */ + zResE = zP1; + /* there are no primes with positive var */ + zResP = dd->zero; + cuddRef( zResP ); + /* primes with negative var are primes of F0 that are not primes of F01 */ + zResN = cuddZddDiff( dd, zP0, zP1 ); + if ( zResN == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zResE ); + Cudd_RecursiveDerefZdd( dd, zResP ); + Cudd_RecursiveDerefZdd( dd, zP0 ); + return NULL; + } + cuddRef( zResN ); + Cudd_RecursiveDerefZdd( dd, zP0 ); + } + else /* not unate */ + { + /* primes without the top var are primes of F10 */ + zResE = extraZddPrimes( dd, bF01 ); + if ( zResE == NULL ) + { + Cudd_RecursiveDerefZdd( dd, bF01 ); + Cudd_RecursiveDerefZdd( dd, zP0 ); + Cudd_RecursiveDerefZdd( dd, zP1 ); + return NULL; + } + cuddRef( zResE ); + Cudd_RecursiveDeref( dd, bF01 ); + + /* primes with the negative top var are those of P0 that are not in F10 */ + zResN = cuddZddDiff( dd, zP0, zResE ); + if ( zResN == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zResE ); + Cudd_RecursiveDerefZdd( dd, zP0 ); + Cudd_RecursiveDerefZdd( dd, zP1 ); + return NULL; + } + cuddRef( zResN ); + Cudd_RecursiveDerefZdd( dd, zP0 ); + + /* primes with the positive top var are those of P1 that are not in F10 */ + zResP = cuddZddDiff( dd, zP1, zResE ); + if ( zResP == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zResE ); + Cudd_RecursiveDerefZdd( dd, zResN ); + Cudd_RecursiveDerefZdd( dd, zP1 ); + return NULL; + } + cuddRef( zResP ); + Cudd_RecursiveDerefZdd( dd, zP1 ); + } + + zRes = extraComposeCover( dd, zResN, zResP, zResE, Cudd_Regular(F)->index ); + if ( zRes == NULL ) return NULL; + + /* insert the result into cache */ + cuddCacheInsert1(dd, extraZddPrimes, F, zRes); + return zRes; + } +} /* end of extraZddPrimes */ + +/**Function******************************************************************** + + Synopsis [Implements the recursive step of Cudd_bddPermute.] + + Description [ Recursively puts the BDD in the order given in the array permut. + Checks for trivial cases to terminate recursion, then splits on the + children of this node. Once the solutions for the children are + obtained, it puts into the current position the node from the rest of + the BDD that should be here. Then returns this BDD. + The key here is that the node being visited is NOT put in its proper + place by this instance, but rather is switched when its proper position + is reached in the recursion tree.

+ The DdNode * that is returned is the same BDD as passed in as node, + but in the new order.] + + SideEffects [None] + + SeeAlso [Cudd_bddPermute cuddAddPermuteRecur] + +******************************************************************************/ +static DdNode * +cuddBddPermuteRecur( DdManager * manager /* DD manager */ , + DdHashTable * table /* computed table */ , + DdNode * node /* BDD to be reordered */ , + int *permut /* permutation array */ ) +{ + DdNode *N, *T, *E; + DdNode *res; + int index; + + statLine( manager ); + N = Cudd_Regular( node ); + + /* Check for terminal case of constant node. */ + if ( cuddIsConstant( N ) ) + { + return ( node ); + } + + /* If problem already solved, look up answer and return. */ + if ( N->ref != 1 && ( res = cuddHashTableLookup1( table, N ) ) != NULL ) + { + return ( Cudd_NotCond( res, N != node ) ); + } + + /* Split and recur on children of this node. */ + T = cuddBddPermuteRecur( manager, table, cuddT( N ), permut ); + if ( T == NULL ) + return ( NULL ); + cuddRef( T ); + E = cuddBddPermuteRecur( manager, table, cuddE( N ), permut ); + if ( E == NULL ) + { + Cudd_IterDerefBdd( manager, T ); + return ( NULL ); + } + cuddRef( E ); + + /* Move variable that should be in this position to this position + ** by retrieving the single var BDD for that variable, and calling + ** cuddBddIteRecur with the T and E we just created. + */ + index = permut[N->index]; + res = cuddBddIteRecur( manager, manager->vars[index], T, E ); + if ( res == NULL ) + { + Cudd_IterDerefBdd( manager, T ); + Cudd_IterDerefBdd( manager, E ); + return ( NULL ); + } + cuddRef( res ); + Cudd_IterDerefBdd( manager, T ); + Cudd_IterDerefBdd( manager, E ); + + /* Do not keep the result if the reference count is only 1, since + ** it will not be visited again. + */ + if ( N->ref != 1 ) + { + ptrint fanout = ( ptrint ) N->ref; + cuddSatDec( fanout ); + if ( !cuddHashTableInsert1( table, N, res, fanout ) ) + { + Cudd_IterDerefBdd( manager, res ); + return ( NULL ); + } + } + cuddDeref( res ); + return ( Cudd_NotCond( res, N != node ) ); + +} /* end of cuddBddPermuteRecur */ + + +/**Function******************************************************************** + + Synopsis [Performs the reordering-sensitive step of Extra_bddChangePolarity().] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * extraBddChangePolarity( + DdManager * dd, /* the DD manager */ + DdNode * bFunc, + DdNode * bVars) +{ + DdNode * bRes; + + if ( bVars == b1 ) + return bFunc; + if ( Cudd_IsConstant(bFunc) ) + return bFunc; + + if ( (bRes = cuddCacheLookup2(dd, extraBddChangePolarity, bFunc, bVars)) ) + return bRes; + else + { + DdNode * bFR = Cudd_Regular(bFunc); + int LevelF = dd->perm[bFR->index]; + int LevelV = dd->perm[bVars->index]; + + if ( LevelV < LevelF ) + bRes = extraBddChangePolarity( dd, bFunc, cuddT(bVars) ); + else // if ( LevelF <= LevelV ) + { + DdNode * bRes0, * bRes1; + DdNode * bF0, * bF1; + DdNode * bVarsNext; + + // cofactor the functions + if ( bFR != bFunc ) // bFunc is complemented + { + bF0 = Cudd_Not( cuddE(bFR) ); + bF1 = Cudd_Not( cuddT(bFR) ); + } + else + { + bF0 = cuddE(bFR); + bF1 = cuddT(bFR); + } + + if ( LevelF == LevelV ) + bVarsNext = cuddT(bVars); + else + bVarsNext = bVars; + + bRes0 = extraBddChangePolarity( dd, bF0, bVarsNext ); + if ( bRes0 == NULL ) + return NULL; + cuddRef( bRes0 ); + + bRes1 = extraBddChangePolarity( dd, bF1, bVarsNext ); + if ( bRes1 == NULL ) + { + Cudd_RecursiveDeref( dd, bRes0 ); + return NULL; + } + cuddRef( bRes1 ); + + if ( LevelF == LevelV ) + { // swap the cofactors + DdNode * bTemp; + bTemp = bRes0; + bRes0 = bRes1; + bRes1 = bTemp; + } + + /* only aRes0 and aRes1 are referenced at this point */ + + /* consider the case when Res0 and Res1 are the same node */ + if ( bRes0 == bRes1 ) + bRes = bRes1; + /* consider the case when Res1 is complemented */ + else if ( Cudd_IsComplement(bRes1) ) + { + bRes = cuddUniqueInter(dd, bFR->index, Cudd_Not(bRes1), Cudd_Not(bRes0)); + if ( bRes == NULL ) + { + Cudd_RecursiveDeref(dd,bRes0); + Cudd_RecursiveDeref(dd,bRes1); + return NULL; + } + bRes = Cudd_Not(bRes); + } + else + { + bRes = cuddUniqueInter( dd, bFR->index, bRes1, bRes0 ); + if ( bRes == NULL ) + { + Cudd_RecursiveDeref(dd,bRes0); + Cudd_RecursiveDeref(dd,bRes1); + return NULL; + } + } + cuddDeref( bRes0 ); + cuddDeref( bRes1 ); + } + + /* insert the result into cache */ + cuddCacheInsert2(dd, extraBddChangePolarity, bFunc, bVars, bRes); + return bRes; + } +} /* end of extraBddChangePolarity */ + + + +static int Counter = 0; + +/**Function************************************************************* + + Synopsis [Computes the AND of two BDD with different orders.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * extraBddAndPermute( DdHashTable * table, DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode * bG, int * pPermute ) +{ + DdNode * bF0, * bF1, * bG0, * bG1, * bRes0, * bRes1, * bRes, * bVar; + int LevF, LevG, Lev; + + // if F == 0, return 0 + if ( bF == Cudd_Not(ddF->one) ) + return Cudd_Not(ddF->one); + // if G == 0, return 0 + if ( bG == Cudd_Not(ddG->one) ) + return Cudd_Not(ddF->one); + // if G == 1, return F + if ( bG == ddG->one ) + return bF; + // cannot use F == 1, because the var order of G has to be changed + + // check cache + if ( //(Cudd_Regular(bF)->ref != 1 || Cudd_Regular(bG)->ref != 1) && + (bRes = cuddHashTableLookup2(table, bF, bG)) ) + return bRes; + Counter++; + + if ( ddF->TimeStop && Abc_Clock() > ddF->TimeStop ) + return NULL; + if ( ddG->TimeStop && Abc_Clock() > ddG->TimeStop ) + return NULL; + + // find the topmost variable in F and G using var order of F + LevF = cuddI( ddF, Cudd_Regular(bF)->index ); + LevG = cuddI( ddF, pPermute ? pPermute[Cudd_Regular(bG)->index] : Cudd_Regular(bG)->index ); + Lev = Abc_MinInt( LevF, LevG ); + assert( Lev < ddF->size ); + bVar = ddF->vars[ddF->invperm[Lev]]; + + // cofactor + bF0 = (Lev < LevF) ? bF : Cudd_NotCond( cuddE(Cudd_Regular(bF)), Cudd_IsComplement(bF) ); + bF1 = (Lev < LevF) ? bF : Cudd_NotCond( cuddT(Cudd_Regular(bF)), Cudd_IsComplement(bF) ); + bG0 = (Lev < LevG) ? bG : Cudd_NotCond( cuddE(Cudd_Regular(bG)), Cudd_IsComplement(bG) ); + bG1 = (Lev < LevG) ? bG : Cudd_NotCond( cuddT(Cudd_Regular(bG)), Cudd_IsComplement(bG) ); + + // call for cofactors + bRes0 = extraBddAndPermute( table, ddF, bF0, ddG, bG0, pPermute ); + if ( bRes0 == NULL ) + return NULL; + cuddRef( bRes0 ); + // call for cofactors + bRes1 = extraBddAndPermute( table, ddF, bF1, ddG, bG1, pPermute ); + if ( bRes1 == NULL ) + { + Cudd_IterDerefBdd( ddF, bRes0 ); + return NULL; + } + cuddRef( bRes1 ); + + // compose the result + bRes = cuddBddIteRecur( ddF, bVar, bRes1, bRes0 ); + if ( bRes == NULL ) + { + Cudd_IterDerefBdd( ddF, bRes0 ); + Cudd_IterDerefBdd( ddF, bRes1 ); + return NULL; + } + cuddRef( bRes ); + Cudd_IterDerefBdd( ddF, bRes0 ); + Cudd_IterDerefBdd( ddF, bRes1 ); + + // cache the result +// if ( Cudd_Regular(bF)->ref != 1 || Cudd_Regular(bG)->ref != 1 ) + { + ptrint fanout = (ptrint)Cudd_Regular(bF)->ref * Cudd_Regular(bG)->ref; + cuddSatDec(fanout); + cuddHashTableInsert2( table, bF, bG, bRes, fanout ); + } + cuddDeref( bRes ); + return bRes; +} + +/**Function************************************************************* + + Synopsis [Testbench.] + + Description [This procedure takes BDD manager ddF and two BDDs + in this manager (bF and bG). It creates a new manager ddG, + transfers bG into it and then reorders it, resulting in bG2. + Then it tries to compute the product of bF and bG2 in ddF.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Extra_TestAndPerm( DdManager * ddF, DdNode * bF, DdNode * bG ) +{ + DdManager * ddG; + DdNode * bG2, * bRes1, * bRes2; + abctime clk; + // disable variable ordering in ddF + Cudd_AutodynDisable( ddF ); + + // create new BDD manager + ddG = Cudd_Init( ddF->size, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); + // transfer BDD into it + Cudd_ShuffleHeap( ddG, ddF->invperm ); + bG2 = Extra_TransferLevelByLevel( ddF, ddG, bG ); Cudd_Ref( bG2 ); + // reorder the new manager + Cudd_ReduceHeap( ddG, CUDD_REORDER_SYMM_SIFT, 1 ); + + // compute the result +clk = Abc_Clock(); + bRes1 = Cudd_bddAnd( ddF, bF, bG ); Cudd_Ref( bRes1 ); +Abc_PrintTime( 1, "Runtime of Cudd_bddAnd ", Abc_Clock() - clk ); + + // compute the result +Counter = 0; +clk = Abc_Clock(); + bRes2 = Extra_bddAndPermute( ddF, bF, ddG, bG2, NULL ); Cudd_Ref( bRes2 ); +Abc_PrintTime( 1, "Runtime of new procedure", Abc_Clock() - clk ); +printf( "Recursive calls = %d\n", Counter ); +printf( "|F| =%6d |G| =%6d |H| =%6d |F|*|G| =%9d ", + Cudd_DagSize(bF), Cudd_DagSize(bG), Cudd_DagSize(bRes2), + Cudd_DagSize(bF) * Cudd_DagSize(bG) ); + + if ( bRes1 == bRes2 ) + printf( "Result verified.\n\n" ); + else + printf( "Result is incorrect.\n\n" ); + + Cudd_RecursiveDeref( ddF, bRes1 ); + Cudd_RecursiveDeref( ddF, bRes2 ); + // quit the new manager + Cudd_RecursiveDeref( ddG, bG2 ); + Extra_StopManager( ddG ); + + // re-enable variable ordering in ddF + Cudd_AutodynEnable( ddF, CUDD_REORDER_SYMM_SIFT ); +} + +/**Function************************************************************* + + Synopsis [Writes ZDD into a PLA file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Extra_zddDumpPla( DdManager * dd, DdNode * F, int nVars, char * pFileName ) +{ + DdGen *gen; + char * pCube; + int * pPath, i; + FILE * pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) + { + printf( "Cannot open file \"%s\" for writing.\n", pFileName ); + return; + } + fprintf( pFile, "# PLA file dumped by Extra_zddDumpPla() in ABC\n" ); + fprintf( pFile, ".i %d\n", nVars ); + fprintf( pFile, ".o 1\n" ); + pCube = ABC_CALLOC( char, dd->sizeZ ); + Cudd_zddForeachPath( dd, F, gen, pPath ) + { + for ( i = 0; i < nVars; i++ ) + pCube[i] = '-'; + for ( i = 0; i < nVars; i++ ) + if ( pPath[2*i] == 1 || pPath[2*i+1] == 1 ) + pCube[i] = '0' + (pPath[2*i] == 1); + fprintf( pFile, "%s 1\n", pCube ); + } + fprintf( pFile, ".e\n\n" ); + fclose( pFile ); + ABC_FREE( pCube ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/bdd/extrab/extraBddSymm.c b/src/bdd/extrab/extraBddSymm.c new file mode 100644 index 00000000..9dd2c8e5 --- /dev/null +++ b/src/bdd/extrab/extraBddSymm.c @@ -0,0 +1,1474 @@ +/**CFile**************************************************************** + + FileName [extraBddSymm.c] + + PackageName [extra] + + Synopsis [Efficient methods to compute the information about + symmetric variables using the algorithm presented in the paper: + A. Mishchenko. Fast Computation of Symmetries in Boolean Functions. + Transactions on CAD, Nov. 2003.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 2.0. Started - September 1, 2003.] + + Revision [$Id: extraBddSymm.c,v 1.0 2003/09/01 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "extraBdd.h" + +ABC_NAMESPACE_IMPL_START + + +/*---------------------------------------------------------------------------*/ +/* Constant declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Stucture declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Type declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Variable declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Macro declarations */ +/*---------------------------------------------------------------------------*/ + +#define DD_GET_SYMM_VARS_TAG 0x0a /* former DD_BDD_XOR_EXIST_ABSTRACT_TAG */ + +/**AutomaticStart*************************************************************/ + +/*---------------------------------------------------------------------------*/ +/* Static function prototypes */ +/*---------------------------------------------------------------------------*/ + +/**AutomaticEnd***************************************************************/ + +/*---------------------------------------------------------------------------*/ +/* Definition of exported functions */ +/*---------------------------------------------------------------------------*/ + +/**Function******************************************************************** + + Synopsis [Computes the classical symmetry information for the function.] + + Description [Returns the symmetry information in the form of Extra_SymmInfo_t structure.] + + SideEffects [If the ZDD variables are not derived from BDD variables with + multiplicity 2, this function may derive them in a wrong way.] + + SeeAlso [] + +******************************************************************************/ +Extra_SymmInfo_t * Extra_SymmPairsCompute( + DdManager * dd, /* the manager */ + DdNode * bFunc) /* the function whose symmetries are computed */ +{ + DdNode * bSupp; + DdNode * zRes; + Extra_SymmInfo_t * p; + + bSupp = Cudd_Support( dd, bFunc ); Cudd_Ref( bSupp ); + zRes = Extra_zddSymmPairsCompute( dd, bFunc, bSupp ); Cudd_Ref( zRes ); + + p = Extra_SymmPairsCreateFromZdd( dd, zRes, bSupp ); + + Cudd_RecursiveDeref( dd, bSupp ); + Cudd_RecursiveDerefZdd( dd, zRes ); + + return p; + +} /* end of Extra_SymmPairsCompute */ + + +/**Function******************************************************************** + + Synopsis [Computes the classical symmetry information as a ZDD.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * Extra_zddSymmPairsCompute( + DdManager * dd, /* the DD manager */ + DdNode * bF, + DdNode * bVars) +{ + DdNode * res; + do { + dd->reordered = 0; + res = extraZddSymmPairsCompute( dd, bF, bVars ); + } while (dd->reordered == 1); + return(res); + +} /* end of Extra_zddSymmPairsCompute */ + +/**Function******************************************************************** + + Synopsis [Returns a singleton-set ZDD containing all variables that are symmetric with the given one.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * Extra_zddGetSymmetricVars( + DdManager * dd, /* the DD manager */ + DdNode * bF, /* the first function - originally, the positive cofactor */ + DdNode * bG, /* the second fucntion - originally, the negative cofactor */ + DdNode * bVars) /* the set of variables, on which F and G depend */ +{ + DdNode * res; + do { + dd->reordered = 0; + res = extraZddGetSymmetricVars( dd, bF, bG, bVars ); + } while (dd->reordered == 1); + return(res); + +} /* end of Extra_zddGetSymmetricVars */ + + +/**Function******************************************************************** + + Synopsis [Converts a set of variables into a set of singleton subsets.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * Extra_zddGetSingletons( + DdManager * dd, /* the DD manager */ + DdNode * bVars) /* the set of variables */ +{ + DdNode * res; + do { + dd->reordered = 0; + res = extraZddGetSingletons( dd, bVars ); + } while (dd->reordered == 1); + return(res); + +} /* end of Extra_zddGetSingletons */ + +/**Function******************************************************************** + + Synopsis [Filters the set of variables using the support of the function.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * Extra_bddReduceVarSet( + DdManager * dd, /* the DD manager */ + DdNode * bVars, /* the set of variables to be reduced */ + DdNode * bF) /* the function whose support is used for reduction */ +{ + DdNode * res; + do { + dd->reordered = 0; + res = extraBddReduceVarSet( dd, bVars, bF ); + } while (dd->reordered == 1); + return(res); + +} /* end of Extra_bddReduceVarSet */ + + +/**Function******************************************************************** + + Synopsis [Allocates symmetry information structure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +Extra_SymmInfo_t * Extra_SymmPairsAllocate( int nVars ) +{ + int i; + Extra_SymmInfo_t * p; + + // allocate and clean the storage for symmetry info + p = ABC_ALLOC( Extra_SymmInfo_t, 1 ); + memset( p, 0, sizeof(Extra_SymmInfo_t) ); + p->nVars = nVars; + p->pVars = ABC_ALLOC( int, nVars ); + p->pSymms = ABC_ALLOC( char *, nVars ); + p->pSymms[0] = ABC_ALLOC( char , nVars * nVars ); + memset( p->pSymms[0], 0, nVars * nVars * sizeof(char) ); + + for ( i = 1; i < nVars; i++ ) + p->pSymms[i] = p->pSymms[i-1] + nVars; + + return p; +} /* end of Extra_SymmPairsAllocate */ + +/**Function******************************************************************** + + Synopsis [Deallocates symmetry information structure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +void Extra_SymmPairsDissolve( Extra_SymmInfo_t * p ) +{ + ABC_FREE( p->pVars ); + ABC_FREE( p->pSymms[0] ); + ABC_FREE( p->pSymms ); + ABC_FREE( p ); +} /* end of Extra_SymmPairsDissolve */ + +/**Function******************************************************************** + + Synopsis [Allocates symmetry information structure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +void Extra_SymmPairsPrint( Extra_SymmInfo_t * p ) +{ + int i, k; + printf( "\n" ); + for ( i = 0; i < p->nVars; i++ ) + { + for ( k = 0; k <= i; k++ ) + printf( " " ); + for ( k = i+1; k < p->nVars; k++ ) + if ( p->pSymms[i][k] ) + printf( "1" ); + else + printf( "." ); + printf( "\n" ); + } +} /* end of Extra_SymmPairsPrint */ + + +/**Function******************************************************************** + + Synopsis [Creates the symmetry information structure from ZDD.] + + Description [ZDD representation of symmetries is the set of cubes, each + of which has two variables in the positive polarity. These variables correspond + to the symmetric variable pair.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +Extra_SymmInfo_t * Extra_SymmPairsCreateFromZdd( DdManager * dd, DdNode * zPairs, DdNode * bSupp ) +{ + int i; + int nSuppSize; + Extra_SymmInfo_t * p; + int * pMapVars2Nums; + DdNode * bTemp; + DdNode * zSet, * zCube, * zTemp; + int iVar1, iVar2; + + nSuppSize = Extra_bddSuppSize( dd, bSupp ); + + // allocate and clean the storage for symmetry info + p = Extra_SymmPairsAllocate( nSuppSize ); + + // allocate the storage for the temporary map + pMapVars2Nums = ABC_ALLOC( int, dd->size ); + memset( pMapVars2Nums, 0, dd->size * sizeof(int) ); + + // assign the variables + p->nVarsMax = dd->size; +// p->nNodes = Cudd_DagSize( zPairs ); + p->nNodes = 0; + for ( i = 0, bTemp = bSupp; bTemp != b1; bTemp = cuddT(bTemp), i++ ) + { + p->pVars[i] = bTemp->index; + pMapVars2Nums[bTemp->index] = i; + } + + // write the symmetry info into the structure + zSet = zPairs; Cudd_Ref( zSet ); + while ( zSet != z0 ) + { + // get the next cube + zCube = Extra_zddSelectOneSubset( dd, zSet ); Cudd_Ref( zCube ); + + // add these two variables to the data structure + assert( cuddT( cuddT(zCube) ) == z1 ); + iVar1 = zCube->index/2; + iVar2 = cuddT(zCube)->index/2; + if ( pMapVars2Nums[iVar1] < pMapVars2Nums[iVar2] ) + p->pSymms[ pMapVars2Nums[iVar1] ][ pMapVars2Nums[iVar2] ] = 1; + else + p->pSymms[ pMapVars2Nums[iVar2] ][ pMapVars2Nums[iVar1] ] = 1; + // count the symmetric pairs + p->nSymms ++; + + // update the cuver and deref the cube + zSet = Cudd_zddDiff( dd, zTemp = zSet, zCube ); Cudd_Ref( zSet ); + Cudd_RecursiveDerefZdd( dd, zTemp ); + Cudd_RecursiveDerefZdd( dd, zCube ); + + } // for each cube + Cudd_RecursiveDerefZdd( dd, zSet ); + + ABC_FREE( pMapVars2Nums ); + return p; + +} /* end of Extra_SymmPairsCreateFromZdd */ + + +/**Function******************************************************************** + + Synopsis [Checks the possibility of two variables being symmetric.] + + Description [Returns 0 if vars are not symmetric. Return 1 if vars can be symmetric.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Extra_bddCheckVarsSymmetric( + DdManager * dd, /* the DD manager */ + DdNode * bF, + int iVar1, + int iVar2) +{ + DdNode * bVars; + int Res; + +// return 1; + + assert( iVar1 != iVar2 ); + assert( iVar1 < dd->size ); + assert( iVar2 < dd->size ); + + bVars = Cudd_bddAnd( dd, dd->vars[iVar1], dd->vars[iVar2] ); Cudd_Ref( bVars ); + + Res = (int)( extraBddCheckVarsSymmetric( dd, bF, bVars ) == b1 ); + + Cudd_RecursiveDeref( dd, bVars ); + + return Res; +} /* end of Extra_bddCheckVarsSymmetric */ + + +/**Function******************************************************************** + + Synopsis [Computes the classical symmetry information for the function.] + + Description [Uses the naive way of comparing cofactors.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +Extra_SymmInfo_t * Extra_SymmPairsComputeNaive( DdManager * dd, DdNode * bFunc ) +{ + DdNode * bSupp, * bTemp; + int nSuppSize; + Extra_SymmInfo_t * p; + int i, k; + + // compute the support + bSupp = Cudd_Support( dd, bFunc ); Cudd_Ref( bSupp ); + nSuppSize = Extra_bddSuppSize( dd, bSupp ); +//printf( "Support = %d. ", nSuppSize ); +//Extra_bddPrint( dd, bSupp ); +//printf( "%d ", nSuppSize ); + + // allocate the storage for symmetry info + p = Extra_SymmPairsAllocate( nSuppSize ); + + // assign the variables + p->nVarsMax = dd->size; + for ( i = 0, bTemp = bSupp; bTemp != b1; bTemp = cuddT(bTemp), i++ ) + p->pVars[i] = bTemp->index; + + // go through the candidate pairs and check using Idea1 + for ( i = 0; i < nSuppSize; i++ ) + for ( k = i+1; k < nSuppSize; k++ ) + { + p->pSymms[k][i] = p->pSymms[i][k] = Extra_bddCheckVarsSymmetricNaive( dd, bFunc, p->pVars[i], p->pVars[k] ); + if ( p->pSymms[i][k] ) + p->nSymms++; + } + + Cudd_RecursiveDeref( dd, bSupp ); + return p; + +} /* end of Extra_SymmPairsComputeNaive */ + +/**Function******************************************************************** + + Synopsis [Checks if the two variables are symmetric.] + + Description [Returns 0 if vars are not symmetric. Return 1 if vars are symmetric.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Extra_bddCheckVarsSymmetricNaive( + DdManager * dd, /* the DD manager */ + DdNode * bF, + int iVar1, + int iVar2) +{ + DdNode * bCube1, * bCube2; + DdNode * bCof01, * bCof10; + int Res; + + assert( iVar1 != iVar2 ); + assert( iVar1 < dd->size ); + assert( iVar2 < dd->size ); + + bCube1 = Cudd_bddAnd( dd, Cudd_Not( dd->vars[iVar1] ), dd->vars[iVar2] ); Cudd_Ref( bCube1 ); + bCube2 = Cudd_bddAnd( dd, Cudd_Not( dd->vars[iVar2] ), dd->vars[iVar1] ); Cudd_Ref( bCube2 ); + + bCof01 = Cudd_Cofactor( dd, bF, bCube1 ); Cudd_Ref( bCof01 ); + bCof10 = Cudd_Cofactor( dd, bF, bCube2 ); Cudd_Ref( bCof10 ); + + Res = (int)( bCof10 == bCof01 ); + + Cudd_RecursiveDeref( dd, bCof01 ); + Cudd_RecursiveDeref( dd, bCof10 ); + Cudd_RecursiveDeref( dd, bCube1 ); + Cudd_RecursiveDeref( dd, bCube2 ); + + return Res; +} /* end of Extra_bddCheckVarsSymmetricNaive */ + + +/**Function******************************************************************** + + Synopsis [Builds ZDD representing the set of fixed-size variable tuples.] + + Description [Creates ZDD of all combinations of variables in Support that + is represented by a BDD.] + + SideEffects [New ZDD variables are created if indices of the variables + present in the combination are larger than the currently + allocated number of ZDD variables.] + + SeeAlso [] + +******************************************************************************/ +DdNode* Extra_zddTuplesFromBdd( + DdManager * dd, /* the DD manager */ + int K, /* the number of variables in tuples */ + DdNode * bVarsN) /* the set of all variables represented as a BDD */ +{ + DdNode *zRes; + int autoDynZ; + + autoDynZ = dd->autoDynZ; + dd->autoDynZ = 0; + + do { + /* transform the numeric arguments (K) into a DdNode* argument; + * this allows us to use the standard internal CUDD cache */ + DdNode *bVarSet = bVarsN, *bVarsK = bVarsN; + int nVars = 0, i; + + /* determine the number of variables in VarSet */ + while ( bVarSet != b1 ) + { + nVars++; + /* make sure that the VarSet is a cube */ + if ( cuddE( bVarSet ) != b0 ) + return NULL; + bVarSet = cuddT( bVarSet ); + } + /* make sure that the number of variables in VarSet is less or equal + that the number of variables that should be present in the tuples + */ + if ( K > nVars ) + return NULL; + + /* the second argument in the recursive call stannds for ; + * reate the first argument, which stands for + * as when we are talking about the tuple of out of */ + for ( i = 0; i < nVars-K; i++ ) + bVarsK = cuddT( bVarsK ); + + dd->reordered = 0; + zRes = extraZddTuplesFromBdd(dd, bVarsK, bVarsN ); + + } while (dd->reordered == 1); + dd->autoDynZ = autoDynZ; + return zRes; + +} /* end of Extra_zddTuplesFromBdd */ + +/**Function******************************************************************** + + Synopsis [Selects one subset from the set of subsets represented by a ZDD.] + + Description [] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +DdNode* Extra_zddSelectOneSubset( + DdManager * dd, /* the DD manager */ + DdNode * zS) /* the ZDD */ +{ + DdNode *res; + do { + dd->reordered = 0; + res = extraZddSelectOneSubset(dd, zS); + } while (dd->reordered == 1); + return(res); + +} /* end of Extra_zddSelectOneSubset */ + + +/*---------------------------------------------------------------------------*/ +/* Definition of internal functions */ +/*---------------------------------------------------------------------------*/ + +/**Function******************************************************************** + + Synopsis [Performs a recursive step of Extra_SymmPairsCompute.] + + Description [Returns the set of symmetric variable pairs represented as a set + of two-literal ZDD cubes. Both variables always appear in the positive polarity + in the cubes. This function works without building new BDD nodes. Some relatively + small number of ZDD nodes may be built to ensure proper bookkeeping of the + symmetry information.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * +extraZddSymmPairsCompute( + DdManager * dd, /* the manager */ + DdNode * bFunc, /* the function whose symmetries are computed */ + DdNode * bVars ) /* the set of variables on which this function depends */ +{ + DdNode * zRes; + DdNode * bFR = Cudd_Regular(bFunc); + + if ( cuddIsConstant(bFR) ) + { + int nVars, i; + + // determine how many vars are in the bVars + nVars = Extra_bddSuppSize( dd, bVars ); + if ( nVars < 2 ) + return z0; + else + { + DdNode * bVarsK; + + // create the BDD bVarsK corresponding to K = 2; + bVarsK = bVars; + for ( i = 0; i < nVars-2; i++ ) + bVarsK = cuddT( bVarsK ); + return extraZddTuplesFromBdd( dd, bVarsK, bVars ); + } + } + assert( bVars != b1 ); + + if ( (zRes = cuddCacheLookup2Zdd(dd, extraZddSymmPairsCompute, bFunc, bVars)) ) + return zRes; + else + { + DdNode * zRes0, * zRes1; + DdNode * zTemp, * zPlus, * zSymmVars; + DdNode * bF0, * bF1; + DdNode * bVarsNew; + int nVarsExtra; + int LevelF; + + // every variable in bF should be also in bVars, therefore LevelF cannot be above LevelV + // if LevelF is below LevelV, scroll through the vars in bVars to the same level as F + // count how many extra vars are there in bVars + nVarsExtra = 0; + LevelF = dd->perm[bFR->index]; + for ( bVarsNew = bVars; LevelF > dd->perm[bVarsNew->index]; bVarsNew = cuddT(bVarsNew) ) + nVarsExtra++; + // the indexes (level) of variables should be synchronized now + assert( bFR->index == bVarsNew->index ); + + // cofactor the function + if ( bFR != bFunc ) // bFunc is complemented + { + bF0 = Cudd_Not( cuddE(bFR) ); + bF1 = Cudd_Not( cuddT(bFR) ); + } + else + { + bF0 = cuddE(bFR); + bF1 = cuddT(bFR); + } + + // solve subproblems + zRes0 = extraZddSymmPairsCompute( dd, bF0, cuddT(bVarsNew) ); + if ( zRes0 == NULL ) + return NULL; + cuddRef( zRes0 ); + + // if there is no symmetries in the negative cofactor + // there is no need to test the positive cofactor + if ( zRes0 == z0 ) + zRes = zRes0; // zRes takes reference + else + { + zRes1 = extraZddSymmPairsCompute( dd, bF1, cuddT(bVarsNew) ); + if ( zRes1 == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + return NULL; + } + cuddRef( zRes1 ); + + // only those variables are pair-wise symmetric + // that are pair-wise symmetric in both cofactors + // therefore, intersect the solutions + zRes = cuddZddIntersect( dd, zRes0, zRes1 ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + Cudd_RecursiveDerefZdd( dd, zRes1 ); + return NULL; + } + cuddRef( zRes ); + Cudd_RecursiveDerefZdd( dd, zRes0 ); + Cudd_RecursiveDerefZdd( dd, zRes1 ); + } + + // consider the current top-most variable and find all the vars + // that are pairwise symmetric with it + // these variables are returned as a set of ZDD singletons + zSymmVars = extraZddGetSymmetricVars( dd, bF1, bF0, cuddT(bVarsNew) ); + if ( zSymmVars == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes ); + return NULL; + } + cuddRef( zSymmVars ); + + // attach the topmost variable to the set, to get the variable pairs + // use the positive polarity ZDD variable for the purpose + + // there is no need to do so, if zSymmVars is empty + if ( zSymmVars == z0 ) + Cudd_RecursiveDerefZdd( dd, zSymmVars ); + else + { + zPlus = cuddZddGetNode( dd, 2*bFR->index, zSymmVars, z0 ); + if ( zPlus == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes ); + Cudd_RecursiveDerefZdd( dd, zSymmVars ); + return NULL; + } + cuddRef( zPlus ); + cuddDeref( zSymmVars ); + + // add these variable pairs to the result + zRes = cuddZddUnion( dd, zTemp = zRes, zPlus ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zTemp ); + Cudd_RecursiveDerefZdd( dd, zPlus ); + return NULL; + } + cuddRef( zRes ); + Cudd_RecursiveDerefZdd( dd, zTemp ); + Cudd_RecursiveDerefZdd( dd, zPlus ); + } + + // only zRes is referenced at this point + + // if we skipped some variables, these variables cannot be symmetric with + // any variables that are currently in the support of bF, but they can be + // symmetric with the variables that are in bVars but not in the support of bF + if ( nVarsExtra ) + { + // it is possible to improve this step: + // (1) there is no need to enter here, if nVarsExtra < 2 + + // create the set of topmost nVarsExtra in bVars + DdNode * bVarsExtra; + int nVars; + + // remove from bVars all the variable that are in the support of bFunc + bVarsExtra = extraBddReduceVarSet( dd, bVars, bFunc ); + if ( bVarsExtra == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes ); + return NULL; + } + cuddRef( bVarsExtra ); + + // determine how many vars are in the bVarsExtra + nVars = Extra_bddSuppSize( dd, bVarsExtra ); + if ( nVars < 2 ) + { + Cudd_RecursiveDeref( dd, bVarsExtra ); + } + else + { + int i; + DdNode * bVarsK; + + // create the BDD bVarsK corresponding to K = 2; + bVarsK = bVarsExtra; + for ( i = 0; i < nVars-2; i++ ) + bVarsK = cuddT( bVarsK ); + + // create the 2 variable tuples + zPlus = extraZddTuplesFromBdd( dd, bVarsK, bVarsExtra ); + if ( zPlus == NULL ) + { + Cudd_RecursiveDeref( dd, bVarsExtra ); + Cudd_RecursiveDerefZdd( dd, zRes ); + return NULL; + } + cuddRef( zPlus ); + Cudd_RecursiveDeref( dd, bVarsExtra ); + + // add these to the result + zRes = cuddZddUnion( dd, zTemp = zRes, zPlus ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zTemp ); + Cudd_RecursiveDerefZdd( dd, zPlus ); + return NULL; + } + cuddRef( zRes ); + Cudd_RecursiveDerefZdd( dd, zTemp ); + Cudd_RecursiveDerefZdd( dd, zPlus ); + } + } + cuddDeref( zRes ); + + + /* insert the result into cache */ + cuddCacheInsert2(dd, extraZddSymmPairsCompute, bFunc, bVars, zRes); + return zRes; + } +} /* end of extraZddSymmPairsCompute */ + +/**Function******************************************************************** + + Synopsis [Performs a recursive step of Extra_zddGetSymmetricVars.] + + Description [Returns the set of ZDD singletons, containing those positive + ZDD variables that correspond to BDD variables x, for which it is true + that bF(x=0) == bG(x=1).] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * extraZddGetSymmetricVars( + DdManager * dd, /* the DD manager */ + DdNode * bF, /* the first function - originally, the positive cofactor */ + DdNode * bG, /* the second function - originally, the negative cofactor */ + DdNode * bVars) /* the set of variables, on which F and G depend */ +{ + DdNode * zRes; + DdNode * bFR = Cudd_Regular(bF); + DdNode * bGR = Cudd_Regular(bG); + + if ( cuddIsConstant(bFR) && cuddIsConstant(bGR) ) + { + if ( bF == bG ) + return extraZddGetSingletons( dd, bVars ); + else + return z0; + } + assert( bVars != b1 ); + + if ( (zRes = cuddCacheLookupZdd(dd, DD_GET_SYMM_VARS_TAG, bF, bG, bVars)) ) + return zRes; + else + { + DdNode * zRes0, * zRes1; + DdNode * zPlus, * zTemp; + DdNode * bF0, * bF1; + DdNode * bG0, * bG1; + DdNode * bVarsNew; + + int LevelF = cuddI(dd,bFR->index); + int LevelG = cuddI(dd,bGR->index); + int LevelFG; + + if ( LevelF < LevelG ) + LevelFG = LevelF; + else + LevelFG = LevelG; + + // at least one of the arguments is not a constant + assert( LevelFG < dd->size ); + + // every variable in bF and bG should be also in bVars, therefore LevelFG cannot be above LevelV + // if LevelFG is below LevelV, scroll through the vars in bVars to the same level as LevelFG + for ( bVarsNew = bVars; LevelFG > dd->perm[bVarsNew->index]; bVarsNew = cuddT(bVarsNew) ); + assert( LevelFG == dd->perm[bVarsNew->index] ); + + // cofactor the functions + if ( LevelF == LevelFG ) + { + if ( bFR != bF ) // bF is complemented + { + bF0 = Cudd_Not( cuddE(bFR) ); + bF1 = Cudd_Not( cuddT(bFR) ); + } + else + { + bF0 = cuddE(bFR); + bF1 = cuddT(bFR); + } + } + else + bF0 = bF1 = bF; + + if ( LevelG == LevelFG ) + { + if ( bGR != bG ) // bG is complemented + { + bG0 = Cudd_Not( cuddE(bGR) ); + bG1 = Cudd_Not( cuddT(bGR) ); + } + else + { + bG0 = cuddE(bGR); + bG1 = cuddT(bGR); + } + } + else + bG0 = bG1 = bG; + + // solve subproblems + zRes0 = extraZddGetSymmetricVars( dd, bF0, bG0, cuddT(bVarsNew) ); + if ( zRes0 == NULL ) + return NULL; + cuddRef( zRes0 ); + + // if there is not symmetries in the negative cofactor + // there is no need to test the positive cofactor + if ( zRes0 == z0 ) + zRes = zRes0; // zRes takes reference + else + { + zRes1 = extraZddGetSymmetricVars( dd, bF1, bG1, cuddT(bVarsNew) ); + if ( zRes1 == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + return NULL; + } + cuddRef( zRes1 ); + + // only those variables should belong to the resulting set + // for which the property is true for both cofactors + zRes = cuddZddIntersect( dd, zRes0, zRes1 ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + Cudd_RecursiveDerefZdd( dd, zRes1 ); + return NULL; + } + cuddRef( zRes ); + Cudd_RecursiveDerefZdd( dd, zRes0 ); + Cudd_RecursiveDerefZdd( dd, zRes1 ); + } + + // add one more singleton if the property is true for this variable + if ( bF0 == bG1 ) + { + zPlus = cuddZddGetNode( dd, 2*bVarsNew->index, z1, z0 ); + if ( zPlus == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes ); + return NULL; + } + cuddRef( zPlus ); + + // add these variable pairs to the result + zRes = cuddZddUnion( dd, zTemp = zRes, zPlus ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zTemp ); + Cudd_RecursiveDerefZdd( dd, zPlus ); + return NULL; + } + cuddRef( zRes ); + Cudd_RecursiveDerefZdd( dd, zTemp ); + Cudd_RecursiveDerefZdd( dd, zPlus ); + } + + if ( bF == bG && bVars != bVarsNew ) + { + // if the functions are equal, so are their cofactors + // add those variables from V that are above F and G + + DdNode * bVarsExtra; + + assert( LevelFG > dd->perm[bVars->index] ); + + // create the BDD of the extra variables + bVarsExtra = cuddBddExistAbstractRecur( dd, bVars, bVarsNew ); + if ( bVarsExtra == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes ); + return NULL; + } + cuddRef( bVarsExtra ); + + zPlus = extraZddGetSingletons( dd, bVarsExtra ); + if ( zPlus == NULL ) + { + Cudd_RecursiveDeref( dd, bVarsExtra ); + Cudd_RecursiveDerefZdd( dd, zRes ); + return NULL; + } + cuddRef( zPlus ); + Cudd_RecursiveDeref( dd, bVarsExtra ); + + // add these to the result + zRes = cuddZddUnion( dd, zTemp = zRes, zPlus ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zTemp ); + Cudd_RecursiveDerefZdd( dd, zPlus ); + return NULL; + } + cuddRef( zRes ); + Cudd_RecursiveDerefZdd( dd, zTemp ); + Cudd_RecursiveDerefZdd( dd, zPlus ); + } + cuddDeref( zRes ); + + cuddCacheInsert( dd, DD_GET_SYMM_VARS_TAG, bF, bG, bVars, zRes ); + return zRes; + } +} /* end of extraZddGetSymmetricVars */ + + +/**Function******************************************************************** + + Synopsis [Performs a recursive step of Extra_zddGetSingletons.] + + Description [Returns the set of ZDD singletons, containing those positive + polarity ZDD variables that correspond to the BDD variables in bVars.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * extraZddGetSingletons( + DdManager * dd, /* the DD manager */ + DdNode * bVars) /* the set of variables */ +{ + DdNode * zRes; + + if ( bVars == b1 ) +// if ( bVars == b0 ) // bug fixed by Jin Zhang, Jan 23, 2004 + return z1; + + if ( (zRes = cuddCacheLookup1Zdd(dd, extraZddGetSingletons, bVars)) ) + return zRes; + else + { + DdNode * zTemp, * zPlus; + + // solve subproblem + zRes = extraZddGetSingletons( dd, cuddT(bVars) ); + if ( zRes == NULL ) + return NULL; + cuddRef( zRes ); + + zPlus = cuddZddGetNode( dd, 2*bVars->index, z1, z0 ); + if ( zPlus == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes ); + return NULL; + } + cuddRef( zPlus ); + + // add these to the result + zRes = cuddZddUnion( dd, zTemp = zRes, zPlus ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zTemp ); + Cudd_RecursiveDerefZdd( dd, zPlus ); + return NULL; + } + cuddRef( zRes ); + Cudd_RecursiveDerefZdd( dd, zTemp ); + Cudd_RecursiveDerefZdd( dd, zPlus ); + cuddDeref( zRes ); + + cuddCacheInsert1( dd, extraZddGetSingletons, bVars, zRes ); + return zRes; + } +} /* end of extraZddGetSingletons */ + + +/**Function******************************************************************** + + Synopsis [Performs a recursive step of Extra_bddReduceVarSet.] + + Description [Returns the set of all variables in the given set that are not in the + support of the given function.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * extraBddReduceVarSet( + DdManager * dd, /* the DD manager */ + DdNode * bVars, /* the set of variables to be reduced */ + DdNode * bF) /* the function whose support is used for reduction */ +{ + DdNode * bRes; + DdNode * bFR = Cudd_Regular(bF); + + if ( cuddIsConstant(bFR) || bVars == b1 ) + return bVars; + + if ( (bRes = cuddCacheLookup2(dd, extraBddReduceVarSet, bVars, bF)) ) + return bRes; + else + { + DdNode * bF0, * bF1; + DdNode * bVarsThis, * bVarsLower, * bTemp; + int LevelF; + + // if LevelF is below LevelV, scroll through the vars in bVars + LevelF = dd->perm[bFR->index]; + for ( bVarsThis = bVars; LevelF > cuddI(dd,bVarsThis->index); bVarsThis = cuddT(bVarsThis) ); + // scroll also through the current var, because it should be not be added + if ( LevelF == cuddI(dd,bVarsThis->index) ) + bVarsLower = cuddT(bVarsThis); + else + bVarsLower = bVarsThis; + + // cofactor the function + if ( bFR != bF ) // bFunc is complemented + { + bF0 = Cudd_Not( cuddE(bFR) ); + bF1 = Cudd_Not( cuddT(bFR) ); + } + else + { + bF0 = cuddE(bFR); + bF1 = cuddT(bFR); + } + + // solve subproblems + bRes = extraBddReduceVarSet( dd, bVarsLower, bF0 ); + if ( bRes == NULL ) + return NULL; + cuddRef( bRes ); + + bRes = extraBddReduceVarSet( dd, bTemp = bRes, bF1 ); + if ( bRes == NULL ) + { + Cudd_RecursiveDeref( dd, bTemp ); + return NULL; + } + cuddRef( bRes ); + Cudd_RecursiveDeref( dd, bTemp ); + + // the current var should not be added + // add the skipped vars + if ( bVarsThis != bVars ) + { + DdNode * bVarsExtra; + + // extract the skipped variables + bVarsExtra = cuddBddExistAbstractRecur( dd, bVars, bVarsThis ); + if ( bVarsExtra == NULL ) + { + Cudd_RecursiveDeref( dd, bRes ); + return NULL; + } + cuddRef( bVarsExtra ); + + // add these variables + bRes = cuddBddAndRecur( dd, bTemp = bRes, bVarsExtra ); + if ( bRes == NULL ) + { + Cudd_RecursiveDeref( dd, bTemp ); + Cudd_RecursiveDeref( dd, bVarsExtra ); + return NULL; + } + cuddRef( bRes ); + Cudd_RecursiveDeref( dd, bTemp ); + Cudd_RecursiveDeref( dd, bVarsExtra ); + } + cuddDeref( bRes ); + + cuddCacheInsert2( dd, extraBddReduceVarSet, bVars, bF, bRes ); + return bRes; + } +} /* end of extraBddReduceVarSet */ + + +/**Function******************************************************************** + + Synopsis [Performs the recursive step of Extra_bddCheckVarsSymmetric().] + + Description [Returns b0 if the variables are not symmetric. Returns b1 if the + variables can be symmetric. The variables are represented in the form of a + two-variable cube. In case the cube contains one variable (below Var1 level), + the cube's pointer is complemented if the variable Var1 occurred on the + current path; otherwise, the cube's pointer is regular. Uses additional + complemented bit (Hash_Not) to mark the result if in the BDD rooted that this + node there is a branch passing though the node labeled with Var2.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * extraBddCheckVarsSymmetric( + DdManager * dd, /* the DD manager */ + DdNode * bF, + DdNode * bVars) +{ + DdNode * bRes; + + if ( bF == b0 ) + return b1; + + assert( bVars != b1 ); + + if ( (bRes = cuddCacheLookup2(dd, extraBddCheckVarsSymmetric, bF, bVars)) ) + return bRes; + else + { + DdNode * bRes0, * bRes1; + DdNode * bF0, * bF1; + DdNode * bFR = Cudd_Regular(bF); + int LevelF = cuddI(dd,bFR->index); + + DdNode * bVarsR = Cudd_Regular(bVars); + int fVar1Pres; + int iLev1; + int iLev2; + + if ( bVarsR != bVars ) // cube's pointer is complemented + { + assert( cuddT(bVarsR) == b1 ); + fVar1Pres = 1; // the first var is present on the path + iLev1 = -1; // we are already below the first var level + iLev2 = dd->perm[bVarsR->index]; // the level of the second var + } + else // cube's pointer is NOT complemented + { + fVar1Pres = 0; // the first var is absent on the path + if ( cuddT(bVars) == b1 ) + { + iLev1 = -1; // we are already below the first var level + iLev2 = dd->perm[bVars->index]; // the level of the second var + } + else + { + assert( cuddT(cuddT(bVars)) == b1 ); + iLev1 = dd->perm[bVars->index]; // the level of the first var + iLev2 = dd->perm[cuddT(bVars)->index]; // the level of the second var + } + } + + // cofactor the function + // the cofactors are needed only if we are above the second level + if ( LevelF < iLev2 ) + { + if ( bFR != bF ) // bFunc is complemented + { + bF0 = Cudd_Not( cuddE(bFR) ); + bF1 = Cudd_Not( cuddT(bFR) ); + } + else + { + bF0 = cuddE(bFR); + bF1 = cuddT(bFR); + } + } + else + bF0 = bF1 = NULL; + + // consider five cases: + // (1) F is above iLev1 + // (2) F is on the level iLev1 + // (3) F is between iLev1 and iLev2 + // (4) F is on the level iLev2 + // (5) F is below iLev2 + + // (1) F is above iLev1 + if ( LevelF < iLev1 ) + { + // the returned result cannot have the hash attribute + // because we still did not reach the level of Var1; + // the attribute never travels above the level of Var1 + bRes0 = extraBddCheckVarsSymmetric( dd, bF0, bVars ); +// assert( !Hash_IsComplement( bRes0 ) ); + assert( bRes0 != z0 ); + if ( bRes0 == b0 ) + bRes = b0; + else + bRes = extraBddCheckVarsSymmetric( dd, bF1, bVars ); +// assert( !Hash_IsComplement( bRes ) ); + assert( bRes != z0 ); + } + // (2) F is on the level iLev1 + else if ( LevelF == iLev1 ) + { + bRes0 = extraBddCheckVarsSymmetric( dd, bF0, Cudd_Not( cuddT(bVars) ) ); + if ( bRes0 == b0 ) + bRes = b0; + else + { + bRes1 = extraBddCheckVarsSymmetric( dd, bF1, Cudd_Not( cuddT(bVars) ) ); + if ( bRes1 == b0 ) + bRes = b0; + else + { +// if ( Hash_IsComplement( bRes0 ) || Hash_IsComplement( bRes1 ) ) + if ( bRes0 == z0 || bRes1 == z0 ) + bRes = b1; + else + bRes = b0; + } + } + } + // (3) F is between iLev1 and iLev2 + else if ( LevelF < iLev2 ) + { + bRes0 = extraBddCheckVarsSymmetric( dd, bF0, bVars ); + if ( bRes0 == b0 ) + bRes = b0; + else + { + bRes1 = extraBddCheckVarsSymmetric( dd, bF1, bVars ); + if ( bRes1 == b0 ) + bRes = b0; + else + { +// if ( Hash_IsComplement( bRes0 ) || Hash_IsComplement( bRes1 ) ) +// bRes = Hash_Not( b1 ); + if ( bRes0 == z0 || bRes1 == z0 ) + bRes = z0; + else + bRes = b1; + } + } + } + // (4) F is on the level iLev2 + else if ( LevelF == iLev2 ) + { + // this is the only place where the hash attribute (Hash_Not) can be added + // to the result; it can be added only if the path came through the node + // lebeled with Var1; therefore, the hash attribute cannot be returned + // to the caller function + if ( fVar1Pres ) +// bRes = Hash_Not( b1 ); + bRes = z0; + else + bRes = b0; + } + // (5) F is below iLev2 + else // if ( LevelF > iLev2 ) + { + // it is possible that the path goes through the node labeled by Var1 + // and still everything is okay; we do not label with Hash_Not here + // because the path does not go through node labeled by Var2 + bRes = b1; + } + + cuddCacheInsert2(dd, extraBddCheckVarsSymmetric, bF, bVars, bRes); + return bRes; + } +} /* end of extraBddCheckVarsSymmetric */ + +/**Function******************************************************************** + + Synopsis [Performs the reordering-sensitive step of Extra_zddTupleFromBdd().] + + Description [Generates in a bottom-up fashion ZDD for all combinations + composed of k variables out of variables belonging to Support.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode* extraZddTuplesFromBdd( + DdManager * dd, /* the DD manager */ + DdNode * bVarsK, /* the number of variables in tuples */ + DdNode * bVarsN) /* the set of all variables */ +{ + DdNode *zRes, *zRes0, *zRes1; + statLine(dd); + + /* terminal cases */ +/* if ( k < 0 || k > n ) + * return dd->zero; + * if ( n == 0 ) + * return dd->one; + */ + if ( cuddI( dd, bVarsK->index ) < cuddI( dd, bVarsN->index ) ) + return z0; + if ( bVarsN == b1 ) + return z1; + + /* check cache */ + zRes = cuddCacheLookup2Zdd(dd, extraZddTuplesFromBdd, bVarsK, bVarsN); + if (zRes) + return(zRes); + + /* ZDD in which this variable is 0 */ +/* zRes0 = extraZddTuplesFromBdd( dd, k, n-1 ); */ + zRes0 = extraZddTuplesFromBdd( dd, bVarsK, cuddT(bVarsN) ); + if ( zRes0 == NULL ) + return NULL; + cuddRef( zRes0 ); + + /* ZDD in which this variable is 1 */ +/* zRes1 = extraZddTuplesFromBdd( dd, k-1, n-1 ); */ + if ( bVarsK == b1 ) + { + zRes1 = z0; + cuddRef( zRes1 ); + } + else + { + zRes1 = extraZddTuplesFromBdd( dd, cuddT(bVarsK), cuddT(bVarsN) ); + if ( zRes1 == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + return NULL; + } + cuddRef( zRes1 ); + } + + /* compose Res0 and Res1 with the given ZDD variable */ + zRes = cuddZddGetNode( dd, 2*bVarsN->index, zRes1, zRes0 ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + Cudd_RecursiveDerefZdd( dd, zRes1 ); + return NULL; + } + cuddDeref( zRes0 ); + cuddDeref( zRes1 ); + + /* insert the result into cache */ + cuddCacheInsert2(dd, extraZddTuplesFromBdd, bVarsK, bVarsN, zRes); + return zRes; + +} /* end of extraZddTuplesFromBdd */ + + +/**Function******************************************************************** + + Synopsis [Performs the recursive step of Extra_zddSelectOneSubset.] + + Description [] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +DdNode * extraZddSelectOneSubset( + DdManager * dd, + DdNode * zS ) +// selects one subset from the ZDD zS +// returns z0 if and only if zS is an empty set of cubes +{ + DdNode * zRes; + + if ( zS == z0 ) return z0; + if ( zS == z1 ) return z1; + + // check cache + if ( (zRes = cuddCacheLookup1Zdd( dd, extraZddSelectOneSubset, zS )) ) + return zRes; + else + { + DdNode * zS0, * zS1, * zTemp; + + zS0 = cuddE(zS); + zS1 = cuddT(zS); + + if ( zS0 != z0 ) + { + zRes = extraZddSelectOneSubset( dd, zS0 ); + if ( zRes == NULL ) + return NULL; + } + else // if ( zS0 == z0 ) + { + assert( zS1 != z0 ); + zRes = extraZddSelectOneSubset( dd, zS1 ); + if ( zRes == NULL ) + return NULL; + cuddRef( zRes ); + + zRes = cuddZddGetNode( dd, zS->index, zTemp = zRes, z0 ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zTemp ); + return NULL; + } + cuddDeref( zTemp ); + } + + // insert the result into cache + cuddCacheInsert1( dd, extraZddSelectOneSubset, zS, zRes ); + return zRes; + } +} /* end of extraZddSelectOneSubset */ + + +/*---------------------------------------------------------------------------*/ +/* Definition of static Functions */ +/*---------------------------------------------------------------------------*/ +ABC_NAMESPACE_IMPL_END + diff --git a/src/bdd/extrab/extraBddTime.c b/src/bdd/extrab/extraBddTime.c new file mode 100644 index 00000000..dc9ff147 --- /dev/null +++ b/src/bdd/extrab/extraBddTime.c @@ -0,0 +1,660 @@ +/**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 + diff --git a/src/bdd/extrab/extraBddUnate.c b/src/bdd/extrab/extraBddUnate.c new file mode 100644 index 00000000..9ebdd4e5 --- /dev/null +++ b/src/bdd/extrab/extraBddUnate.c @@ -0,0 +1,646 @@ +/**CFile**************************************************************** + + FileName [extraBddUnate.c] + + PackageName [extra] + + Synopsis [Efficient methods to compute the information about + unate variables using an algorithm that is conceptually similar to + the algorithm for two-variable symmetry computation presented in: + A. Mishchenko. Fast Computation of Symmetries in Boolean Functions. + Transactions on CAD, Nov. 2003.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 2.0. Started - September 1, 2003.] + + Revision [$Id: extraBddUnate.c,v 1.0 2003/09/01 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "extraBdd.h" + +ABC_NAMESPACE_IMPL_START + + +/*---------------------------------------------------------------------------*/ +/* Constant declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Stucture declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Type declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Variable declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Macro declarations */ +/*---------------------------------------------------------------------------*/ + +/**AutomaticStart*************************************************************/ + +/*---------------------------------------------------------------------------*/ +/* Static function prototypes */ +/*---------------------------------------------------------------------------*/ + +/**AutomaticEnd***************************************************************/ + +/*---------------------------------------------------------------------------*/ +/* Definition of exported functions */ +/*---------------------------------------------------------------------------*/ + + +/**Function******************************************************************** + + Synopsis [Computes the classical symmetry information for the function.] + + Description [Returns the symmetry information in the form of Extra_UnateInfo_t structure.] + + SideEffects [If the ZDD variables are not derived from BDD variables with + multiplicity 2, this function may derive them in a wrong way.] + + SeeAlso [] + +******************************************************************************/ +Extra_UnateInfo_t * Extra_UnateComputeFast( + DdManager * dd, /* the manager */ + DdNode * bFunc) /* the function whose symmetries are computed */ +{ + DdNode * bSupp; + DdNode * zRes; + Extra_UnateInfo_t * p; + + bSupp = Cudd_Support( dd, bFunc ); Cudd_Ref( bSupp ); + zRes = Extra_zddUnateInfoCompute( dd, bFunc, bSupp ); Cudd_Ref( zRes ); + + p = Extra_UnateInfoCreateFromZdd( dd, zRes, bSupp ); + + Cudd_RecursiveDeref( dd, bSupp ); + Cudd_RecursiveDerefZdd( dd, zRes ); + + return p; + +} /* end of Extra_UnateInfoCompute */ + + +/**Function******************************************************************** + + Synopsis [Computes the classical symmetry information as a ZDD.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * Extra_zddUnateInfoCompute( + DdManager * dd, /* the DD manager */ + DdNode * bF, + DdNode * bVars) +{ + DdNode * res; + do { + dd->reordered = 0; + res = extraZddUnateInfoCompute( dd, bF, bVars ); + } while (dd->reordered == 1); + return(res); + +} /* end of Extra_zddUnateInfoCompute */ + + +/**Function******************************************************************** + + Synopsis [Converts a set of variables into a set of singleton subsets.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * Extra_zddGetSingletonsBoth( + DdManager * dd, /* the DD manager */ + DdNode * bVars) /* the set of variables */ +{ + DdNode * res; + do { + dd->reordered = 0; + res = extraZddGetSingletonsBoth( dd, bVars ); + } while (dd->reordered == 1); + return(res); + +} /* end of Extra_zddGetSingletonsBoth */ + +/**Function******************************************************************** + + Synopsis [Allocates unateness information structure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +Extra_UnateInfo_t * Extra_UnateInfoAllocate( int nVars ) +{ + Extra_UnateInfo_t * p; + // allocate and clean the storage for unateness info + p = ABC_ALLOC( Extra_UnateInfo_t, 1 ); + memset( p, 0, sizeof(Extra_UnateInfo_t) ); + p->nVars = nVars; + p->pVars = ABC_ALLOC( Extra_UnateVar_t, nVars ); + memset( p->pVars, 0, nVars * sizeof(Extra_UnateVar_t) ); + return p; +} /* end of Extra_UnateInfoAllocate */ + +/**Function******************************************************************** + + Synopsis [Deallocates symmetry information structure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +void Extra_UnateInfoDissolve( Extra_UnateInfo_t * p ) +{ + ABC_FREE( p->pVars ); + ABC_FREE( p ); +} /* end of Extra_UnateInfoDissolve */ + +/**Function******************************************************************** + + Synopsis [Allocates symmetry information structure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +void Extra_UnateInfoPrint( Extra_UnateInfo_t * p ) +{ + char * pBuffer; + int i; + pBuffer = ABC_ALLOC( char, p->nVarsMax+1 ); + memset( pBuffer, ' ', p->nVarsMax ); + pBuffer[p->nVarsMax] = 0; + for ( i = 0; i < p->nVars; i++ ) + if ( p->pVars[i].Neg ) + pBuffer[ p->pVars[i].iVar ] = 'n'; + else if ( p->pVars[i].Pos ) + pBuffer[ p->pVars[i].iVar ] = 'p'; + else + pBuffer[ p->pVars[i].iVar ] = '.'; + printf( "%s\n", pBuffer ); + ABC_FREE( pBuffer ); +} /* end of Extra_UnateInfoPrint */ + + +/**Function******************************************************************** + + Synopsis [Creates the symmetry information structure from ZDD.] + + Description [ZDD representation of symmetries is the set of cubes, each + of which has two variables in the positive polarity. These variables correspond + to the symmetric variable pair.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +Extra_UnateInfo_t * Extra_UnateInfoCreateFromZdd( DdManager * dd, DdNode * zPairs, DdNode * bSupp ) +{ + Extra_UnateInfo_t * p; + DdNode * bTemp, * zSet, * zCube, * zTemp; + int * pMapVars2Nums; + int i, nSuppSize; + + nSuppSize = Extra_bddSuppSize( dd, bSupp ); + + // allocate and clean the storage for symmetry info + p = Extra_UnateInfoAllocate( nSuppSize ); + + // allocate the storage for the temporary map + pMapVars2Nums = ABC_ALLOC( int, dd->size ); + memset( pMapVars2Nums, 0, dd->size * sizeof(int) ); + + // assign the variables + p->nVarsMax = dd->size; + for ( i = 0, bTemp = bSupp; bTemp != b1; bTemp = cuddT(bTemp), i++ ) + { + p->pVars[i].iVar = bTemp->index; + pMapVars2Nums[bTemp->index] = i; + } + + // write the symmetry info into the structure + zSet = zPairs; Cudd_Ref( zSet ); +// Cudd_zddPrintCover( dd, zPairs ); printf( "\n" ); + while ( zSet != z0 ) + { + // get the next cube + zCube = Extra_zddSelectOneSubset( dd, zSet ); Cudd_Ref( zCube ); + + // add this var to the data structure + assert( cuddT(zCube) == z1 && cuddE(zCube) == z0 ); + if ( zCube->index & 1 ) // neg + p->pVars[ pMapVars2Nums[zCube->index/2] ].Neg = 1; + else + p->pVars[ pMapVars2Nums[zCube->index/2] ].Pos = 1; + // count the unate vars + p->nUnate++; + + // update the cuver and deref the cube + zSet = Cudd_zddDiff( dd, zTemp = zSet, zCube ); Cudd_Ref( zSet ); + Cudd_RecursiveDerefZdd( dd, zTemp ); + Cudd_RecursiveDerefZdd( dd, zCube ); + + } // for each cube + Cudd_RecursiveDerefZdd( dd, zSet ); + ABC_FREE( pMapVars2Nums ); + return p; + +} /* end of Extra_UnateInfoCreateFromZdd */ + + + +/**Function******************************************************************** + + Synopsis [Computes the classical unateness information for the function.] + + Description [Uses the naive way of comparing cofactors.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +Extra_UnateInfo_t * Extra_UnateComputeSlow( DdManager * dd, DdNode * bFunc ) +{ + int nSuppSize; + DdNode * bSupp, * bTemp; + Extra_UnateInfo_t * p; + int i, Res; + + // compute the support + bSupp = Cudd_Support( dd, bFunc ); Cudd_Ref( bSupp ); + nSuppSize = Extra_bddSuppSize( dd, bSupp ); +//printf( "Support = %d. ", nSuppSize ); +//Extra_bddPrint( dd, bSupp ); +//printf( "%d ", nSuppSize ); + + // allocate the storage for symmetry info + p = Extra_UnateInfoAllocate( nSuppSize ); + + // assign the variables + p->nVarsMax = dd->size; + for ( i = 0, bTemp = bSupp; bTemp != b1; bTemp = cuddT(bTemp), i++ ) + { + Res = Extra_bddCheckUnateNaive( dd, bFunc, bTemp->index ); + p->pVars[i].iVar = bTemp->index; + if ( Res == -1 ) + p->pVars[i].Neg = 1; + else if ( Res == 1 ) + p->pVars[i].Pos = 1; + p->nUnate += (Res != 0); + } + Cudd_RecursiveDeref( dd, bSupp ); + return p; + +} /* end of Extra_UnateComputeSlow */ + +/**Function******************************************************************** + + Synopsis [Checks if the two variables are symmetric.] + + Description [Returns 0 if vars are not unate. Return -1/+1 if the var is neg/pos unate.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Extra_bddCheckUnateNaive( + DdManager * dd, /* the DD manager */ + DdNode * bF, + int iVar) +{ + DdNode * bCof0, * bCof1; + int Res; + + assert( iVar < dd->size ); + + bCof0 = Cudd_Cofactor( dd, bF, Cudd_Not(Cudd_bddIthVar(dd,iVar)) ); Cudd_Ref( bCof0 ); + bCof1 = Cudd_Cofactor( dd, bF, Cudd_bddIthVar(dd,iVar) ); Cudd_Ref( bCof1 ); + + if ( Cudd_bddLeq( dd, bCof0, bCof1 ) ) + Res = 1; + else if ( Cudd_bddLeq( dd, bCof1, bCof0 ) ) + Res =-1; + else + Res = 0; + + Cudd_RecursiveDeref( dd, bCof0 ); + Cudd_RecursiveDeref( dd, bCof1 ); + return Res; +} /* end of Extra_bddCheckUnateNaive */ + + + +/*---------------------------------------------------------------------------*/ +/* Definition of internal functions */ +/*---------------------------------------------------------------------------*/ + +/**Function******************************************************************** + + Synopsis [Performs a recursive step of Extra_UnateInfoCompute.] + + Description [Returns the set of symmetric variable pairs represented as a set + of two-literal ZDD cubes. Both variables always appear in the positive polarity + in the cubes. This function works without building new BDD nodes. Some relatively + small number of ZDD nodes may be built to ensure proper bookkeeping of the + symmetry information.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * +extraZddUnateInfoCompute( + DdManager * dd, /* the manager */ + DdNode * bFunc, /* the function whose symmetries are computed */ + DdNode * bVars ) /* the set of variables on which this function depends */ +{ + DdNode * zRes; + DdNode * bFR = Cudd_Regular(bFunc); + + if ( cuddIsConstant(bFR) ) + { + if ( cuddIsConstant(bVars) ) + return z0; + return extraZddGetSingletonsBoth( dd, bVars ); + } + assert( bVars != b1 ); + + if ( (zRes = cuddCacheLookup2Zdd(dd, extraZddUnateInfoCompute, bFunc, bVars)) ) + return zRes; + else + { + DdNode * zRes0, * zRes1; + DdNode * zTemp, * zPlus; + DdNode * bF0, * bF1; + DdNode * bVarsNew; + int nVarsExtra; + int LevelF; + int AddVar; + + // every variable in bF should be also in bVars, therefore LevelF cannot be above LevelV + // if LevelF is below LevelV, scroll through the vars in bVars to the same level as F + // count how many extra vars are there in bVars + nVarsExtra = 0; + LevelF = dd->perm[bFR->index]; + for ( bVarsNew = bVars; LevelF > dd->perm[bVarsNew->index]; bVarsNew = cuddT(bVarsNew) ) + nVarsExtra++; + // the indexes (level) of variables should be synchronized now + assert( bFR->index == bVarsNew->index ); + + // cofactor the function + if ( bFR != bFunc ) // bFunc is complemented + { + bF0 = Cudd_Not( cuddE(bFR) ); + bF1 = Cudd_Not( cuddT(bFR) ); + } + else + { + bF0 = cuddE(bFR); + bF1 = cuddT(bFR); + } + + // solve subproblems + zRes0 = extraZddUnateInfoCompute( dd, bF0, cuddT(bVarsNew) ); + if ( zRes0 == NULL ) + return NULL; + cuddRef( zRes0 ); + + // if there is no symmetries in the negative cofactor + // there is no need to test the positive cofactor + if ( zRes0 == z0 ) + zRes = zRes0; // zRes takes reference + else + { + zRes1 = extraZddUnateInfoCompute( dd, bF1, cuddT(bVarsNew) ); + if ( zRes1 == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + return NULL; + } + cuddRef( zRes1 ); + + // only those variables are pair-wise symmetric + // that are pair-wise symmetric in both cofactors + // therefore, intersect the solutions + zRes = cuddZddIntersect( dd, zRes0, zRes1 ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + Cudd_RecursiveDerefZdd( dd, zRes1 ); + return NULL; + } + cuddRef( zRes ); + Cudd_RecursiveDerefZdd( dd, zRes0 ); + Cudd_RecursiveDerefZdd( dd, zRes1 ); + } + + // consider the current top-most variable + AddVar = -1; + if ( Cudd_bddLeq( dd, bF0, bF1 ) ) // pos + AddVar = 0; + else if ( Cudd_bddLeq( dd, bF1, bF0 ) ) // neg + AddVar = 1; + if ( AddVar >= 0 ) + { + // create the singleton + zPlus = cuddZddGetNode( dd, 2*bFR->index + AddVar, z1, z0 ); + if ( zPlus == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes ); + return NULL; + } + cuddRef( zPlus ); + + // add these to the result + zRes = cuddZddUnion( dd, zTemp = zRes, zPlus ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zTemp ); + Cudd_RecursiveDerefZdd( dd, zPlus ); + return NULL; + } + cuddRef( zRes ); + Cudd_RecursiveDerefZdd( dd, zTemp ); + Cudd_RecursiveDerefZdd( dd, zPlus ); + } + // only zRes is referenced at this point + + // if we skipped some variables, these variables cannot be symmetric with + // any variables that are currently in the support of bF, but they can be + // symmetric with the variables that are in bVars but not in the support of bF + for ( bVarsNew = bVars; LevelF > dd->perm[bVarsNew->index]; bVarsNew = cuddT(bVarsNew) ) + { + // create the negative singleton + zPlus = cuddZddGetNode( dd, 2*bVarsNew->index+1, z1, z0 ); + if ( zPlus == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes ); + return NULL; + } + cuddRef( zPlus ); + + // add these to the result + zRes = cuddZddUnion( dd, zTemp = zRes, zPlus ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zTemp ); + Cudd_RecursiveDerefZdd( dd, zPlus ); + return NULL; + } + cuddRef( zRes ); + Cudd_RecursiveDerefZdd( dd, zTemp ); + Cudd_RecursiveDerefZdd( dd, zPlus ); + + + // create the positive singleton + zPlus = cuddZddGetNode( dd, 2*bVarsNew->index, z1, z0 ); + if ( zPlus == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes ); + return NULL; + } + cuddRef( zPlus ); + + // add these to the result + zRes = cuddZddUnion( dd, zTemp = zRes, zPlus ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zTemp ); + Cudd_RecursiveDerefZdd( dd, zPlus ); + return NULL; + } + cuddRef( zRes ); + Cudd_RecursiveDerefZdd( dd, zTemp ); + Cudd_RecursiveDerefZdd( dd, zPlus ); + } + cuddDeref( zRes ); + + /* insert the result into cache */ + cuddCacheInsert2(dd, extraZddUnateInfoCompute, bFunc, bVars, zRes); + return zRes; + } +} /* end of extraZddUnateInfoCompute */ + + +/**Function******************************************************************** + + Synopsis [Performs a recursive step of Extra_zddGetSingletons.] + + Description [Returns the set of ZDD singletons, containing those pos/neg + polarity ZDD variables that correspond to the BDD variables in bVars.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * extraZddGetSingletonsBoth( + DdManager * dd, /* the DD manager */ + DdNode * bVars) /* the set of variables */ +{ + DdNode * zRes; + + if ( bVars == b1 ) + return z1; + + if ( (zRes = cuddCacheLookup1Zdd(dd, extraZddGetSingletonsBoth, bVars)) ) + return zRes; + else + { + DdNode * zTemp, * zPlus; + + // solve subproblem + zRes = extraZddGetSingletonsBoth( dd, cuddT(bVars) ); + if ( zRes == NULL ) + return NULL; + cuddRef( zRes ); + + + // create the negative singleton + zPlus = cuddZddGetNode( dd, 2*bVars->index+1, z1, z0 ); + if ( zPlus == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes ); + return NULL; + } + cuddRef( zPlus ); + + // add these to the result + zRes = cuddZddUnion( dd, zTemp = zRes, zPlus ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zTemp ); + Cudd_RecursiveDerefZdd( dd, zPlus ); + return NULL; + } + cuddRef( zRes ); + Cudd_RecursiveDerefZdd( dd, zTemp ); + Cudd_RecursiveDerefZdd( dd, zPlus ); + + + // create the positive singleton + zPlus = cuddZddGetNode( dd, 2*bVars->index, z1, z0 ); + if ( zPlus == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes ); + return NULL; + } + cuddRef( zPlus ); + + // add these to the result + zRes = cuddZddUnion( dd, zTemp = zRes, zPlus ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zTemp ); + Cudd_RecursiveDerefZdd( dd, zPlus ); + return NULL; + } + cuddRef( zRes ); + Cudd_RecursiveDerefZdd( dd, zTemp ); + Cudd_RecursiveDerefZdd( dd, zPlus ); + + cuddDeref( zRes ); + cuddCacheInsert1( dd, extraZddGetSingletonsBoth, bVars, zRes ); + return zRes; + } +} /* end of extraZddGetSingletonsBoth */ + + +/*---------------------------------------------------------------------------*/ +/* Definition of static Functions */ +/*---------------------------------------------------------------------------*/ +ABC_NAMESPACE_IMPL_END + diff --git a/src/bdd/extrab/module.make b/src/bdd/extrab/module.make new file mode 100644 index 00000000..38cdddb6 --- /dev/null +++ b/src/bdd/extrab/module.make @@ -0,0 +1,8 @@ +SRC += src/bdd/extrab/extraBddAuto.c \ + src/bdd/extrab/extraBddCas.c \ + src/bdd/extrab/extraBddImage.c \ + src/bdd/extrab/extraBddKmap.c \ + src/bdd/extrab/extraBddMisc.c \ + src/bdd/extrab/extraBddSymm.c \ + src/bdd/extrab/extraBddTime.c \ + src/bdd/extrab/extraBddUnate.c -- cgit v1.2.3