From b791a54377d468946a3aec7e740f4eb33c640372 Mon Sep 17 00:00:00 2001 From: lianah Date: Thu, 21 Mar 2013 15:43:58 -0400 Subject: [PATCH] incorporated dejan's constant evaluation; now getting destruction seg fault --- src/theory/bv/bv_subtheory.h | 2 +- src/theory/bv/bv_subtheory_core.cpp | 15 ++++++++++----- src/theory/bv/bv_subtheory_core.h | 6 +++--- src/theory/bv/slicer.cpp | 7 +++---- src/theory/bv/slicer.h | 8 ++++---- 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 AssertionQueue; +typedef context::CDQueue 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::const_iterator it = d_assertions.begin(); - for (; it!= d_assertions.end(); ++it) { + context::CDQueue::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 d_assertions; Slicer* d_slicer; context::CDO d_isCoreTheory; - + /** To make sure we keep the explanations */ + context::CDHashSet d_reasons; bool assertFactToEqualityEngine(TNode fact, TNode reason); bool decomposeFact(TNode fact); Node getBaseDecomposition(TNode a, std::vector& 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::const_iterator it = d_nodeToId.find(node); + __gnu_cxx::hash_map::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& decomp, std::vector& explanation) { +void Slicer::getBaseDecomposition(TNode node, std::vector& decomp, std::vector& 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& 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 > d_idToNode; - __gnu_cxx::hash_map d_nodeToId; - __gnu_cxx::hash_map d_coreTermCache; - __gnu_cxx::hash_map d_explanationToId; - std::vector d_explanations; + __gnu_cxx::hash_map d_nodeToId; + __gnu_cxx::hash_map d_coreTermCache; + __gnu_cxx::hash_map d_explanationToId; + std::vector d_explanations; UnionFind d_unionFind; context::CDQueue d_newSplits; -- 2.30.2