Adding support for reading wrong assumptions

[satlib.git] / glucose-syrup / incremental / Main.cc

diff --git a/glucose-syrup/incremental/Main.cc b/glucose-syrup/incremental/Main.cc
index 5ea6c13a1c68b5c5a8e9284e036c763b9a852000..b973afbdb9a75deb832e4fe556354a48827a0d4b 100644 (file)
--- a/glucose-syrup/incremental/Main.cc
+++ b/glucose-syrup/incremental/Main.cc
@@ -67,17 +67,15 @@ int outoffset;
 
 int getInt() {
   if (offset>=length) {
-    ssize_t ptr;
     offset = 0;
-    do {
-      ptr=read(0, buffer, sizeof(int)*IS_BUFFERSIZE);
-      if (ptr == -1)
-        exit(-1);
-    } while(ptr==0);
+               ssize_t ptr=read(0, buffer, sizeof(int)*IS_BUFFERSIZE);
+               if (ptr == -1 || ptr == 0)
+                       exit(-1);
+
     ssize_t bytestoread=(4-(ptr & 3)) & 3;
     while(bytestoread != 0) {
       ssize_t p=read(0, &((char *)buffer)[ptr], bytestoread);
-      if (p == -1)
+      if (p == -1 || p == 0)
         exit(-1);
       bytestoread -= p;
       ptr += p;
@@ -115,9 +113,11 @@ void readClauses(Solver *solver) {
   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) {
+//     fprintf(stderr,"%d ", lit);
       int var = abs(lit) - 1;
       while (var >= numvars) {
         numvars++;
@@ -126,11 +126,13 @@ void readClauses(Solver *solver) {
       clause.push( (lit>0) ? mkLit(var) : ~mkLit(var));
       haveClause = true;
     } else {
+//         fprintf(stderr, "\n");
       if (haveClause) {
         solver->addClause_(clause);
         haveClause = false;
         clause.clear();
       } else {
+//           fprintf(stderr, "****************************************************************\n");
         //done with clauses
         return;
       }
@@ -144,12 +146,20 @@ void processCommands(SimpSolver *solver) {
     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;
+//      SimpSolver* solver2 = (SimpSolver*)solver->clone();
+      double time1 = cpuTime();
       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());
@@ -158,6 +168,15 @@ void processCommands(SimpSolver *solver) {
         }
       } 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);
       }
@@ -208,7 +227,7 @@ int main(int argc, char** argv) {
 #endif
     // Extra options:
     //
-    IntOption    verb   ("MAIN", "verb",   "Verbosity level (0=silent, 1=some, 2=more).", 1, IntRange(0, 2));
+    IntOption    verb   ("MAIN", "verb",   "Verbosity level (0=silent, 1=some, 2=more).", 0, IntRange(0, 2));
     BoolOption   mod   ("MAIN", "model",   "show model.", false);
     IntOption    vv  ("MAIN", "vv",   "Verbosity every vv conflicts", 10000, IntRange(1,INT32_MAX));
     BoolOption   pre    ("MAIN", "pre",    "Completely turn on/off any preprocessing.", true);