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