Base Commit
[satune.git] / src / 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
14 IncrementalSolver::IncrementalSolver() :
15         buffer((int *)model_malloc(sizeof(int)*IS_BUFFERSIZE)),
16         solution(NULL),
17         solutionsize(0),
18         offset(0)
19 {
20         createSolver();
21 }
22
23 IncrementalSolver::~IncrementalSolver() {
24         killSolver();
25         model_free(buffer);
26         if (solution != NULL)
27                 model_free(solution);
28 }
29
30 void IncrementalSolver::reset() {
31         killSolver();
32         offset = 0;
33         createSolver();
34 }
35
36 void IncrementalSolver::addClauseLiteral(int literal) {
37         buffer[offset++]=literal;
38         if (offset==IS_BUFFERSIZE) {
39                 flushBuffer();
40         }
41 }
42
43 void IncrementalSolver::finishedClauses() {
44         addClauseLiteral(0);
45 }
46
47 void IncrementalSolver::freeze(int variable) {
48         addClauseLiteral(IS_FREEZE);
49         addClauseLiteral(variable);
50 }
51
52 int IncrementalSolver::solve() {
53         //add an empty clause
54         startSolve();
55         return getSolution();
56 }
57
58
59 void IncrementalSolver::startSolve() {
60         addClauseLiteral(IS_RUNSOLVER);
61         flushBuffer();
62 }
63
64 int IncrementalSolver::getSolution() {
65         int result=readIntSolver();
66         if (result == IS_SAT) {
67                 int numVars=readIntSolver();
68                 if (numVars > solutionsize) {
69                         if (solution != NULL)
70                                 model_free(solution);
71                         solution = (int *) model_malloc((numVars+1)*sizeof(int));
72                         solution[0] = 0;
73                 }
74                 readSolver(&solution[1], numVars * sizeof(int));
75         }
76         return result;
77 }
78
79 int IncrementalSolver::readIntSolver() {
80         int value;
81         readSolver(&value, 4);
82         return value;
83 }
84
85 void IncrementalSolver::readSolver(void * tmp, ssize_t size) {
86         char *result = (char *) tmp;
87         ssize_t bytestoread=size;
88         ssize_t bytesread=0;
89         do {
90                 ssize_t n=read(from_solver_fd, &((char *)result)[bytesread], bytestoread);
91                 if (n == -1) {
92                         model_print("Read failure\n");
93                         exit(-1);
94                 }
95                 bytestoread -= n;
96                 bytesread += n;
97         } while(bytestoread != 0);
98 }
99
100 bool IncrementalSolver::getValue(int variable) {
101         return solution[variable];
102 }
103
104 void IncrementalSolver::createSolver() {
105         int to_pipe[2];
106         int from_pipe[2];
107         if (pipe(to_pipe) || pipe(from_pipe)) {
108                 model_print("Error creating pipe.\n");
109                 exit(-1);
110         }
111         if ((solver_pid = fork()) == -1) {
112                 model_print("Error forking.\n");
113                 exit(-1);
114         }
115         if (solver_pid == 0) {
116                 //Solver process
117                 close(to_pipe[1]);
118                 close(from_pipe[0]);
119                 int fd=open("log_file", O_WRONLY|O_CREAT|O_TRUNC, S_IRWXU);
120
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");
125                 }
126                 //    setsid();
127                 execlp(SATSOLVER, SATSOLVER, NULL);
128                 model_print("execlp Failed\n");
129                 close(fd);
130         } else {
131                 //Our process
132                 to_solver_fd = to_pipe[1];
133                 from_solver_fd = from_pipe[0];
134                 close(to_pipe[0]);
135                 close(from_pipe[1]);
136         }
137 }
138
139 void IncrementalSolver::killSolver() {
140         close(to_solver_fd);
141         close(from_solver_fd);
142         //Stop the solver
143         if (solver_pid > 0) {
144                 int status;
145                 kill(solver_pid, SIGKILL);
146                 waitpid(solver_pid, &status, 0);
147         }
148 }
149
150 void IncrementalSolver::flushBuffer() {
151         ssize_t bytestowrite=sizeof(int)*offset;
152         ssize_t byteswritten=0;
153         do {
154                 ssize_t n=write(to_solver_fd, &((char *)buffer)[byteswritten], bytestowrite);
155                 if (n == -1) {
156                         perror("Write failure\n");
157                         model_print("to_solver_fd=%d\n",to_solver_fd);
158                         exit(-1);
159                 }
160                 bytestowrite -= n;
161                 byteswritten += n;
162         } while(bytestowrite != 0);
163         offset = 0;
164 }