SmtEngine: Convert members owned by SmtEngine to unique pointers. (#4108)

5 files changed, 14 insertions, 10 deletions

diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h
index 62ba6f7da..b08221cf0 100644
--- a/test/unit/prop/cnf_stream_white.h
+++ b/test/unit/prop/cnf_stream_white.h
@@ -140,7 +140,7 @@ class CnfStreamWhite : public CxxTest::TestSuite {
     // engine d_smt. We must ensure that d_smt is properly initialized via
     // the following call, which constructs its underlying theory engine.
     d_smt->finalOptionsAreSet();
-    d_theoryEngine = d_smt->d_theoryEngine;
+    d_theoryEngine = d_smt->getTheoryEngine();
 
     d_satSolver = new FakeSatSolver();
     d_cnfContext = new context::Context();
diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h
index 2c696af91..7404bceaa 100644
--- a/test/unit/theory/theory_arith_white.h
+++ b/test/unit/theory/theory_arith_white.h
@@ -103,8 +103,8 @@ public:
     d_nm = NodeManager::fromExprManager(d_em);
     d_smt = new SmtEngine(d_em);
     d_smt->setOption("incremental", CVC4::SExpr(false));
-    d_ctxt = d_smt->d_context;
-    d_uctxt = d_smt->d_userContext;
+    d_ctxt = d_smt->getContext();
+    d_uctxt = d_smt->getUserContext();
     d_scope = new SmtScope(d_smt);
     d_outputChannel.clear();
     d_logicInfo.lock();
diff --git a/test/unit/theory/theory_bv_white.h b/test/unit/theory/theory_bv_white.h
index 5af01c0cf..051de83dc 100644
--- a/test/unit/theory/theory_bv_white.h
+++ b/test/unit/theory/theory_bv_white.h
@@ -79,7 +79,7 @@ public:
     EagerBitblaster* bb = new EagerBitblaster(
         dynamic_cast<TheoryBV*>(
             d_smt->d_theoryEngine->d_theoryTable[THEORY_BV]),
-        d_smt->d_context);
+        d_smt->getContext());
     Node x = d_nm->mkVar("x", d_nm->mkBitVectorType(16));
     Node y = d_nm->mkVar("y", d_nm->mkBitVectorType(16));
     Node x_plus_y = d_nm->mkNode(kind::BITVECTOR_PLUS, x, y);
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index 88f8ed6dd..5af670d5e 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -215,7 +215,11 @@ public:
   void registerTerm(TNode) { Unimplemented(); }
   void check(Theory::Effort) override { Unimplemented(); }
   void propagate(Theory::Effort) override { Unimplemented(); }
-  Node explain(TNode) override { Unimplemented(); }
+  Node explain(TNode) override
+  {
+    Unimplemented();
+    return Node::null();
+  }
   Node getValue(TNode n) { return Node::null(); }
 };/* class FakeTheory */
 
@@ -246,8 +250,8 @@ public:
     d_nm = NodeManager::fromExprManager(d_em);
     d_scope = new SmtScope(d_smt);
 
-    d_ctxt = d_smt->d_context;
-    d_uctxt = d_smt->d_userContext;
+    d_ctxt = d_smt->getContext();
+    d_uctxt = d_smt->getUserContext();
 
     d_nullChannel = new FakeOutputChannel();
 
@@ -255,7 +259,7 @@ public:
     // engine d_smt. We must ensure that d_smt is properly initialized via
     // the following call, which constructs its underlying theory engine.
     d_smt->finalOptionsAreSet();
-    d_theoryEngine = d_smt->d_theoryEngine;
+    d_theoryEngine = d_smt->getTheoryEngine();
     for(TheoryId id = THEORY_FIRST; id != THEORY_LAST; ++id) {
       delete d_theoryEngine->d_theoryOut[id];
       delete d_theoryEngine->d_theoryTable[id];
diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h
index 5f7543f05..0dd52be8c 100644
--- a/test/unit/theory/theory_white.h
+++ b/test/unit/theory/theory_white.h
@@ -162,8 +162,8 @@ class TheoryBlack : public CxxTest::TestSuite {
     d_em = new ExprManager();
     d_nm = NodeManager::fromExprManager(d_em);
     d_smt = new SmtEngine(d_em);
-    d_ctxt = d_smt->d_context;
-    d_uctxt = d_smt->d_userContext;
+    d_ctxt = d_smt->getContext();
+    d_uctxt = d_smt->getUserContext();
     d_scope = new SmtScope(d_smt);
     d_logicInfo = new LogicInfo();
     d_logicInfo->lock();