From 23cbbacd68e917a66bb1334193d4e2c53c176071 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
Date: Wed, 31 Dec 2014 17:10:12 +0900
Subject: [PATCH] edits

---
 inc_solver.cc      | 23 ++++++++++++-----------
 inc_solver.h       | 10 +---------
 solver_interface.h |  6 ++++--
 3 files changed, 17 insertions(+), 22 deletions(-)

diff --git a/inc_solver.cc b/inc_solver.cc
index 2c2dad3..28444bc 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();
   }
 }
@@ -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 91f0d79..8e9ec18 100644
--- 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 295c52e..cd2f076 100644
--- 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
-- 
2.34.1