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         }
  92         return result;
  93 }
  94
  95 int readIntSolver(IncrementalSolver * This) {
  96         int value;
  97         readSolver(This, &value, 4);
  98         return value;
  99 }
 100
 101 void readSolver(IncrementalSolver * This, void * tmp, ssize_t size) {
 102         char *result = (char *) tmp;
 103         ssize_t bytestoread=size;
 104         ssize_t bytesread=0;
 105         do {
 106                 ssize_t n=read(This->from_solver_fd, &((char *)result)[bytesread], bytestoread);
 107                 if (n == -1) {
 108                         model_print("Read failure\n");
 109                         exit(-1);
 110                 }
 111                 bytestoread -= n;
 112                 bytesread += n;
 113         } while(bytestoread != 0);
 114 }
 115
 116 bool getValueSolver(IncrementalSolver * This, int variable) {
 117         return This->solution[variable];
 118 }
 119
 120 void createSolver(IncrementalSolver * This) {
 121         int to_pipe[2];
 122         int from_pipe[2];
 123         if (pipe(to_pipe) || pipe(from_pipe)) {
 124                 model_print("Error creating pipe.\n");
 125                 exit(-1);
 126         }
 127         if ((This->solver_pid = fork()) == -1) {
 128                 model_print("Error forking.\n");
 129                 exit(-1);
 130         }
 131         if (This->solver_pid == 0) {
 132                 //Solver process
 133                 close(to_pipe[1]);
 134                 close(from_pipe[0]);
 135                 int fd=open("log_file", O_WRONLY|O_CREAT|O_TRUNC, S_IRWXU);
 136
 137                 if ((dup2(to_pipe[0], 0) == -1) ||
 138                                 (dup2(from_pipe[1], IS_OUT_FD) == -1) ||
 139                                 (dup2(fd, 1) == -1)) {
 140                         model_print("Error duplicating pipes\n");
 141                 }
 142                 //    setsid();
 143                 execlp(SATSOLVER, SATSOLVER, NULL);
 144                 model_print("execlp Failed\n");
 145                 close(fd);
 146         } else {
 147                 //Our process
 148                 This->to_solver_fd = to_pipe[1];
 149                 This->from_solver_fd = from_pipe[0];
 150                 close(to_pipe[0]);
 151                 close(from_pipe[1]);
 152         }
 153 }
 154
 155 void killSolver(IncrementalSolver * This) {
 156         close(This->to_solver_fd);
 157         close(This->from_solver_fd);
 158         //Stop the solver
 159         if (This->solver_pid > 0) {
 160                 int status;
 161                 kill(This->solver_pid, SIGKILL);
 162                 waitpid(This->solver_pid, &status, 0);
 163         }
 164 }
 165
 166 void flushBufferSolver(IncrementalSolver * This) {
 167         ssize_t bytestowrite=sizeof(int)*This->offset;
 168         ssize_t byteswritten=0;
 169         do {
 170                 ssize_t n=write(This->to_solver_fd, &((char *)This->buffer)[byteswritten], bytestowrite);
 171                 if (n == -1) {
 172                         perror("Write failure\n");
 173                         model_print("to_solver_fd=%d\n",This->to_solver_fd);
 174                         exit(-1);
 175                 }
 176                 bytestowrite -= n;
 177                 byteswritten += n;
 178         } while(bytestowrite != 0);
 179         This->offset = 0;
 180 }