Integrating Glucose into &qbf.

1 files changed, 32 insertions, 9 deletions

diff --git a/src/aig/gia/giaQbf.c b/src/aig/gia/giaQbf.c
index 2dfd83fc..5917a3ef 100644
--- a/src/aig/gia/giaQbf.c
+++ b/src/aig/gia/giaQbf.c
@@ -22,6 +22,7 @@
 #include "sat/cnf/cnf.h"
 #include "sat/bsat/satStore.h"
 #include "misc/extra/extra.h"
+#include "sat/glucose/AbcGlucose.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -41,6 +42,7 @@ struct Qbf_Man_t_
     int             iParVarBeg;     // SAT var ID of the first par variable in the ver solver
     sat_solver *    pSatVer;        // verification instance
     sat_solver *    pSatSyn;        // synthesis instance
+    bmcg_sat_solver*pSatSynG;       // synthesis instance
     Vec_Int_t *     vValues;        // variable values
     Vec_Int_t *     vParMap;        // parameter mapping
     Vec_Int_t *     vLits;          // literals for the SAT solver
@@ -284,7 +286,7 @@ void Gia_QbfDumpFile( Gia_Man_t * pGia, int nPars )
   SeeAlso     []
 
 ***********************************************************************/
-Qbf_Man_t * Gia_QbfAlloc( Gia_Man_t * pGia, int nPars, int fVerbose )
+Qbf_Man_t * Gia_QbfAlloc( Gia_Man_t * pGia, int nPars, int fGlucose, int fVerbose )
 {
     Qbf_Man_t * p;
     Cnf_Dat_t * pCnf;
@@ -300,10 +302,12 @@ Qbf_Man_t * Gia_QbfAlloc( Gia_Man_t * pGia, int nPars, int fVerbose )
     p->iParVarBeg = pCnf->nVars - Gia_ManPiNum(pGia);// - 1;
     p->pSatVer    = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
     p->pSatSyn    = sat_solver_new();
+    p->pSatSynG   = fGlucose ? bmcg_sat_solver_start() : 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 );
     Cnf_DataFree( pCnf );
     return p;
 }
@@ -311,6 +315,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 );
     Vec_IntFree( p->vLits );
     Vec_IntFree( p->vValues );
     Vec_IntFree( p->vParMap );
@@ -481,6 +486,21 @@ int Gia_QbfAddCofactor( Qbf_Man_t * p, Gia_Man_t * pCof )
                 return 0;
     return 1;
 }
+int Gia_QbfAddCofactorG( 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, bmcg_sat_solver_varnum(p->pSatSynG), iFirstVar, iFirstVar + Gia_ManPiNum(p->pGia) );
+    for ( i = 0; i < pCnf->nClauses; i++ )
+        if ( !bmcg_sat_solver_addclause( p->pSatSynG, pCnf->pClauses[i], pCnf->pClauses[i+1]-pCnf->pClauses[i] ) )
+        {
+            Cnf_DataFree( pCnf );
+            return 0;
+        }
+    Cnf_DataFree( pCnf );
+    return 1;
+}
 
 /**Function*************************************************************
 
@@ -498,16 +518,16 @@ 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, sat_solver_var_value(p->pSatSyn, i) );
+        Vec_IntPush( vValues, 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 = %6d  ", sat_solver_nvars(p->pSatSyn) );
-    printf( "Cla = %6d  ", sat_solver_nclauses(p->pSatSyn) );
-    printf( "Conf = %6d  ", sat_solver_nconflicts(p->pSatSyn) );
+    printf( "Var = %6d  ",  p->pSatSynG ? bmcg_sat_solver_varnum(p->pSatSynG)      : sat_solver_nvars(p->pSatSyn)      );
+    printf( "Cla = %6d  ",  p->pSatSynG ? bmcg_sat_solver_clausenum(p->pSatSynG)   : sat_solver_nclauses(p->pSatSyn)   );
+    printf( "Conf = %6d  ", p->pSatSynG ? bmcg_sat_solver_conflictnum(p->pSatSynG) : sat_solver_nconflicts(p->pSatSyn) );
     Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
 }
 
@@ -601,9 +621,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 fVerbose )
+int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, int nTimeOut, int fGlucose, int fVerbose )
 {
-    Qbf_Man_t * p = Gia_QbfAlloc( pGia, nPars, fVerbose );
+    Qbf_Man_t * p = Gia_QbfAlloc( pGia, nPars, fGlucose, fVerbose );
     Gia_Man_t * pCof;
     int i, status, RetValue = 0;
     abctime clk;
@@ -618,12 +638,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 = Gia_QbfAddCofactor( p, pCof );
+        status = 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();
-        status = sat_solver_solve( p->pSatSyn, NULL, NULL, (ABC_INT64_T)nConfLimit, 0, 0, 0 );
+        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 );
         p->clkSat += Abc_Clock() - clk;
         if ( fVerbose )
             Gia_QbfPrint( p, p->vValues, i );