bug fix
[satlib.git] / 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 }