glucose-syrup/incremental/Main.cc

   1
   2 #include "solver_interface.h"
   3 #include <errno.h>
   4
   5 #include <signal.h>
   6 #include <zlib.h>
   7 #include <sys/resource.h>
   8
   9 #include "utils/System.h"
  10 #include "utils/ParseUtils.h"
  11 #include "utils/Options.h"
  12 #include "core/Dimacs.h"
  13 #include "simp/SimpSolver.h"
  14
  15 using namespace Glucose;
  16
  17
  18 static const char* _certified = "CORE -- CERTIFIED UNSAT";
  19
  20 void printStats(Solver& solver)
  21 {
  22     double cpu_time = cpuTime();
  23     double mem_used = 0;//memUsedPeak();
  24     printf("c restarts              : %" PRIu64" (%" PRIu64" conflicts in avg)\n", solver.starts,(solver.starts>0 ?solver.conflicts/solver.starts : 0));
  25     printf("c blocked restarts      : %" PRIu64" (multiple: %" PRIu64") \n", solver.nbstopsrestarts,solver.nbstopsrestartssame);
  26     printf("c last block at restart : %" PRIu64"\n",solver.lastblockatrestart);
  27     printf("c nb ReduceDB           : %" PRIu64"\n", solver.nbReduceDB);
  28     printf("c nb removed Clauses    : %" PRIu64"\n",solver.nbRemovedClauses);
  29     printf("c nb learnts DL2        : %" PRIu64"\n", solver.nbDL2);
  30     printf("c nb learnts size 2     : %" PRIu64"\n", solver.nbBin);
  31     printf("c nb learnts size 1     : %" PRIu64"\n", solver.nbUn);
  32
  33     printf("c conflicts             : %-12" PRIu64"   (%.0f /sec)\n", solver.conflicts   , solver.conflicts   /cpu_time);
  34     printf("c decisions             : %-12" PRIu64"   (%4.2f %% random) (%.0f /sec)\n", solver.decisions, (float)solver.rnd_decisions*100 / (float)solver.decisions, solver.decisions   /cpu_time);
  35     printf("c propagations          : %-12" PRIu64"   (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time);
  36     printf("c conflict literals     : %-12" PRIu64"   (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals);
  37     printf("c nb reduced Clauses    : %" PRIu64"\n",solver.nbReducedClauses);
  38
  39     if (mem_used != 0) printf("Memory used           : %.2f MB\n", mem_used);
  40     printf("c CPU time              : %g s\n", cpu_time);
  41 }
  42
  43
  44
  45 static Solver* solver;
  46 // Terminate by notifying the solver and back out gracefully. This is mainly to have a test-case
  47 // for this feature of the Solver as it may take longer than an immediate call to '_exit()'.
  48 static void SIGINT_interrupt(int signum) { solver->interrupt(); }
  49
  50 // Note that '_exit()' rather than 'exit()' has to be used. The reason is that 'exit()' calls
  51 // destructors and may cause deadlocks if a malloc/free function happens to be running (these
  52 // functions are guarded by locks for multithreaded use).
  53 static void SIGINT_exit(int signum) {
  54     printf("\n"); printf("*** INTERRUPTED ***\n");
  55     if (solver->verbosity > 0){
  56         printStats(*solver);
  57         printf("\n"); printf("*** INTERRUPTED ***\n"); }
  58     _exit(1); }
  59
  60
  61 int *buffer;
  62 int length;
  63 int offset;
  64
  65 int *outbuffer;
  66 int outoffset;
  67
  68 int getInt() {
  69   if (offset>=length) {
  70     offset = 0;
  71                 ssize_t ptr=read(0, buffer, sizeof(int)*IS_BUFFERSIZE);
  72                 if (ptr == -1 || ptr == 0)
  73                         exit(-1);
  74
  75     ssize_t bytestoread=(4-(ptr & 3)) & 3;
  76     while(bytestoread != 0) {
  77       ssize_t p=read(0, &((char *)buffer)[ptr], bytestoread);
  78       if (p == -1 || p == 0)
  79         exit(-1);
  80       bytestoread -= p;
  81       ptr += p;
  82     }
  83     length = ptr / 4;
  84     offset = 0;
  85   }
  86
  87   return buffer[offset++];
  88 }
  89
  90 void flushInts() {
  91   ssize_t bytestowrite=sizeof(int)*outoffset;
  92   ssize_t byteswritten=0;
  93   do {
  94     ssize_t n=write(IS_OUT_FD, &((char *)outbuffer)[byteswritten], bytestowrite);
  95     if (n == -1) {
  96       fprintf(stderr, "Write failure\n");
  97       exit(-1);
  98     }
  99     bytestowrite -= n;
 100     byteswritten += n;
 101   } while(bytestowrite != 0);
 102   outoffset = 0;
 103 }
 104
 105 void putInt(int value) {
 106   if (outoffset>=IS_BUFFERSIZE) {
 107     flushInts();
 108   }
 109   outbuffer[outoffset++]=value;
 110 }
 111
 112 void readClauses(Solver *solver) {
 113   vec<Lit> clause;
 114   int numvars = solver->nVars();
 115   bool haveClause = false;
 116         fprintf(stderr,"Let's read clauses ...\n");
 117   while(true) {
 118     int lit=getInt();
 119     if (lit!=0) {
 120 //      fprintf(stderr,"%d ", lit);
 121       int var = abs(lit) - 1;
 122       while (var >= numvars) {
 123         numvars++;
 124         solver->newVar();
 125       }
 126       clause.push( (lit>0) ? mkLit(var) : ~mkLit(var));
 127       haveClause = true;
 128     } else {
 129 //          fprintf(stderr, "\n");
 130       if (haveClause) {
 131         solver->addClause_(clause);
 132         haveClause = false;
 133         clause.clear();
 134       } else {
 135 //            fprintf(stderr, "****************************************************************\n");
 136         //done with clauses
 137         return;
 138       }
 139     }
 140   }
 141 }
 142
 143 void processCommands(SimpSolver *solver) {
 144   while(true) {
 145     int command=getInt();
 146     switch(command) {
 147     case IS_FREEZE: {
 148       int var=getInt()-1;
 149 //      fprintf(stderr, "Freezing %d\n", var);
 150       solver->setFrozen(var, true);
 151       break;
 152     }
 153     case IS_RUNSOLVER: {
 154       vec<Lit> dummy;
 155 //      SimpSolver* solver2 = (SimpSolver*)solver->clone();
 156       double time1 = cpuTime();
 157       lbool ret = solver->solveLimited(dummy);
 158 //      double time2 = cpuTime();
 159 //      vec<Lit> dummy2;
 160 //      lbool ret2 = solver2->solveLimited(dummy2);
 161 //      double time3 = cpuTime();
 162 //      fprintf( stderr, "First execution time: %f\t second execution time: %f\n", time2 - time1, time3-time2);
 163       if (ret == l_True) {
 164         putInt(IS_SAT);
 165         putInt(solver->nVars());
 166         for(int i=0;i<solver->nVars();i++) {
 167           putInt(solver->model[i]==l_True);
 168         }
 169       } else if (ret == l_False) {
 170         putInt(IS_UNSAT);
 171         putInt(solver->assumptionsSize());
 172         fprintf(stderr, "assumption size = %d\nConflict Array: ",solver->assumptionsSize());
 173         for(int i=0;i<solver->conflict.size();i++) {
 174           fprintf(stderr, "%d = %d, ", i, sign(solver->conflict[i])==true);
 175         }
 176         fprintf(stderr, "\n***********************\n");
 177         for(int i=0;i<solver->assumptionsSize();i++) {
 178           putInt(sign(solver->conflict[i])==true);
 179         }
 180       } else {
 181         putInt(IS_INDETER);
 182       }
 183       flushInts();
 184       return;
 185     }
 186     default:
 187       fprintf(stderr, "Unreconized command\n");
 188       exit(-1);
 189     }
 190   }
 191 }
 192
 193 void processSAT(SimpSolver *solver) {
 194   buffer=(int *) malloc(sizeof(int)*IS_BUFFERSIZE);
 195   offset=0;
 196   length=0;
 197   outbuffer=(int *) malloc(sizeof(int)*IS_BUFFERSIZE);
 198   outoffset=0;
 199
 200   while(true) {
 201     double initial_time = cpuTime();
 202     readClauses(solver);
 203     double parse_time = cpuTime();
 204     processCommands(solver);
 205     double finish_time = cpuTime();
 206     printf("Parse time: %12.2f s Solve time:%12.2f s\n", parse_time-initial_time, finish_time-parse_time);
 207   }
 208 }
 209
 210
 211
 212 //=================================================================================================
 213 // Main:
 214
 215 int main(int argc, char** argv) {
 216   try {
 217     printf("c\nc This is glucose 4.0 --  based on MiniSAT (Many thanks to MiniSAT team)\nc\n");
 218
 219
 220     setUsageHelp("c USAGE: %s [options] <input-file> <result-output-file>\n\n  where input may be either in plain or gzipped DIMACS.\n");
 221
 222
 223 #if defined(__linux__)
 224     fpu_control_t oldcw, newcw;
 225     _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw);
 226     //printf("c WARNING: for repeatability, setting FPU to use double precision\n");
 227 #endif
 228     // Extra options:
 229     //
 230     IntOption    verb   ("MAIN", "verb",   "Verbosity level (0=silent, 1=some, 2=more).", 0, IntRange(0, 2));
 231     BoolOption   mod   ("MAIN", "model",   "show model.", false);
 232     IntOption    vv  ("MAIN", "vv",   "Verbosity every vv conflicts", 10000, IntRange(1,INT32_MAX));
 233     BoolOption   pre    ("MAIN", "pre",    "Completely turn on/off any preprocessing.", true);
 234     StringOption dimacs ("MAIN", "dimacs", "If given, stop after preprocessing and write the result to this file.");
 235     IntOption    cpu_lim("MAIN", "cpu-lim","Limit on CPU time allowed in seconds.\n", INT32_MAX, IntRange(0, INT32_MAX));
 236     IntOption    mem_lim("MAIN", "mem-lim","Limit on memory usage in megabytes.\n", INT32_MAX, IntRange(0, INT32_MAX));
 237
 238     BoolOption    opt_certified      (_certified, "certified",    "Certified UNSAT using DRUP format", false);
 239     StringOption  opt_certified_file      (_certified, "certified-output",    "Certified UNSAT output file", "NULL");
 240
 241     parseOptions(argc, argv, true);
 242
 243     SimpSolver  S;
 244     S.parsing = 1;
 245     S.verbosity = verb;
 246     S.verbEveryConflicts = vv;
 247     S.showModel = mod;
 248     solver = &S;
 249     // Use signal handlers that forcibly quit until the solver will be
 250     // able to respond to interrupts:
 251     signal(SIGINT, SIGINT_exit);
 252     signal(SIGXCPU,SIGINT_exit);
 253
 254
 255     // Set limit on CPU-time:
 256     if (cpu_lim != INT32_MAX){
 257       rlimit rl;
 258       getrlimit(RLIMIT_CPU, &rl);
 259       if (rl.rlim_max == RLIM_INFINITY || (rlim_t)cpu_lim < rl.rlim_max){
 260         rl.rlim_cur = cpu_lim;
 261         if (setrlimit(RLIMIT_CPU, &rl) == -1)
 262           printf("c WARNING! Could not set resource limit: CPU-time.\n");
 263       } }
 264
 265     // Set limit on virtual memory:
 266     if (mem_lim != INT32_MAX){
 267       rlim_t new_mem_lim = (rlim_t)mem_lim * 1024*1024;
 268       rlimit rl;
 269       getrlimit(RLIMIT_AS, &rl);
 270       if (rl.rlim_max == RLIM_INFINITY || new_mem_lim < rl.rlim_max){
 271         rl.rlim_cur = new_mem_lim;
 272         if (setrlimit(RLIMIT_AS, &rl) == -1)
 273           printf("c WARNING! Could not set resource limit: Virtual memory.\n");
 274       } }
 275
 276     //do solver stuff here
 277     processSAT(&S);
 278
 279     printf("c |  Number of variables:  %12d                                                                   |\n", S.nVars());
 280     printf("c |  Number of clauses:    %12d                                                                   |\n", S.nClauses());
 281
 282
 283     // Change to signal-handlers that will only notify the solver and allow it to terminate
 284     // voluntarily:
 285     signal(SIGINT, SIGINT_interrupt);
 286     signal(SIGXCPU,SIGINT_interrupt);
 287
 288     S.parsing = 0;
 289
 290 #ifdef NDEBUG
 291     exit(0);
 292 #else
 293     return (0);
 294 #endif
 295   } catch (OutOfMemoryException&){
 296     printf("c =========================================================================================================\n");
 297     printf("INDETERMINATE\n");
 298     exit(0);
 299   }
 300 }