diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-12 00:08:32 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-11 22:08:32 -0700 |
commit | 66836c5fd879c92bddbca52d4b1802213f227a44 (patch) | |
tree | b0434cc3be08802a0028193ca91bda2c0e802af6 /src/smt/smt_engine_state.cpp | |
parent | b5b2858807d48136807aba29bb53a1e91cfacc6e (diff) |
Split SmtEngineState from SmtEngine (#4855)
This splits a utility for tracking the "basic" state of the SmtEngine. This class tracks its high-level state, including the "SMT mode", last/expected status and manages the contexts. It is not responsible more detailed state information (e.g. the assertions).
Diffstat (limited to 'src/smt/smt_engine_state.cpp')
-rw-r--r-- | src/smt/smt_engine_state.cpp | 298 |
1 files changed, 298 insertions, 0 deletions
diff --git a/src/smt/smt_engine_state.cpp b/src/smt/smt_engine_state.cpp new file mode 100644 index 000000000..07f1d3321 --- /dev/null +++ b/src/smt/smt_engine_state.cpp @@ -0,0 +1,298 @@ +/********************* */ +/*! \file smt_engine_state.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Utility for maintaining the state of the SMT engine. + **/ + +#include "smt/smt_engine_state.h" + +#include "options/smt_options.h" +#include "smt/smt_engine.h" + +namespace CVC4 { +namespace smt { + +SmtEngineState::SmtEngineState(SmtEngine& smt) + : d_smt(smt), + d_context(new context::Context()), + d_userContext(new context::UserContext()), + d_pendingPops(0), + d_fullyInited(false), + d_queryMade(false), + d_needPostsolve(false), + d_status(), + d_expectedStatus(), + d_smtMode(SmtMode::START) +{ +} + +void SmtEngineState::notifyExpectedStatus(const std::string& status) +{ + Assert(status == "sat" || status == "unsat" || status == "unknown") + << "SmtEngineState::notifyExpectedStatus: unexpected status string " + << status; + d_expectedStatus = Result(status, d_filename); +} + +void SmtEngineState::notifyResetAssertions() +{ + doPendingPops(); + while (!d_userLevels.empty()) + { + userPop(); + } + // 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); + popto(0); +} + +void SmtEngineState::notifyCheckSat(bool hasAssumptions) +{ + // process the pending pops + doPendingPops(); + if (d_queryMade && !options::incrementalSolving()) + { + throw ModalException( + "Cannot make multiple queries unless " + "incremental solving is enabled " + "(try --incremental)"); + } + + // Note that a query has been made and we are in assert mode + d_queryMade = true; + d_smtMode = SmtMode::ASSERT; + + // push if there are assumptions + if (hasAssumptions) + { + internalPush(); + } +} + +void SmtEngineState::notifyCheckSatResult(bool hasAssumptions, Result r) +{ + d_needPostsolve = true; + + // Pop the context + if (hasAssumptions) + { + internalPop(); + } + + // Remember the status + d_status = r; + // Check against expected status + if (!d_expectedStatus.isUnknown() && !d_status.isUnknown() + && d_status != d_expectedStatus) + { + CVC4_FATAL() << "Expected result " << d_expectedStatus << " but got " + << d_status; + } + // clear expected status + d_expectedStatus = Result(); + // Update the SMT mode + switch (d_status.asSatisfiabilityResult().isSat()) + { + case Result::UNSAT: d_smtMode = SmtMode::UNSAT; break; + case Result::SAT: d_smtMode = SmtMode::SAT; break; + default: d_smtMode = SmtMode::SAT_UNKNOWN; + } +} + +void SmtEngineState::notifyGetAbduct(bool success) +{ + if (success) + { + // successfully generated an abduct, update to abduct state + d_smtMode = SmtMode::ABDUCT; + } + else + { + // failed, we revert to the assert state + d_smtMode = SmtMode::ASSERT; + } +} + +void SmtEngineState::setup() +{ + // push a context + push(); +} + +void SmtEngineState::finishInit() +{ + // set the flag to remember that we are fully initialized + d_fullyInited = true; +} + +void SmtEngineState::shutdown() +{ + doPendingPops(); + + while (options::incrementalSolving() && d_userContext->getLevel() > 1) + { + internalPop(true); + } +} + +void SmtEngineState::cleanup() +{ + // pop to level zero + popto(0); +} + +void SmtEngineState::setFilename(const std::string& filename) +{ + d_filename = filename; +} + +void SmtEngineState::userPush() +{ + if (!options::incrementalSolving()) + { + throw ModalException( + "Cannot push when not solving incrementally (use --incremental)"); + } + // The problem isn't really "extended" yet, but this disallows + // get-model after a push, simplifying our lives somewhat and + // staying symmetric with pop. + d_smtMode = SmtMode::ASSERT; + + d_userLevels.push_back(d_userContext->getLevel()); + internalPush(); + Trace("userpushpop") << "SmtEngineState: pushed to level " + << d_userContext->getLevel() << std::endl; +} + +void SmtEngineState::userPop() +{ + if (!options::incrementalSolving()) + { + throw ModalException( + "Cannot pop when not solving incrementally (use --incremental)"); + } + if (d_userLevels.size() == 0) + { + throw ModalException("Cannot pop beyond the first user frame"); + } + // The problem isn't really "extended" yet, but this disallows + // get-model after a pop, simplifying our lives somewhat. It might + // not be strictly necessary to do so, since the pops occur lazily, + // but also it would be weird to have a legally-executed (get-model) + // that only returns a subset of the assignment (because the rest + // is no longer in scope!). + d_smtMode = SmtMode::ASSERT; + + AlwaysAssert(d_userContext->getLevel() > 0); + AlwaysAssert(d_userLevels.back() < d_userContext->getLevel()); + while (d_userLevels.back() < d_userContext->getLevel()) + { + internalPop(true); + } + d_userLevels.pop_back(); +} + +void SmtEngineState::push() +{ + d_userContext->push(); + d_context->push(); +} + +void SmtEngineState::pop() +{ + d_userContext->pop(); + d_context->pop(); +} + +void SmtEngineState::popto(int toLevel) +{ + d_context->popto(toLevel); + d_userContext->popto(toLevel); +} + +context::UserContext* SmtEngineState::getUserContext() +{ + return d_userContext.get(); +} + +context::Context* SmtEngineState::getContext() { return d_context.get(); } + +Result SmtEngineState::getStatus() const { return d_status; } + +bool SmtEngineState::isFullyInited() const { return d_fullyInited; } +bool SmtEngineState::isFullyReady() const +{ + return d_fullyInited && d_pendingPops == 0; +} +bool SmtEngineState::isQueryMade() const { return d_queryMade; } +size_t SmtEngineState::getNumUserLevels() const { return d_userLevels.size(); } + +SmtMode SmtEngineState::getMode() const { return d_smtMode; } + +const std::string& SmtEngineState::getFilename() const { return d_filename; } + +void SmtEngineState::internalPush() +{ + Assert(d_fullyInited); + Trace("smt") << "SmtEngineState::internalPush()" << std::endl; + doPendingPops(); + if (options::incrementalSolving()) + { + // notifies the SmtEngine to process the assertions immediately + d_smt.notifyPushPre(); + d_userContext->push(); + // the context push is done inside of the SAT solver + d_smt.notifyPushPost(); + } +} + +void SmtEngineState::internalPop(bool immediate) +{ + Assert(d_fullyInited); + Trace("smt") << "SmtEngineState::internalPop()" << std::endl; + if (options::incrementalSolving()) + { + ++d_pendingPops; + } + if (immediate) + { + doPendingPops(); + } +} + +void SmtEngineState::doPendingPops() +{ + Trace("smt") << "SmtEngineState::doPendingPops()" << std::endl; + Assert(d_pendingPops == 0 || options::incrementalSolving()); + // check to see if a postsolve() is pending + if (d_needPostsolve) + { + d_smt.notifyPostSolvePre(); + } + while (d_pendingPops > 0) + { + // the context pop is done inside of the SAT solver + d_smt.notifyPopPre(); + // pop the context + d_userContext->pop(); + --d_pendingPops; + // no need for pop post (for now) + } + if (d_needPostsolve) + { + d_smt.notifyPostSolvePost(); + d_needPostsolve = false; + } +} + +} // namespace smt +} // namespace CVC4 |