incorporated dejan's constant evaluation; now getting destruction seg fault

5 files changed, 21 insertions, 17 deletions

diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h
index 73050ea73..c442fa6dd 100644
--- a/src/theory/bv/bv_subtheory.h
+++ b/src/theory/bv/bv_subtheory.h
@@ -61,7 +61,7 @@ const bool d_useSatPropagation = true;
 // forward declaration 
 class TheoryBV; 
 
-typedef context::CDQueue<TNode> AssertionQueue; 
+typedef context::CDQueue<Node> AssertionQueue; 
 /**
  * Abstract base class for bit-vector subtheory solvers
  *
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index 85ae64d05..d7dab10f9 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -32,9 +32,9 @@ CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv)
   : SubtheorySolver(c, bv),
     d_notify(*this),
     d_equalityEngine(d_notify, c, "theory::bv::TheoryBV"),
-    d_assertions(c),
     d_slicer(new Slicer(c, this)),
-    d_isCoreTheory(c, true)
+    d_isCoreTheory(c, true),
+    d_reasons(c)
 {
   if (d_useEqualityEngine) {
 
@@ -124,7 +124,8 @@ bool CoreSolver::decomposeFact(TNode fact) {
 
     explanation.push_back(fact);
     Node reason = utils::mkAnd(explanation); 
-  
+    d_reasons.insert(reason);
+    
     Assert (utils::getSize(new_a) == utils::getSize(new_b) &&
             utils::getSize(new_a) == utils::getSize(a)); 
     // FIXME: do we still need to assert these? 
@@ -132,6 +133,9 @@ bool CoreSolver::decomposeFact(TNode fact) {
     Node a_eq_new_a = nm->mkNode(kind::EQUAL, a, new_a);
     Node b_eq_new_b = nm->mkNode(kind::EQUAL, b, new_b);
 
+    d_reasons.insert(a_eq_new_a);
+    d_reasons.insert(b_eq_new_b); 
+    
     bool ok = true; 
     ok = assertFactToEqualityEngine(a_eq_new_a, utils::mkTrue());
     if (!ok) return false; 
@@ -145,6 +149,7 @@ bool CoreSolver::decomposeFact(TNode fact) {
       for (unsigned i = 0; i < new_a.getNumChildren(); ++i) {
         Node eq_i = nm->mkNode(kind::EQUAL, new_a[i], new_b[i]);
         ok = assertFactToEqualityEngine(eq_i, reason);
+        d_reasons.insert(eq_i); 
         if (!ok) return false;
       }
     }
@@ -269,8 +274,8 @@ void CoreSolver::conflict(TNode a, TNode b) {
 
 void CoreSolver::collectModelInfo(TheoryModel* m) {
   if (Debug.isOn("bitvector-model")) {
-    context::CDList<TNode>::const_iterator it = d_assertions.begin();
-    for (; it!= d_assertions.end(); ++it) {
+    context::CDQueue<Node>::const_iterator it = d_assertionQueue.begin();
+    for (; it!= d_assertionQueue.end(); ++it) {
       Debug("bitvector-model") << "CoreSolver::collectModelInfo (assert "
                                << *it << ")\n";
     }
diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h
index 230817e13..f37cf5bf3 100644
--- a/src/theory/bv/bv_subtheory_core.h
+++ b/src/theory/bv/bv_subtheory_core.h
@@ -19,6 +19,7 @@
 #include "cvc4_private.h"
 #include "theory/bv/bv_subtheory.h"
 #include "context/cdhashmap.h"
+#include "context/cdhashset.h"
 
 namespace CVC4 {
 namespace theory {
@@ -60,11 +61,10 @@ class CoreSolver : public SubtheorySolver {
   /** Store a conflict from merging two constants */
   void conflict(TNode a, TNode b);
 
-  /** FIXME: for debugging purposes only */
-  context::CDList<TNode> d_assertions;
   Slicer* d_slicer;
   context::CDO<bool> d_isCoreTheory;
-
+  /** To make sure we keep the explanations */
+  context::CDHashSet<Node, NodeHashFunction> d_reasons; 
   bool assertFactToEqualityEngine(TNode fact, TNode reason);  
   bool decomposeFact(TNode fact);
   Node getBaseDecomposition(TNode a, std::vector<TNode>& explanation);
diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp
index 474c70052..ef87e83b6 100644
--- a/src/theory/bv/slicer.cpp
+++ b/src/theory/bv/slicer.cpp
@@ -521,7 +521,6 @@ void UnionFind::ensureSlicing(const ExtractTerm& term) {
 }
 
 void UnionFind::backtrack() {
-  return; 
   int size = d_undoStack.size(); 
   for (int i = size; i > (int)d_undoStackIndex.get(); --i) {
     Operation op = d_undoStack.back(); 
@@ -619,7 +618,7 @@ void Slicer::assertEquality(TNode eq) {
 }
 
 TermId Slicer::getId(TNode node) const {
-  __gnu_cxx::hash_map<TNode, TermId, TNodeHashFunction >::const_iterator it = d_nodeToId.find(node);
+  __gnu_cxx::hash_map<Node, TermId, NodeHashFunction >::const_iterator it = d_nodeToId.find(node);
   Assert (it != d_nodeToId.end());
   return it->second; 
 }
@@ -632,7 +631,7 @@ void Slicer::registerEquality(TNode eq) {
   }
 }
 
-void Slicer::getBaseDecomposition(TNode node, std::vector<Node>& decomp, std::vector<TNode>& explanation) {
+void Slicer::getBaseDecomposition(TNode node, std::vector<Node>& decomp, std::vector<Node>& explanation) {
   Debug("bv-slicer") << "Slicer::getBaseDecomposition " << node << endl;
   
   Index high = utils::getSize(node) - 1;
@@ -652,7 +651,7 @@ void Slicer::getBaseDecomposition(TNode node, std::vector<Node>& decomp, std::ve
 
   for (unsigned i = 0; i < explanation_ids.size(); ++i) {
     Assert (hasExplanation(explanation_ids[i])); 
-    TNode exp = getExplanation(explanation_ids[i]);
+    Node exp = getExplanation(explanation_ids[i]);
     explanation.push_back(exp); 
   }
   
diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h
index 6bbe2f467..f63cf7284 100644
--- a/src/theory/bv/slicer.h
+++ b/src/theory/bv/slicer.h
@@ -315,10 +315,10 @@ class CoreSolver;
 
 class Slicer {
   __gnu_cxx::hash_map<TermId, TNode, __gnu_cxx::hash<TermId> > d_idToNode;
-  __gnu_cxx::hash_map<TNode, TermId, TNodeHashFunction> d_nodeToId;
-  __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> d_coreTermCache;
-  __gnu_cxx::hash_map<TNode, ExplanationId, TNodeHashFunction> d_explanationToId;
-  std::vector<TNode> d_explanations; 
+  __gnu_cxx::hash_map<Node, TermId, NodeHashFunction> d_nodeToId;
+  __gnu_cxx::hash_map<Node, bool, NodeHashFunction> d_coreTermCache;
+  __gnu_cxx::hash_map<Node, ExplanationId, NodeHashFunction> d_explanationToId;
+  std::vector<Node> d_explanations; 
   UnionFind d_unionFind;
 
   context::CDQueue<Node> d_newSplits;