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