From: Tim King <taking@cs.nyu.edu>
Date: Mon, 13 Nov 2017 23:39:56 +0000 (-0800)
Subject: Initializing SharedTermsDatabase::d_conflictPolarity. Resolves 1172045. (#1355)
X-Git-Tag: cvc5-1.0.0~5484
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c5e230e012c57a4605e99a165934afc98bc4d9fc;p=cvc5.git

Initializing SharedTermsDatabase::d_conflictPolarity. Resolves 1172045. (#1355)
---

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 */