diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/base/abci/abc.c | 4 | ||||
| -rw-r--r-- | src/base/abci/abcCollapse.c | 21 | ||||
| -rw-r--r-- | src/sat/bmc/bmcClp.c | 4 |
3 files changed, 16 insertions, 13 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 9b62c622..c1f7eb5a 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -3102,8 +3102,8 @@ usage: int Abc_CommandSatClp( Abc_Frame_t * pAbc, int argc, char ** argv ) { Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc), * pNtkRes; - int nCubeLim = 1000; - int nBTLimit = 1000000; + int nCubeLim = 0; + int nBTLimit = 1000000; int nCostMax = 20000000; int fCanon = 0; int fReverse = 0; diff --git a/src/base/abci/abcCollapse.c b/src/base/abci/abcCollapse.c index e6618e15..dad22e2b 100644 --- a/src/base/abci/abcCollapse.c +++ b/src/base/abci/abcCollapse.c @@ -431,16 +431,19 @@ Abc_Ntk_t * Abc_NtkFromSops( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int n // order CO nodes by support size vCoNodes = Abc_NtkCreateCoOrder( pNtk, vSupps ); // compute cost of the largest node - pNode = (Abc_Obj_t *)Vec_PtrEntry( vCoNodes, 0 ); - vDfsNodes = Abc_NtkDfsNodes( pNtk, &pNode, 1 ); - vLevel = Vec_WecEntry( vSupps, Abc_ObjFaninId0(pNode) ); - Cost = Vec_PtrSize(vDfsNodes) * Vec_IntSize(vLevel) * nCubeLim; - Vec_PtrFree( vDfsNodes ); - if ( Cost > nCostMax ) + if ( nCubeLim > 0 ) { - Vec_PtrFree( vCoNodes ); - Vec_WecFree( vSupps ); - return NULL; + pNode = (Abc_Obj_t *)Vec_PtrEntry( vCoNodes, 0 ); + vDfsNodes = Abc_NtkDfsNodes( pNtk, &pNode, 1 ); + vLevel = Vec_WecEntry( vSupps, Abc_ObjFaninId0(pNode) ); + Cost = Vec_PtrSize(vDfsNodes) * Vec_IntSize(vLevel) * nCubeLim; + Vec_PtrFree( vDfsNodes ); + if ( Cost > nCostMax ) + { + Vec_PtrFree( vCoNodes ); + Vec_WecFree( vSupps ); + return NULL; + } } // collect CO IDs in this order vNodeCoIds = Vec_IntAlloc( Abc_NtkCoNum(pNtk) ); diff --git a/src/sat/bmc/bmcClp.c b/src/sat/bmc/bmcClp.c index d1ce061b..81f81063 100644 --- a/src/sat/bmc/bmcClp.c +++ b/src/sat/bmc/bmcClp.c @@ -450,7 +450,7 @@ Vec_Str_t * Bmc_CollapseOneInt( Gia_Man_t * p, int nCubeLim, int nBTLimit, int f if ( status == l_False ) break; // check number of cubes - if ( Count == nCubeLim ) + if ( nCubeLim > 0 && Count == nCubeLim ) { //printf( "The number of cubes exceeded the limit (%d).\n", nCubeLim ); Vec_StrFreeP( &vSop ); @@ -622,7 +622,7 @@ Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCan } // compute cube pairs - for ( iCube = 0; iCube < nCubeLim; iCube++ ) + for ( iCube = 0; nCubeLim == 0 || iCube < nCubeLim; iCube++ ) { for ( n = 0; n < 2; n++ ) { |