From 077c191da9739ebb09e689a4809abbf779d99593 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Tue, 12 Oct 2021 10:53:03 -0700 Subject: Rename SmtEngineState to SolverEngineState. (#7344) --- src/CMakeLists.txt | 4 +- src/smt/quant_elim_solver.cpp | 2 +- src/smt/smt_engine_state.cpp | 302 --------------------------------------- src/smt/smt_engine_state.h | 249 -------------------------------- src/smt/smt_solver.cpp | 4 +- src/smt/smt_solver.h | 6 +- src/smt/solver_engine.cpp | 4 +- src/smt/solver_engine.h | 6 +- src/smt/solver_engine_state.cpp | 305 ++++++++++++++++++++++++++++++++++++++++ src/smt/solver_engine_state.h | 249 ++++++++++++++++++++++++++++++++ 10 files changed, 567 insertions(+), 564 deletions(-) delete mode 100644 src/smt/smt_engine_state.cpp delete mode 100644 src/smt/smt_engine_state.h create mode 100644 src/smt/solver_engine_state.cpp create mode 100644 src/smt/solver_engine_state.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 52f2f2065..733186d16 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -351,8 +351,8 @@ libcvc5_add_sources( smt/solver_engine.h smt/solver_engine_scope.cpp smt/solver_engine_scope.h - smt/smt_engine_state.cpp - smt/smt_engine_state.h + smt/solver_engine_state.cpp + smt/solver_engine_state.h smt/solver_engine_stats.cpp smt/solver_engine_stats.h smt/smt_mode.cpp diff --git a/src/smt/quant_elim_solver.cpp b/src/smt/quant_elim_solver.cpp index 5ccb2cf14..8bd29b16f 100644 --- a/src/smt/quant_elim_solver.cpp +++ b/src/smt/quant_elim_solver.cpp @@ -72,7 +72,7 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as, << std::endl; Assert(ne.getNumChildren() == 3); // We consider this to be an entailment check, which also avoids incorrect - // status reporting (see SmtEngineState::d_expectedStatus). + // status reporting (see SolverEngineState::d_expectedStatus). Result r = d_smtSolver.checkSatisfiability(as, std::vector{ne}, true); Trace("smt-qe") << "Query returned " << r << std::endl; if (r.asSatisfiabilityResult().isSat() != Result::UNSAT) diff --git a/src/smt/smt_engine_state.cpp b/src/smt/smt_engine_state.cpp deleted file mode 100644 index becfd1466..000000000 --- a/src/smt/smt_engine_state.cpp +++ /dev/null @@ -1,302 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Morgan Deters, Ying Sheng - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Utility for maintaining the state of the SMT engine. - */ - -#include "smt/smt_engine_state.h" - -#include "base/modal_exception.h" -#include "options/base_options.h" -#include "options/main_options.h" -#include "options/option_exception.h" -#include "options/smt_options.h" -#include "smt/env.h" -#include "smt/solver_engine.h" - -namespace cvc5 { -namespace smt { - -SmtEngineState::SmtEngineState(Env& env, SolverEngine& slv) - : EnvObj(env), - d_slv(slv), - 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, options().driver.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 && userContext()->getLevel() == 1); - popto(0); -} - -void SmtEngineState::notifyCheckSat(bool hasAssumptions) -{ - // process the pending pops - doPendingPops(); - if (d_queryMade && !options().base.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) - { - CVC5_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::notifyGetInterpol(bool success) -{ - if (success) - { - // successfully generated an interpolant, update to interpol state - d_smtMode = SmtMode::INTERPOL; - } - 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().base.incrementalSolving && userContext()->getLevel() > 1) - { - internalPop(true); - } -} - -void SmtEngineState::cleanup() -{ - // pop to level zero - popto(0); -} - -void SmtEngineState::userPush() -{ - if (!options().base.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(userContext()->getLevel()); - internalPush(); - Trace("userpushpop") << "SmtEngineState: pushed to level " - << userContext()->getLevel() << std::endl; -} - -void SmtEngineState::userPop() -{ - if (!options().base.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(userContext()->getLevel() > 0); - AlwaysAssert(d_userLevels.back() < userContext()->getLevel()); - while (d_userLevels.back() < userContext()->getLevel()) - { - internalPop(true); - } - d_userLevels.pop_back(); -} -void SmtEngineState::push() -{ - userContext()->push(); - context()->push(); -} - -void SmtEngineState::pop() -{ - userContext()->pop(); - context()->pop(); -} - -void SmtEngineState::popto(int toLevel) -{ - context()->popto(toLevel); - userContext()->popto(toLevel); -} - -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; } - -void SmtEngineState::internalPush() -{ - Assert(d_fullyInited); - Trace("smt") << "SmtEngineState::internalPush()" << std::endl; - doPendingPops(); - if (options().base.incrementalSolving) - { - // notifies the SolverEngine to process the assertions immediately - d_slv.notifyPushPre(); - userContext()->push(); - // the context push is done inside of the SAT solver - d_slv.notifyPushPost(); - } -} - -void SmtEngineState::internalPop(bool immediate) -{ - Assert(d_fullyInited); - Trace("smt") << "SmtEngineState::internalPop()" << std::endl; - if (options().base.incrementalSolving) - { - ++d_pendingPops; - } - if (immediate) - { - doPendingPops(); - } -} - -void SmtEngineState::doPendingPops() -{ - Trace("smt") << "SmtEngineState::doPendingPops()" << std::endl; - Assert(d_pendingPops == 0 || options().base.incrementalSolving); - // check to see if a postsolve() is pending - if (d_needPostsolve) - { - d_slv.notifyPostSolvePre(); - } - while (d_pendingPops > 0) - { - // the context pop is done inside of the SAT solver - d_slv.notifyPopPre(); - // pop the context - userContext()->pop(); - --d_pendingPops; - // no need for pop post (for now) - } - if (d_needPostsolve) - { - d_slv.notifyPostSolvePost(); - d_needPostsolve = false; - } -} - -} // namespace smt -} // namespace cvc5 diff --git a/src/smt/smt_engine_state.h b/src/smt/smt_engine_state.h deleted file mode 100644 index d7a0e2290..000000000 --- a/src/smt/smt_engine_state.h +++ /dev/null @@ -1,249 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Ying Sheng, Morgan Deters - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Utility for maintaining the state of the SMT engine. - */ - -#include "cvc5_private.h" - -#ifndef CVC5__SMT__SMT_ENGINE_STATE_H -#define CVC5__SMT__SMT_ENGINE_STATE_H - -#include - -#include "context/context.h" -#include "smt/env_obj.h" -#include "smt/smt_mode.h" -#include "util/result.h" - -namespace cvc5 { - -class SolverEngine; - -namespace smt { - -/** - * This utility is responsible for maintaining the basic state of the - * SolverEngine. - * - * It has no concept of anything related to the assertions of the SolverEngine, - * or more generally it does not depend on Node. - * - * This class has three sets of interfaces: - * (1) notification methods that are used by SolverEngine to notify when an - * event occurs (e.g. the beginning of a check-sat call), (2) maintaining the - * SAT and user contexts to be used by the SolverEngine, (3) general information - * queries, including the mode that the SolverEngine is in, based on the - * notifications it has received. - * - * It maintains a reference to the SolverEngine for the sake of making - * callbacks. - */ -class SmtEngineState : protected EnvObj -{ - public: - SmtEngineState(Env& env, SolverEngine& smt); - ~SmtEngineState() {} - /** - * Notify that the expected status of the next check-sat is given by the - * string status, which should be one of "sat", "unsat" or "unknown". - */ - void notifyExpectedStatus(const std::string& status); - /** - * Notify that the SolverEngine is fully initialized, which is called when - * options are finalized. - */ - void notifyFullyInited(); - /** - * Notify that we are resetting the assertions, called when a reset-assertions - * command is issued by the user. - */ - void notifyResetAssertions(); - /** - * Notify that we are about to call check-sat. This call is made prior to - * initializing the assertions. It processes pending pops and pushes a - * (user) context if necessary. - * - * @param hasAssumptions Whether the call to check-sat has assumptions. If - * so, we push a context. - */ - void notifyCheckSat(bool hasAssumptions); - /** - * Notify that the result of the last check-sat was r. This should be called - * once immediately following notifyCheckSat() if the check-sat call - * returned normal (i.e. it was not interupted). - * - * @param hasAssumptions Whether the prior call to check-sat had assumptions. - * If so, we pop a context. - * @param r The result of the check-sat call. - */ - void notifyCheckSatResult(bool hasAssumptions, Result r); - /** - * Notify that we finished an abduction query, where success is whether the - * command was successful. This is managed independently of the above - * calls for notifying check-sat. In other words, if a get-abduct command - * is issued to an SolverEngine, it may use a satisfiability call (if desired) - * to solve the abduction query. This method is called *in addition* to - * the above calls to notifyCheckSat / notifyCheckSatResult in this case. - * In particular, it is called after these two methods are completed. - * This overwrites the SMT mode to the "ABDUCT" mode if the call to abduction - * was successful. - */ - void notifyGetAbduct(bool success); - /** - * Notify that we finished an interpolation query, where success is whether - * the command was successful. This is managed independently of the above - * calls for notifying check-sat. In other words, if a get-interpol command - * is issued to an SolverEngine, it may use a satisfiability call (if desired) - * to solve the interpolation query. This method is called *in addition* to - * the above calls to notifyCheckSat / notifyCheckSatResult in this case. - * In particular, it is called after these two methods are completed. - * This overwrites the SMT mode to the "INTERPOL" mode if the call to - * interpolation was successful. - */ - void notifyGetInterpol(bool success); - /** - * Setup the context, which makes a single push to maintain a global - * context around everything. - */ - void setup(); - /** - * Set that we are in a fully initialized state. - */ - void finishInit(); - /** - * Prepare for a shutdown of the SolverEngine, which does pending pops and - * pops the user context to zero. - */ - void shutdown(); - /** - * Cleanup, which pops all contexts to level zero. - */ - void cleanup(); - - //---------------------------- context management - /** - * Do all pending pops, which ensures that the context levels are up-to-date. - * This method should be called by the SolverEngine before using any of its - * members that rely on the context (e.g. PropEngine or TheoryEngine). - */ - void doPendingPops(); - /** - * Called when the user of SolverEngine issues a push. This corresponds to - * the SMT-LIB command push. - */ - void userPush(); - /** - * Called when the user of SolverEngine issues a pop. This corresponds to - * the SMT-LIB command pop. - */ - void userPop(); - //---------------------------- end context management - - //---------------------------- queries - /** - * Return true if the SolverEngine is fully initialized (post-construction). - * This post-construction initialization is automatically triggered by the - * use of the SolverEngine; e.g. when the first formula is asserted, a call - * to simplify() is issued, a scope is pushed, etc. - */ - bool isFullyInited() const; - /** - * Return true if the SolverEngine is fully initialized and there are no - * pending pops. - */ - bool isFullyReady() const; - /** - * Return true if a notifyCheckSat call has been made, e.g. a query has been - * issued to the SolverEngine. - */ - bool isQueryMade() const; - /** Return the user context level. */ - size_t getNumUserLevels() const; - /** Get the status of the last check-sat */ - Result getStatus() const; - /** Get the SMT mode we are in */ - SmtMode getMode() const; - //---------------------------- end queries - - private: - /** Pushes the user and SAT contexts */ - void push(); - /** Pops the user and SAT contexts */ - void pop(); - /** Pops the user and SAT contexts to the given level */ - void popto(int toLevel); - /** - * Internal push, which processes any pending pops, and pushes (if in - * incremental mode). - */ - void internalPush(); - /** - * Internal pop. If immediate is true, this processes any pending pops, and - * pops (if in incremental mode). Otherwise, it increments the pending pop - * counter and does nothing. - */ - void internalPop(bool immediate = false); - /** Reference to the SolverEngine */ - SolverEngine& d_slv; - /** The context levels of user pushes */ - std::vector d_userLevels; - - /** - * Number of internal pops that have been deferred. - */ - unsigned d_pendingPops; - - /** - * Whether or not the SolverEngine is fully initialized (post-construction). - * This post-construction initialization is automatically triggered by the - * use of the SolverEngine which calls the finishInit method above; e.g. when - * the first formula is asserted, a call to simplify() is issued, a scope is - * pushed, etc. - */ - bool d_fullyInited; - - /** - * Whether or not a notifyCheckSat call has been made, which corresponds to - * when a checkEntailed() or checkSatisfiability() has already been - * made through the SolverEngine. If true, and incrementalSolving is false, - * then attempting an additional checks for satisfiability will fail with - * a ModalException during notifyCheckSat. - */ - bool d_queryMade; - - /** - * Internal status flag to indicate whether we have been issued a - * notifyCheckSat call and have yet to process the "postsolve" methods of - * SolverEngine via SolverEngine::notifyPostSolvePre/notifyPostSolvePost. - */ - bool d_needPostsolve; - - /** - * Most recent result of last checkSatisfiability/checkEntailed in the - * SolverEngine. - */ - Result d_status; - - /** - * The expected status of the next satisfiability check. - */ - Result d_expectedStatus; - - /** The SMT mode, for details see enumeration above. */ - SmtMode d_smtMode; -}; - -} // namespace smt -} // namespace cvc5 - -#endif diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 41f9a67b1..bd87ca35c 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -21,8 +21,8 @@ #include "smt/assertions.h" #include "smt/env.h" #include "smt/preprocessor.h" -#include "smt/smt_engine_state.h" #include "smt/solver_engine.h" +#include "smt/solver_engine_state.h" #include "smt/solver_engine_stats.h" #include "theory/logic_info.h" #include "theory/theory_engine.h" @@ -34,7 +34,7 @@ namespace cvc5 { namespace smt { SmtSolver::SmtSolver(Env& env, - SmtEngineState& state, + SolverEngineState& state, AbstractValues& abs, SolverEngineStatistics& stats) : d_env(env), diff --git a/src/smt/smt_solver.h b/src/smt/smt_solver.h index 83e591835..850c5b9b4 100644 --- a/src/smt/smt_solver.h +++ b/src/smt/smt_solver.h @@ -44,7 +44,7 @@ class QuantifiersEngine; namespace smt { class Assertions; -class SmtEngineState; +class SolverEngineState; struct SolverEngineStatistics; /** @@ -65,7 +65,7 @@ class SmtSolver { public: SmtSolver(Env& env, - SmtEngineState& state, + SolverEngineState& state, AbstractValues& abs, SolverEngineStatistics& stats); ~SmtSolver(); @@ -127,7 +127,7 @@ class SmtSolver /** Reference to the environment */ Env& d_env; /** Reference to the state of the SolverEngine */ - SmtEngineState& d_state; + SolverEngineState& d_state; /** The preprocessor of this SMT solver */ Preprocessor d_pp; /** Reference to the statistics of SolverEngine */ diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index cefc59631..911e0a960 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -53,9 +53,9 @@ #include "smt/proof_manager.h" #include "smt/quant_elim_solver.h" #include "smt/set_defaults.h" -#include "smt/smt_engine_state.h" #include "smt/smt_solver.h" #include "smt/solver_engine_scope.h" +#include "smt/solver_engine_state.h" #include "smt/solver_engine_stats.h" #include "smt/sygus_solver.h" #include "smt/unsat_core_manager.h" @@ -86,7 +86,7 @@ namespace cvc5 { SolverEngine::SolverEngine(NodeManager* nm, const Options* optr) : d_env(new Env(nm, optr)), - d_state(new SmtEngineState(*d_env.get(), *this)), + d_state(new SolverEngineState(*d_env.get(), *this)), d_absValues(new AbstractValues(getNodeManager())), d_asserts(new Assertions(*d_env.get(), *d_absValues.get())), d_routListener(new ResourceOutListener(*this)), diff --git a/src/smt/solver_engine.h b/src/smt/solver_engine.h index c627a63d6..75e653656 100644 --- a/src/smt/solver_engine.h +++ b/src/smt/solver_engine.h @@ -77,7 +77,7 @@ class PropEngine; namespace smt { /** Utilities */ -class SmtEngineState; +class SolverEngineState; class AbstractValues; class Assertions; class DumpManager; @@ -113,7 +113,7 @@ class QuantifiersEngine; class CVC5_EXPORT SolverEngine { friend class ::cvc5::api::Solver; - friend class ::cvc5::smt::SmtEngineState; + friend class ::cvc5::smt::SolverEngineState; friend class ::cvc5::smt::SolverEngineScope; /* ....................................................................... */ @@ -1047,7 +1047,7 @@ class CVC5_EXPORT SolverEngine * The state of this SolverEngine, which is responsible for maintaining which * SMT mode we are in, the contexts, the last result, etc. */ - std::unique_ptr d_state; + std::unique_ptr d_state; /** Abstract values */ std::unique_ptr d_absValues; diff --git a/src/smt/solver_engine_state.cpp b/src/smt/solver_engine_state.cpp new file mode 100644 index 000000000..8558e91cf --- /dev/null +++ b/src/smt/solver_engine_state.cpp @@ -0,0 +1,305 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Morgan Deters, Ying Sheng + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Utility for maintaining the state of the SMT engine. + */ + +#include "smt/solver_engine_state.h" + +#include "base/modal_exception.h" +#include "options/base_options.h" +#include "options/main_options.h" +#include "options/option_exception.h" +#include "options/smt_options.h" +#include "smt/env.h" +#include "smt/solver_engine.h" + +namespace cvc5 { +namespace smt { + +SolverEngineState::SolverEngineState(Env& env, SolverEngine& slv) + : EnvObj(env), + d_slv(slv), + d_pendingPops(0), + d_fullyInited(false), + d_queryMade(false), + d_needPostsolve(false), + d_status(), + d_expectedStatus(), + d_smtMode(SmtMode::START) +{ +} + +void SolverEngineState::notifyExpectedStatus(const std::string& status) +{ + Assert(status == "sat" || status == "unsat" || status == "unknown") + << "SolverEngineState::notifyExpectedStatus: unexpected status string " + << status; + d_expectedStatus = Result(status, options().driver.filename); +} + +void SolverEngineState::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 && userContext()->getLevel() == 1); + popto(0); +} + +void SolverEngineState::notifyCheckSat(bool hasAssumptions) +{ + // process the pending pops + doPendingPops(); + if (d_queryMade && !options().base.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 SolverEngineState::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) + { + CVC5_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 SolverEngineState::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 SolverEngineState::notifyGetInterpol(bool success) +{ + if (success) + { + // successfully generated an interpolant, update to interpol state + d_smtMode = SmtMode::INTERPOL; + } + else + { + // failed, we revert to the assert state + d_smtMode = SmtMode::ASSERT; + } +} + +void SolverEngineState::setup() +{ + // push a context + push(); +} + +void SolverEngineState::finishInit() +{ + // set the flag to remember that we are fully initialized + d_fullyInited = true; +} + +void SolverEngineState::shutdown() +{ + doPendingPops(); + + while (options().base.incrementalSolving && userContext()->getLevel() > 1) + { + internalPop(true); + } +} + +void SolverEngineState::cleanup() +{ + // pop to level zero + popto(0); +} + +void SolverEngineState::userPush() +{ + if (!options().base.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(userContext()->getLevel()); + internalPush(); + Trace("userpushpop") << "SolverEngineState: pushed to level " + << userContext()->getLevel() << std::endl; +} + +void SolverEngineState::userPop() +{ + if (!options().base.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(userContext()->getLevel() > 0); + AlwaysAssert(d_userLevels.back() < userContext()->getLevel()); + while (d_userLevels.back() < userContext()->getLevel()) + { + internalPop(true); + } + d_userLevels.pop_back(); +} +void SolverEngineState::push() +{ + userContext()->push(); + context()->push(); +} + +void SolverEngineState::pop() +{ + userContext()->pop(); + context()->pop(); +} + +void SolverEngineState::popto(int toLevel) +{ + context()->popto(toLevel); + userContext()->popto(toLevel); +} + +Result SolverEngineState::getStatus() const { return d_status; } + +bool SolverEngineState::isFullyInited() const { return d_fullyInited; } +bool SolverEngineState::isFullyReady() const +{ + return d_fullyInited && d_pendingPops == 0; +} +bool SolverEngineState::isQueryMade() const { return d_queryMade; } +size_t SolverEngineState::getNumUserLevels() const +{ + return d_userLevels.size(); +} + +SmtMode SolverEngineState::getMode() const { return d_smtMode; } + +void SolverEngineState::internalPush() +{ + Assert(d_fullyInited); + Trace("smt") << "SolverEngineState::internalPush()" << std::endl; + doPendingPops(); + if (options().base.incrementalSolving) + { + // notifies the SolverEngine to process the assertions immediately + d_slv.notifyPushPre(); + userContext()->push(); + // the context push is done inside of the SAT solver + d_slv.notifyPushPost(); + } +} + +void SolverEngineState::internalPop(bool immediate) +{ + Assert(d_fullyInited); + Trace("smt") << "SolverEngineState::internalPop()" << std::endl; + if (options().base.incrementalSolving) + { + ++d_pendingPops; + } + if (immediate) + { + doPendingPops(); + } +} + +void SolverEngineState::doPendingPops() +{ + Trace("smt") << "SolverEngineState::doPendingPops()" << std::endl; + Assert(d_pendingPops == 0 || options().base.incrementalSolving); + // check to see if a postsolve() is pending + if (d_needPostsolve) + { + d_slv.notifyPostSolvePre(); + } + while (d_pendingPops > 0) + { + // the context pop is done inside of the SAT solver + d_slv.notifyPopPre(); + // pop the context + userContext()->pop(); + --d_pendingPops; + // no need for pop post (for now) + } + if (d_needPostsolve) + { + d_slv.notifyPostSolvePost(); + d_needPostsolve = false; + } +} + +} // namespace smt +} // namespace cvc5 diff --git a/src/smt/solver_engine_state.h b/src/smt/solver_engine_state.h new file mode 100644 index 000000000..7a06b0510 --- /dev/null +++ b/src/smt/solver_engine_state.h @@ -0,0 +1,249 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Ying Sheng, Morgan Deters + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Utility for maintaining the state of the SMT engine. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__SMT__SMT_ENGINE_STATE_H +#define CVC5__SMT__SMT_ENGINE_STATE_H + +#include + +#include "context/context.h" +#include "smt/env_obj.h" +#include "smt/smt_mode.h" +#include "util/result.h" + +namespace cvc5 { + +class SolverEngine; + +namespace smt { + +/** + * This utility is responsible for maintaining the basic state of the + * SolverEngine. + * + * It has no concept of anything related to the assertions of the SolverEngine, + * or more generally it does not depend on Node. + * + * This class has three sets of interfaces: + * (1) notification methods that are used by SolverEngine to notify when an + * event occurs (e.g. the beginning of a check-sat call), (2) maintaining the + * SAT and user contexts to be used by the SolverEngine, (3) general information + * queries, including the mode that the SolverEngine is in, based on the + * notifications it has received. + * + * It maintains a reference to the SolverEngine for the sake of making + * callbacks. + */ +class SolverEngineState : protected EnvObj +{ + public: + SolverEngineState(Env& env, SolverEngine& smt); + ~SolverEngineState() {} + /** + * Notify that the expected status of the next check-sat is given by the + * string status, which should be one of "sat", "unsat" or "unknown". + */ + void notifyExpectedStatus(const std::string& status); + /** + * Notify that the SolverEngine is fully initialized, which is called when + * options are finalized. + */ + void notifyFullyInited(); + /** + * Notify that we are resetting the assertions, called when a reset-assertions + * command is issued by the user. + */ + void notifyResetAssertions(); + /** + * Notify that we are about to call check-sat. This call is made prior to + * initializing the assertions. It processes pending pops and pushes a + * (user) context if necessary. + * + * @param hasAssumptions Whether the call to check-sat has assumptions. If + * so, we push a context. + */ + void notifyCheckSat(bool hasAssumptions); + /** + * Notify that the result of the last check-sat was r. This should be called + * once immediately following notifyCheckSat() if the check-sat call + * returned normal (i.e. it was not interupted). + * + * @param hasAssumptions Whether the prior call to check-sat had assumptions. + * If so, we pop a context. + * @param r The result of the check-sat call. + */ + void notifyCheckSatResult(bool hasAssumptions, Result r); + /** + * Notify that we finished an abduction query, where success is whether the + * command was successful. This is managed independently of the above + * calls for notifying check-sat. In other words, if a get-abduct command + * is issued to an SolverEngine, it may use a satisfiability call (if desired) + * to solve the abduction query. This method is called *in addition* to + * the above calls to notifyCheckSat / notifyCheckSatResult in this case. + * In particular, it is called after these two methods are completed. + * This overwrites the SMT mode to the "ABDUCT" mode if the call to abduction + * was successful. + */ + void notifyGetAbduct(bool success); + /** + * Notify that we finished an interpolation query, where success is whether + * the command was successful. This is managed independently of the above + * calls for notifying check-sat. In other words, if a get-interpol command + * is issued to an SolverEngine, it may use a satisfiability call (if desired) + * to solve the interpolation query. This method is called *in addition* to + * the above calls to notifyCheckSat / notifyCheckSatResult in this case. + * In particular, it is called after these two methods are completed. + * This overwrites the SMT mode to the "INTERPOL" mode if the call to + * interpolation was successful. + */ + void notifyGetInterpol(bool success); + /** + * Setup the context, which makes a single push to maintain a global + * context around everything. + */ + void setup(); + /** + * Set that we are in a fully initialized state. + */ + void finishInit(); + /** + * Prepare for a shutdown of the SolverEngine, which does pending pops and + * pops the user context to zero. + */ + void shutdown(); + /** + * Cleanup, which pops all contexts to level zero. + */ + void cleanup(); + + //---------------------------- context management + /** + * Do all pending pops, which ensures that the context levels are up-to-date. + * This method should be called by the SolverEngine before using any of its + * members that rely on the context (e.g. PropEngine or TheoryEngine). + */ + void doPendingPops(); + /** + * Called when the user of SolverEngine issues a push. This corresponds to + * the SMT-LIB command push. + */ + void userPush(); + /** + * Called when the user of SolverEngine issues a pop. This corresponds to + * the SMT-LIB command pop. + */ + void userPop(); + //---------------------------- end context management + + //---------------------------- queries + /** + * Return true if the SolverEngine is fully initialized (post-construction). + * This post-construction initialization is automatically triggered by the + * use of the SolverEngine; e.g. when the first formula is asserted, a call + * to simplify() is issued, a scope is pushed, etc. + */ + bool isFullyInited() const; + /** + * Return true if the SolverEngine is fully initialized and there are no + * pending pops. + */ + bool isFullyReady() const; + /** + * Return true if a notifyCheckSat call has been made, e.g. a query has been + * issued to the SolverEngine. + */ + bool isQueryMade() const; + /** Return the user context level. */ + size_t getNumUserLevels() const; + /** Get the status of the last check-sat */ + Result getStatus() const; + /** Get the SMT mode we are in */ + SmtMode getMode() const; + //---------------------------- end queries + + private: + /** Pushes the user and SAT contexts */ + void push(); + /** Pops the user and SAT contexts */ + void pop(); + /** Pops the user and SAT contexts to the given level */ + void popto(int toLevel); + /** + * Internal push, which processes any pending pops, and pushes (if in + * incremental mode). + */ + void internalPush(); + /** + * Internal pop. If immediate is true, this processes any pending pops, and + * pops (if in incremental mode). Otherwise, it increments the pending pop + * counter and does nothing. + */ + void internalPop(bool immediate = false); + /** Reference to the SolverEngine */ + SolverEngine& d_slv; + /** The context levels of user pushes */ + std::vector d_userLevels; + + /** + * Number of internal pops that have been deferred. + */ + unsigned d_pendingPops; + + /** + * Whether or not the SolverEngine is fully initialized (post-construction). + * This post-construction initialization is automatically triggered by the + * use of the SolverEngine which calls the finishInit method above; e.g. when + * the first formula is asserted, a call to simplify() is issued, a scope is + * pushed, etc. + */ + bool d_fullyInited; + + /** + * Whether or not a notifyCheckSat call has been made, which corresponds to + * when a checkEntailed() or checkSatisfiability() has already been + * made through the SolverEngine. If true, and incrementalSolving is false, + * then attempting an additional checks for satisfiability will fail with + * a ModalException during notifyCheckSat. + */ + bool d_queryMade; + + /** + * Internal status flag to indicate whether we have been issued a + * notifyCheckSat call and have yet to process the "postsolve" methods of + * SolverEngine via SolverEngine::notifyPostSolvePre/notifyPostSolvePost. + */ + bool d_needPostsolve; + + /** + * Most recent result of last checkSatisfiability/checkEntailed in the + * SolverEngine. + */ + Result d_status; + + /** + * The expected status of the next satisfiability check. + */ + Result d_expectedStatus; + + /** The SMT mode, for details see enumeration above. */ + SmtMode d_smtMode; +}; + +} // namespace smt +} // namespace cvc5 + +#endif -- cgit v1.2.3