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     ssize_t ptr;
  72     offset = 0;
  73     do {
  74       ptr=read(0, buffer, sizeof(int)*IS_BUFFERSIZE);
  75       if (ptr == -1 || ptr == 0)
  76         exit(-1);
  77     } while(ptr==0);
  78     ssize_t bytestoread=(4-(ptr & 3)) & 3;
  79     while(bytestoread != 0) {
  80       ssize_t p=read(0, &((char *)buffer)[ptr], bytestoread);
  81       if (p == -1 || p == 0)
  82         exit(-1);
  83       bytestoread -= p;
  84       ptr += p;
  85     }
  86     length = ptr / 4;
  87     offset = 0;
  88   }
  89
  90   return buffer[offset++];
  91 }
  92 void flushInts() {
  93   ssize_t bytestowrite=sizeof(int)*outoffset;
  94   ssize_t byteswritten=0;
  95   do {
  96     ssize_t n=write(IS_OUT_FD, &((char *)outbuffer)[byteswritten], bytestowrite);
  97     if (n == -1) {
  98       fprintf(stderr, "Write failure\n");
  99       exit(-1);
 100     }
 101     bytestowrite -= n;
 102     byteswritten += n;
 103   } while(bytestowrite != 0);
 104   outoffset = 0;
 105 }
 106
 107 void putInt(int value) {
 108   if (outoffset>=IS_BUFFERSIZE) {
 109     flushInts();
 110   }
 111   outbuffer[outoffset++]=value;
 112 }
 113
 114 int numvars=0;
 115 void readClauses(SAT_Manager solver) {
 116   vector<int> clause;
 117   bool haveClause = false;
 118   while(true) {
 119     int lit=getInt();
 120     if (lit!=0) {
 121       int var = abs(lit);
 122       while (var > numvars) {
 123         numvars++;
 124         SAT_AddVariable(solver);
 125       }
 126       int shvar=var << 1;
 127       clause.push_back( (lit>0) ? shvar : shvar+1);
 128       haveClause = true;
 129     } else {
 130       if (haveClause) {
 131         SAT_AddClause(solver, & clause.begin()[0], clause.size());
 132         haveClause = false;
 133         clause.clear();
 134       } else {
 135         //done with clauses
 136         return;
 137       }
 138     }
 139   }
 140 }
 141 bool first=true;;
 142
 143 void processCommands(SAT_Manager solver) {
 144   while(true) {
 145     int command=getInt();
 146     switch(command) {
 147     case IS_FREEZE: {
 148       int var=getInt();
 149       break;
 150     }
 151     case IS_RUNSOLVER: {
 152       if (!first) {
 153         SAT_Reset(solver);
 154       }
 155       first=false;
 156       int ret = SAT_Solve(solver);
 157
 158       if (ret == SATISFIABLE) {
 159         putInt(IS_SAT);
 160         putInt(numvars);
 161         for(int i=1;i<=numvars;i++) {
 162           putInt(SAT_GetVarAsgnment(solver, i)==1);
 163         }
 164       } else if (ret == UNSATISFIABLE) {
 165         putInt(IS_UNSAT);
 166       } else {
 167         putInt(IS_INDETER);
 168       }
 169       flushInts();
 170       return;
 171     }
 172     default:
 173       fprintf(stderr, "Unreconized command\n");
 174       exit(-1);
 175     }
 176   }
 177 }
 178 void processSAT(SAT_Manager solver) {
 179   buffer=(int *) malloc(sizeof(int)*IS_BUFFERSIZE);
 180   offset=0;
 181   length=0;
 182   outbuffer=(int *) malloc(sizeof(int)*IS_BUFFERSIZE);
 183   outoffset=0;
 184
 185   while(true) {
 186     double initial_time = cpuTime();
 187     readClauses(solver);
 188     double parse_time = cpuTime();
 189     processCommands(solver);
 190     double finish_time = cpuTime();
 191     printf("Parse time: %12.2f s Solve time:%12.2f s\n", parse_time-initial_time, finish_time-parse_time);
 192   }
 193 }
 194
 195
 196 int main(int argc, char ** argv) {
 197   SAT_Manager mng = SAT_InitManager();
 198   processSAT(mng);
 199   return 0;
 200 }