zchaff64/inc_solver.cpp

   1 /* =========FOR INTERNAL USE ONLY. NO DISTRIBUTION PLEASE ========== */
   2
   3 /*********************************************************************
   4  Copyright 2000-2004, Princeton University.  All rights reserved.
   5  By using this software the USER indicates that he or she has read,
   6  understood and will comply with the following:
   7
   8  --- Princeton University hereby grants USER nonexclusive permission
   9  to use, copy and/or modify this software for internal, noncommercial,
  10  research purposes only. Any distribution, including commercial sale
  11  or license, of this software, copies of the software, its associated
  12  documentation and/or modifications of either is strictly prohibited
  13  without the prior consent of Princeton University.  Title to copyright
  14  to this software and its associated documentation shall at all times
  15  remain with Princeton University.  Appropriate copyright notice shall
  16  be placed on all software copies, and a complete copy of this notice
  17  shall be included in all copies of the associated documentation.
  18  No right is  granted to use in advertising, publicity or otherwise
  19  any trademark,  service mark, or the name of Princeton University.
  20
  21
  22  --- This software and any associated documentation is provided "as is"
  23
  24  PRINCETON UNIVERSITY MAKES NO REPRESENTATIONS OR WARRANTIES, EXPRESS
  25  OR IMPLIED, INCLUDING THOSE OF MERCHANTABILITY OR FITNESS FOR A
  26  PARTICULAR PURPOSE, OR THAT  USE OF THE SOFTWARE, MODIFICATIONS, OR
  27  ASSOCIATED DOCUMENTATION WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS,
  28  TRADEMARKS OR OTHER INTELLECTUAL PROPERTY RIGHTS OF A THIRD PARTY.
  29
  30  Princeton University shall not be liable under any circumstances for
  31  any direct, indirect, special, incidental, or consequential damages
  32  with respect to any claim by USER or any third party on account of
  33  or arising from the use, or inability to use, this software or its
  34  associated documentation, even if Princeton University has been advised
  35  of the possibility of those damages.
  36 *********************************************************************/
  37 #include <iostream>
  38 #include <fstream>
  39 #include <cstdlib>
  40 #include <cstdio>
  41
  42 #include <set>
  43 #include <vector>
  44 #include <dirent.h>
  45 #include "SAT.h"
  46 #include "solver_interface.h"
  47 #include <sys/time.h>
  48 #include <sys/resource.h>
  49 #include <unistd.h>
  50
  51 using namespace std;
  52
  53
  54
  55
  56 static inline double cpuTime(void) {
  57   struct rusage ru;
  58   getrusage(RUSAGE_SELF, &ru);
  59   return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000;
  60 }
  61
  62 int *buffer;
  63 int length;
  64 int offset;
  65
  66 int *outbuffer;
  67 int outoffset;
  68
  69 int getInt() {
  70   if (offset>=length) {
  71     offset = 0;
  72                 ssize_t ptr=read(0, buffer, sizeof(int)*IS_BUFFERSIZE);
  73                 if (ptr == -1 || ptr == 0)
  74                         exit(-1);
  75
  76     ssize_t bytestoread=(4-(ptr & 3)) & 3;
  77     while(bytestoread != 0) {
  78       ssize_t p=read(0, &((char *)buffer)[ptr], bytestoread);
  79       if (p == -1 || p == 0)
  80         exit(-1);
  81       bytestoread -= p;
  82       ptr += p;
  83     }
  84     length = ptr / 4;
  85     offset = 0;
  86   }
  87
  88   return buffer[offset++];
  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 int numvars=0;
 113 void readClauses(SAT_Manager solver) {
 114   vector<int> clause;
 115   bool haveClause = false;
 116   while(true) {
 117     int lit=getInt();
 118     if (lit!=0) {
 119       int var = abs(lit);
 120       while (var > numvars) {
 121         numvars++;
 122         SAT_AddVariable(solver);
 123       }
 124       int shvar=var << 1;
 125       clause.push_back( (lit>0) ? shvar : shvar+1);
 126       haveClause = true;
 127     } else {
 128       if (haveClause) {
 129         SAT_AddClause(solver, & clause.begin()[0], clause.size());
 130         haveClause = false;
 131         clause.clear();
 132       } else {
 133         //done with clauses
 134         return;
 135       }
 136     }
 137   }
 138 }
 139 bool first=true;;
 140
 141 void processCommands(SAT_Manager solver) {
 142   while(true) {
 143     int command=getInt();
 144     switch(command) {
 145     case IS_FREEZE: {
 146       int var=getInt();
 147       break;
 148     }
 149     case IS_RUNSOLVER: {
 150       if (!first) {
 151         SAT_Reset(solver);
 152       }
 153       first=false;
 154       int ret = SAT_Solve(solver);
 155
 156       if (ret == SATISFIABLE) {
 157         putInt(IS_SAT);
 158         putInt(numvars);
 159         for(int i=1;i<=numvars;i++) {
 160           putInt(SAT_GetVarAsgnment(solver, i)==1);
 161         }
 162       } else if (ret == UNSATISFIABLE) {
 163         putInt(IS_UNSAT);
 164       } else {
 165         putInt(IS_INDETER);
 166       }
 167       flushInts();
 168       return;
 169     }
 170     default:
 171       fprintf(stderr, "Unreconized command\n");
 172       exit(-1);
 173     }
 174   }
 175 }
 176 void processSAT(SAT_Manager solver) {
 177   buffer=(int *) malloc(sizeof(int)*IS_BUFFERSIZE);
 178   offset=0;
 179   length=0;
 180   outbuffer=(int *) malloc(sizeof(int)*IS_BUFFERSIZE);
 181   outoffset=0;
 182
 183   while(true) {
 184     double initial_time = cpuTime();
 185     readClauses(solver);
 186     double parse_time = cpuTime();
 187     processCommands(solver);
 188     double finish_time = cpuTime();
 189     printf("Parse time: %12.2f s Solve time:%12.2f s\n", parse_time-initial_time, finish_time-parse_time);
 190   }
 191 }
 192
 193
 194 int main(int argc, char ** argv) {
 195   SAT_Manager mng = SAT_InitManager();
 196   processSAT(mng);
 197   return 0;
 198 }