1 #include "inc_solver.h"
3 #define SATSOLVER "sat_solver"
5 IncrementalSolver::IncrementalSolver() :
6 buffer((int *)malloc(sizeof(int)*IS_BUFFERSIZE)),
14 IncrementalSolver::~IncrementalSolver() {
19 void IncrementalSolver::reset() {
25 void IncrementalSolver::addClauseLiteral(int literal) {
26 buffer[offset++]=literal;
27 if (offset==IS_BUFFERSIZE) {
32 void IncrementalSolver::finishedClauses() {
36 void IncrementalSolver::freeze(int variable) {
37 addClauseLiteral(IS_FREEZE);
38 addClauseLiteral(variable);
41 int IncrementalSolver::solve() {
43 addClauseLiteral(IS_RUNSOLVER);
45 int result=readIntSolver();
46 if (result == IS_SAT) {
47 int numVars=readIntSolver();
48 if (numVars > solutionsize) {
51 solution = (int *) malloc((numVars+1)*sizeof(int));
54 readSolver(&solution[1], numVars * sizeof(int));
59 int IncrementalSolver::readIntSolver() {
61 readSolver(&value, 4);
65 void IncrementalSolver::readSolver(void * tmp, ssize_t size) {
66 char *result = (char *) tmp;
67 ssize_t bytestoread=size;
70 ssize_t n=read(from_solver_fd, &((char *)result)[bytesread], bytestoread);
72 fprintf(stderr, "Read failure\n");
77 } while(bytestoread != 0);
80 bool IncrementalSolver::getValue(int variable) {
81 return solution[variable];
84 void IncrementalSolver::createSolver() {
87 if (pipe(to_pipe) || pipe(from_pipe)) {
88 fprintf(stderr, "Error creating pipe.\n");
91 if ((solver_pid = fork()) == -1) {
92 fprintf(stderr, "Error forking.\n");
95 if (solver_pid == 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");
103 execlp(SATSOLVER, SATSOLVER, NULL);
104 fprintf(stderr, "execlp Failed\n");
107 to_solver_fd = to_pipe[1];
108 from_solver_fd = from_pipe[0];
114 void IncrementalSolver::killSolver() {
116 close(from_solver_fd);
119 kill(solver_pid, SIGKILL);
122 void IncrementalSolver::flushBuffer() {
123 ssize_t bytestowrite=sizeof(int)*offset;
124 ssize_t byteswritten=0;
126 ssize_t n=write(to_solver_fd, &((char *)buffer)[byteswritten], bytestowrite);
128 perror("Write failure\n");
129 printf("to_solver_fd=%d\n",to_solver_fd);
134 } while(bytestowrite != 0);