From 5c825235dd99b7c0767789db9d782e24c581ace5 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Mon, 16 Mar 2020 21:35:21 -0700 Subject: [PATCH] SmtEngine: Convert members owned by SmtEngine to unique pointers. (#4108) --- .../preprocessing_pass_context.cpp | 4 +- .../preprocessing_pass_context.h | 6 +- src/smt/smt_engine.cpp | 94 +++++++++---------- src/smt/smt_engine.h | 32 +++++-- src/smt/smt_engine_scope.cpp | 4 +- test/unit/prop/cnf_stream_white.h | 2 +- test/unit/theory/theory_arith_white.h | 4 +- test/unit/theory/theory_bv_white.h | 2 +- test/unit/theory/theory_engine_white.h | 12 ++- test/unit/theory/theory_white.h | 4 +- 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(d_logic)); + d_theoryEngine.reset(new TheoryEngine(getContext(), + getUserContext(), + d_private->d_iteRemover, + const_cast(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 d_context; /** User level context */ - context::UserContext* d_userContext; + std::unique_ptr d_userContext; /** The context levels of user pushes */ std::vector d_userLevels; @@ -1064,12 +1082,12 @@ class CVC4_PUBLIC SmtEngine NodeManager* d_nodeManager; /** The theory engine */ - TheoryEngine* d_theoryEngine; + std::unique_ptr d_theoryEngine; /** The propositional engine */ std::unique_ptr d_propEngine; /** The proof manager */ - ProofManager* d_proofManager; + std::unique_ptr 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 d_private; - StatisticsRegistry* d_statisticsRegistry; + std::unique_ptr d_statisticsRegistry; - smt::SmtEngineStatistics* d_stats; + std::unique_ptr 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( 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(); -- 2.30.2