X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satlib.git;a=blobdiff_plain;f=inc_solver.cc;h=ebc54447f3f98854de8607065124816192c6a220;hp=2c2dad351280c90fb1e91252515f07e53aa5b2ec;hb=a6e90307691746f99342a033e194356f77445db4;hpb=78e4e4dd8f01dbd2119953d815711634ddd4f5bb

diff --git a/inc_solver.cc b/inc_solver.cc
index 2c2dad3..ebc5444 100644
--- a/inc_solver.cc
+++ b/inc_solver.cc
@@ -3,7 +3,7 @@
 #define SATSOLVER "sat_solver"
 
 IncrementalSolver::IncrementalSolver() :
-  buffer((int *)malloc(sizeof(int)*BUFFERSIZE)),
+  buffer((int *)malloc(sizeof(int)*IS_BUFFERSIZE)),
   solution(NULL),
   solutionsize(0),
   offset(0)
@@ -24,7 +24,7 @@ void IncrementalSolver::reset() {
 
 void IncrementalSolver::addClauseLiteral(int literal) {
   buffer[offset++]=literal;
-  if (offset==BUFFERSIZE) {
+  if (offset==IS_BUFFERSIZE) {
     flushBuffer();
   }
 }
@@ -48,9 +48,10 @@ int IncrementalSolver::solve() {
     if (numVars > solutionsize) {
       if (solution != NULL)
         free(solution);
-      solution = (int *) malloc(numVars*sizeof(int));
+      solution = (int *) malloc((numVars+1)*sizeof(int));
+      solution[0] = 0;
     }
-    readSolver(solution, numVars * sizeof(int));
+    readSolver(&solution[1], numVars * sizeof(int));
   }
   return result;
 }
@@ -93,21 +94,20 @@ void IncrementalSolver::createSolver() {
   }
   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)) {
+    close(to_pipe[1]);
+    close(from_pipe[0]);
+    if ((dup2(to_pipe[0], 0) == -1) ||
+        (dup2(from_pipe[1], IS_OUT_FD) == -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]);
+    to_solver_fd = to_pipe[1];
+    from_solver_fd = from_pipe[0];
+    close(to_pipe[0]);
+    close(from_pipe[1]);
   }
 }
 
@@ -116,7 +116,7 @@ void IncrementalSolver::killSolver() {
   close(from_solver_fd);
   //Stop the solver
   if (solver_pid > 0)
-    killpg(solver_pid, SIGKILL);
+    kill(solver_pid, SIGKILL);
 }
 
 void IncrementalSolver::flushBuffer() {
@@ -125,7 +125,8 @@ void IncrementalSolver::flushBuffer() {
   do {
     ssize_t n=write(to_solver_fd, &((char *)buffer)[byteswritten], bytestowrite);
     if (n == -1) {
-      fprintf(stderr, "Write failure\n");
+      perror("Write failure\n");
+      printf("to_solver_fd=%d\n",to_solver_fd);
       exit(-1);
     }
     bytestowrite -= n;