diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-10-31 16:41:25 -0400 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-10-31 16:41:25 -0400 |
| commit | 695231148faf8651b0299db234607cc545b962d3 (patch) | |
| tree | 766651ee5855b4e93402e67916e6c14ef0fc6902 /src/sat/bmc/bmcICheck.c | |
| parent | 313caa456a4b15af0673c6729d7eeb299544a13e (diff) | |
| download | abc-695231148faf8651b0299db234607cc545b962d3.tar.gz abc-695231148faf8651b0299db234607cc545b962d3.tar.bz2 abc-695231148faf8651b0299db234607cc545b962d3.zip | |
Specialized induction check.
Diffstat (limited to 'src/sat/bmc/bmcICheck.c')
| -rw-r--r-- | src/sat/bmc/bmcICheck.c | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/sat/bmc/bmcICheck.c b/src/sat/bmc/bmcICheck.c index 61d42f29..d7048c21 100644 --- a/src/sat/bmc/bmcICheck.c +++ b/src/sat/bmc/bmcICheck.c @@ -170,6 +170,8 @@ void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fVerbos { iVar0 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj)]; iVar1 = Vec_IntEntry( vLits, i ); + if ( iVar1 == -1 ) + continue; sat_solver_add_buffer( pSat, iVar0, iVar1, 0 ); } // add equality clauses for the COs @@ -204,6 +206,7 @@ void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fVerbos sat_solver_compress( pSat ); while ( 1 ) { +// sat_solver_bookmark( pSat ); 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 ) { @@ -226,6 +229,7 @@ void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fVerbos if ( nLits == Vec_IntSize(vLits) ) break; break; +// sat_solver_rollback( pSat ); // add another large OR clause Vec_IntClear( vLits ); @@ -235,7 +239,7 @@ void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fVerbos // create new literals Vec_IntClear( vLits ); for ( i = 0; i < nLits; i++ ) - Vec_IntPush( vLits, pLits[i] ); + Vec_IntPush( vLits, Abc_LitNot(pLits[i]) ); } sat_solver_delete( pSat ); |