Merge pull request #443 from MyskYko/fix4

QBF using CaDiCaL

Author: alanminko

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 );

src/base/abci/abc.c

@@ -51291,7 +51291,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;
@@ -51300,9 +51300,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 )
         {
@@ -51370,6 +51371,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;
@@ -51404,11 +51408,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 );
@@ -51418,6 +51422,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"); 

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 ====================================================
 

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*************************************************************
 

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

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

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

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 *);
 
 /*------------------------------------------------------------------------*/