inc_solver.cc

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