edits

diff --git a/inc_solver.cc b/inc_solver.cc
index 2c2dad351280c90fb1e91252515f07e53aa5b2ec..28444bcf6ff702368b24d38a7e6444fd05e4c1e5 100644 (file)
--- 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();
   }
 }
@@ -93,10 +93,10 @@ 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();
@@ -104,10 +104,10 @@ void IncrementalSolver::createSolver() {
     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]);
   }
 }
 
@@ -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;

diff --git a/inc_solver.h b/inc_solver.h
index 91f0d790977041c326368739684a284e76aa5e5c..8e9ec181ac1bbb903248e7df95d7300241e72341 100644 (file)
--- a/inc_solver.h
+++ b/inc_solver.h
@@ -5,15 +5,7 @@
 #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
+#include "solver_interface.h"
 
 class IncrementalSolver {
  public:

diff --git a/solver_interface.h b/solver_interface.h
index 295c52e2a5f62a167613ad28815183838377bde2..cd2f0760d54ae0e934606ca0c58c8d2b54540aa3 100644 (file)
--- a/solver_interface.h
+++ b/solver_interface.h
@@ -1,12 +1,14 @@
 #ifndef SOLVER_INTERFACE_H
 #define SOLVER_INTERFACE_H
 
+#define IS_OUT_FD 3
+
 #define IS_UNSAT 0
 #define IS_SAT 1
 #define IS_INDETER 2
-#define IS_RUNSOLVER 3
 #define IS_FREEZE 3
+#define IS_RUNSOLVER 4
 
-#define BUFFERSIZE 1024
+#define IS_BUFFERSIZE 1024
 
 #endif