diff options
author | Tim King <taking@cs.nyu.edu> | 2017-11-13 15:39:56 -0800 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-13 17:39:56 -0600 |
commit | c5e230e012c57a4605e99a165934afc98bc4d9fc (patch) | |
tree | 2e9cdfa996b9d06d66fa50369104a24af57cd928 | |
parent | c3c7e380f2997c95a8356685cfa5dd32f1b4e211 (diff) |
Initializing SharedTermsDatabase::d_conflictPolarity. Resolves 1172045. (#1355)
-rw-r--r-- | src/theory/shared_terms_database.cpp | 34 |
1 files 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 */ |