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