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
<< 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<Node>{ne}, true);
Trace("smt-qe") << "Query returned " << r << std::endl;
if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
+++ /dev/null
-/******************************************************************************
- * 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
+++ /dev/null
-/******************************************************************************
- * 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 <string>
-
-#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<int> 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
#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"
namespace smt {
SmtSolver::SmtSolver(Env& env,
- SmtEngineState& state,
+ SolverEngineState& state,
AbstractValues& abs,
SolverEngineStatistics& stats)
: d_env(env),
namespace smt {
class Assertions;
-class SmtEngineState;
+class SolverEngineState;
struct SolverEngineStatistics;
/**
{
public:
SmtSolver(Env& env,
- SmtEngineState& state,
+ SolverEngineState& state,
AbstractValues& abs,
SolverEngineStatistics& stats);
~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 */
#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"
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)),
namespace smt {
/** Utilities */
-class SmtEngineState;
+class SolverEngineState;
class AbstractValues;
class Assertions;
class DumpManager;
class CVC5_EXPORT SolverEngine
{
friend class ::cvc5::api::Solver;
- friend class ::cvc5::smt::SmtEngineState;
+ friend class ::cvc5::smt::SolverEngineState;
friend class ::cvc5::smt::SolverEngineScope;
/* ....................................................................... */
* 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<smt::SmtEngineState> d_state;
+ std::unique_ptr<smt::SolverEngineState> d_state;
/** Abstract values */
std::unique_ptr<smt::AbstractValues> d_absValues;
--- /dev/null
+/******************************************************************************
+ * 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
--- /dev/null
+/******************************************************************************
+ * 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 <string>
+
+#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<int> 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
projects / cvc5.git / commitdiff