diff --git a/src/aig/gia/giaQbf.c b/src/aig/gia/giaQbf.c index 1525e7d831..8af8c6c6f0 100644 --- a/src/aig/gia/giaQbf.c +++ b/src/aig/gia/giaQbf.c @@ -23,6 +23,7 @@ #include "sat/bsat/satStore.h" #include "misc/extra/extra.h" #include "sat/glucose/AbcGlucose.h" +#include "sat/cadical/cadicalSolver.h" #include "misc/util/utilTruth.h" #include "base/io/ioResub.h" @@ -45,6 +46,7 @@ struct Qbf_Man_t_ sat_solver * pSatVer; // verification instance sat_solver * pSatSyn; // synthesis instance bmcg_sat_solver*pSatSynG; // synthesis instance + cadical_solver* pSatSynC; // synthesis instance Vec_Int_t * vValues; // variable values Vec_Int_t * vParMap; // parameter mapping Vec_Int_t * vLits; // literals for the SAT solver @@ -534,7 +536,7 @@ void Gia_QbfDumpFileInv( Gia_Man_t * pGia, int nPars ) SeeAlso [] ***********************************************************************/ -Qbf_Man_t * Gia_QbfAlloc( Gia_Man_t * pGia, int nPars, int fGlucose, int fVerbose ) +Qbf_Man_t * Gia_QbfAlloc( Gia_Man_t * pGia, int nPars, int fGlucose, int fCadical, int fVerbose ) { Qbf_Man_t * p; Cnf_Dat_t * pCnf; @@ -551,11 +553,13 @@ Qbf_Man_t * Gia_QbfAlloc( Gia_Man_t * pGia, int nPars, int fGlucose, int fVerbos p->pSatVer = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); p->pSatSyn = sat_solver_new(); p->pSatSynG = fGlucose ? bmcg_sat_solver_start() : NULL; + p->pSatSynC = fCadical ? cadical_solver_new() : NULL; p->vValues = Vec_IntAlloc( Gia_ManPiNum(pGia) ); p->vParMap = Vec_IntStartFull( nPars ); p->vLits = Vec_IntAlloc( nPars ); sat_solver_setnvars( p->pSatSyn, nPars ); if ( p->pSatSynG ) bmcg_sat_solver_set_nvars( p->pSatSynG, nPars ); + if ( p->pSatSynC ) cadical_solver_setnvars( p->pSatSynC, nPars ); Cnf_DataFree( pCnf ); return p; } @@ -564,6 +568,7 @@ void Gia_QbfFree( Qbf_Man_t * p ) sat_solver_delete( p->pSatVer ); sat_solver_delete( p->pSatSyn ); if ( p->pSatSynG ) bmcg_sat_solver_stop( p->pSatSynG ); + if ( p->pSatSynC ) cadical_solver_delete( p->pSatSynC ); Vec_IntFree( p->vLits ); Vec_IntFree( p->vValues ); Vec_IntFree( p->vParMap ); @@ -749,6 +754,21 @@ int Gia_QbfAddCofactorG( Qbf_Man_t * p, Gia_Man_t * pCof ) Cnf_DataFree( pCnf ); return 1; } +int Gia_QbfAddCofactorC( Qbf_Man_t * p, Gia_Man_t * pCof ) +{ + Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pCof, 8, 0, 1, 0, 0 ); + int i, iFirstVar = pCnf->nVars - Gia_ManPiNum(pCof); //-1 + pCnf->pMan = NULL; + Cnf_SpecialDataLift( pCnf, cadical_solver_nvars(p->pSatSynC), iFirstVar, iFirstVar + Gia_ManPiNum(p->pGia) ); + for ( i = 0; i < pCnf->nClauses; i++ ) + if ( !cadical_solver_addclause( p->pSatSynC, pCnf->pClauses[i], pCnf->pClauses[i+1] ) ) + { + Cnf_DataFree( pCnf ); + return 0; + } + Cnf_DataFree( pCnf ); + return 1; +} /**Function************************************************************* @@ -766,16 +786,20 @@ void Gia_QbfOnePattern( Qbf_Man_t * p, Vec_Int_t * vValues ) int i; Vec_IntClear( vValues ); for ( i = 0; i < p->nPars; i++ ) - Vec_IntPush( vValues, p->pSatSynG ? bmcg_sat_solver_read_cex_varvalue(p->pSatSynG, i) : sat_solver_var_value(p->pSatSyn, i) ); + Vec_IntPush( vValues, p->pSatSynC ? cadical_solver_get_var_value(p->pSatSynC, i) : + p->pSatSynG ? bmcg_sat_solver_read_cex_varvalue(p->pSatSynG, i) : sat_solver_var_value(p->pSatSyn, i) ); } void Gia_QbfPrint( Qbf_Man_t * p, Vec_Int_t * vValues, int Iter ) { printf( "%5d : ", Iter ); assert( Vec_IntSize(vValues) == p->nVars ); Vec_IntPrintBinary( vValues ); printf( " " ); - printf( "Var =%7d ", p->pSatSynG ? bmcg_sat_solver_varnum(p->pSatSynG) : sat_solver_nvars(p->pSatSyn) ); - printf( "Cla =%7d ", p->pSatSynG ? bmcg_sat_solver_clausenum(p->pSatSynG) : sat_solver_nclauses(p->pSatSyn) ); - printf( "Conf =%9d ", p->pSatSynG ? bmcg_sat_solver_conflictnum(p->pSatSynG) : sat_solver_nconflicts(p->pSatSyn) ); + printf( "Var =%7d ", p->pSatSynC ? cadical_solver_nvars(p->pSatSynC) : + p->pSatSynG ? bmcg_sat_solver_varnum(p->pSatSynG) : sat_solver_nvars(p->pSatSyn) ); + printf( "Cla =%7d ", p->pSatSynC ? cadical_solver_nclauses(p->pSatSynC) : + p->pSatSynG ? bmcg_sat_solver_clausenum(p->pSatSynG) : sat_solver_nclauses(p->pSatSyn) ); + printf( "Conf =%9d ", p->pSatSynC ? cadical_solver_nconflicts(p->pSatSynC) : + p->pSatSynG ? bmcg_sat_solver_conflictnum(p->pSatSynG) : sat_solver_nconflicts(p->pSatSyn) ); Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart ); } @@ -869,9 +893,9 @@ void Gia_QbfLearnConstraint( Qbf_Man_t * p, Vec_Int_t * vValues ) SeeAlso [] ***********************************************************************/ -int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, int nTimeOut, int nEncVars, int fGlucose, int fVerbose ) +int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, int nTimeOut, int nEncVars, int fGlucose, int fCadical, int fVerbose ) { - Qbf_Man_t * p = Gia_QbfAlloc( pGia, nPars, fGlucose, fVerbose ); + Qbf_Man_t * p = Gia_QbfAlloc( pGia, nPars, fGlucose, fCadical, fVerbose ); Gia_Man_t * pCof; int i, status, RetValue = 0; abctime clk; @@ -886,12 +910,15 @@ int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, i // generate next constraint assert( Vec_IntSize(p->vValues) == p->nVars ); pCof = Gia_QbfCofactor( pGia, nPars, p->vValues, p->vParMap ); - status = p->pSatSynG ? Gia_QbfAddCofactorG( p, pCof ) : Gia_QbfAddCofactor( p, pCof ); + status = p->pSatSynC ? Gia_QbfAddCofactorC( p, pCof ) : + p->pSatSynG ? Gia_QbfAddCofactorG( p, pCof ) : Gia_QbfAddCofactor( p, pCof ); Gia_ManStop( pCof ); if ( status == 0 ) { RetValue = 1; break; } // synthesize next assignment clk = Abc_Clock(); - if ( p->pSatSynG ) + if ( p->pSatSynC ) + status = cadical_solver_solve( p->pSatSynC, NULL, NULL, 0, 0, 0, 0 ); + else if ( p->pSatSynG ) status = bmcg_sat_solver_solve( p->pSatSynG, NULL, 0 ); else status = sat_solver_solve( p->pSatSyn, NULL, NULL, (ABC_INT64_T)nConfLimit, 0, 0, 0 ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index e9a21e0d88..f5b00ee849 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -51058,7 +51058,7 @@ int Abc_CommandAbc9Qbf( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern void Gia_QbfDumpFile( Gia_Man_t * pGia, int nPars ); extern void Gia_QbfDumpFileInv( Gia_Man_t * pGia, int nPars ); - extern int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, int nTimeOut, int nEncVars, int fGlucose, int fVerbose ); + extern int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, int nTimeOut, int nEncVars, int fGlucose, int fCadical, int fVerbose ); int c, nPars = -1; int nIterLimit = 0; int nConfLimit = 0; @@ -51067,9 +51067,10 @@ int Abc_CommandAbc9Qbf( Abc_Frame_t * pAbc, int argc, char ** argv ) int fDumpCnf = 0; int fDumpCnf2 = 0; int fGlucose = 0; + int fCadical = 0; int fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "PICTKdegvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "PICTKdegcvh" ) ) != EOF ) { switch ( c ) { @@ -51137,6 +51138,9 @@ int Abc_CommandAbc9Qbf( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'g': fGlucose ^= 1; break; + case 'c': + fCadical ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -51171,11 +51175,11 @@ int Abc_CommandAbc9Qbf( Abc_Frame_t * pAbc, int argc, char ** argv ) else if ( fDumpCnf2 ) Gia_QbfDumpFileInv( pAbc->pGia, nPars ); else - Gia_QbfSolve( pAbc->pGia, nPars, nIterLimit, nConfLimit, nTimeOut, nEncVars, fGlucose, fVerbose ); + Gia_QbfSolve( pAbc->pGia, nPars, nIterLimit, nConfLimit, nTimeOut, nEncVars, fGlucose, fCadical, fVerbose ); return 0; usage: - Abc_Print( -2, "usage: &qbf [-PICTK num] [-degvh]\n" ); + Abc_Print( -2, "usage: &qbf [-PICTK num] [-degcvh]\n" ); Abc_Print( -2, "\t solves QBF problem EpVxM(p,x)\n" ); Abc_Print( -2, "\t-P num : number of parameters p (should be the first PIs) [default = %d]\n", nPars ); Abc_Print( -2, "\t-I num : quit after the given iteration even if unsolved [default = %d]\n", nIterLimit ); @@ -51185,6 +51189,7 @@ int Abc_CommandAbc9Qbf( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -2, "\t-d : toggle dumping QDIMACS file instead of solving (complemented QBF) [default = %s]\n", fDumpCnf? "yes": "no" ); Abc_Print( -2, "\t-e : toggle dumping QDIMACS file instead of solving (original QBF) [default = %s]\n", fDumpCnf2? "yes": "no" ); Abc_Print( -2, "\t-g : toggle using Glucose 3.0 by Gilles Audemard and Laurent Simon [default = %s]\n", fGlucose? "yes": "no" ); + Abc_Print( -2, "\t-c : toggle using CaDiCaL by Armin Biere [default = %s]\n", fCadical? "yes": "no" ); Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n\n"); Abc_Print( -2, "\t As an example of using this command, consider specification (the three-input AND-gate) and implementation\n"); diff --git a/src/sat/cadical/cadical.hpp b/src/sat/cadical/cadical.hpp index c9ed413328..64a5d9ef79 100644 --- a/src/sat/cadical/cadical.hpp +++ b/src/sat/cadical/cadical.hpp @@ -982,6 +982,10 @@ class Solver { // static void build (FILE *file, const char *prefix = "c "); + // Extra APIs + int clauses (); + int conflicts (); + private: //==== start of state ==================================================== diff --git a/src/sat/cadical/cadicalSolver.c b/src/sat/cadical/cadicalSolver.c index bf6df9512b..dee2beaf38 100644 --- a/src/sat/cadical/cadicalSolver.c +++ b/src/sat/cadical/cadicalSolver.c @@ -261,6 +261,36 @@ int cadical_solver_get_var_value(cadical_solver* s, int v) { return ccadical_val((CCaDiCaL*)s->p, v + 1) > 0; } +/**Function************************************************************* + + Synopsis [get number of clauses] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int cadical_solver_nclauses(cadical_solver* s) { + return ccadical_clauses((CCaDiCaL*)s->p); +} + +/**Function************************************************************* + + Synopsis [get number of conflicts] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int cadical_solver_nconflicts(cadical_solver* s) { + return ccadical_conflicts((CCaDiCaL*)s->p); +} + /**Function************************************************************* diff --git a/src/sat/cadical/cadicalSolver.h b/src/sat/cadical/cadicalSolver.h index 0192ada3c0..2aec06c2ab 100644 --- a/src/sat/cadical/cadicalSolver.h +++ b/src/sat/cadical/cadicalSolver.h @@ -65,6 +65,8 @@ extern int cadical_solver_nvars(cadical_solver* s); extern int cadical_solver_addvar(cadical_solver* s); 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 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 ae5c1093f1..ccc616c80c 100644 --- a/src/sat/cadical/cadical_ccadical.cpp +++ b/src/sat/cadical/cadical_ccadical.cpp @@ -208,4 +208,12 @@ int ccadical_is_inconsistent(CCaDiCaL *ptr) { return ((Wrapper *) ptr)->solver->inconsistent (); } +int ccadical_clauses(CCaDiCaL *ptr) { + return ((Wrapper *) ptr)->solver->clauses (); +} + +int ccadical_conflicts(CCaDiCaL *ptr) { + return ((Wrapper *) ptr)->solver->conflicts (); +} + ABC_NAMESPACE_IMPL_END diff --git a/src/sat/cadical/cadical_solver.cpp b/src/sat/cadical/cadical_solver.cpp index df051f4dea..84d350cf25 100644 --- a/src/sat/cadical/cadical_solver.cpp +++ b/src/sat/cadical/cadical_solver.cpp @@ -1759,6 +1759,16 @@ void Solver::error (const char *fmt, ...) { va_end (ap); } +/*------------------------------------------------------------------------*/ + +int Solver::clauses () { + return internal->stats.added.total; +} + +int Solver::conflicts () { + return internal->stats.conflicts; +} + } // namespace CaDiCaL ABC_NAMESPACE_IMPL_END diff --git a/src/sat/cadical/ccadical.h b/src/sat/cadical/ccadical.h index ec5292a79d..d4c2ce8f0c 100644 --- a/src/sat/cadical/ccadical.h +++ b/src/sat/cadical/ccadical.h @@ -58,6 +58,8 @@ int ccadical_reserve_difference (CCaDiCaL *, int number_of_vars); void ccadical_reserve(CCaDiCaL *, int min_max_var); int ccadical_is_inconsistent(CCaDiCaL *); +int ccadical_clauses(CCaDiCaL *); +int ccadical_conflicts(CCaDiCaL *); /*------------------------------------------------------------------------*/