Fix compile errors with some versions of GCC.

diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h
index 25de81f2ca657feb42a8a4f01fbdcf25e37a701b..8971d289f2c9f9a4b99cb19c04f588771fa7682f 100644 (file)
--- a/src/theory/bv/bitblaster_template.h
+++ b/src/theory/bv/bitblaster_template.h
@@ -134,9 +134,9 @@ class TLazyBitblaster :  public TBitblaster<Node> {
   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 c09994c0644be75acd3760b47b8403fc21d08b31..4ec9c9231521fc61b008e2852fdcf9e077cc46f0 100644 (file)
--- 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<Node, NodeHashFunction> NodeSet;
-typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
-
 class TLazyBitblaster; 
 class TheoryBV;
 

diff --git a/src/theory/bv/lazy_bitblaster.h b/src/theory/bv/lazy_bitblaster.h
index 013e230f6c6a678722f962c7f54182f89269cbba..57054986655c7a2c4a5022f71b4c1a35d08a6e4a 100644 (file)
--- 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<Node>()
   , d_bv(bv)
   , d_ctx(c)
-  , d_assertedAtoms(c)
-  , d_explanations(c)
+  , d_assertedAtoms(new(true) context::CDList<prop::SatLiteral>(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<TNode>& explanation) {
 
   ++(d_statistics.d_numExplainedPropagations);
   if (options::bvEagerExplanations()) {
-    Assert (d_explanations.find(lit) != d_explanations.end());
-    const std::vector<prop::SatLiteral>& literal_explanation = d_explanations[lit].get();
+    Assert (d_explanations->find(lit) != d_explanations->end());
+    const std::vector<prop::SatLiteral>& 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<prop::SatLiteral>::const_iterator it = d_assertedAtoms.begin();
-    for (; it != d_assertedAtoms.end(); ++it) {
+    context::CDList<prop::SatLiteral>::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<prop::SatLiteral>::const_iterator it = d_assertedAtoms.begin();
-    for (; it != d_assertedAtoms.end(); ++it) {
+    context::CDList<prop::SatLiteral>::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<prop::SatLiteral> 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<prop::SatLiteral>(d_ctx);
-  d_explanations = ExplanationMap(d_ctx);
+  d_assertedAtoms->deleteSelf();
+  d_assertedAtoms = new(true) context::CDList<prop::SatLiteral>(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 9679c0260db68e9d2dbc8b90fc8c2141ff9a4600..4dfea9d1d5b913d2cca6fa8c9b08170b503489cb 100644 (file)
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -24,10 +24,13 @@
 #include <sstream>
 #include "expr/node_manager.h"
 
-
 namespace CVC4 {
 namespace theory {
 namespace bv {
+
+typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
+typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> 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<TNode, TNodeHashFunction> TNodeSet;
-
 inline Node mkOr(const std::vector<Node>& nodes) {
   std::set<TNode> all;
   all.insert(nodes.begin(), nodes.end());