diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 998b3e16b..b5362ec36 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -30691,7 +30691,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; Saig_ParBmcSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "SFTHGCDJIPQRLWaxdursgvzh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "SFTHGCDJIPQRLWaxdursgvzhc" ) ) != EOF ) { switch ( c ) { @@ -30866,6 +30866,9 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'g': pPars->fUseGlucose ^= 1; break; + case 'c': + pPars->fUseCadical ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -30960,6 +30963,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -2, "\t-r : toggle disabling periodic restarts [default = %s]\n", pPars->fNoRestarts? "yes": "no" ); Abc_Print( -2, "\t-s : toggle using Satoko by Bruno Schmitt [default = %s]\n", pPars->fUseSatoko? "yes": "no" ); Abc_Print( -2, "\t-g : toggle using Glucose 3.0 by Gilles Audemard and Laurent Simon [default = %s]\n",pPars->fUseGlucose? "yes": "no" ); + Abc_Print( -2, "\t-c : toggle using CaDiCaL by Armin Biere, University of Freiburg [default = %s]\n",pPars->fUseCadical? "yes": "no" ); Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-z : toggle suppressing report about solved outputs [default = %s]\n", pPars->fNotVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index 1e6d51a24..265c6ebc5 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -134,6 +134,7 @@ struct Saig_ParBmc_t_ int fNoRestarts; // disables periodic restarts int fUseSatoko; // enables using Satoko int fUseGlucose; // enables using Glucose 3.0 + int fUseCadical; // enables using CaDiCaL int nLearnedStart; // starting learned clause limit int nLearnedDelta; // delta of learned clause limit int nLearnedPerce; // ratio of learned clause limit diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c index 7e0a6cfdc..a6d5bc594 100644 --- a/src/sat/bmc/bmcBmc3.c +++ b/src/sat/bmc/bmcBmc3.c @@ -23,12 +23,21 @@ #include "sat/bsat/satStore.h" #include "sat/satoko/satoko.h" #include "sat/glucose/AbcGlucose.h" +#include "sat/cadical/cadicalSolver.h" +#include "sat/cadical/ccadical.h" #include "misc/vec/vecHsh.h" #include "misc/vec/vecWec.h" #include "bmc.h" ABC_NAMESPACE_IMPL_START +static inline void Bmc3_CadicalSetRuntimeLimit( cadical_solver * pSat4, abctime nSeconds ) +{ + if ( pSat4 == NULL || nSeconds <= 0 ) + return; + ccadical_limit( (CCaDiCaL *)pSat4->p, "seconds", nSeconds ); +} + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -64,6 +73,7 @@ struct Gia_ManBmc_t_ sat_solver * pSat; // SAT solver satoko_t * pSat2; // SAT solver bmcg_sat_solver * pSat3; // SAT solver + cadical_solver * pSat4; // SAT solver int nSatVars; // SAT variables int nObjNums; // SAT objects int nWordNum; // unsigned words for ternary simulation @@ -718,7 +728,7 @@ Vec_Int_t * Saig_ManBmcComputeMappingRefs( Aig_Man_t * p, Vec_Int_t * vMap ) SeeAlso [] ***********************************************************************/ -Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig, int nTimeOutOne, int nConfLimit, int fUseSatoko, int fUseGlucose ) +Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig, int nTimeOutOne, int nConfLimit, int fUseSatoko, int fUseGlucose, int fUseCadical ) { Gia_ManBmc_t * p; Aig_Obj_t * pObj; @@ -763,6 +773,11 @@ Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig, int nTimeOutOne, int nConfLi for ( i = 0; i < 1000; i++ ) bmcg_sat_solver_addvar( p->pSat3 ); } + else if ( fUseCadical ) + { + p->pSat4 = cadical_solver_new(); + cadical_solver_setnvars(p->pSat4, 1000); + } else { p->pSat = sat_solver_new(); @@ -806,9 +821,9 @@ void Saig_Bmc3ManStop( Gia_ManBmc_t * p ) p->pSat ? p->pSat->nLearntDelta : 0, p->pSat ? p->pSat->nLearntRatio : 0, p->pSat ? p->pSat->nDBreduces : 0, - p->pSat ? sat_solver_nvars(p->pSat) : p->pSat3 ? bmcg_sat_solver_varnum(p->pSat3) : satoko_varnum(p->pSat2), + p->pSat ? sat_solver_nvars(p->pSat) : p->pSat4 ? cadical_solver_nvars(p->pSat4) : p->pSat3 ? bmcg_sat_solver_varnum(p->pSat3) : satoko_varnum(p->pSat2), nUsedVars, - 100.0*nUsedVars/(p->pSat ? sat_solver_nvars(p->pSat) : p->pSat3 ? bmcg_sat_solver_varnum(p->pSat3) : satoko_varnum(p->pSat2)) ); + 100.0*nUsedVars/(p->pSat ? sat_solver_nvars(p->pSat) : p->pSat4 ? cadical_solver_nvars(p->pSat4) : p->pSat3 ? bmcg_sat_solver_varnum(p->pSat3) : satoko_varnum(p->pSat2)) ); Abc_Print( 1, "Buffs = %d. Dups = %d. Hash hits = %d. Hash misses = %d. UniProps = %d.\n", p->nBufNum, p->nDupNum, p->nHashHit, p->nHashMiss, p->nUniProps ); } @@ -830,6 +845,7 @@ void Saig_Bmc3ManStop( Gia_ManBmc_t * p ) if ( p->pSat ) sat_solver_delete( p->pSat ); if ( p->pSat2 ) satoko_destroy( p->pSat2 ); if ( p->pSat3 ) bmcg_sat_solver_stop( p->pSat3 ); + if ( p->pSat4 ) cadical_solver_delete( p->pSat4 ); ABC_FREE( p->pTime4Outs ); Vec_IntFree( p->vData ); Hsh_IntManStop( p->vHash ); @@ -1029,6 +1045,11 @@ static inline void Saig_ManBmcAddClauses( Gia_ManBmc_t * p, int uTruth, int Lits if ( !bmcg_sat_solver_addclause( p->pSat3, ClaLits, nClaLits ) ) assert( 0 ); } + else if ( p->pSat4 ) + { + if ( !cadical_solver_addclause( p->pSat4, ClaLits, ClaLits+nClaLits ) ) + assert( 0 ); + } else { if ( !sat_solver_addclause( p->pSat, ClaLits, ClaLits+nClaLits ) ) @@ -1287,6 +1308,11 @@ int Saig_ManBmcCreateCnf( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame ) for ( i = bmcg_sat_solver_varnum(p->pSat3); i < p->nSatVars; i++ ) bmcg_sat_solver_addvar( p->pSat3 ); } + else if ( p->pSat4 ) + { + for ( i = cadical_solver_nvars(p->pSat4); i < p->nSatVars; i++ ) + cadical_solver_addvar( p->pSat4 ); + } else sat_solver_setnvars( p->pSat, p->nSatVars ); return Lit; @@ -1411,6 +1437,11 @@ Abc_Cex_t * Saig_ManGenerateCex( Gia_ManBmc_t * p, int f, int i ) if ( iLit != ~0 && bmcg_sat_solver_read_cex_varvalue(p->pSat3, lit_var(iLit)) ) Abc_InfoSetBit( pCex->pData, iBit + k ); } + else if ( p->pSat4) + { + if ( iLit != ~0 && cadical_solver_get_var_value(p->pSat4, lit_var(iLit)) ) + Abc_InfoSetBit( pCex->pData, iBit + k ); + } else { if ( iLit != ~0 && sat_solver_var_value(p->pSat, lit_var(iLit)) ) @@ -1445,6 +1476,10 @@ int Saig_ManCallSolver( Gia_ManBmc_t * p, int Lit ) bmcg_sat_solver_set_conflict_budget( p->pSat3, p->pPars->nConfLimit ); return bmcg_sat_solver_solve( p->pSat3, &Lit, 1 ); } + else if ( p->pSat4 ) + { + return cadical_solver_solve( p->pSat4, &Lit, &Lit + 1, (ABC_INT64_T)p->pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + } else return sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)p->pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); } @@ -1482,7 +1517,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) nTimeToStopNG = pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0; nTimeToStop = Saig_ManBmcTimeToStop( pPars, nTimeToStopNG ); // create BMC manager - p = Saig_Bmc3ManStart( pAig, pPars->nTimeOutOne, pPars->nConfLimit, pPars->fUseSatoko, pPars->fUseGlucose ); + p = Saig_Bmc3ManStart( pAig, pPars->nTimeOutOne, pPars->nConfLimit, pPars->fUseSatoko, pPars->fUseGlucose, pPars->fUseCadical ); p->pPars = pPars; if ( p->pSat ) { @@ -1498,6 +1533,10 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) { // satoko_set_runid(p->pSat3, p->pPars->RunId); // satoko_set_stop_func(p->pSat3, p->pPars->pFuncStop); + } + else if ( p->pSat4 ) + { + } else { @@ -1522,6 +1561,8 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) satoko_set_runtime_limit( p->pSat2, nTimeToStop ); else if ( p->pSat3 ) bmcg_sat_solver_set_runtime_limit( p->pSat3, nTimeToStop ); + else if ( p-> pSat4 ) + Bmc3_CadicalSetRuntimeLimit( p->pSat4, nTimeToStop ); else sat_solver_set_runtime_limit( p->pSat, nTimeToStop ); } @@ -1659,6 +1700,8 @@ clkOther += Abc_Clock() - clk2; satoko_set_runtime_limit( p->pSat2, p->pTime4Outs[i] + Abc_Clock() ); else if ( p->pSat3 ) bmcg_sat_solver_set_runtime_limit( p->pSat3, p->pTime4Outs[i] + Abc_Clock() ); + else if ( p-> pSat4 ) + Bmc3_CadicalSetRuntimeLimit( p->pSat4, p->pTime4Outs[i] + Abc_Clock() ); else sat_solver_set_runtime_limit( p->pSat, p->pTime4Outs[i] + Abc_Clock() ); } @@ -1690,6 +1733,8 @@ nTimeUnsat += clkSatRun; status = satoko_add_clause( p->pSat2, &Lit, 1 ); else if ( p->pSat3 ) status = bmcg_sat_solver_addclause( p->pSat3, &Lit, 1 ); + else if ( p->pSat4 ) + status = cadical_solver_addclause( p->pSat4, &Lit, &Lit + 1 ); else status = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ); assert( status ); @@ -1721,12 +1766,12 @@ nTimeSat += clkSatRun; { Abc_Print( 1, "%4d %s : ", f, fUnfinished ? "-" : "+" ); Abc_Print( 1, "Var =%8.0f. ", (double)p->nSatVars ); - Abc_Print( 1, "Cla =%9.0f. ", (double)(p->pSat ? p->pSat->stats.clauses : p->pSat3 ? bmcg_sat_solver_clausenum(p->pSat3) : satoko_clausenum(p->pSat2)) ); - Abc_Print( 1, "Conf =%7.0f. ", (double)(p->pSat ? p->pSat->stats.conflicts : p->pSat3 ? bmcg_sat_solver_conflictnum(p->pSat3) : satoko_conflictnum(p->pSat2)) ); + Abc_Print( 1, "Cla =%9.0f. ", (double)(p->pSat ? p->pSat->stats.clauses : p->pSat4 ? cadical_solver_nclauses(p->pSat4) : p->pSat3 ? bmcg_sat_solver_clausenum(p->pSat3) : satoko_clausenum(p->pSat2)) ); + Abc_Print( 1, "Conf =%7.0f. ", (double)(p->pSat ? p->pSat->stats.conflicts : p->pSat4 ? cadical_solver_nconflicts(p->pSat4) : p->pSat3 ? bmcg_sat_solver_conflictnum(p->pSat3) : satoko_conflictnum(p->pSat2)) ); // Abc_Print( 1, "Imp =%10.0f. ", (double)p->pSat->stats.propagations ); // Abc_Print( 1, "Uni =%7.0f. ",(double)(p->pSat ? sat_solver_count_assigned(p->pSat) : 0) ); // ABC_PRT( "Time", Abc_Clock() - clk ); - Abc_Print( 1, "Learn =%7.0f. ", (double)(p->pSat ? p->pSat->stats.learnts : p->pSat3 ? bmcg_sat_solver_learntnum(p->pSat3) : satoko_learntnum(p->pSat2)) ); + Abc_Print( 1, "Learn =%7.0f. ", (double)(p->pSat ? p->pSat->stats.learnts : p->pSat4 ? cadical_solver_nlearned(p->pSat4) : p->pSat3 ? bmcg_sat_solver_learntnum(p->pSat3) : satoko_learntnum(p->pSat2)) ); Abc_Print( 1, "%4.0f MB", 4.25*(f+1)*p->nObjNums /(1<<20) ); Abc_Print( 1, "%4.0f MB", 1.0*(p->pSat ? sat_solver_memory(p->pSat) : 0)/(1<<20) ); Abc_Print( 1, "%9.2f sec ", (float)(Abc_Clock() - clkTotal)/(float)(CLOCKS_PER_SEC) ); @@ -1773,6 +1818,8 @@ nTimeSat += clkSatRun; satoko_set_runtime_limit( p->pSat2, nTimeToStop ); else if ( p->pSat3 ) bmcg_sat_solver_set_runtime_limit( p->pSat3, nTimeToStop ); + else if ( p->pSat4 ) + Bmc3_CadicalSetRuntimeLimit ( p->pSat4, nTimeToStop ); else sat_solver_set_runtime_limit( p->pSat, nTimeToStop ); } @@ -1798,6 +1845,11 @@ nTimeSat += clkSatRun; if ( bmcg_sat_solver_read_cex_varvalue(p->pSat3, lit_var(Lit)) == Abc_LitIsCompl(Lit) ) continue; } + else if (p->pSat4) + { + if ( cadical_solver_get_var_value(p->pSat4, lit_var(Lit)) == Abc_LitIsCompl(Lit) ) + continue; + } else { if ( sat_solver_var_value(p->pSat, lit_var(Lit)) == Abc_LitIsCompl(Lit) ) @@ -1841,7 +1893,7 @@ nTimeUndec += clkSatRun; } if ( pPars->fVerbose ) { - if ( fFirst == 1 && f > 0 && (p->pSat ? p->pSat->stats.conflicts : p->pSat3 ? bmcg_sat_solver_conflictnum(p->pSat3) : satoko_conflictnum(p->pSat2)) > 1 ) + if ( fFirst == 1 && f > 0 && (p->pSat ? p->pSat->stats.conflicts : p->pSat4 ? cadical_solver_nconflicts(p->pSat4) : p->pSat3 ? bmcg_sat_solver_conflictnum(p->pSat3) : satoko_conflictnum(p->pSat2)) > 1 ) { fFirst = 0; // Abc_Print( 1, "Outputs of frames up to %d are trivially UNSAT.\n", f ); @@ -1849,11 +1901,11 @@ nTimeUndec += clkSatRun; Abc_Print( 1, "%4d %s : ", f, fUnfinished ? "-" : "+" ); Abc_Print( 1, "Var =%8.0f. ", (double)p->nSatVars ); // Abc_Print( 1, "Used =%8.0f. ", (double)sat_solver_count_usedvars(p->pSat) ); - Abc_Print( 1, "Cla =%9.0f. ", (double)(p->pSat ? p->pSat->stats.clauses : p->pSat3 ? bmcg_sat_solver_clausenum(p->pSat3) : satoko_clausenum(p->pSat2)) ); - Abc_Print( 1, "Conf =%7.0f. ",(double)(p->pSat ? p->pSat->stats.conflicts : p->pSat3 ? bmcg_sat_solver_conflictnum(p->pSat3) : satoko_conflictnum(p->pSat2)) ); + Abc_Print( 1, "Cla =%9.0f. ", (double)(p->pSat ? p->pSat->stats.clauses : p->pSat4 ? cadical_solver_nclauses(p->pSat4) : p->pSat3 ? bmcg_sat_solver_clausenum(p->pSat3) : satoko_clausenum(p->pSat2)) ); + Abc_Print( 1, "Conf =%7.0f. ",(double)(p->pSat ? p->pSat->stats.conflicts : p->pSat4 ? cadical_solver_nconflicts(p->pSat4) : p->pSat3 ? bmcg_sat_solver_conflictnum(p->pSat3) : satoko_conflictnum(p->pSat2)) ); // Abc_Print( 1, "Imp =%10.0f. ", (double)p->pSat->stats.propagations ); // Abc_Print( 1, "Uni =%7.0f. ", (double)(p->pSat ? sat_solver_count_assigned(p->pSat) : 0) ); - Abc_Print( 1, "Learn =%7.0f. ", (double)(p->pSat ? p->pSat->stats.learnts : p->pSat3 ? bmcg_sat_solver_learntnum(p->pSat3) : satoko_learntnum(p->pSat2)) ); + Abc_Print( 1, "Learn =%7.0f. ", (double)(p->pSat ? p->pSat->stats.learnts : p->pSat4 ? cadical_solver_nlearned(p->pSat4) : p->pSat3 ? bmcg_sat_solver_learntnum(p->pSat3) : satoko_learntnum(p->pSat2)) ); if ( pPars->fSolveAll ) Abc_Print( 1, "CEX =%5d. ", pPars->nFailOuts ); if ( pPars->nTimeOutOne ) diff --git a/src/sat/cadical/cadical.hpp b/src/sat/cadical/cadical.hpp index 7ceedcec4..4ef09e0c4 100644 --- a/src/sat/cadical/cadical.hpp +++ b/src/sat/cadical/cadical.hpp @@ -1058,6 +1058,7 @@ class Solver { // Extra APIs int clauses (); int conflicts (); + int learned (); private: //==== start of state ==================================================== diff --git a/src/sat/cadical/cadicalSolver.c b/src/sat/cadical/cadicalSolver.c index f27fe19f9..30cd6c68c 100644 --- a/src/sat/cadical/cadicalSolver.c +++ b/src/sat/cadical/cadicalSolver.c @@ -297,6 +297,21 @@ int cadical_solver_nconflicts(cadical_solver* s) { return ccadical_conflicts((CCaDiCaL*)s->p); } +/**Function************************************************************* + + Synopsis [get number of learned clauses] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int cadical_solver_nlearned(cadical_solver* s) { + return ccadical_learned((CCaDiCaL*)s->p); +} + /**Function************************************************************* diff --git a/src/sat/cadical/cadicalSolver.h b/src/sat/cadical/cadicalSolver.h index 2aec06c2a..9e6394ff5 100644 --- a/src/sat/cadical/cadicalSolver.h +++ b/src/sat/cadical/cadicalSolver.h @@ -67,6 +67,7 @@ extern void cadical_solver_setnvars(cadical_solver* s,int n); extern int cadical_solver_get_var_value(cadical_solver* s, int v); extern int cadical_solver_nclauses(cadical_solver* s); extern int cadical_solver_nconflicts(cadical_solver* s); +extern int cadical_solver_nlearned(cadical_solver* s); extern Vec_Int_t * cadical_solve_cnf( Cnf_Dat_t * pCnf, char * pArgs, int nConfs, int nTimeLimit, int fSat, int fUnsat, int fPrintCex, int fVerbose ); ABC_NAMESPACE_HEADER_END diff --git a/src/sat/cadical/cadical_ccadical.cpp b/src/sat/cadical/cadical_ccadical.cpp index 3b61a0373..a929a4743 100644 --- a/src/sat/cadical/cadical_ccadical.cpp +++ b/src/sat/cadical/cadical_ccadical.cpp @@ -228,4 +228,8 @@ int ccadical_conflicts(CCaDiCaL *ptr) { return ((Wrapper *) ptr)->solver->conflicts (); } +int ccadical_learned(CCaDiCaL *ptr) { + return ((Wrapper *) ptr)->solver->learned (); +} + ABC_NAMESPACE_IMPL_END diff --git a/src/sat/cadical/cadical_solver.cpp b/src/sat/cadical/cadical_solver.cpp index 7dd03e8be..0efeddaa8 100644 --- a/src/sat/cadical/cadical_solver.cpp +++ b/src/sat/cadical/cadical_solver.cpp @@ -1853,6 +1853,10 @@ int Solver::conflicts () { return internal->stats.conflicts; } +int Solver::learned () { + return internal->stats.learned.clauses; +} + } // namespace CaDiCaL ABC_NAMESPACE_IMPL_END diff --git a/src/sat/cadical/ccadical.h b/src/sat/cadical/ccadical.h index ef442e7a3..b4401305c 100644 --- a/src/sat/cadical/ccadical.h +++ b/src/sat/cadical/ccadical.h @@ -63,6 +63,7 @@ void ccadical_resize(CCaDiCaL *, int min_max_var); int ccadical_is_inconsistent(CCaDiCaL *); int ccadical_clauses(CCaDiCaL *); int ccadical_conflicts(CCaDiCaL *); +int ccadical_learned(CCaDiCaL *); /*------------------------------------------------------------------------*/