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"
14 IncrementalSolver::IncrementalSolver() :
15 buffer((int *)model_malloc(sizeof(int)*IS_BUFFERSIZE)),
23 IncrementalSolver::~IncrementalSolver() {
30 void IncrementalSolver::reset() {
36 void IncrementalSolver::addClauseLiteral(int literal) {
37 buffer[offset++]=literal;
38 if (offset==IS_BUFFERSIZE) {
43 void IncrementalSolver::finishedClauses() {
47 void IncrementalSolver::freeze(int variable) {
48 addClauseLiteral(IS_FREEZE);
49 addClauseLiteral(variable);
52 int IncrementalSolver::solve() {
59 void IncrementalSolver::startSolve() {
60 addClauseLiteral(IS_RUNSOLVER);
64 int IncrementalSolver::getSolution() {
65 int result=readIntSolver();
66 if (result == IS_SAT) {
67 int numVars=readIntSolver();
68 if (numVars > solutionsize) {
71 solution = (int *) model_malloc((numVars+1)*sizeof(int));
74 readSolver(&solution[1], numVars * sizeof(int));
79 int IncrementalSolver::readIntSolver() {
81 readSolver(&value, 4);
85 void IncrementalSolver::readSolver(void * tmp, ssize_t size) {
86 char *result = (char *) tmp;
87 ssize_t bytestoread=size;
90 ssize_t n=read(from_solver_fd, &((char *)result)[bytesread], bytestoread);
92 model_print("Read failure\n");
97 } while(bytestoread != 0);
100 bool IncrementalSolver::getValue(int variable) {
101 return solution[variable];
104 void IncrementalSolver::createSolver() {
107 if (pipe(to_pipe) || pipe(from_pipe)) {
108 model_print("Error creating pipe.\n");
111 if ((solver_pid = fork()) == -1) {
112 model_print("Error forking.\n");
115 if (solver_pid == 0) {
119 int fd=open("log_file", O_WRONLY|O_CREAT|O_TRUNC, S_IRWXU);
121 if ((dup2(to_pipe[0], 0) == -1) ||
122 (dup2(from_pipe[1], IS_OUT_FD) == -1) ||
123 (dup2(fd, 1) == -1)) {
124 model_print("Error duplicating pipes\n");
127 execlp(SATSOLVER, SATSOLVER, NULL);
128 model_print("execlp Failed\n");
132 to_solver_fd = to_pipe[1];
133 from_solver_fd = from_pipe[0];
139 void IncrementalSolver::killSolver() {
141 close(from_solver_fd);
143 if (solver_pid > 0) {
145 kill(solver_pid, SIGKILL);
146 waitpid(solver_pid, &status, 0);
150 void IncrementalSolver::flushBuffer() {
151 ssize_t bytestowrite=sizeof(int)*offset;
152 ssize_t byteswritten=0;
154 ssize_t n=write(to_solver_fd, &((char *)buffer)[byteswritten], bytestowrite);
156 perror("Write failure\n");
157 model_print("to_solver_fd=%d\n",to_solver_fd);
162 } while(bytestowrite != 0);