From 077c191da9739ebb09e689a4809abbf779d99593 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Tue, 12 Oct 2021 10:53:03 -0700 Subject: [PATCH] Rename SmtEngineState to SolverEngineState. (#7344) --- src/CMakeLists.txt | 4 +- src/smt/quant_elim_solver.cpp | 2 +- src/smt/smt_solver.cpp | 4 +- src/smt/smt_solver.h | 6 +- src/smt/solver_engine.cpp | 4 +- src/smt/solver_engine.h | 6 +- ...gine_state.cpp => solver_engine_state.cpp} | 65 ++++++++++--------- ...t_engine_state.h => solver_engine_state.h} | 6 +- 8 files changed, 50 insertions(+), 47 deletions(-) rename src/smt/{smt_engine_state.cpp => solver_engine_state.cpp} (78%) rename src/smt/{smt_engine_state.h => solver_engine_state.h} (98%) 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_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/smt_engine_state.cpp b/src/smt/solver_engine_state.cpp similarity index 78% rename from src/smt/smt_engine_state.cpp rename to src/smt/solver_engine_state.cpp index becfd1466..8558e91cf 100644 --- a/src/smt/smt_engine_state.cpp +++ b/src/smt/solver_engine_state.cpp @@ -13,7 +13,7 @@ * Utility for maintaining the state of the SMT engine. */ -#include "smt/smt_engine_state.h" +#include "smt/solver_engine_state.h" #include "base/modal_exception.h" #include "options/base_options.h" @@ -26,7 +26,7 @@ namespace cvc5 { namespace smt { -SmtEngineState::SmtEngineState(Env& env, SolverEngine& slv) +SolverEngineState::SolverEngineState(Env& env, SolverEngine& slv) : EnvObj(env), d_slv(slv), d_pendingPops(0), @@ -39,15 +39,15 @@ SmtEngineState::SmtEngineState(Env& env, SolverEngine& slv) { } -void SmtEngineState::notifyExpectedStatus(const std::string& status) +void SolverEngineState::notifyExpectedStatus(const std::string& status) { Assert(status == "sat" || status == "unsat" || status == "unknown") - << "SmtEngineState::notifyExpectedStatus: unexpected status string " + << "SolverEngineState::notifyExpectedStatus: unexpected status string " << status; d_expectedStatus = Result(status, options().driver.filename); } -void SmtEngineState::notifyResetAssertions() +void SolverEngineState::notifyResetAssertions() { doPendingPops(); while (!d_userLevels.empty()) @@ -60,7 +60,7 @@ void SmtEngineState::notifyResetAssertions() popto(0); } -void SmtEngineState::notifyCheckSat(bool hasAssumptions) +void SolverEngineState::notifyCheckSat(bool hasAssumptions) { // process the pending pops doPendingPops(); @@ -83,7 +83,7 @@ void SmtEngineState::notifyCheckSat(bool hasAssumptions) } } -void SmtEngineState::notifyCheckSatResult(bool hasAssumptions, Result r) +void SolverEngineState::notifyCheckSatResult(bool hasAssumptions, Result r) { d_needPostsolve = true; @@ -113,7 +113,7 @@ void SmtEngineState::notifyCheckSatResult(bool hasAssumptions, Result r) } } -void SmtEngineState::notifyGetAbduct(bool success) +void SolverEngineState::notifyGetAbduct(bool success) { if (success) { @@ -127,7 +127,7 @@ void SmtEngineState::notifyGetAbduct(bool success) } } -void SmtEngineState::notifyGetInterpol(bool success) +void SolverEngineState::notifyGetInterpol(bool success) { if (success) { @@ -141,19 +141,19 @@ void SmtEngineState::notifyGetInterpol(bool success) } } -void SmtEngineState::setup() +void SolverEngineState::setup() { // push a context push(); } -void SmtEngineState::finishInit() +void SolverEngineState::finishInit() { // set the flag to remember that we are fully initialized d_fullyInited = true; } -void SmtEngineState::shutdown() +void SolverEngineState::shutdown() { doPendingPops(); @@ -163,13 +163,13 @@ void SmtEngineState::shutdown() } } -void SmtEngineState::cleanup() +void SolverEngineState::cleanup() { // pop to level zero popto(0); } -void SmtEngineState::userPush() +void SolverEngineState::userPush() { if (!options().base.incrementalSolving) { @@ -183,11 +183,11 @@ void SmtEngineState::userPush() d_userLevels.push_back(userContext()->getLevel()); internalPush(); - Trace("userpushpop") << "SmtEngineState: pushed to level " + Trace("userpushpop") << "SolverEngineState: pushed to level " << userContext()->getLevel() << std::endl; } -void SmtEngineState::userPop() +void SolverEngineState::userPop() { if (!options().base.incrementalSolving) { @@ -214,40 +214,43 @@ void SmtEngineState::userPop() } d_userLevels.pop_back(); } -void SmtEngineState::push() +void SolverEngineState::push() { userContext()->push(); context()->push(); } -void SmtEngineState::pop() +void SolverEngineState::pop() { userContext()->pop(); context()->pop(); } -void SmtEngineState::popto(int toLevel) +void SolverEngineState::popto(int toLevel) { context()->popto(toLevel); userContext()->popto(toLevel); } -Result SmtEngineState::getStatus() const { return d_status; } +Result SolverEngineState::getStatus() const { return d_status; } -bool SmtEngineState::isFullyInited() const { return d_fullyInited; } -bool SmtEngineState::isFullyReady() const +bool SolverEngineState::isFullyInited() const { return d_fullyInited; } +bool SolverEngineState::isFullyReady() const { return d_fullyInited && d_pendingPops == 0; } -bool SmtEngineState::isQueryMade() const { return d_queryMade; } -size_t SmtEngineState::getNumUserLevels() const { return d_userLevels.size(); } +bool SolverEngineState::isQueryMade() const { return d_queryMade; } +size_t SolverEngineState::getNumUserLevels() const +{ + return d_userLevels.size(); +} -SmtMode SmtEngineState::getMode() const { return d_smtMode; } +SmtMode SolverEngineState::getMode() const { return d_smtMode; } -void SmtEngineState::internalPush() +void SolverEngineState::internalPush() { Assert(d_fullyInited); - Trace("smt") << "SmtEngineState::internalPush()" << std::endl; + Trace("smt") << "SolverEngineState::internalPush()" << std::endl; doPendingPops(); if (options().base.incrementalSolving) { @@ -259,10 +262,10 @@ void SmtEngineState::internalPush() } } -void SmtEngineState::internalPop(bool immediate) +void SolverEngineState::internalPop(bool immediate) { Assert(d_fullyInited); - Trace("smt") << "SmtEngineState::internalPop()" << std::endl; + Trace("smt") << "SolverEngineState::internalPop()" << std::endl; if (options().base.incrementalSolving) { ++d_pendingPops; @@ -273,9 +276,9 @@ void SmtEngineState::internalPop(bool immediate) } } -void SmtEngineState::doPendingPops() +void SolverEngineState::doPendingPops() { - Trace("smt") << "SmtEngineState::doPendingPops()" << std::endl; + Trace("smt") << "SolverEngineState::doPendingPops()" << std::endl; Assert(d_pendingPops == 0 || options().base.incrementalSolving); // check to see if a postsolve() is pending if (d_needPostsolve) diff --git a/src/smt/smt_engine_state.h b/src/smt/solver_engine_state.h similarity index 98% rename from src/smt/smt_engine_state.h rename to src/smt/solver_engine_state.h index d7a0e2290..7a06b0510 100644 --- a/src/smt/smt_engine_state.h +++ b/src/smt/solver_engine_state.h @@ -48,11 +48,11 @@ namespace smt { * It maintains a reference to the SolverEngine for the sake of making * callbacks. */ -class SmtEngineState : protected EnvObj +class SolverEngineState : protected EnvObj { public: - SmtEngineState(Env& env, SolverEngine& smt); - ~SmtEngineState() {} + 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". -- 2.30.2