From 4c87c0794b7e954afd090cfbf441caa0b09c3ef5 Mon Sep 17 00:00:00 2001
From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Fri, 5 Oct 2012 22:07:16 +0000
Subject: BoolExpr removed and replaced with Expr

---
 src/prop/cnf_stream.cpp         |  4 ++--
 src/prop/cnf_stream.h           |  1 +
 src/prop/minisat/core/Solver.cc | 24 ++++++++++++++++--------
 src/prop/prop_engine.cpp        |  4 ++--
 4 files changed, 21 insertions(+), 12 deletions(-)

(limited to 'src/prop')

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index f47637b72..e7c74525d 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -75,7 +75,7 @@ void CnfStream::assertClause(TNode node, SatClause& c) {
   Debug("cnf") << "Inserting into stream " << c << endl;
   if(Dump.isOn("clauses")) {
     if(c.size() == 1) {
-      Dump("clauses") << AssertCommand(BoolExpr(getNode(c[0]).toExpr()));
+      Dump("clauses") << AssertCommand(Expr(getNode(c[0]).toExpr()));
     } else {
       Assert(c.size() > 1);
       NodeBuilder<> b(kind::OR);
@@ -83,7 +83,7 @@ void CnfStream::assertClause(TNode node, SatClause& c) {
         b << getNode(c[i]);
       }
       Node n = b;
-      Dump("clauses") << AssertCommand(BoolExpr(n.toExpr()));
+      Dump("clauses") << AssertCommand(Expr(n.toExpr()));
     }
   }
   d_satSolver->addClause(c, d_removable);
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 5efedd4ca..a6e2b2e02 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -30,6 +30,7 @@
 #include "expr/node.h"
 #include "prop/theory_proxy.h"
 #include "prop/registrar.h"
+#include "context/cdlist.h"
 
 #include <ext/hash_map>
 
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 5e19eb776..7fc7a1d9c 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -349,11 +349,11 @@ void Solver::cancelUntil(int level) {
         }
         for (int c = trail.size()-1; c >= trail_lim[level]; c--){
             Var      x  = var(trail[c]);
+            assigns [x] = l_Undef;
+            vardata[x].trail_index = -1;
+            if ((phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last()) && (polarity[x] & 0x2) == 0)
+              polarity[x] = sign(trail[c]);
             if(intro_level(x) != -1) {// might be unregistered
-              assigns [x] = l_Undef;
-              vardata[x].trail_index = -1;
-              if ((phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last()) && (polarity[x] & 0x2) == 0)
-                polarity[x] = sign(trail[c]);
               insertVarOrder(x);
             }
         }
@@ -1409,6 +1409,9 @@ void Solver::push()
   trail_ok.push(ok);
   trail_user_lim.push(trail.size());
   assert(trail_user_lim.size() == assertionLevel);
+
+  context->push();
+
   Debug("minisat") << "MINISAT PUSH assertionLevel is " << assertionLevel << ", trail.size is " << trail.size() << std::endl;
 }
 
@@ -1438,10 +1441,10 @@ void Solver::pop()
   while(downto < trail.size()) {
     Debug("minisat") << "== unassigning " << trail.last() << std::endl;
     Var      x  = var(trail.last());
+    assigns [x] = l_Undef;
+    vardata[x].trail_index = -1;
+    polarity[x] = sign(trail.last());
     if(intro_level(x) != -1) {// might be unregistered
-      assigns [x] = l_Undef;
-      vardata[x].trail_index = -1;
-      polarity[x] = sign(trail.last());
       insertVarOrder(x);
     }
     trail.pop();
@@ -1458,9 +1461,12 @@ void Solver::pop()
     Debug("minisat") << "== unassigning " << l << std::endl;
     Var      x  = var(l);
     assigns [x] = l_Undef;
+    vardata[x].trail_index = -1;
     if (phase_saving >= 1 && (polarity[x] & 0x2) == 0)
       polarity[x] = sign(l);
-    insertVarOrder(x);
+    if(intro_level(x) != -1) {// might be unregistered
+      insertVarOrder(x);
+    }
     trail_user.pop();
   }
   trail_user.pop();
@@ -1470,6 +1476,8 @@ void Solver::pop()
 
   Debug("minisat") << "about to removeClausesAboveLevel(" << assertionLevel << ") in CNF" << std::endl;
 
+  context->pop();
+
   // Notify the cnf
   proxy->removeClausesAboveLevel(assertionLevel);
 }
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 973adc67f..12e85de13 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -111,9 +111,9 @@ void PropEngine::assertLemma(TNode node, bool negated, bool removable) {
   Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl;
 
   if(!d_inCheckSat && Dump.isOn("learned")) {
-    Dump("learned") << AssertCommand(BoolExpr(node.toExpr()));
+    Dump("learned") << AssertCommand(node.toExpr());
   } else if(Dump.isOn("lemmas")) {
-    Dump("lemmas") << AssertCommand(BoolExpr(node.toExpr()));
+    Dump("lemmas") << AssertCommand(node.toExpr());
   }
 
   // Assert as removable
-- 
cgit v1.2.3