diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2020-03-10 14:51:32 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-10 14:51:32 -0700 |
commit | e9f4cec2cad02e270747759223090c16b9d2d44c (patch) | |
tree | ff902073b926d48cb0ae23848bee4b90e96000c7 /src/smt/smt_engine.cpp | |
parent | bcaebfa163bb27e1cf14c0f763afb47b185a5f99 (diff) |
Fix issue with reset-assertions. (#3988)
Calling (reset-assertions) in start mode was not handled correctly.
Additionally, when calling (check-sat) after (reset-assertions) after a
(check-sat) call that answered unsat, we answered unsat instead of sat.
This cleans up and fixes reset-assertions) handling.
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 60 |
1 files changed, 45 insertions, 15 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index ec16409a7..bfb126e9e 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -851,8 +851,8 @@ SmtEngine::SmtEngine(ExprManager* em) d_userLevels(), d_exprManager(em), d_nodeManager(d_exprManager->getNodeManager()), - d_theoryEngine(NULL), - d_propEngine(NULL), + d_theoryEngine(nullptr), + d_propEngine(nullptr), d_proofManager(NULL), d_definedFunctions(NULL), d_fmfRecFunctionsDefined(NULL), @@ -936,14 +936,18 @@ void SmtEngine::finishInit() Trace("smt-debug") << "Making decision engine..." << std::endl; Trace("smt-debug") << "Making prop engine..." << std::endl; - d_propEngine = new PropEngine(d_theoryEngine, - d_context, - d_userContext, - d_private->getReplayLog(), - d_replayStream); + /* force destruction of referenced PropEngine to enforce that 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_private->getReplayLog(), + d_replayStream)); Trace("smt-debug") << "Setting up theory engine..." << std::endl; - d_theoryEngine->setPropEngine(d_propEngine); + d_theoryEngine->setPropEngine(getPropEngine()); Trace("smt-debug") << "Finishing init for theory engine..." << std::endl; d_theoryEngine->finishInit(); @@ -1022,10 +1026,12 @@ void SmtEngine::shutdown() { internalPop(true); } - if(d_propEngine != NULL) { + if (d_propEngine != nullptr) + { d_propEngine->shutdown(); } - if(d_theoryEngine != NULL) { + if (d_theoryEngine != nullptr) + { d_theoryEngine->shutdown(); } } @@ -1082,8 +1088,7 @@ SmtEngine::~SmtEngine() delete d_theoryEngine; d_theoryEngine = NULL; - delete d_propEngine; - d_propEngine = NULL; + d_propEngine.reset(nullptr); delete d_stats; d_stats = NULL; @@ -5546,24 +5551,49 @@ void SmtEngine::reset() void SmtEngine::resetAssertions() { SmtScope smts(this); + + if (!d_fullyInited) + { + // We're still in Start Mode, nothing asserted yet, do nothing. + // (see solver execution modes in the SMT-LIB standard) + Assert(d_context->getLevel() == 0); + Assert(d_userContext->getLevel() == 0); + DeleteAndClearCommandVector(d_modelGlobalCommands); + return; + } + doPendingPops(); Trace("smt") << "SMT resetAssertions()" << endl; - if(Dump.isOn("benchmark")) { + if (Dump.isOn("benchmark")) + { Dump("benchmark") << ResetAssertionsCommand(); } - while(!d_userLevels.empty()) { + while (!d_userLevels.empty()) + { pop(); } - // Also remember the global push/pop around everything. + // Remember the global push/pop around everything when beyond Start mode + // (see solver execution modes in the SMT-LIB standard) Assert(d_userLevels.size() == 0 && d_userContext->getLevel() == 1); d_context->popto(0); d_userContext->popto(0); DeleteAndClearCommandVector(d_modelGlobalCommands); d_userContext->push(); d_context->push(); + + /* Create new PropEngine. + * First force destruction of referenced PropEngine to enforce that + * 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_private->getReplayLog(), + d_replayStream)); } void SmtEngine::interrupt() |