src/Backend/inc_solver.c

   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         addClauseLiteral(This, 0);
  71 }
  72
  73 void freeze(IncrementalSolver * This, int variable) {
  74         addClauseLiteral(This, IS_FREEZE);
  75         addClauseLiteral(This, variable);
  76 }
  77
  78 int solve(IncrementalSolver * This) {
  79         //add an empty clause
  80         startSolve(This);
  81         return getSolution(This);
  82 }
  83
  84
  85 void startSolve(IncrementalSolver *This) {
  86         addClauseLiteral(This, IS_RUNSOLVER);
  87         flushBufferSolver(This);
  88 }
  89
  90 int getSolution(IncrementalSolver * This) {
  91         int result=readIntSolver(This);
  92         if (result == IS_SAT) {
  93                 int numVars=readIntSolver(This);
  94                 if (numVars > This->solutionsize) {
  95                         if (This->solution != NULL)
  96                                 ourfree(This->solution);
  97                         This->solution = (int *) ourmalloc((numVars+1)*sizeof(int));
  98                         This->solution[0] = 0;
  99                 }
 100                 readSolver(This, &This->solution[1], numVars * sizeof(int));
 101         }
 102         return result;
 103 }
 104
 105 int readIntSolver(IncrementalSolver * This) {
 106         int value;
 107         readSolver(This, &value, 4);
 108         return value;
 109 }
 110
 111 void readSolver(IncrementalSolver * This, void * tmp, ssize_t size) {
 112         char *result = (char *) tmp;
 113         ssize_t bytestoread=size;
 114         ssize_t bytesread=0;
 115         do {
 116                 ssize_t n=read(This->from_solver_fd, &((char *)result)[bytesread], bytestoread);
 117                 if (n == -1) {
 118                         model_print("Read failure\n");
 119                         exit(-1);
 120                 }
 121                 bytestoread -= n;
 122                 bytesread += n;
 123         } while(bytestoread != 0);
 124 }
 125
 126 bool getValueSolver(IncrementalSolver * This, int variable) {
 127         return This->solution[variable];
 128 }
 129
 130 void createSolver(IncrementalSolver * This) {
 131         int to_pipe[2];
 132         int from_pipe[2];
 133         if (pipe(to_pipe) || pipe(from_pipe)) {
 134                 model_print("Error creating pipe.\n");
 135                 exit(-1);
 136         }
 137         if ((This->solver_pid = fork()) == -1) {
 138                 model_print("Error forking.\n");
 139                 exit(-1);
 140         }
 141         if (This->solver_pid == 0) {
 142                 //Solver process
 143                 close(to_pipe[1]);
 144                 close(from_pipe[0]);
 145                 int fd=open("log_file", O_WRONLY|O_CREAT|O_TRUNC, S_IRWXU);
 146
 147                 if ((dup2(to_pipe[0], 0) == -1) ||
 148                                 (dup2(from_pipe[1], IS_OUT_FD) == -1) ||
 149                                 (dup2(fd, 1) == -1)) {
 150                         model_print("Error duplicating pipes\n");
 151                 }
 152                 //    setsid();
 153                 execlp(SATSOLVER, SATSOLVER, NULL);
 154                 model_print("execlp Failed\n");
 155                 close(fd);
 156         } else {
 157                 //Our process
 158                 This->to_solver_fd = to_pipe[1];
 159                 This->from_solver_fd = from_pipe[0];
 160                 close(to_pipe[0]);
 161                 close(from_pipe[1]);
 162         }
 163 }
 164
 165 void killSolver(IncrementalSolver * This) {
 166         close(This->to_solver_fd);
 167         close(This->from_solver_fd);
 168         //Stop the solver
 169         if (This->solver_pid > 0) {
 170                 int status;
 171                 kill(This->solver_pid, SIGKILL);
 172                 waitpid(This->solver_pid, &status, 0);
 173         }
 174 }
 175 bool first=true;
 176
 177 void flushBufferSolver(IncrementalSolver * This) {
 178         ssize_t bytestowrite=sizeof(int)*This->offset;
 179         ssize_t byteswritten=0;
 180         for(uint i=0;i<This->offset;i++) {
 181                 if (first)
 182                         printf("(");
 183                 if (This->buffer[i]==0) {
 184                         printf(")\n");
 185                         first=true;
 186                 } else {
 187                         if (!first)
 188                                 printf(" + ");
 189                         first=false;
 190                         printf("%d", This->buffer[i]);
 191                 }
 192         }
 193         do {
 194                 ssize_t n=write(This->to_solver_fd, &((char *)This->buffer)[byteswritten], bytestowrite);
 195                 if (n == -1) {
 196                         perror("Write failure\n");
 197                         model_print("to_solver_fd=%d\n",This->to_solver_fd);
 198                         exit(-1);
 199                 }
 200                 bytestowrite -= n;
 201                 byteswritten += n;
 202         } while(bytestowrite != 0);
 203         This->offset = 0;
 204 }