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"
15 IncrementalSolver * allocIncrementalSolver() {
16 IncrementalSolver *this=(IncrementalSolver *)ourmalloc(sizeof(IncrementalSolver));
17 this->buffer=((int *)ourmalloc(sizeof(int)*IS_BUFFERSIZE));
25 void deleteIncrementalSolver(IncrementalSolver * this) {
27 ourfree(this->buffer);
28 if (this->solution != NULL)
29 ourfree(this->solution);
32 void resetSolver(IncrementalSolver * this) {
38 void addClauseLiteral(IncrementalSolver * this, int literal) {
39 this->buffer[this->offset++]=literal;
40 if (this->offset==IS_BUFFERSIZE) {
41 flushBufferSolver(this);
45 void finishedClauses(IncrementalSolver * this) {
46 addClauseLiteral(this, 0);
49 void freeze(IncrementalSolver * this, int variable) {
50 addClauseLiteral(this, IS_FREEZE);
51 addClauseLiteral(this, variable);
54 int solve(IncrementalSolver * this) {
57 return getSolution(this);
61 void startSolve(IncrementalSolver *this) {
62 addClauseLiteral(this, IS_RUNSOLVER);
63 flushBufferSolver(this);
66 int getSolution(IncrementalSolver * this) {
67 int result=readIntSolver(this);
68 if (result == IS_SAT) {
69 int numVars=readIntSolver(this);
70 if (numVars > this->solutionsize) {
71 if (this->solution != NULL)
72 ourfree(this->solution);
73 this->solution = (int *) ourmalloc((numVars+1)*sizeof(int));
74 this->solution[0] = 0;
76 readSolver(this, &this->solution[1], numVars * sizeof(int));
81 int readIntSolver(IncrementalSolver * this) {
83 readSolver(this, &value, 4);
87 void readSolver(IncrementalSolver * this, void * tmp, ssize_t size) {
88 char *result = (char *) tmp;
89 ssize_t bytestoread=size;
92 ssize_t n=read(this->from_solver_fd, &((char *)result)[bytesread], bytestoread);
94 model_print("Read failure\n");
99 } while(bytestoread != 0);
102 bool getValueSolver(IncrementalSolver * this, int variable) {
103 return this->solution[variable];
106 void createSolver(IncrementalSolver * this) {
109 if (pipe(to_pipe) || pipe(from_pipe)) {
110 model_print("Error creating pipe.\n");
113 if ((this->solver_pid = fork()) == -1) {
114 model_print("Error forking.\n");
117 if (this->solver_pid == 0) {
121 int fd=open("log_file", O_WRONLY|O_CREAT|O_TRUNC, S_IRWXU);
123 if ((dup2(to_pipe[0], 0) == -1) ||
124 (dup2(from_pipe[1], IS_OUT_FD) == -1) ||
125 (dup2(fd, 1) == -1)) {
126 model_print("Error duplicating pipes\n");
129 execlp(SATSOLVER, SATSOLVER, NULL);
130 model_print("execlp Failed\n");
134 this->to_solver_fd = to_pipe[1];
135 this->from_solver_fd = from_pipe[0];
141 void killSolver(IncrementalSolver * this) {
142 close(this->to_solver_fd);
143 close(this->from_solver_fd);
145 if (this->solver_pid > 0) {
147 kill(this->solver_pid, SIGKILL);
148 waitpid(this->solver_pid, &status, 0);
152 void flushBufferSolver(IncrementalSolver * this) {
153 ssize_t bytestowrite=sizeof(int)*this->offset;
154 ssize_t byteswritten=0;
156 ssize_t n=write(this->to_solver_fd, &((char *)this->buffer)[byteswritten], bytestowrite);
158 perror("Write failure\n");
159 model_print("to_solver_fd=%d\n",this->to_solver_fd);
164 } while(bytestowrite != 0);