From d382a03402d52b7b4c69779498036b23a333160a Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Sun, 15 Jun 2014 22:30:48 -0400 Subject: [PATCH] Fix compile errors with some versions of GCC. --- src/theory/bv/bitblaster_template.h | 4 ++-- src/theory/bv/bv_quick_check.h | 6 +---- src/theory/bv/lazy_bitblaster.h | 34 +++++++++++++++-------------- src/theory/bv/theory_bv_utils.h | 7 +++--- 4 files changed, 25 insertions(+), 26 deletions(-) diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h index 25de81f2c..8971d289f 100644 --- a/src/theory/bv/bitblaster_template.h +++ b/src/theory/bv/bitblaster_template.h @@ -134,9 +134,9 @@ class TLazyBitblaster : public TBitblaster { prop::BVSatSolverInterface* d_satSolver; prop::CnfStream* d_cnfStream; - AssertionList d_assertedAtoms; /**< context dependent list storing the atoms + AssertionList* d_assertedAtoms; /**< context dependent list storing the atoms currently asserted by the DPLL SAT solver. */ - ExplanationMap d_explanations; /**< context dependent list of explanations for the propagated literals. + ExplanationMap* d_explanations; /**< context dependent list of explanations for the propagated literals. Only used when bvEagerPropagate option enabled. */ VarSet d_variables; AtomSet d_bbAtoms; diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h index c09994c06..4ec9c9231 100644 --- a/src/theory/bv/bv_quick_check.h +++ b/src/theory/bv/bv_quick_check.h @@ -26,6 +26,7 @@ #include "context/cdo.h" #include "prop/sat_solver_types.h" #include "util/statistics_registry.h" +#include "theory/bv/theory_bv_utils.h" namespace CVC4 { namespace theory { @@ -34,11 +35,6 @@ class TheoryModel; namespace bv { - - -typedef __gnu_cxx::hash_set NodeSet; -typedef __gnu_cxx::hash_set TNodeSet; - class TLazyBitblaster; class TheoryBV; diff --git a/src/theory/bv/lazy_bitblaster.h b/src/theory/bv/lazy_bitblaster.h index 013e230f6..570549866 100644 --- a/src/theory/bv/lazy_bitblaster.h +++ b/src/theory/bv/lazy_bitblaster.h @@ -36,11 +36,11 @@ namespace theory { namespace bv { TLazyBitblaster::TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const std::string name, bool emptyNotify) - : TBitblaster() + : TBitblaster() , d_bv(bv) , d_ctx(c) - , d_assertedAtoms(c) - , d_explanations(c) + , d_assertedAtoms(new(true) context::CDList(c)) + , d_explanations(new(true) ExplanationMap(c)) , d_variables() , d_bbAtoms() , d_abstraction(NULL) @@ -192,8 +192,8 @@ void TLazyBitblaster::explain(TNode atom, std::vector& explanation) { ++(d_statistics.d_numExplainedPropagations); if (options::bvEagerExplanations()) { - Assert (d_explanations.find(lit) != d_explanations.end()); - const std::vector& literal_explanation = d_explanations[lit].get(); + Assert (d_explanations->find(lit) != d_explanations->end()); + const std::vector& literal_explanation = (*d_explanations)[lit].get(); for (unsigned i = 0; i < literal_explanation.size(); ++i) { explanation.push_back(d_cnfStream->getNode(literal_explanation[i])); } @@ -241,7 +241,7 @@ bool TLazyBitblaster::assertToSat(TNode lit, bool propagate) { prop::SatValue ret = d_satSolver->assertAssumption(markerLit, propagate); - d_assertedAtoms.push_back(markerLit); + d_assertedAtoms->push_back(markerLit); return ret == prop::SAT_VALUE_TRUE || ret == prop::SAT_VALUE_UNKNOWN; } @@ -256,24 +256,24 @@ bool TLazyBitblaster::assertToSat(TNode lit, bool propagate) { bool TLazyBitblaster::solve() { if (Trace.isOn("bitvector")) { Trace("bitvector") << "TLazyBitblaster::solve() asserted atoms "; - context::CDList::const_iterator it = d_assertedAtoms.begin(); - for (; it != d_assertedAtoms.end(); ++it) { + context::CDList::const_iterator it = d_assertedAtoms->begin(); + for (; it != d_assertedAtoms->end(); ++it) { Trace("bitvector") << " " << d_cnfStream->getNode(*it) << "\n"; } } - Debug("bitvector") << "TLazyBitblaster::solve() asserted atoms " << d_assertedAtoms.size() <<"\n"; + Debug("bitvector") << "TLazyBitblaster::solve() asserted atoms " << d_assertedAtoms->size() <<"\n"; return prop::SAT_VALUE_TRUE == d_satSolver->solve(); } prop::SatValue TLazyBitblaster::solveWithBudget(unsigned long budget) { if (Trace.isOn("bitvector")) { Trace("bitvector") << "TLazyBitblaster::solveWithBudget() asserted atoms "; - context::CDList::const_iterator it = d_assertedAtoms.begin(); - for (; it != d_assertedAtoms.end(); ++it) { + context::CDList::const_iterator it = d_assertedAtoms->begin(); + for (; it != d_assertedAtoms->end(); ++it) { Trace("bitvector") << " " << d_cnfStream->getNode(*it) << "\n"; } } - Debug("bitvector") << "TLazyBitblaster::solveWithBudget() asserted atoms " << d_assertedAtoms.size() <<"\n"; + Debug("bitvector") << "TLazyBitblaster::solveWithBudget() asserted atoms " << d_assertedAtoms->size() <<"\n"; return d_satSolver->solve(budget); } @@ -327,10 +327,10 @@ TLazyBitblaster::Statistics::~Statistics() { bool TLazyBitblaster::MinisatNotify::notify(prop::SatLiteral lit) { if(options::bvEagerExplanations()) { // compute explanation - if (d_lazyBB->d_explanations.find(lit) == d_lazyBB->d_explanations.end()) { + if (d_lazyBB->d_explanations->find(lit) == d_lazyBB->d_explanations->end()) { std::vector literal_explanation; d_lazyBB->d_satSolver->explain(lit, literal_explanation); - d_lazyBB->d_explanations.insert(lit, literal_explanation); + d_lazyBB->d_explanations->insert(lit, literal_explanation); } else { // we propagated it at a lower level return true; @@ -478,8 +478,10 @@ void TLazyBitblaster::clearSolver() { Assert (d_ctx->getLevel() == 0); delete d_satSolver; delete d_cnfStream; - d_assertedAtoms = context::CDList(d_ctx); - d_explanations = ExplanationMap(d_ctx); + d_assertedAtoms->deleteSelf(); + d_assertedAtoms = new(true) context::CDList(d_ctx); + d_explanations->deleteSelf(); + d_explanations = new(true) ExplanationMap(d_ctx); d_bbAtoms.clear(); d_variables.clear(); d_termCache.clear(); diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index 9679c0260..4dfea9d1d 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -24,10 +24,13 @@ #include #include "expr/node_manager.h" - namespace CVC4 { namespace theory { namespace bv { + +typedef __gnu_cxx::hash_set NodeSet; +typedef __gnu_cxx::hash_set TNodeSet; + namespace utils { inline uint32_t pow2(uint32_t power) { @@ -254,8 +257,6 @@ inline unsigned isPow2Const(TNode node) { return bv.isPow2(); } -typedef __gnu_cxx::hash_set TNodeSet; - inline Node mkOr(const std::vector& nodes) { std::set all; all.insert(nodes.begin(), nodes.end()); -- 2.30.2