Bug fix in Glucose integration.

4 files changed, 78 insertions, 27 deletions

diff --git a/src/sat/glucose/AbcGlucose.cpp b/src/sat/glucose/AbcGlucose.cpp
index 9011665a..f4bc41b7 100644
--- a/src/sat/glucose/AbcGlucose.cpp
+++ b/src/sat/glucose/AbcGlucose.cpp
@@ -28,6 +28,7 @@
 
 #include "aig/gia/gia.h"
 #include "sat/cnf/cnf.h"
+#include "misc/extra/extra.h"
 
 using namespace Gluco;
 
@@ -46,7 +47,6 @@ extern "C" {
 ////////////////////////////////////////////////////////////////////////
 
 #ifdef USE_SIMP_SOLVER
-
     
 /**Function*************************************************************
 
@@ -547,7 +547,57 @@ void glucose_print_stats(SimpSolver& s, abctime clk)
   SeeAlso     []
 
 ***********************************************************************/
-void Glucose_SolveCnf( char * pFilename, Glucose_Pars * pPars )
+void Glucose_ReadDimacs( char * pFileName, SimpSolver& s )
+{
+    vec<Lit> * lits = &s.user_lits;
+    char * pBuffer = Extra_FileReadContents( pFileName );
+    char * pTemp; int fComp, Var, VarMax = 0;
+    lits->clear();
+    for ( pTemp = pBuffer; *pTemp; pTemp++ )
+    {
+        if ( *pTemp == 'c' || *pTemp == 'p' ) {
+            while ( *pTemp != '\n' )
+                pTemp++;
+            continue;
+        }
+        while ( *pTemp == ' ' || *pTemp == '\t' || *pTemp == '\r' || *pTemp == '\n' )
+            pTemp++;
+        fComp = 0;
+        if ( *pTemp == '-' )
+            fComp = 1, pTemp++;
+        if ( *pTemp == '+' )
+            pTemp++;
+        Var = atoi( pTemp );
+        if ( Var == 0 ) {
+            if ( lits->size() > 0 ) {
+                s.addVar( VarMax );
+                s.addClause(*lits);
+                lits->clear();
+            }
+        }
+        else {
+            Var--;
+            VarMax = Abc_MaxInt( VarMax, Var );
+            lits->push( toLit(Abc_Var2Lit(Var, fComp)) );
+        }
+        while ( *pTemp >= '0' && *pTemp <= '9' )
+            pTemp++;
+    }
+    ABC_FREE( pBuffer );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Glucose_SolveCnf( char * pFileName, Glucose_Pars * pPars )
 {
     abctime clk = Abc_Clock();
 
@@ -555,9 +605,10 @@ void Glucose_SolveCnf( char * pFilename, Glucose_Pars * pPars )
     S.verbosity = pPars->verb;
     S.setConfBudget( pPars->nConfls > 0 ? (int64_t)pPars->nConfls : -1 );
 
-    gzFile in = gzopen(pFilename, "rb");
-    parse_DIMACS(in, S);
-    gzclose(in);
+//    gzFile in = gzopen(pFilename, "rb");
+//    parse_DIMACS(in, S);
+//    gzclose(in);
+    Glucose_ReadDimacs( pFileName, S );
 
     if ( pPars->verb )
     {
@@ -570,7 +621,7 @@ void Glucose_SolveCnf( char * pFilename, Glucose_Pars * pPars )
     if ( pPars->pre ) S.eliminate(true);
 
     vec<Lit> dummy;
-    lbool ret = S.solveLimited(dummy);
+    lbool ret = S.solveLimited(dummy, 0);
     if ( pPars->verb ) glucose_print_stats(S, Abc_Clock() - clk);
     printf(ret == l_True ? "SATISFIABLE" : ret == l_False ? "UNSATISFIABLE" : "INDETERMINATE");
     Abc_PrintTime( 1, "      Time", Abc_Clock() - clk );
@@ -587,23 +638,17 @@ void Glucose_SolveCnf( char * pFilename, Glucose_Pars * pPars )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Glucose_SolverFromAig( Gia_Man_t * p, SimpSolver& S )
+Vec_Int_t * Glucose_SolverFromAig( Gia_Man_t * p, SimpSolver& s )
 {
     abctime clk = Abc_Clock();
-    int * pLit, * pStop, i;
+    vec<Lit> * lits = &s.user_lits;
     Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8 /*nLutSize*/, 0 /*fCnfObjIds*/, 1/*fAddOrCla*/, 0, 0/*verbose*/ );
-    for ( i = 0; i < pCnf->nClauses; i++ )
+    for ( int i = 0; i < pCnf->nClauses; i++ )
     {
-        vec<Lit> lits;
-        for ( pLit = pCnf->pClauses[i], pStop = pCnf->pClauses[i+1]; pLit < pStop; pLit++ )
-        {
-            int Lit = *pLit;
-            int parsed_lit = (Lit & 1)? -(Lit >> 1)-1 : (Lit >> 1)+1;
-            int var = abs(parsed_lit)-1;
-            while (var >= S.nVars()) S.newVar();
-            lits.push( (parsed_lit > 0) ? mkLit(var) : ~mkLit(var) );
-        }
-        S.addClause(lits);
+        lits->clear();
+        for ( int * pLit = pCnf->pClauses[i]; pLit < pCnf->pClauses[i+1]; pLit++ )
+            lits->push( toLit(*pLit) ), s.addVar( *pLit >> 1 );
+        s.addClause(*lits);
     }
     Vec_Int_t * vCnfIds = Vec_IntAllocArrayCopy(pCnf->pVarNums,pCnf->nVars);
     printf( "CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
diff --git a/src/sat/glucose/Glucose.cpp b/src/sat/glucose/Glucose.cpp
index 8d520474..2a67d903 100644
--- a/src/sat/glucose/Glucose.cpp
+++ b/src/sat/glucose/Glucose.cpp
@@ -209,7 +209,7 @@ Var Solver::newVar(bool sign, bool dvar)
     //activity .push(0);
     activity .push(rnd_init_act ? drand(random_seed) * 0.00001 : 0);
     seen     .push(0);
-    permDiff  .push(0);
+    permDiff .push(0);
     polarity .push(sign);
     decision .push();
     trail    .capacity(v+1);
@@ -226,7 +226,7 @@ bool Solver::addClause_(vec<Lit>& ps)
 
     if ( 0 ) {
         for ( int i = 0; i < ps.size(); i++ )
-            printf( "%d ", toInt(ps[i]) );
+            printf( "%s%d ", (toInt(ps[i]) & 1) ? "-":"", toInt(ps[i]) >> 1 );
         printf( "\n" );
     }
 
diff --git a/src/sat/glucose/SimpSolver.h b/src/sat/glucose/SimpSolver.h
index 8daf99d1..260ab5e3 100644
--- a/src/sat/glucose/SimpSolver.h
+++ b/src/sat/glucose/SimpSolver.h
@@ -40,6 +40,7 @@ class SimpSolver : public Solver {
     // Problem specification:
     //
     Var     newVar    (bool polarity = true, bool dvar = true);
+    void    addVar    (Var v);               
     bool    addClause (const vec<Lit>& ps);
     bool    addEmptyClause();                // Add the empty clause to the solver.
     bool    addClause (Lit p);               // Add a unit clause to the solver.
@@ -193,6 +194,8 @@ inline bool SimpSolver::solve        (const vec<Lit>& assumps, bool do_simp, boo
 inline lbool SimpSolver::solveLimited (const vec<Lit>& assumps, bool do_simp, bool turn_off_simp){ 
     assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp); }
 
+inline void SimpSolver::addVar(Var v) { while (v >= nVars()) newVar(); }
+
 //=================================================================================================
 }
 
diff --git a/src/sat/glucose/Solver.h b/src/sat/glucose/Solver.h
index 3a90f847..bb4c6d0f 100644
--- a/src/sat/glucose/Solver.h
+++ b/src/sat/glucose/Solver.h
@@ -61,10 +61,12 @@ public:
     int * pstop;                         // another callback
     uint64_t nRuntimeLimit;              // runtime limit
     vec<int> user_vec;
+    vec<Lit> user_lits;
 
     // Problem specification:
     //
     Var     newVar    (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode.
+    void    addVar    (Var v);                                  // Add enough variables to make sure there is variable v.
 
     bool    addClause (const vec<Lit>& ps);                     // Add a clause to the solver. 
     bool    addEmptyClause();                                   // Add the empty clause, making the solver contradictory.
@@ -129,7 +131,7 @@ public:
 
     // Memory managment:
     //
-    /*virtual*/ void garbageCollect(); // virtuality causes segfault for some reason
+    virtual void garbageCollect(); // virtuality causes segfault for some reason
     void    checkGarbage(double gf);
     void    checkGarbage();
 
@@ -393,7 +395,7 @@ inline bool     Solver::addEmptyClause  ()                      { add_tmp.clear(
 inline bool     Solver::addClause       (Lit p)                 { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp); }
 inline bool     Solver::addClause       (Lit p, Lit q)          { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp); }
 inline bool     Solver::addClause       (Lit p, Lit q, Lit r)   { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp); }
- inline bool     Solver::locked          (const Clause& c) const { 
+inline bool     Solver::locked          (const Clause& c) const { 
    if(c.size()>2) 
      return value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && ca.lea(reason(var(c[0]))) == &c; 
    return 
@@ -444,11 +446,12 @@ inline bool     Solver::solve         (const vec<Lit>& assumps){ budgetOff(); as
 inline lbool    Solver::solveLimited  (const vec<Lit>& assumps){ assumps.copyTo(assumptions); return solve_(); }
 inline bool     Solver::okay          ()      const   { return ok; }
 
-inline void     Solver::toDimacs     (const char* file){ vec<Lit> as; toDimacs(file, as); }
-inline void     Solver::toDimacs     (const char* file, Lit p){ vec<Lit> as; as.push(p); toDimacs(file, as); }
-inline void     Solver::toDimacs     (const char* file, Lit p, Lit q){ vec<Lit> as; as.push(p); as.push(q); toDimacs(file, as); }
-inline void     Solver::toDimacs     (const char* file, Lit p, Lit q, Lit r){ vec<Lit> as; as.push(p); as.push(q); as.push(r); toDimacs(file, as); }
+inline void     Solver::toDimacs      (const char* file){ vec<Lit> as; toDimacs(file, as); }
+inline void     Solver::toDimacs      (const char* file, Lit p){ vec<Lit> as; as.push(p); toDimacs(file, as); }
+inline void     Solver::toDimacs      (const char* file, Lit p, Lit q){ vec<Lit> as; as.push(p); as.push(q); toDimacs(file, as); }
+inline void     Solver::toDimacs      (const char* file, Lit p, Lit q, Lit r){ vec<Lit> as; as.push(p); as.push(q); as.push(r); toDimacs(file, as); }
 
+inline void     Solver::addVar(Var v) { while (v >= nVars()) newVar(); }
 
 //=================================================================================================
 // Debug etc: