Adding support for reading wrong assumptions

diff --git a/glucose-syrup/core/Solver.h b/glucose-syrup/core/Solver.h
index 63d531615697437459ac5ec74c0b677617a1930f..b0cd3b004a90faa9d78eb12ceecec93900427051 100644 (file)
--- a/glucose-syrup/core/Solver.h
+++ b/glucose-syrup/core/Solver.h
@@ -135,6 +135,7 @@ public:
     int     nClauses   ()      const;       // The current number of original clauses.
     int     nLearnts   ()      const;       // The current number of learnt clauses.
     int     nVars      ()      const;       // The current number of variables.
     int     nClauses   ()      const;       // The current number of original clauses.
     int     nLearnts   ()      const;       // The current number of learnt clauses.
     int     nVars      ()      const;       // The current number of variables.

+    int     assumptionsSize      ()      const;       // The current number of variables.

     int     nFreeVars  ()      const;
 
     inline char valuePhase(Var v) {return polarity[v];}
     int     nFreeVars  ()      const;
 
     inline char valuePhase(Var v) {return polarity[v];}


@@ -477,6 +478,7 @@ inline int      Solver::nAssigns      ()      const   { return trail.size(); }
 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::nClauses      ()      const   { return clauses.size(); }
 inline int      Solver::nLearnts      ()      const   { return learnts.size(); }
 inline int      Solver::nVars         ()      const   { return vardata.size(); }

+inline int      Solver::assumptionsSize         ()      const   { return assumptions.size(); }

 inline int      Solver::nFreeVars     ()      const   { return (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]); }
 inline void     Solver::setPolarity   (Var v, bool b) { polarity[v] = b; }
 inline void     Solver::setDecisionVar(Var v, bool b) 
 inline int      Solver::nFreeVars     ()      const   { return (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]); }
 inline void     Solver::setPolarity   (Var v, bool b) { polarity[v] = b; }
 inline void     Solver::setDecisionVar(Var v, bool b) 

diff --git a/glucose-syrup/incremental/Main.cc b/glucose-syrup/incremental/Main.cc
index 9183e8ecb8043c72342ba026b398d0a59d8ab1dd..b973afbdb9a75deb832e4fe556354a48827a0d4b 100644 (file)
--- a/glucose-syrup/incremental/Main.cc
+++ b/glucose-syrup/incremental/Main.cc
@@ -113,9 +113,11 @@ void readClauses(Solver *solver) {
   vec<Lit> clause;
   int numvars = solver->nVars();
   bool haveClause = false;
   vec<Lit> clause;
   int numvars = solver->nVars();
   bool haveClause = false;

+       fprintf(stderr,"Let's read clauses ...\n");

   while(true) {
     int lit=getInt();
     if (lit!=0) {
   while(true) {
     int lit=getInt();
     if (lit!=0) {

+//     fprintf(stderr,"%d ", lit);

       int var = abs(lit) - 1;
       while (var >= numvars) {
         numvars++;
       int var = abs(lit) - 1;
       while (var >= numvars) {
         numvars++;


@@ -124,11 +126,13 @@ void readClauses(Solver *solver) {
       clause.push( (lit>0) ? mkLit(var) : ~mkLit(var));
       haveClause = true;
     } else {
       clause.push( (lit>0) ? mkLit(var) : ~mkLit(var));
       haveClause = true;
     } else {

+//         fprintf(stderr, "\n");

       if (haveClause) {
         solver->addClause_(clause);
         haveClause = false;
         clause.clear();
       } else {
       if (haveClause) {
         solver->addClause_(clause);
         haveClause = false;
         clause.clear();
       } else {

+//           fprintf(stderr, "****************************************************************\n");

         //done with clauses
         return;
       }
         //done with clauses
         return;
       }


@@ -142,12 +146,20 @@ void processCommands(SimpSolver *solver) {
     switch(command) {
     case IS_FREEZE: {
       int var=getInt()-1;
     switch(command) {
     case IS_FREEZE: {
       int var=getInt()-1;

+//      fprintf(stderr, "Freezing %d\n", var);

       solver->setFrozen(var, true);
       break;
     }
     case IS_RUNSOLVER: {
       vec<Lit> dummy;
       solver->setFrozen(var, true);
       break;
     }
     case IS_RUNSOLVER: {
       vec<Lit> dummy;

+//      SimpSolver* solver2 = (SimpSolver*)solver->clone();
+      double time1 = cpuTime();

       lbool ret = solver->solveLimited(dummy);
       lbool ret = solver->solveLimited(dummy);

+//      double time2 = cpuTime();
+//      vec<Lit> dummy2;
+//      lbool ret2 = solver2->solveLimited(dummy2);
+//      double time3 = cpuTime();
+//      fprintf( stderr, "First execution time: %f\t second execution time: %f\n", time2 - time1, time3-time2);

       if (ret == l_True) {
         putInt(IS_SAT);
         putInt(solver->nVars());
       if (ret == l_True) {
         putInt(IS_SAT);
         putInt(solver->nVars());


@@ -156,6 +168,15 @@ void processCommands(SimpSolver *solver) {
         }
       } else if (ret == l_False) {
         putInt(IS_UNSAT);
         }
       } else if (ret == l_False) {
         putInt(IS_UNSAT);

+       putInt(solver->assumptionsSize());
+       fprintf(stderr, "assumption size = %d\nConflict Array: ",solver->assumptionsSize());
+       for(int i=0;i<solver->conflict.size();i++) {
+          fprintf(stderr, "%d = %d, ", i, sign(solver->conflict[i])==true);
+        }
+       fprintf(stderr, "\n***********************\n");
+       for(int i=0;i<solver->assumptionsSize();i++) {
+          putInt(sign(solver->conflict[i])==true);
+        }

       } else {
         putInt(IS_INDETER);
       }
       } else {
         putInt(IS_INDETER);
       }

diff --git a/glucose-syrup/simp/SimpSolver.h b/glucose-syrup/simp/SimpSolver.h
index 5f457a803701431ea405dcd1e0b2247768c44211..c7dcff76172d7c0b026270c9c9e1912286282f4e 100644 (file)
--- a/glucose-syrup/simp/SimpSolver.h
+++ b/glucose-syrup/simp/SimpSolver.h
@@ -193,7 +193,7 @@ class SimpSolver : public Solver {
     bool          backwardSubsumptionCheck (bool verbose = false);
     bool          eliminateVar             (Var v);
     void          extendModel              ();
     bool          backwardSubsumptionCheck (bool verbose = false);
     bool          eliminateVar             (Var v);
     void          extendModel              ();

-
+    void       unsatExplanation();

     void          removeClause             (CRef cr,bool inPurgatory=false);
     bool          strengthenClause         (CRef cr, Lit l);
     void          cleanUpClauses           ();
     void          removeClause             (CRef cr,bool inPurgatory=false);
     bool          strengthenClause         (CRef cr, Lit l);
     void          cleanUpClauses           ();