1 /* Copyright (c) 2015 Regents of the University of California
3 * Author: Brian Demsky <bdemsky@uci.edu>
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.
10 #include "inc_solver.h"
11 #define SATSOLVER "sat_solver"
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;
22 This->timeout = NOTIMEOUT;
27 void deleteIncrementalSolver(IncrementalSolver *This) {
29 ourfree(This->buffer);
30 if (This->solution != NULL)
31 ourfree(This->solution);
35 void resetSolver(IncrementalSolver *This) {
41 void addClauseLiteral(IncrementalSolver *This, int literal) {
42 This->buffer[This->offset++] = literal;
43 if (This->offset == IS_BUFFERSIZE) {
44 flushBufferSolver(This);
48 void addArrayClauseLiteral(IncrementalSolver *This, uint numliterals, int *literals) {
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);
62 memcpy(&This->buffer[This->offset], &literals[index], bufferspace * sizeof(int));
63 This->offset += bufferspace;
65 flushBufferSolver(This);
70 void finishedClauses(IncrementalSolver *This) {
71 This->buffer[This->offset++] = 0;
72 if (This->offset == IS_BUFFERSIZE) {
73 flushBufferSolver(This);
77 void freeze(IncrementalSolver *This, int variable) {
78 addClauseLiteral(This, IS_FREEZE);
79 addClauseLiteral(This, variable);
82 int solve(IncrementalSolver *This) {
85 return getSolution(This);
88 void startSolve(IncrementalSolver *This) {
89 addClauseLiteral(This, IS_RUNSOLVER);
90 flushBufferSolver(This);
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;
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;
113 readSolver(This, &This->solution[1], numVars * sizeof(int));
114 This->solutionsize = numVars;
119 int readIntSolver(IncrementalSolver *This) {
121 readSolver(This, &value, 4);
125 int readStatus(IncrementalSolver *This) {
129 FD_SET(This->from_solver_fd, &rfds);
131 if (This->timeout == NOTIMEOUT) {
132 retval = select(This->from_solver_fd + 1, &rfds, NULL, NULL, NULL);
135 tv.tv_sec = This->timeout;
137 retval = select(This->from_solver_fd + 1, &rfds, NULL, NULL, &tv);
140 perror("Error in select()");
144 printf("Data is available now.\n");
145 return readIntSolver(This);
147 printf("Timeout for the solver\n");
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;
157 ssize_t n = read(This->from_solver_fd, &((char *)result)[bytesread], bytestoread);
159 model_print("Read failure\n");
164 } while (bytestoread != 0);
167 bool getValueSolver(IncrementalSolver *This, int variable) {
168 return This->solution[variable];
171 void createSolver(IncrementalSolver *This) {
174 if (pipe(to_pipe) || pipe(from_pipe)) {
175 model_print("Error creating pipe.\n");
178 if ((This->solver_pid = fork()) == -1) {
179 model_print("Error forking.\n");
182 if (This->solver_pid == 0) {
186 int fd = open("log_file", O_WRONLY | O_CREAT | O_TRUNC, S_IRWXU);
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");
194 execlp(SATSOLVER, SATSOLVER, NULL);
195 model_print("execlp Failed\n");
199 This->to_solver_fd = to_pipe[1];
200 This->from_solver_fd = from_pipe[0];
206 void killSolver(IncrementalSolver *This) {
207 close(This->to_solver_fd);
208 close(This->from_solver_fd);
210 if (This->solver_pid > 0) {
212 kill(This->solver_pid, SIGKILL);
213 waitpid(This->solver_pid, &status, 0);
217 //DEBUGGING CODE STARTS
219 //DEBUGGING CODE ENDS
221 void flushBufferSolver(IncrementalSolver *This) {
222 ssize_t bytestowrite = sizeof(int) * This->offset;
223 ssize_t byteswritten = 0;
225 for (uint i = 0; i < This->offset; i++) {
228 if (This->buffer[i] == 0) {
235 printf("%d", This->buffer[i]);
240 ssize_t n = write(This->to_solver_fd, &((char *)This->buffer)[byteswritten], bytestowrite);
242 perror("Write failure\n");
243 model_print("to_solver_fd=%d\n",This->to_solver_fd);
248 } while (bytestowrite != 0);