From: bdemsky <bdemsky@uci.edu>
Date: Wed, 31 Dec 2014 08:10:30 +0000 (+0900)
Subject: Test case
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satlib.git;a=commitdiff_plain;h=86725bc55bda5236052704e72c294fc69fa44eac;hp=23cbbacd68e917a66bb1334193d4e2c53c176071;ds=sidebyside

Test case
---

diff --git a/test_solver.cc b/test_solver.cc
new file mode 100644
index 0000000..90e03fe
--- /dev/null
+++ b/test_solver.cc
@@ -0,0 +1,16 @@
+#include "inc_solver.h"
+
+int main(int argc, char **argv) {
+  IncrementalSolver * s=new IncrementalSolver();
+  s->addClauseLiteral(1);s->addClauseLiteral(2);s->addClauseLiteral(0);
+  s->finishedClauses();
+  s->freeze(1); s->freeze(2);
+  printf("solution=%d\n", s->solve());
+  s->addClauseLiteral(-1);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());
+  delete s;
+}