inc_solver.cc

   1 #include "inc_solver.h"
   2
   3 #define SATSOLVER "sat_solver"
   4
   5 IncrementalSolver::IncrementalSolver() :
   6   buffer((int *)malloc(sizeof(int)*IS_BUFFERSIZE)),
   7   solution(NULL),
   8   solutionsize(0),
   9   offset(0)
  10 {
  11   createSolver();
  12 }
  13
  14 IncrementalSolver::~IncrementalSolver() {
  15   killSolver();
  16   free(buffer);
  17 }
  18
  19 void IncrementalSolver::reset() {
  20   killSolver();
  21   offset = 0;
  22   createSolver();
  23 }
  24
  25 void IncrementalSolver::addClauseLiteral(int literal) {
  26   buffer[offset++]=literal;
  27   if (offset==IS_BUFFERSIZE) {
  28     flushBuffer();
  29   }
  30 }
  31
  32 void IncrementalSolver::finishedClauses() {
  33   addClauseLiteral(0);
  34 }
  35
  36 void IncrementalSolver::freeze(int variable) {
  37   addClauseLiteral(IS_FREEZE);
  38   addClauseLiteral(variable);
  39 }
  40
  41 int IncrementalSolver::solve() {
  42   //add an empty clause
  43   addClauseLiteral(IS_RUNSOLVER);
  44   flushBuffer();
  45   int result=readIntSolver();
  46   if (result == IS_SAT) {
  47     int numVars=readIntSolver();
  48     if (numVars > solutionsize) {
  49       if (solution != NULL)
  50         free(solution);
  51       solution = (int *) malloc((numVars+1)*sizeof(int));
  52       solution[0] = 0;
  53     }
  54     readSolver(&solution[1], numVars * sizeof(int));
  55   }
  56   return result;
  57 }
  58
  59 int IncrementalSolver::readIntSolver() {
  60   int value;
  61   readSolver(&value, 4);
  62   return value;
  63 }
  64
  65 void IncrementalSolver::readSolver(void * tmp, ssize_t size) {
  66   char *result = (char *) tmp;
  67   ssize_t bytestoread=size;
  68   ssize_t bytesread=0;
  69   do {
  70     ssize_t n=read(from_solver_fd, &((char *)result)[bytesread], bytestoread);
  71     if (n == -1) {
  72       fprintf(stderr, "Read failure\n");
  73       exit(-1);
  74     }
  75     bytestoread -= n;
  76     bytesread += n;
  77   } while(bytestoread != 0);
  78 }
  79
  80 bool IncrementalSolver::getValue(int variable) {
  81   return solution[variable];
  82 }
  83
  84 void IncrementalSolver::createSolver() {
  85   int to_pipe[2];
  86   int from_pipe[2];
  87   if (pipe(to_pipe) || pipe(from_pipe)) {
  88     fprintf(stderr, "Error creating pipe.\n");
  89     exit(-1);
  90   }
  91   if ((solver_pid = fork()) == -1) {
  92     fprintf(stderr, "Error forking.\n");
  93     exit(-1);
  94   }
  95   if (solver_pid == 0) {
  96     //Solver process
  97     close(to_pipe[1]);
  98     close(from_pipe[0]);
  99     if ((dup2(to_pipe[0], 0) == -1) ||
 100         (dup2(from_pipe[1], IS_OUT_FD) == -1)) {
 101       fprintf(stderr, "Error duplicating pipes\n");
 102     }
 103     execlp(SATSOLVER, SATSOLVER, NULL);
 104     fprintf(stderr, "execlp Failed\n");
 105   } else {
 106     //Our process
 107     to_solver_fd = to_pipe[1];
 108     from_solver_fd = from_pipe[0];
 109     close(to_pipe[0]);
 110     close(from_pipe[1]);
 111   }
 112 }
 113
 114 void IncrementalSolver::killSolver() {
 115   close(to_solver_fd);
 116   close(from_solver_fd);
 117   //Stop the solver
 118   if (solver_pid > 0)
 119     kill(solver_pid, SIGKILL);
 120 }
 121
 122 void IncrementalSolver::flushBuffer() {
 123   ssize_t bytestowrite=sizeof(int)*offset;
 124   ssize_t byteswritten=0;
 125   do {
 126     ssize_t n=write(to_solver_fd, &((char *)buffer)[byteswritten], bytestowrite);
 127     if (n == -1) {
 128       perror("Write failure\n");
 129       printf("to_solver_fd=%d\n",to_solver_fd);
 130       exit(-1);
 131     }
 132     bytestowrite -= n;
 133     byteswritten += n;
 134   } while(bytestowrite != 0);
 135   offset = 0;
 136 }