Improvements to the SAT solver.

3 files changed, 15 insertions, 8 deletions

diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c
index 45f56cf0..80a4b853 100644
--- a/src/proof/cec/cecSatG2.c
+++ b/src/proof/cec/cecSatG2.c
@@ -1196,7 +1196,7 @@ int Cec4_ManCandIterNext( Cec4_Man_t * p )
     while ( Vec_IntSize(p->vCands) > 0 )
     {
         int fStop, iCand = Vec_IntEntry( p->vCands, p->iPosRead );
-        if ( fStop = (Gia_ObjRepr(p->pAig, iCand) != GIA_VOID) )
+        if ( (fStop = (Gia_ObjRepr(p->pAig, iCand) != GIA_VOID)) )
             Vec_IntWriteEntry( p->vCands, p->iPosWrite++, iCand );
         if ( ++p->iPosRead == Vec_IntSize(p->vCands) )
         {
@@ -1273,7 +1273,7 @@ void Cec4_ManSatSolverRecycle( Cec4_Man_t * p )
 int Cec4_ManSolveTwo( Cec4_Man_t * p, int iObj0, int iObj1, int fPhase, int * pfEasy, int fVerbose )
 {
     abctime clk;
-    int nBTLimit = Vec_BitEntry(p->vFails, iObj0) || Vec_BitEntry(p->vFails, iObj1) ? p->pPars->nBTLimit/10 : p->pPars->nBTLimit;
+    int nBTLimit = (Vec_BitEntry(p->vFails, iObj0) || Vec_BitEntry(p->vFails, iObj1)) ? p->pPars->nBTLimit/10 : p->pPars->nBTLimit;
     int nConfEnd, nConfBeg, status, iVar0, iVar1, Lits[2];
     int UnsatConflicts[3] = {0};
     if ( iObj1 <  iObj0 ) 
@@ -1385,7 +1385,7 @@ int Cec4_ManSweepNode( Cec4_Man_t * p, int iObj, int iRepr )
         assert( p->pAig->iPatsPi > 0 && p->pAig->iPatsPi < 64 * p->pAig->nSimWords );
         //Vec_IntForEachEntryDouble( &p->pNew->vCopiesTwo, IdAig, IdSat, i )
         //    Cec4_ObjSimSetInputBit( p->pAig, IdAig, sat_solver_read_cex_varvalue(p->pSat, IdSat) );
-        pCex = NULL;//sat_solver_read_cex( p->pSat );
+        pCex = sat_solver_read_cex( p->pSat );
         Vec_IntClear( p->vPat );
         if ( pCex == NULL )
         {
diff --git a/src/sat/glucose2/Glucose2.cpp b/src/sat/glucose2/Glucose2.cpp
index f32d1210..aa3d361f 100644
--- a/src/sat/glucose2/Glucose2.cpp
+++ b/src/sat/glucose2/Glucose2.cpp
@@ -1153,6 +1153,13 @@ lbool Solver::search(int nof_conflicts)
 
     for (;;){
         CRef confl = propagate();
+
+        // exact conflict limit
+        if ( !withinBudget() && confl != CRef_Undef ) {
+          lbdQueue.fastclear();
+          cancelUntil(0);
+          return l_Undef; }
+
         if (confl != CRef_Undef){
 
             // CONFLICT
@@ -1395,15 +1402,15 @@ printf("c ==================================[ Search Statistics (every %6d confl
 
     if (status == l_True){
 
-        if( justUsage() && false ){
+        if( justUsage() ){
           assert(jheap.empty());
           //JustModel.growTo(nVars());
-          int i = 0;
+          int i = 0, j = 0;
           JustModel.push(toLit(0));
           for (; i < trail.size(); i++) 
             if( isRoundWatch(var(trail[i])) && !isTwoFanin(var(trail[i])) )
-              JustModel.push(trail[i]);
-          JustModel[0] = toLit(i);
+              JustModel.push(trail[i]), j++;
+          JustModel[0] = toLit(j);
         } else {
           // Extend & copy model:
           model.growTo(nVars());
diff --git a/src/sat/glucose2/Solver.h b/src/sat/glucose2/Solver.h
index ab73dbc5..26b3bdcb 100644
--- a/src/sat/glucose2/Solver.h
+++ b/src/sat/glucose2/Solver.h
@@ -546,7 +546,7 @@ inline int      Solver::nClauses      ()      const   { return clauses.size(); }
 inline int      Solver::nLearnts      ()      const   { return learnts.size(); }
 inline int      Solver::nVars         ()      const   { return vardata.size(); }
 inline int      Solver::nFreeVars     ()      const   { return (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]); }
-inline int *    Solver::getCex        ()      const   { return NULL; }
+inline int *    Solver::getCex        ()      const   { return (int*) &JustModel[0]; }
 inline void     Solver::setPolarity   (Var v, bool b) { polarity[v] = b; }
 inline void     Solver::setDecisionVar(Var v, bool b) 
 {