X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satlib.git;a=blobdiff_plain;f=inc_solver.cc;h=28444bcf6ff702368b24d38a7e6444fd05e4c1e5;hp=2c2dad351280c90fb1e91252515f07e53aa5b2ec;hb=23cbbacd68e917a66bb1334193d4e2c53c176071;hpb=16db0f7120215c74f5a4ab47e70b97df59bf7513 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;