projects
/
satlib.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
fix bug with zombie sat solver processes
[satlib.git]
/
test_solver.cc
diff --git
a/test_solver.cc
b/test_solver.cc
index 90e03fecabdee97ae2f191761be3538abf495cbe..09bc923663df7d8831c47707949d1a44f94b49f2 100644
(file)
--- a/
test_solver.cc
+++ b/
test_solver.cc
@@
-6,11
+6,20
@@
int main(int argc, char **argv) {
s->finishedClauses();
s->freeze(1); s->freeze(2);
printf("solution=%d\n", s->solve());
s->finishedClauses();
s->freeze(1); s->freeze(2);
printf("solution=%d\n", s->solve());
+ for(int i=0;i<=2;i++) {
+ printf("%d: %d\n",i, s->getValue(i));
+ }
s->addClauseLiteral(-1);s->addClauseLiteral(0);
s->finishedClauses();
printf("solution=%d\n", s->solve());
s->addClauseLiteral(-1);s->addClauseLiteral(0);
s->finishedClauses();
printf("solution=%d\n", s->solve());
+ for(int i=0;i<=2;i++) {
+ printf("%d: %d\n",i, s->getValue(i));
+ }
s->addClauseLiteral(-2);s->addClauseLiteral(0);
s->finishedClauses();
printf("solution=%d\n", s->solve());
s->addClauseLiteral(-2);s->addClauseLiteral(0);
s->finishedClauses();
printf("solution=%d\n", s->solve());
+ for(int i=0;i<=2;i++) {
+ printf("%d: %d\n",i, s->getValue(i));
+ }
delete s;
}
delete s;
}