1 /* =========FOR INTERNAL USE ONLY. NO DISTRIBUTION PLEASE ========== */
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:
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.
22 --- This software and any associated documentation is provided "as is"
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.
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 *********************************************************************/
46 #include "solver_interface.h"
48 #include <sys/resource.h>
56 static inline double cpuTime(void) {
58 getrusage(RUSAGE_SELF, &ru);
59 return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000;
72 ssize_t ptr=read(0, buffer, sizeof(int)*IS_BUFFERSIZE);
73 if (ptr == -1 || ptr == 0)
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)
88 return buffer[offset++];
91 ssize_t bytestowrite=sizeof(int)*outoffset;
92 ssize_t byteswritten=0;
94 ssize_t n=write(IS_OUT_FD, &((char *)outbuffer)[byteswritten], bytestowrite);
96 fprintf(stderr, "Write failure\n");
101 } while(bytestowrite != 0);
105 void putInt(int value) {
106 if (outoffset>=IS_BUFFERSIZE) {
109 outbuffer[outoffset++]=value;
113 void readClauses(SAT_Manager solver) {
115 bool haveClause = false;
120 while (var > numvars) {
122 SAT_AddVariable(solver);
125 clause.push_back( (lit>0) ? shvar : shvar+1);
129 SAT_AddClause(solver, & clause.begin()[0], clause.size());
141 void processCommands(SAT_Manager solver) {
143 int command=getInt();
154 int ret = SAT_Solve(solver);
156 if (ret == SATISFIABLE) {
159 for(int i=1;i<=numvars;i++) {
160 putInt(SAT_GetVarAsgnment(solver, i)==1);
162 } else if (ret == UNSATISFIABLE) {
171 fprintf(stderr, "Unreconized command\n");
176 void processSAT(SAT_Manager solver) {
177 buffer=(int *) malloc(sizeof(int)*IS_BUFFERSIZE);
180 outbuffer=(int *) malloc(sizeof(int)*IS_BUFFERSIZE);
184 double initial_time = cpuTime();
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);
194 int main(int argc, char ** argv) {
195 SAT_Manager mng = SAT_InitManager();