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

10 files changed, 89 insertions, 75 deletions

diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp
index b04c05b9e..75085d7c4 100644
--- a/src/preprocessing/preprocessing_pass_context.cpp
+++ b/src/preprocessing/preprocessing_pass_context.cpp
@@ -29,9 +29,9 @@ PreprocessingPassContext::PreprocessingPassContext(
     : d_smt(smt),
       d_resourceManager(resourceManager),
       d_iteRemover(iteRemover),
-      d_topLevelSubstitutions(smt->d_userContext),
+      d_topLevelSubstitutions(smt->getUserContext()),
       d_circuitPropagator(circuitPropagator),
-      d_symsInAssertions(smt->d_userContext)
+      d_symsInAssertions(smt->getUserContext())
 {
 }
 
diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h
index 106b1aadb..f4317d786 100644
--- a/src/preprocessing/preprocessing_pass_context.h
+++ b/src/preprocessing/preprocessing_pass_context.h
@@ -44,10 +44,10 @@ class PreprocessingPassContext
       theory::booleans::CircuitPropagator* circuitPropagator);
 
   SmtEngine* getSmt() { return d_smt; }
-  TheoryEngine* getTheoryEngine() { return d_smt->d_theoryEngine; }
+  TheoryEngine* getTheoryEngine() { return d_smt->getTheoryEngine(); }
   prop::PropEngine* getPropEngine() { return d_smt->getPropEngine(); }
-  context::Context* getUserContext() { return d_smt->d_userContext; }
-  context::Context* getDecisionContext() { return d_smt->d_context; }
+  context::Context* getUserContext() { return d_smt->getUserContext(); }
+  context::Context* getDecisionContext() { return d_smt->getContext(); }
   RemoveTermFormulas* getIteRemover() { return d_iteRemover; }
 
   theory::booleans::CircuitPropagator* getCircuitPropagator()
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index d2919143b..3f8160ce9 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -557,15 +557,15 @@ class SmtEnginePrivate : public NodeManagerListener {
         d_listenerRegistrations(new ListenerRegistrationList()),
         d_propagator(true, true),
         d_assertions(),
-        d_assertionsProcessed(smt.d_userContext, false),
+        d_assertionsProcessed(smt.getUserContext(), false),
         d_fakeContext(),
         d_abstractValueMap(&d_fakeContext),
         d_abstractValues(),
         d_simplifyAssertionsDepth(0),
         // d_needsExpandDefs(true),  //TODO?
-        d_exprNames(smt.d_userContext),
-        d_iteRemover(smt.d_userContext),
-        d_sygusConjectureStale(smt.d_userContext, true)
+        d_exprNames(smt.getUserContext()),
+        d_iteRemover(smt.getUserContext()),
+        d_sygusConjectureStale(smt.getUserContext(), true)
   {
     d_smt.d_nodeManager->subscribeEvents(this);
     d_true = NodeManager::currentNM()->mkConst(true);
@@ -853,13 +853,13 @@ SmtEngine::SmtEngine(ExprManager* em)
       d_nodeManager(d_exprManager->getNodeManager()),
       d_theoryEngine(nullptr),
       d_propEngine(nullptr),
-      d_proofManager(NULL),
-      d_definedFunctions(NULL),
-      d_fmfRecFunctionsDefined(NULL),
-      d_assertionList(NULL),
-      d_assignments(NULL),
+      d_proofManager(nullptr),
+      d_definedFunctions(nullptr),
+      d_fmfRecFunctionsDefined(nullptr),
+      d_assertionList(nullptr),
+      d_assignments(nullptr),
       d_modelGlobalCommands(),
-      d_modelCommands(NULL),
+      d_modelCommands(nullptr),
       d_dumpCommands(),
       d_defineCommands(),
       d_logic(),
@@ -874,34 +874,34 @@ SmtEngine::SmtEngine(ExprManager* em)
       d_status(),
       d_expectedStatus(),
       d_smtMode(SMT_MODE_START),
-      d_replayStream(NULL),
-      d_private(NULL),
-      d_statisticsRegistry(NULL),
-      d_stats(NULL)
+      d_replayStream(nullptr),
+      d_private(nullptr),
+      d_statisticsRegistry(nullptr),
+      d_stats(nullptr)
 {
   SmtScope smts(this);
   d_originalOptions.copyValues(em->getOptions());
-  d_private = new smt::SmtEnginePrivate(*this);
-  d_statisticsRegistry = new StatisticsRegistry();
-  d_stats = new SmtEngineStatistics();
+  d_private.reset(new smt::SmtEnginePrivate(*this));
+  d_statisticsRegistry.reset(new StatisticsRegistry());
+  d_stats.reset(new SmtEngineStatistics());
   d_stats->d_resourceUnitsUsed.setData(
       d_private->getResourceManager()->getResourceUsage());
 
   // The ProofManager is constructed before any other proof objects such as
   // SatProof and TheoryProofs. The TheoryProofEngine and the SatProof are
   // initialized in TheoryEngine and PropEngine respectively.
-  Assert(d_proofManager == NULL);
+  Assert(d_proofManager == nullptr);
 
   // d_proofManager must be created before Options has been finished
   // being parsed from the input file. Because of this, we cannot trust
   // that options::proof() is set correctly yet.
 #ifdef CVC4_PROOF
-  d_proofManager = new ProofManager(d_userContext);
+  d_proofManager.reset(new ProofManager(getUserContext()));
 #endif
 
-  d_definedFunctions = new (true) DefinedFunctionMap(d_userContext);
-  d_fmfRecFunctionsDefined = new (true) NodeList(d_userContext);
-  d_modelCommands = new (true) smt::CommandList(d_userContext);
+  d_definedFunctions = new (true) DefinedFunctionMap(getUserContext());
+  d_fmfRecFunctionsDefined = new (true) NodeList(getUserContext());
+  d_modelCommands = new (true) smt::CommandList(getUserContext());
 }
 
 void SmtEngine::finishInit()
@@ -909,21 +909,21 @@ void SmtEngine::finishInit()
   Trace("smt-debug") << "SmtEngine::finishInit" << std::endl;
   // We have mutual dependency here, so we add the prop engine to the theory
   // engine later (it is non-essential there)
-  d_theoryEngine = new TheoryEngine(d_context,
-                                    d_userContext,
-                                    d_private->d_iteRemover,
-                                    const_cast<const LogicInfo&>(d_logic));
+  d_theoryEngine.reset(new TheoryEngine(getContext(),
+                                        getUserContext(),
+                                        d_private->d_iteRemover,
+                                        const_cast<const LogicInfo&>(d_logic)));
 
   // Add the theories
   for(TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
-    TheoryConstructor::addTheory(d_theoryEngine, id);
+    TheoryConstructor::addTheory(getTheoryEngine(), id);
     //register with proof engine if applicable
 #ifdef CVC4_PROOF
     ProofManager::currentPM()->getTheoryProofEngine()->registerTheory(d_theoryEngine->theoryOf(id));
 #endif
   }
 
-  d_private->addUseTheoryListListener(d_theoryEngine);
+  d_private->addUseTheoryListListener(getTheoryEngine());
 
   // ensure that our heuristics are properly set up
   setDefaults();
@@ -935,9 +935,9 @@ void SmtEngine::finishInit()
    * are unregistered by the obsolete PropEngine object before registered
    * again by the new PropEngine object */
   d_propEngine.reset(nullptr);
-  d_propEngine.reset(new PropEngine(d_theoryEngine,
-                                    d_context,
-                                    d_userContext,
+  d_propEngine.reset(new PropEngine(getTheoryEngine(),
+                                    getContext(),
+                                    getUserContext(),
                                     d_private->getReplayLog(),
                                     d_replayStream));
 
@@ -960,7 +960,7 @@ void SmtEngine::finishInit()
      options::incrementalSolving()) {
     // In the case of incremental solving, we appear to need these to
     // ensure the relevant Nodes remain live.
-    d_assertionList = new(true) AssertionList(d_userContext);
+    d_assertionList = new (true) AssertionList(getUserContext());
   }
 
   // dump out a set-logic command only when raw-benchmark is disabled to avoid
@@ -1082,27 +1082,19 @@ SmtEngine::~SmtEngine()
     // Because the destruction of the proofs depends on contexts owned be the
     // theory solvers.
 #ifdef CVC4_PROOF
-    delete d_proofManager;
-    d_proofManager = NULL;
+    d_proofManager.reset(nullptr);
 #endif
 
-    delete d_theoryEngine;
-    d_theoryEngine = NULL;
+    d_theoryEngine.reset(nullptr);
     d_propEngine.reset(nullptr);
 
-    delete d_stats;
-    d_stats = NULL;
-    delete d_statisticsRegistry;
-    d_statisticsRegistry = NULL;
+    d_stats.reset(nullptr);
+    d_statisticsRegistry.reset(nullptr);
 
-    delete d_private;
-    d_private = NULL;
-
-    delete d_userContext;
-    d_userContext = NULL;
-    delete d_context;
-    d_context = NULL;
+    d_private.reset(nullptr);
 
+    d_userContext.reset(nullptr);
+    d_context.reset(nullptr);
   } catch(Exception& e) {
     Warning() << "CVC4 threw an exception during cleanup." << endl
               << e << endl;
@@ -4298,7 +4290,7 @@ bool SmtEngine::addToAssignment(const Expr& ex) {
     return false;
   }
   if(d_assignments == NULL) {
-    d_assignments = new(true) AssignmentSet(d_context);
+    d_assignments = new (true) AssignmentSet(getContext());
   }
   d_assignments->insert(n);
 
@@ -5548,9 +5540,9 @@ void SmtEngine::resetAssertions()
    * statistics are unregistered by the obsolete PropEngine object before
    * registered again by the new PropEngine object */
   d_propEngine.reset(nullptr);
-  d_propEngine.reset(new PropEngine(d_theoryEngine,
-                                    d_context,
-                                    d_userContext,
+  d_propEngine.reset(new PropEngine(getTheoryEngine(),
+                                    getContext(),
+                                    getUserContext(),
                                     d_private->getReplayLog(),
                                     d_replayStream));
   d_theoryEngine->setPropEngine(getPropEngine());
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 61f8b7540..fbd92bcf2 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -859,9 +859,27 @@ class CVC4_PUBLIC SmtEngine
   SmtEngine(const SmtEngine&) = delete;
   SmtEngine& operator=(const SmtEngine&) = delete;
 
+  /** Get a pointer to the TheoryEngine owned by this SmtEngine. */
+  TheoryEngine* getTheoryEngine() { return d_theoryEngine.get(); }
+
   /** Get a pointer to the PropEngine owned by this SmtEngine. */
   prop::PropEngine* getPropEngine() { return d_propEngine.get(); }
 
+  /** Get a pointer to the UserContext owned by this SmtEngine. */
+  context::UserContext* getUserContext() { return d_userContext.get(); };
+
+  /** Get a pointer to the Context owned by this SmtEngine. */
+  context::Context* getContext() { return d_context.get(); };
+
+  /** Get a pointer to the ProofManager owned by this SmtEngine. */
+  ProofManager* getProofManager() { return d_proofManager.get(); };
+
+  /** Get a pointer to the StatisticsRegistry owned by this SmtEngine. */
+  StatisticsRegistry* getStatisticsRegistry()
+  {
+    return d_statisticsRegistry.get();
+  };
+
   /**
    * Check that a generated proof (via getProof()) checks.
    */
@@ -1052,9 +1070,9 @@ class CVC4_PUBLIC SmtEngine
   /* Members -------------------------------------------------------------- */
 
   /** Expr manager context */
-  context::Context* d_context;
+  std::unique_ptr<context::Context> d_context;
   /** User level context */
-  context::UserContext* d_userContext;
+  std::unique_ptr<context::UserContext> d_userContext;
   /** The context levels of user pushes */
   std::vector<int> d_userLevels;
 
@@ -1064,12 +1082,12 @@ class CVC4_PUBLIC SmtEngine
   NodeManager* d_nodeManager;
 
   /** The theory engine */
-  TheoryEngine* d_theoryEngine;
+  std::unique_ptr<TheoryEngine> d_theoryEngine;
   /** The propositional engine */
   std::unique_ptr<prop::PropEngine> d_propEngine;
 
   /** The proof manager */
-  ProofManager* d_proofManager;
+  std::unique_ptr<ProofManager> d_proofManager;
 
   /** An index of our defined functions */
   DefinedFunctionMap* d_definedFunctions;
@@ -1235,11 +1253,11 @@ class CVC4_PUBLIC SmtEngine
   /**
    * A private utility class to SmtEngine.
    */
-  smt::SmtEnginePrivate* d_private;
+  std::unique_ptr<smt::SmtEnginePrivate> d_private;
 
-  StatisticsRegistry* d_statisticsRegistry;
+  std::unique_ptr<StatisticsRegistry> d_statisticsRegistry;
 
-  smt::SmtEngineStatistics* d_stats;
+  std::unique_ptr<smt::SmtEngineStatistics> d_stats;
 
   /*---------------------------- sygus commands  ---------------------------*/
 
diff --git a/src/smt/smt_engine_scope.cpp b/src/smt/smt_engine_scope.cpp
index 4b593f075..55af4bfd2 100644
--- a/src/smt/smt_engine_scope.cpp
+++ b/src/smt/smt_engine_scope.cpp
@@ -38,7 +38,7 @@ bool smtEngineInScope() { return s_smtEngine_current != NULL; }
 ProofManager* currentProofManager() {
 #if IS_PROOFS_BUILD
   Assert(s_smtEngine_current != NULL);
-  return s_smtEngine_current->d_proofManager;
+  return s_smtEngine_current->getProofManager();
 #else  /* IS_PROOFS_BUILD */
   InternalError()
       << "proofs/unsat cores are not on, but ProofManager requested";
@@ -62,7 +62,7 @@ SmtScope::~SmtScope() {
 
 StatisticsRegistry* SmtScope::currentStatisticsRegistry() {
   Assert(smtEngineInScope());
-  return s_smtEngine_current->d_statisticsRegistry;
+  return s_smtEngine_current->getStatisticsRegistry();
 }
 
 }/* CVC4::smt namespace */
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();