From c5e230e012c57a4605e99a165934afc98bc4d9fc Mon Sep 17 00:00:00 2001 From: Tim King Date: Mon, 13 Nov 2017 15:39:56 -0800 Subject: [PATCH] Initializing SharedTermsDatabase::d_conflictPolarity. Resolves 1172045. (#1355) --- src/theory/shared_terms_database.cpp | 34 ++++++++++++++++------------ 1 file changed, 19 insertions(+), 15 deletions(-) diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp index 8e4bd5399..0b4deafb5 100644 --- a/src/theory/shared_terms_database.cpp +++ b/src/theory/shared_terms_database.cpp @@ -19,21 +19,23 @@ #include "theory/theory_engine.h" using namespace std; -using namespace CVC4; -using namespace theory; - -SharedTermsDatabase::SharedTermsDatabase(TheoryEngine* theoryEngine, context::Context* context) -: ContextNotifyObj(context) -, d_statSharedTerms("theory::shared_terms", 0) -, d_addedSharedTermsSize(context, 0) -, d_termsToTheories(context) -, d_alreadyNotifiedMap(context) -, d_registeredEqualities(context) -, d_EENotify(*this) -, d_equalityEngine(d_EENotify, context, "SharedTermsDatabase", true) -, d_theoryEngine(theoryEngine) -, d_inConflict(context, false) -{ +using namespace CVC4::theory; + +namespace CVC4 { + +SharedTermsDatabase::SharedTermsDatabase(TheoryEngine* theoryEngine, + context::Context* context) + : ContextNotifyObj(context), + d_statSharedTerms("theory::shared_terms", 0), + d_addedSharedTermsSize(context, 0), + d_termsToTheories(context), + d_alreadyNotifiedMap(context), + d_registeredEqualities(context), + d_EENotify(*this), + d_equalityEngine(d_EENotify, context, "SharedTermsDatabase", true), + d_theoryEngine(theoryEngine), + d_inConflict(context, false), + d_conflictPolarity() { smtStatisticsRegistry()->registerStat(&d_statSharedTerms); } @@ -261,3 +263,5 @@ Node SharedTermsDatabase::explain(TNode literal) const { d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions); return mkAnd(assumptions); } + +} /* namespace CVC4 */ -- 2.30.2