projects
/
satlib.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
bug fix
[satlib.git]
/
inc_solver.cc
diff --git
a/inc_solver.cc
b/inc_solver.cc
index 2c2dad351280c90fb1e91252515f07e53aa5b2ec..24c6e88fcb13030d99cf293998fcd2395dadc210 100644
(file)
--- a/
inc_solver.cc
+++ b/
inc_solver.cc
@@
-3,7
+3,7
@@
#define SATSOLVER "sat_solver"
IncrementalSolver::IncrementalSolver() :
#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)
solution(NULL),
solutionsize(0),
offset(0)
@@
-24,7
+24,7
@@
void IncrementalSolver::reset() {
void IncrementalSolver::addClauseLiteral(int literal) {
buffer[offset++]=literal;
void IncrementalSolver::addClauseLiteral(int literal) {
buffer[offset++]=literal;
- if (offset==BUFFERSIZE) {
+ if (offset==
IS_
BUFFERSIZE) {
flushBuffer();
}
}
flushBuffer();
}
}
@@
-48,9
+48,10
@@
int IncrementalSolver::solve() {
if (numVars > solutionsize) {
if (solution != NULL)
free(solution);
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;
}
}
return result;
}
@@
-93,10
+94,10
@@
void IncrementalSolver::createSolver() {
}
if (solver_pid == 0) {
//Solver process
}
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();
fprintf(stderr, "Error duplicating pipes\n");
}
setsid();
@@
-104,10
+105,10
@@
void IncrementalSolver::createSolver() {
fprintf(stderr, "execlp Failed\n");
} else {
//Our process
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
+126,8
@@
void IncrementalSolver::flushBuffer() {
do {
ssize_t n=write(to_solver_fd, &((char *)buffer)[byteswritten], bytestowrite);
if (n == -1) {
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;
exit(-1);
}
bytestowrite -= n;