src/Backend/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 #include "common.h"
  14 #include <string.h>
  15
  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;
  21         This->offset = 0;
  22         This->timeout = NOTIMEOUT;
  23         createSolver(This);
  24         return This;
  25 }
  26
  27 void deleteIncrementalSolver(IncrementalSolver *This) {
  28         killSolver(This);
  29         ourfree(This->buffer);
  30         if (This->solution != NULL)
  31                 ourfree(This->solution);
  32         ourfree(This);
  33 }
  34
  35 void resetSolver(IncrementalSolver *This) {
  36         killSolver(This);
  37         This->offset = 0;
  38         createSolver(This);
  39 }
  40
  41 void addClauseLiteral(IncrementalSolver *This, int literal) {
  42         This->buffer[This->offset++] = literal;
  43         if (This->offset == IS_BUFFERSIZE) {
  44                 flushBufferSolver(This);
  45         }
  46 }
  47
  48 void addArrayClauseLiteral(IncrementalSolver *This, uint numliterals, int *literals) {
  49         uint index = 0;
  50         while (true) {
  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);
  59                         }
  60                         return;
  61                 } else {
  62                         memcpy(&This->buffer[This->offset], &literals[index], bufferspace * sizeof(int));
  63                         This->offset += bufferspace;
  64                         index += bufferspace;
  65                         flushBufferSolver(This);
  66                 }
  67         }
  68 }
  69
  70 void finishedClauses(IncrementalSolver *This) {
  71         This->buffer[This->offset++] = 0;
  72         if (This->offset == IS_BUFFERSIZE) {
  73                 flushBufferSolver(This);
  74         }
  75 }
  76
  77 void freeze(IncrementalSolver *This, int variable) {
  78         addClauseLiteral(This, IS_FREEZE);
  79         addClauseLiteral(This, variable);
  80 }
  81
  82 int solve(IncrementalSolver *This) {
  83         //add an empty clause
  84         startSolve(This);
  85         return getSolution(This);
  86 }
  87
  88 void startSolve(IncrementalSolver *This) {
  89         addClauseLiteral(This, IS_RUNSOLVER);
  90         flushBufferSolver(This);
  91 }
  92
  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;
 102                 }
 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;
 112                 }
 113                 readSolver(This, &This->solution[1], numVars * sizeof(int));
 114                 This->solutionsize = numVars;
 115         }
 116         return result;
 117 }
 118
 119 int readIntSolver(IncrementalSolver *This) {
 120         int value;
 121         readSolver(This, &value, 4);
 122         return value;
 123 }
 124
 125 int readStatus(IncrementalSolver *This) {
 126         int retval;
 127         fd_set rfds;
 128         FD_ZERO(&rfds);
 129         FD_SET(This->from_solver_fd, &rfds);
 130         fd_set *temp;
 131         if (This->timeout == NOTIMEOUT) {
 132                 retval = select(This->from_solver_fd + 1, &rfds, NULL, NULL, NULL);
 133         } else {
 134                 struct timeval tv;
 135                 tv.tv_sec = This->timeout;
 136                 tv.tv_usec = 0;
 137                 retval = select(This->from_solver_fd + 1, &rfds, NULL, NULL, &tv);
 138         }
 139         if (retval == -1) {
 140                 perror("Error in select()");
 141                 exit(EXIT_FAILURE);
 142         }
 143         else if (retval) {
 144                 printf("Data is available now.\n");
 145                 return readIntSolver(This);
 146         } else {
 147                 printf("Timeout for the solver\n");
 148                 return IS_INDETER;
 149         }
 150 }
 151
 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;
 156         do {
 157                 ssize_t n = read(This->from_solver_fd, &((char *)result)[bytesread], bytestoread);
 158                 if (n == -1) {
 159                         model_print("Read failure\n");
 160                         exit(-1);
 161                 }
 162                 bytestoread -= n;
 163                 bytesread += n;
 164         } while (bytestoread != 0);
 165 }
 166
 167 bool getValueSolver(IncrementalSolver *This, int variable) {
 168         return This->solution[variable];
 169 }
 170
 171 void createSolver(IncrementalSolver *This) {
 172         int to_pipe[2];
 173         int from_pipe[2];
 174         if (pipe(to_pipe) || pipe(from_pipe)) {
 175                 model_print("Error creating pipe.\n");
 176                 exit(-1);
 177         }
 178         if ((This->solver_pid = fork()) == -1) {
 179                 model_print("Error forking.\n");
 180                 exit(-1);
 181         }
 182         if (This->solver_pid == 0) {
 183                 //Solver process
 184                 close(to_pipe[1]);
 185                 close(from_pipe[0]);
 186                 int fd = open("log_file", O_WRONLY | O_CREAT | O_TRUNC, S_IRWXU);
 187
 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");
 192                 }
 193                 //    setsid();
 194                 execlp(SATSOLVER, SATSOLVER, NULL);
 195                 model_print("execlp Failed\n");
 196                 close(fd);
 197         } else {
 198                 //Our process
 199                 This->to_solver_fd = to_pipe[1];
 200                 This->from_solver_fd = from_pipe[0];
 201                 close(to_pipe[0]);
 202                 close(from_pipe[1]);
 203         }
 204 }
 205
 206 void killSolver(IncrementalSolver *This) {
 207         close(This->to_solver_fd);
 208         close(This->from_solver_fd);
 209         //Stop the solver
 210         if (This->solver_pid > 0) {
 211                 int status;
 212                 kill(This->solver_pid, SIGKILL);
 213                 waitpid(This->solver_pid, &status, 0);
 214         }
 215 }
 216
 217 //DEBUGGING CODE STARTS
 218 bool first = true;
 219 //DEBUGGING CODE ENDS
 220
 221 void flushBufferSolver(IncrementalSolver *This) {
 222         ssize_t bytestowrite = sizeof(int) * This->offset;
 223         ssize_t byteswritten = 0;
 224 #ifdef CONFIG_DEBUG
 225         for (uint i = 0; i < This->offset; i++) {
 226                 if (first)
 227                         printf("(");
 228                 if (This->buffer[i] == 0) {
 229                         printf(")\n");
 230                         first = true;
 231                 } else {
 232                         if (!first)
 233                                 printf(" + ");
 234                         first = false;
 235                         printf("%d", This->buffer[i]);
 236                 }
 237         }
 238 #endif
 239         do {
 240                 ssize_t n = write(This->to_solver_fd, &((char *)This->buffer)[byteswritten], bytestowrite);
 241                 if (n == -1) {
 242                         perror("Write failure\n");
 243                         model_print("to_solver_fd=%d\n",This->to_solver_fd);
 244                         exit(-1);
 245                 }
 246                 bytestowrite -= n;
 247                 byteswritten += n;
 248         } while (bytestowrite != 0);
 249         This->offset = 0;
 250 }