src/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
  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 }