diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-09-18 17:28:00 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-09-18 17:28:00 -0700 |
| commit | 81b040e61c80e7a2d977b5fcf6266ec3460e395c (patch) | |
| tree | 56853c43548c01edcdc832efdf9331421433c527 /src | |
| parent | f14f5c92032e0a50768723af857ed9de9c792161 (diff) | |
| download | abc-81b040e61c80e7a2d977b5fcf6266ec3460e395c.tar.gz abc-81b040e61c80e7a2d977b5fcf6266ec3460e395c.tar.bz2 abc-81b040e61c80e7a2d977b5fcf6266ec3460e395c.zip | |
Fixed minor issues having to do with the number of BDD vars used.
Diffstat (limited to 'src')
| -rw-r--r-- | src/aig/llb/llb4Nonlin.c | 8 | ||||
| -rw-r--r-- | src/misc/extra/extraBddMisc.c | 3 |
2 files changed, 7 insertions, 4 deletions
diff --git a/src/aig/llb/llb4Nonlin.c b/src/aig/llb/llb4Nonlin.c index 05898165..8d096b20 100644 --- a/src/aig/llb/llb4Nonlin.c +++ b/src/aig/llb/llb4Nonlin.c @@ -923,6 +923,7 @@ void Llb_Nonlin4Reorder( DdManager * dd, int fTwice, int fVerbose ) Llb_Mnx_t * Llb_MnxStart( Aig_Man_t * pAig, Gia_ParLlb_t * pPars ) { Llb_Mnx_t * p; + p = ABC_CALLOC( Llb_Mnx_t, 1 ); p->pAig = pAig; p->pPars = pPars; @@ -944,7 +945,7 @@ Llb_Mnx_t * Llb_MnxStart( Aig_Man_t * pAig, Gia_ParLlb_t * pPars ) { // p->vOrder = Llb_Nonlin4CreateOrderSimple( pAig ); p->vOrder = Llb_Nonlin4CreateOrder( pAig ); - p->dd = Cudd_Init( Vec_IntSize(p->vOrder), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); + p->dd = Cudd_Init( Vec_IntCountPositive(p->vOrder) + 1, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); Cudd_AutodynEnable( p->dd, CUDD_REORDER_SYMM_SIFT ); Cudd_SetMaxGrowth( p->dd, 1.05 ); // set the stop time parameter @@ -1055,6 +1056,11 @@ int Llb_Nonlin4CoreReach( Aig_Man_t * pAig, Gia_ParLlb_t * pPars ) int RetValue = -1; if ( pPars->fVerbose ) Aig_ManPrintStats( pAig ); + if ( pPars->fCluster && Aig_ManObjNum(pAig) >= (1 << 15) ) + { + printf( "The number of objects is more than 2^15. Clustering cannot be used.\n" ); + return RetValue; + } if ( !pPars->fSkipReach ) { int clk = clock(); diff --git a/src/misc/extra/extraBddMisc.c b/src/misc/extra/extraBddMisc.c index 7d63980a..0bc4a8c5 100644 --- a/src/misc/extra/extraBddMisc.c +++ b/src/misc/extra/extraBddMisc.c @@ -1707,9 +1707,6 @@ cuddBddPermuteRecur( DdManager * manager /* DD manager */ , /* If problem already solved, look up answer and return. */ if ( N->ref != 1 && ( res = cuddHashTableLookup1( table, N ) ) != NULL ) { -#ifdef DD_DEBUG - bddPermuteRecurHits++; -#endif return ( Cudd_NotCond( res, N != node ) ); } |