summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2011-09-18 17:28:00 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2011-09-18 17:28:00 -0700
commit81b040e61c80e7a2d977b5fcf6266ec3460e395c (patch)
tree56853c43548c01edcdc832efdf9331421433c527
parentf14f5c92032e0a50768723af857ed9de9c792161 (diff)
downloadabc-81b040e61c80e7a2d977b5fcf6266ec3460e395c.tar.gz
abc-81b040e61c80e7a2d977b5fcf6266ec3460e395c.tar.bz2
abc-81b040e61c80e7a2d977b5fcf6266ec3460e395c.zip
Fixed minor issues having to do with the number of BDD vars used.
-rw-r--r--src/aig/llb/llb4Nonlin.c8
-rw-r--r--src/misc/extra/extraBddMisc.c3
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 ) );
}