fixes to build structure, util classes, lots of fixes to Node and NodeBuilder. outstanding SEGVs fixed

3 files changed, 26 insertions, 2 deletions

diff --git a/src/prop/Makefile.in b/src/prop/Makefile.in
index c6538df38..e5ac92c61 100644
--- a/src/prop/Makefile.in
+++ b/src/prop/Makefile.in
@@ -130,6 +130,8 @@ AUTOCONF = @AUTOCONF@
 AUTOHEADER = @AUTOHEADER@
 AUTOMAKE = @AUTOMAKE@
 AWK = @AWK@
+BUILDING_SHARED = @BUILDING_SHARED@
+BUILDING_STATIC = @BUILDING_STATIC@
 CC = @CC@
 CCDEPMODE = @CCDEPMODE@
 CFLAGS = @CFLAGS@
diff --git a/src/prop/minisat/Makefile.in b/src/prop/minisat/Makefile.in
index 1dbc8da9f..278d68790 100644
--- a/src/prop/minisat/Makefile.in
+++ b/src/prop/minisat/Makefile.in
@@ -92,6 +92,8 @@ AUTOCONF = @AUTOCONF@
 AUTOHEADER = @AUTOHEADER@
 AUTOMAKE = @AUTOMAKE@
 AWK = @AWK@
+BUILDING_SHARED = @BUILDING_SHARED@
+BUILDING_STATIC = @BUILDING_STATIC@
 CC = @CC@
 CCDEPMODE = @CCDEPMODE@
 CFLAGS = @CFLAGS@
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index ffd335453..afc84a5b4 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -64,7 +64,13 @@ static void doAtom(SimpSolver* minisat, map<Node, Var>* vars, Node e, vec<Lit>*
     c->push(Lit(v->second, true));
     return;
   }
-  Unhandled();
+  if(e.getKind() == OR) {
+    for(Node::iterator i = e.begin(); i != e.end(); ++i) {
+      doAtom(minisat, vars, *i, c);
+    }
+    return;
+  }
+  Unhandled(e.getKind());
 }
 
 static void doClause(SimpSolver* minisat, map<Node, Var>* vars, map<Var, Node>* varsReverse, Node e) {
@@ -72,6 +78,20 @@ static void doClause(SimpSolver* minisat, map<Node, Var>* vars, map<Var, Node>*
   Debug("prop") << "  " << e << endl;
   if(e.getKind() == VARIABLE || e.getKind() == NOT) {
     doAtom(minisat, vars, e, &c);
+  } else if(e.getKind() == FALSE) {
+    // inconsistency
+    Notice() << "adding FALSE clause" << endl;
+    Var v = minisat->newVar();
+    c.push(Lit(v, true));
+    minisat->addClause(c);
+    Notice() << "added unit clause " << v << " [[ " << (*varsReverse)[v] << " ]]" << endl;
+    c.clear();
+    c.push(Lit(v, false));
+    minisat->addClause(c);
+    Notice() << "added unit clause -" << v << " [[ -" << (*varsReverse)[v] << " ]]" << endl;
+  } else if(e.getKind() == TRUE) {
+    Notice() << "adding TRUE clause (do nothing)" << endl;
+    // do nothing
   } else {
     Assert(e.getKind() == OR);
     for(Node::iterator i = e.begin(); i != e.end(); ++i) {
@@ -101,7 +121,7 @@ void PropEngine::solve(Node e) {
   d_sat.verbosity = 1;
   bool result = d_sat.solve();
 
-  Notice() << "result is " << (result ? "sat" : "unsat") << endl;
+  Notice() << "result is " << (result ? "sat/invalid" : "unsat/valid") << endl;
   if(result) {
     Notice() << "model:" << endl;
     for(int i = 0; i < d_sat.model.size(); ++i)