From: bdemsky <bdemsky@uci.edu>
Date: Wed, 31 Dec 2014 06:36:58 +0000 (+0900)
Subject: Add incremental solver class
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satlib.git;a=commitdiff_plain;h=78e4e4dd8f01dbd2119953d815711634ddd4f5bb

Add incremental solver class
---

diff --git a/inc_solver.cc b/inc_solver.cc
new file mode 100644
index 0000000..2c2dad3
--- /dev/null
+++ b/inc_solver.cc
@@ -0,0 +1,135 @@
+#include "inc_solver.h"
+
+#define SATSOLVER "sat_solver"
+
+IncrementalSolver::IncrementalSolver() :
+  buffer((int *)malloc(sizeof(int)*BUFFERSIZE)),
+  solution(NULL),
+  solutionsize(0),
+  offset(0)
+{
+  createSolver();
+}
+
+IncrementalSolver::~IncrementalSolver() {
+  killSolver();
+  free(buffer);
+}
+
+void IncrementalSolver::reset() {
+  killSolver();
+  offset = 0;
+  createSolver();
+}
+
+void IncrementalSolver::addClauseLiteral(int literal) {
+  buffer[offset++]=literal;
+  if (offset==BUFFERSIZE) {
+    flushBuffer();
+  }
+}
+
+void IncrementalSolver::finishedClauses() {
+  addClauseLiteral(0);
+}
+
+void IncrementalSolver::freeze(int variable) {
+  addClauseLiteral(IS_FREEZE);
+  addClauseLiteral(variable);
+}
+
+int IncrementalSolver::solve() {
+  //add an empty clause
+  addClauseLiteral(IS_RUNSOLVER);
+  flushBuffer();
+  int result=readIntSolver();
+  if (result == IS_SAT) {
+    int numVars=readIntSolver();
+    if (numVars > solutionsize) {
+      if (solution != NULL)
+        free(solution);
+      solution = (int *) malloc(numVars*sizeof(int));
+    }
+    readSolver(solution, numVars * sizeof(int));
+  }
+  return result;
+}
+
+int IncrementalSolver::readIntSolver() {
+  int value;
+  readSolver(&value, 4);
+  return value;
+}
+
+void IncrementalSolver::readSolver(void * tmp, ssize_t size) {
+  char *result = (char *) tmp;
+  ssize_t bytestoread=size;
+  ssize_t bytesread=0;
+  do {
+    ssize_t n=read(from_solver_fd, &((char *)result)[bytesread], bytestoread);
+    if (n == -1) {
+      fprintf(stderr, "Read failure\n");
+      exit(-1);
+    }
+    bytestoread -= n;
+    bytesread += n;
+  } while(bytestoread != 0);
+}
+
+bool IncrementalSolver::getValue(int variable) {
+  return solution[variable];
+}
+
+void IncrementalSolver::createSolver() {
+  int to_pipe[2];
+  int from_pipe[2];
+  if (pipe(to_pipe) || pipe(from_pipe)) {
+    fprintf(stderr, "Error creating pipe.\n");
+    exit(-1);
+  }
+  if ((solver_pid = fork()) == -1) {
+    fprintf(stderr, "Error forking.\n");
+    exit(-1);
+  }
+  if (solver_pid == 0) {
+    //Solver process
+    close(to_pipe[0]);
+    close(from_pipe[1]);
+    if ((dup2(0, to_pipe[1]) == -1) ||
+        (dup2(1, from_pipe[0]) == -1)) {
+      fprintf(stderr, "Error duplicating pipes\n");
+    }
+    setsid();
+    execlp(SATSOLVER, SATSOLVER, NULL);
+    fprintf(stderr, "execlp Failed\n");
+  } else {
+    //Our process
+    to_solver_fd = to_pipe[0];
+    from_solver_fd = from_pipe[1];
+    close(to_pipe[1]);
+    close(from_pipe[0]);
+  }
+}
+
+void IncrementalSolver::killSolver() {
+  close(to_solver_fd);
+  close(from_solver_fd);
+  //Stop the solver
+  if (solver_pid > 0)
+    killpg(solver_pid, SIGKILL);
+}
+
+void IncrementalSolver::flushBuffer() {
+  ssize_t bytestowrite=sizeof(int)*offset;
+  ssize_t byteswritten=0;
+  do {
+    ssize_t n=write(to_solver_fd, &((char *)buffer)[byteswritten], bytestowrite);
+    if (n == -1) {
+      fprintf(stderr, "Write failure\n");
+      exit(-1);
+    }
+    bytestowrite -= n;
+    byteswritten += n;
+  } while(bytestowrite != 0);
+  offset = 0;
+}
diff --git a/inc_solver.h b/inc_solver.h
new file mode 100644
index 0000000..91f0d79
--- /dev/null
+++ b/inc_solver.h
@@ -0,0 +1,43 @@
+#ifndef INC_SOLVER_H
+#define INC_SOLVER_H
+#include <sys/types.h>
+#include <unistd.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <signal.h>
+
+
+#define IS_UNSAT 0
+#define IS_SAT 1
+#define IS_INDETER 2
+#define IS_RUNSOLVER 3
+#define IS_FREEZE 3
+
+#define BUFFERSIZE 1024
+
+class IncrementalSolver {
+ public:
+  IncrementalSolver();
+  ~IncrementalSolver();
+  void addClauseLiteral(int literal);
+  void finishedClauses();
+  void freeze(int variable);
+  int solve();
+  bool getValue(int variable);
+  void reset();
+
+ private:
+  void createSolver();
+  void killSolver();
+  void flushBuffer();
+  int readIntSolver();
+  void readSolver(void * buffer, ssize_t size);
+  int * buffer;
+  int * solution;
+  int solutionsize;
+  int offset;
+  pid_t solver_pid;
+  int to_solver_fd;
+  int from_solver_fd;
+};
+#endif