edits
[satlib.git] / inc_solver.cc
1 #include "inc_solver.h"
2
3 #define SATSOLVER "sat_solver"
4
5 IncrementalSolver::IncrementalSolver() :
6   buffer((int *)malloc(sizeof(int)*IS_BUFFERSIZE)),
7   solution(NULL),
8   solutionsize(0),
9   offset(0)
10 {
11   createSolver();
12 }
13
14 IncrementalSolver::~IncrementalSolver() {
15   killSolver();
16   free(buffer);
17 }
18
19 void IncrementalSolver::reset() {
20   killSolver();
21   offset = 0;
22   createSolver();
23 }
24
25 void IncrementalSolver::addClauseLiteral(int literal) {
26   buffer[offset++]=literal;
27   if (offset==IS_BUFFERSIZE) {
28     flushBuffer();
29   }
30 }
31
32 void IncrementalSolver::finishedClauses() {
33   addClauseLiteral(0);
34 }
35
36 void IncrementalSolver::freeze(int variable) {
37   addClauseLiteral(IS_FREEZE);
38   addClauseLiteral(variable);
39 }
40
41 int IncrementalSolver::solve() {
42   //add an empty clause
43   addClauseLiteral(IS_RUNSOLVER);
44   flushBuffer();
45   int result=readIntSolver();
46   if (result == IS_SAT) {
47     int numVars=readIntSolver();
48     if (numVars > solutionsize) {
49       if (solution != NULL)
50         free(solution);
51       solution = (int *) malloc((numVars+1)*sizeof(int));
52       solution[0] = 0;
53     }
54     readSolver(&solution[1], numVars * sizeof(int));
55   }
56   return result;
57 }
58
59 int IncrementalSolver::readIntSolver() {
60   int value;
61   readSolver(&value, 4);
62   return value;
63 }
64
65 void IncrementalSolver::readSolver(void * tmp, ssize_t size) {
66   char *result = (char *) tmp;
67   ssize_t bytestoread=size;
68   ssize_t bytesread=0;
69   do {
70     ssize_t n=read(from_solver_fd, &((char *)result)[bytesread], bytestoread);
71     if (n == -1) {
72       fprintf(stderr, "Read failure\n");
73       exit(-1);
74     }
75     bytestoread -= n;
76     bytesread += n;
77   } while(bytestoread != 0);
78 }
79
80 bool IncrementalSolver::getValue(int variable) {
81   return solution[variable];
82 }
83
84 void IncrementalSolver::createSolver() {
85   int to_pipe[2];
86   int from_pipe[2];
87   if (pipe(to_pipe) || pipe(from_pipe)) {
88     fprintf(stderr, "Error creating pipe.\n");
89     exit(-1);
90   }
91   if ((solver_pid = fork()) == -1) {
92     fprintf(stderr, "Error forking.\n");
93     exit(-1);
94   }
95   if (solver_pid == 0) {
96     //Solver process
97     close(to_pipe[1]);
98     close(from_pipe[0]);
99     if ((dup2(to_pipe[0], 0) == -1) ||
100         (dup2(from_pipe[1], IS_OUT_FD) == -1)) {
101       fprintf(stderr, "Error duplicating pipes\n");
102     }
103     setsid();
104     execlp(SATSOLVER, SATSOLVER, NULL);
105     fprintf(stderr, "execlp Failed\n");
106   } else {
107     //Our process
108     to_solver_fd = to_pipe[1];
109     from_solver_fd = from_pipe[0];
110     close(to_pipe[0]);
111     close(from_pipe[1]);
112   }
113 }
114
115 void IncrementalSolver::killSolver() {
116   close(to_solver_fd);
117   close(from_solver_fd);
118   //Stop the solver
119   if (solver_pid > 0)
120     killpg(solver_pid, SIGKILL);
121 }
122
123 void IncrementalSolver::flushBuffer() {
124   ssize_t bytestowrite=sizeof(int)*offset;
125   ssize_t byteswritten=0;
126   do {
127     ssize_t n=write(to_solver_fd, &((char *)buffer)[byteswritten], bytestowrite);
128     if (n == -1) {
129       perror("Write failure\n");
130       printf("to_solver_fd=%d\n",to_solver_fd);
131       exit(-1);
132     }
133     bytestowrite -= n;
134     byteswritten += n;
135   } while(bytestowrite != 0);
136   offset = 0;
137 }