72d34083dcd4b096b32aee4b51816a361f708600
[satune.git] / src / Backend / inc_solver.cc
1 /*      Copyright (c) 2015 Regents of the University of California
2  *
3  *      Author: Brian Demsky <bdemsky@uci.edu>
4  *
5  *      This program is free software; you can redistribute it and/or
6  *      modify it under the terms of the GNU General Public License
7  *      version 2 as published by the Free Software Foundation.
8  */
9
10 #include "inc_solver.h"
11 #define SATSOLVER "sat_solver"
12 #include <fcntl.h>
13 #include "common.h"
14 #include <string.h>
15
16 IncrementalSolver *allocIncrementalSolver() {
17         IncrementalSolver *This = (IncrementalSolver *)ourmalloc(sizeof(IncrementalSolver));
18         This->buffer = ((int *)ourmalloc(sizeof(int) * IS_BUFFERSIZE));
19         This->solution = NULL;
20         This->solutionsize = 0;
21         This->offset = 0;
22         This->timeout = NOTIMEOUT;
23         createSolver(This);
24         return This;
25 }
26
27 void deleteIncrementalSolver(IncrementalSolver *This) {
28         killSolver(This);
29         ourfree(This->buffer);
30         if (This->solution != NULL)
31                 ourfree(This->solution);
32         ourfree(This);
33 }
34
35 void resetSolver(IncrementalSolver *This) {
36         killSolver(This);
37         This->offset = 0;
38         createSolver(This);
39 }
40
41 void addClauseLiteral(IncrementalSolver *This, int literal) {
42         This->buffer[This->offset++] = literal;
43         if (This->offset == IS_BUFFERSIZE) {
44                 flushBufferSolver(This);
45         }
46 }
47
48 void addArrayClauseLiteral(IncrementalSolver *This, uint numliterals, int *literals) {
49         uint index = 0;
50         while (true) {
51                 uint bufferspace = IS_BUFFERSIZE - This->offset;
52                 uint numtowrite = numliterals - index;
53                 if (bufferspace > numtowrite) {
54                         memcpy(&This->buffer[This->offset], &literals[index], numtowrite * sizeof(int));
55                         This->offset += numtowrite;
56                         This->buffer[This->offset++] = 0;       //have one extra spot always
57                         if (This->offset == IS_BUFFERSIZE) {//Check if full
58                                 flushBufferSolver(This);
59                         }
60                         return;
61                 } else {
62                         memcpy(&This->buffer[This->offset], &literals[index], bufferspace * sizeof(int));
63                         This->offset += bufferspace;
64                         index += bufferspace;
65                         flushBufferSolver(This);
66                 }
67         }
68 }
69
70 void finishedClauses(IncrementalSolver *This) {
71         This->buffer[This->offset++] = 0;
72         if (This->offset == IS_BUFFERSIZE) {
73                 flushBufferSolver(This);
74         }
75 }
76
77 void freeze(IncrementalSolver *This, int variable) {
78         addClauseLiteral(This, IS_FREEZE);
79         addClauseLiteral(This, variable);
80 }
81
82 int solve(IncrementalSolver *This) {
83         //add an empty clause
84         startSolve(This);
85         return getSolution(This);
86 }
87
88 void startSolve(IncrementalSolver *This) {
89         addClauseLiteral(This, IS_RUNSOLVER);
90         flushBufferSolver(This);
91 }
92
93 int getSolution(IncrementalSolver *This) {
94         int result = readStatus(This);
95         if (result == IS_SAT) {
96                 int numVars = readIntSolver(This);
97                 if (numVars > This->solutionsize) {
98                         if (This->solution != NULL)
99                                 ourfree(This->solution);
100                         This->solution = (int *) ourmalloc((numVars + 1) * sizeof(int));
101                         This->solution[0] = 0;
102                 }
103                 readSolver(This, &This->solution[1], numVars * sizeof(int));
104                 This->solutionsize = numVars;
105         } else { //Reading unsat explanation
106                 int numVars = readIntSolver(This);
107                 if (numVars > This->solutionsize) {
108                         if (This->solution != NULL)
109                                 ourfree(This->solution);
110                         This->solution = (int *) ourmalloc((numVars + 1) * sizeof(int));
111                         This->solution[0] = 0;
112                 }
113                 readSolver(This, &This->solution[1], numVars * sizeof(int));
114                 This->solutionsize = numVars;
115         }
116         return result;
117 }
118
119 int readIntSolver(IncrementalSolver *This) {
120         int value;
121         readSolver(This, &value, 4);
122         return value;
123 }
124
125 int readStatus(IncrementalSolver *This) {
126         int retval;
127         fd_set rfds;
128         FD_ZERO(&rfds);
129         FD_SET(This->from_solver_fd, &rfds);
130         fd_set *temp;
131         if (This->timeout == NOTIMEOUT) {
132                 retval = select(This->from_solver_fd + 1, &rfds, NULL, NULL, NULL);
133         } else {
134                 struct timeval tv;
135                 tv.tv_sec = This->timeout;
136                 tv.tv_usec = 0;
137                 retval = select(This->from_solver_fd + 1, &rfds, NULL, NULL, &tv);
138         }
139         if (retval == -1) {
140                 perror("Error in select()");
141                 exit(EXIT_FAILURE);
142         }
143         else if (retval) {
144                 printf("Data is available now.\n");
145                 return readIntSolver(This);
146         } else {
147                 printf("Timeout for the solver\n");
148                 return IS_INDETER;
149         }
150 }
151
152 void readSolver(IncrementalSolver *This, void *tmp, ssize_t size) {
153         char *result = (char *) tmp;
154         ssize_t bytestoread = size;
155         ssize_t bytesread = 0;
156         do {
157                 ssize_t n = read(This->from_solver_fd, &((char *)result)[bytesread], bytestoread);
158                 if (n == -1) {
159                         model_print("Read failure\n");
160                         exit(-1);
161                 }
162                 bytestoread -= n;
163                 bytesread += n;
164         } while (bytestoread != 0);
165 }
166
167 bool getValueSolver(IncrementalSolver *This, int variable) {
168         return This->solution[variable];
169 }
170
171 void createSolver(IncrementalSolver *This) {
172         int to_pipe[2];
173         int from_pipe[2];
174         if (pipe(to_pipe) || pipe(from_pipe)) {
175                 model_print("Error creating pipe.\n");
176                 exit(-1);
177         }
178         if ((This->solver_pid = fork()) == -1) {
179                 model_print("Error forking.\n");
180                 exit(-1);
181         }
182         if (This->solver_pid == 0) {
183                 //Solver process
184                 close(to_pipe[1]);
185                 close(from_pipe[0]);
186                 int fd = open("log_file", O_WRONLY | O_CREAT | O_TRUNC, S_IRWXU);
187
188                 if ((dup2(to_pipe[0], 0) == -1) ||
189                                 (dup2(from_pipe[1], IS_OUT_FD) == -1) ||
190                                 (dup2(fd, 1) == -1)) {
191                         model_print("Error duplicating pipes\n");
192                 }
193                 //    setsid();
194                 execlp(SATSOLVER, SATSOLVER, NULL);
195                 model_print("execlp Failed\n");
196                 close(fd);
197         } else {
198                 //Our process
199                 This->to_solver_fd = to_pipe[1];
200                 This->from_solver_fd = from_pipe[0];
201                 close(to_pipe[0]);
202                 close(from_pipe[1]);
203         }
204 }
205
206 void killSolver(IncrementalSolver *This) {
207         close(This->to_solver_fd);
208         close(This->from_solver_fd);
209         //Stop the solver
210         if (This->solver_pid > 0) {
211                 int status;
212                 kill(This->solver_pid, SIGKILL);
213                 waitpid(This->solver_pid, &status, 0);
214         }
215 }
216
217 //DEBUGGING CODE STARTS
218 bool first = true;
219 //DEBUGGING CODE ENDS
220
221 void flushBufferSolver(IncrementalSolver *This) {
222         ssize_t bytestowrite = sizeof(int) * This->offset;
223         ssize_t byteswritten = 0;
224 #ifdef CONFIG_DEBUG
225         for (uint i = 0; i < This->offset; i++) {
226                 if (first)
227                         printf("(");
228                 if (This->buffer[i] == 0) {
229                         printf(")\n");
230                         first = true;
231                 } else {
232                         if (!first)
233                                 printf(" + ");
234                         first = false;
235                         printf("%d", This->buffer[i]);
236                 }
237         }
238 #endif
239         do {
240                 ssize_t n = write(This->to_solver_fd, &((char *)This->buffer)[byteswritten], bytestowrite);
241                 if (n == -1) {
242                         perror("Write failure\n");
243                         model_print("to_solver_fd=%d\n",This->to_solver_fd);
244                         exit(-1);
245                 }
246                 bytestowrite -= n;
247                 byteswritten += n;
248         } while (bytestowrite != 0);
249         This->offset = 0;
250 }