diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-08-16 11:55:10 +0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-08-16 11:55:10 +0700 |
| commit | 6ff66ed49e004900854fb3507385f3392240e1f5 (patch) | |
| tree | a8f12301847b044549a913f5fd164479eeb20774 /src/sat/bmc | |
| parent | 443776fed7471d4a0840bb67e64eb833a70a46ba (diff) | |
| download | abc-6ff66ed49e004900854fb3507385f3392240e1f5.tar.gz abc-6ff66ed49e004900854fb3507385f3392240e1f5.tar.bz2 abc-6ff66ed49e004900854fb3507385f3392240e1f5.zip | |
Changing enconding of the SAT solver return value in &bmcs.
Diffstat (limited to 'src/sat/bmc')
| -rw-r--r-- | src/sat/bmc/bmcBmcS.c | 16 |
1 files changed, 11 insertions, 5 deletions
diff --git a/src/sat/bmc/bmcBmcS.c b/src/sat/bmc/bmcBmcS.c index 231c4161..1366ce31 100644 --- a/src/sat/bmc/bmcBmcS.c +++ b/src/sat/bmc/bmcBmcS.c @@ -28,13 +28,19 @@ #ifdef ABC_USE_EXT_SOLVERS #include "extsat/bmc/bmcApi.h" + #define l_Undef -1 + #define l_True 1 + #define l_False 0 #else + #define l_Undef 0 + #define l_True 1 + #define l_False -1 #define bmc_sat_solver satoko_t #define bmc_sat_solver_start(type) satoko_create() #define bmc_sat_solver_stop satoko_destroy #define bmc_sat_solver_addclause satoko_add_clause #define bmc_sat_solver_addvar(s) satoko_add_variable(s, 0) - #define bmc_sat_solver_solve satoko_solve_with_assumptions + #define bmc_sat_solver_solve satoko_solve_assumptions #define bmc_sat_solver_read_cex_varvalue solver_read_cex_varvalue #define bmc_sat_solver_setstop solver_set_stop #endif @@ -635,7 +641,7 @@ int Bmcs_ManPerformOne( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) if ( pPars->nTimeOut && (Abc_Clock() - clkStart)/CLOCKS_PER_SEC >= pPars->nTimeOut ) break; status = bmc_sat_solver_solve( p->pSats[0], &iLit, 1 ); - if ( status == 1 ) // unsat + if ( status == l_False ) // unsat { if ( i == Gia_ManPoNum(pGia)-1 ) Bmcs_ManPrintFrame( p, f+k, nClauses, -1, clkStart ); @@ -643,7 +649,7 @@ int Bmcs_ManPerformOne( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) pPars->pFuncOnFrameDone(f+k, i, 0); continue; } - if ( status == 0 ) // sat + if ( status == l_True ) // sat { RetValue = 0; pPars->iFrame = f+k; @@ -820,7 +826,7 @@ int Bmcs_ManPerformMulti( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) if ( pPars->nTimeOut && (Abc_Clock() - clkStart)/CLOCKS_PER_SEC >= pPars->nTimeOut ) break; status = Bmcs_ManPerform_Solve( p, iLit, WorkerThread, ThData, pPars->nProcs, &Solver ); - if ( status == 1 ) // unsat + if ( status == l_False ) // unsat { if ( i == Gia_ManPoNum(pGia)-1 ) Bmcs_ManPrintFrame( p, f+k, nClauses, Solver, clkStart ); @@ -828,7 +834,7 @@ int Bmcs_ManPerformMulti( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) pPars->pFuncOnFrameDone(f+k, i, 0); continue; } - if ( status == 0 ) // sat + if ( status == l_True ) // sat { RetValue = 0; pPars->iFrame = f+k; |