diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-11-05 21:17:32 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-11-05 21:17:32 -0800 |
| commit | f29fe2d0c226b33505e544e4560f9357cfed66f0 (patch) | |
| tree | 7ef1bdcc1f73e69059d76100e0833ffbc589b28f /src | |
| parent | 78a0660eabed2e05476dc660f1a09c205d7ee230 (diff) | |
| download | abc-f29fe2d0c226b33505e544e4560f9357cfed66f0.tar.gz abc-f29fe2d0c226b33505e544e4560f9357cfed66f0.tar.bz2 abc-f29fe2d0c226b33505e544e4560f9357cfed66f0.zip | |
Specialized inductive check.
Diffstat (limited to 'src')
| -rw-r--r-- | src/sat/bmc/bmcICheck.c | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/src/sat/bmc/bmcICheck.c b/src/sat/bmc/bmcICheck.c index ff6340f6..c70ed9b3 100644 --- a/src/sat/bmc/bmcICheck.c +++ b/src/sat/bmc/bmcICheck.c @@ -228,10 +228,10 @@ void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fEmpty, // collect positive literals vLits = Vec_IntAlloc( Gia_ManCoNum(p) ); for ( i = 0; i < Gia_ManRegNum(p); i++ ) - Vec_IntPush( vLits, Abc_Var2Lit(i, 0) ); + Vec_IntPush( vLits, Abc_Var2Lit(i, fEmpty) ); // iteratively compute a minimal M-inductive set of next-state functions - nLitsUsed = Vec_IntSize(vLits); + nLitsUsed = fEmpty ? 0 : Vec_IntSize(vLits); vUsed = Vec_IntAlloc( Vec_IntSize(vLits) ); while ( 1 ) { @@ -239,10 +239,7 @@ void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fEmpty, // derive SAT solver pSat = Bmc_DeriveSolver( p, pMiter, pCnf, nFramesMax, nTimeOut, fVerbose ); // sat_solver_bookmark( pSat ); - if ( fEmpty ) - status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); - else - status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); if ( status == l_Undef ) { printf( "Timeout reached after %d seconds.\n", nTimeOut ); |