From f29fe2d0c226b33505e544e4560f9357cfed66f0 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 5 Nov 2013 21:17:32 -0800 Subject: Specialized inductive check. --- src/sat/bmc/bmcICheck.c | 9 +++------ 1 file 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 ); -- cgit v1.2.3