diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 94 |
1 files changed, 43 insertions, 51 deletions
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()); |