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