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         createSolver(This);
  23         return This;
  24 }
  25
  26 void deleteIncrementalSolver(IncrementalSolver *This) {
  27         killSolver(This);
  28         ourfree(This->buffer);
  29         if (This->solution != NULL)
  30                 ourfree(This->solution);
  31         ourfree(This);
  32 }
  33
  34 void resetSolver(IncrementalSolver *This) {
  35         killSolver(This);
  36         This->offset = 0;
  37         createSolver(This);
  38 }
  39
  40 void addClauseLiteral(IncrementalSolver *This, int literal) {
  41         This->buffer[This->offset++] = literal;
  42         if (This->offset == IS_BUFFERSIZE) {
  43                 flushBufferSolver(This);
  44         }
  45 }
  46
  47 void addArrayClauseLiteral(IncrementalSolver *This, uint numliterals, int *literals) {
  48         uint index = 0;
  49         while (true) {
  50                 uint bufferspace = IS_BUFFERSIZE - This->offset;
  51                 uint numtowrite = numliterals - index;
  52                 if (bufferspace > numtowrite) {
  53                         memcpy(&This->buffer[This->offset], &literals[index], numtowrite * sizeof(int));
  54                         This->offset += numtowrite;
  55                         This->buffer[This->offset++] = 0;       //have one extra spot always
  56                         if (This->offset == IS_BUFFERSIZE) {//Check if full
  57                                 flushBufferSolver(This);
  58                         }
  59                         return;
  60                 } else {
  61                         memcpy(&This->buffer[This->offset], &literals[index], bufferspace * sizeof(int));
  62                         This->offset += bufferspace;
  63                         index += bufferspace;
  64                         flushBufferSolver(This);
  65                 }
  66         }
  67 }
  68
  69 void finishedClauses(IncrementalSolver *This) {
  70         This->buffer[This->offset++] = 0;
  71         if (This->offset == IS_BUFFERSIZE) {
  72                 flushBufferSolver(This);
  73         }
  74 }
  75
  76 void freeze(IncrementalSolver *This, int variable) {
  77         addClauseLiteral(This, IS_FREEZE);
  78         addClauseLiteral(This, variable);
  79 }
  80
  81 int solve(IncrementalSolver *This) {
  82         //add an empty clause
  83         startSolve(This);
  84         return getSolution(This);
  85 }
  86
  87 void startSolve(IncrementalSolver *This) {
  88         addClauseLiteral(This, IS_RUNSOLVER);
  89         flushBufferSolver(This);
  90 }
  91
  92 int getSolution(IncrementalSolver *This) {
  93         int result = readIntSolver(This);
  94         if (result == IS_SAT) {
  95                 int numVars = readIntSolver(This);
  96                 if (numVars > This->solutionsize) {
  97                         if (This->solution != NULL)
  98                                 ourfree(This->solution);
  99                         This->solution = (int *) ourmalloc((numVars + 1) * sizeof(int));
 100                         This->solution[0] = 0;
 101                 }
 102                 readSolver(This, &This->solution[1], numVars * sizeof(int));
 103                 This->solutionsize = numVars;
 104         }
 105         return result;
 106 }
 107
 108 int readIntSolver(IncrementalSolver *This) {
 109         int value;
 110         readSolver(This, &value, 4);
 111         return value;
 112 }
 113
 114 void readSolver(IncrementalSolver *This, void *tmp, ssize_t size) {
 115         char *result = (char *) tmp;
 116         ssize_t bytestoread = size;
 117         ssize_t bytesread = 0;
 118         do {
 119                 ssize_t n = read(This->from_solver_fd, &((char *)result)[bytesread], bytestoread);
 120                 if (n == -1) {
 121                         model_print("Read failure\n");
 122                         exit(-1);
 123                 }
 124                 bytestoread -= n;
 125                 bytesread += n;
 126         } while (bytestoread != 0);
 127 }
 128
 129 bool getValueSolver(IncrementalSolver *This, int variable) {
 130         return This->solution[variable];
 131 }
 132
 133 void createSolver(IncrementalSolver *This) {
 134         int to_pipe[2];
 135         int from_pipe[2];
 136         if (pipe(to_pipe) || pipe(from_pipe)) {
 137                 model_print("Error creating pipe.\n");
 138                 exit(-1);
 139         }
 140         if ((This->solver_pid = fork()) == -1) {
 141                 model_print("Error forking.\n");
 142                 exit(-1);
 143         }
 144         if (This->solver_pid == 0) {
 145                 //Solver process
 146                 close(to_pipe[1]);
 147                 close(from_pipe[0]);
 148                 int fd = open("log_file", O_WRONLY | O_CREAT | O_TRUNC, S_IRWXU);
 149
 150                 if ((dup2(to_pipe[0], 0) == -1) ||
 151                                 (dup2(from_pipe[1], IS_OUT_FD) == -1) ||
 152                                 (dup2(fd, 1) == -1)) {
 153                         model_print("Error duplicating pipes\n");
 154                 }
 155                 //    setsid();
 156                 execlp(SATSOLVER, SATSOLVER, NULL);
 157                 model_print("execlp Failed\n");
 158                 close(fd);
 159         } else {
 160                 //Our process
 161                 This->to_solver_fd = to_pipe[1];
 162                 This->from_solver_fd = from_pipe[0];
 163                 close(to_pipe[0]);
 164                 close(from_pipe[1]);
 165         }
 166 }
 167
 168 void killSolver(IncrementalSolver *This) {
 169         close(This->to_solver_fd);
 170         close(This->from_solver_fd);
 171         //Stop the solver
 172         if (This->solver_pid > 0) {
 173                 int status;
 174                 kill(This->solver_pid, SIGKILL);
 175                 waitpid(This->solver_pid, &status, 0);
 176         }
 177 }
 178
 179 //DEBUGGING CODE STARTS
 180 bool first = true;
 181 //DEBUGGING CODE ENDS
 182
 183 void flushBufferSolver(IncrementalSolver *This) {
 184         ssize_t bytestowrite = sizeof(int) * This->offset;
 185         ssize_t byteswritten = 0;
 186 #ifdef CONFIG_DEBUG
 187         for (uint i = 0; i < This->offset; i++) {
 188                 if (first)
 189                         printf("(");
 190                 if (This->buffer[i] == 0) {
 191                         printf(")\n");
 192                         first = true;
 193                 } else {
 194                         if (!first)
 195                                 printf(" + ");
 196                         first = false;
 197                         printf("%d", This->buffer[i]);
 198                 }
 199         }
 200 #endif
 201         do {
 202                 ssize_t n = write(This->to_solver_fd, &((char *)This->buffer)[byteswritten], bytestowrite);
 203                 if (n == -1) {
 204                         perror("Write failure\n");
 205                         model_print("to_solver_fd=%d\n",This->to_solver_fd);
 206                         exit(-1);
 207                 }
 208                 bytestowrite -= n;
 209                 byteswritten += n;
 210         } while (bytestowrite != 0);
 211         This->offset = 0;
 212 }