Rename SmtEngineState to SolverEngineState. (#7344)

8 files changed, 50 insertions, 47 deletions

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<Node>{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<smt::SmtEngineState> d_state;
+  std::unique_ptr<smt::SolverEngineState> d_state;
 
   /** Abstract values */
   std::unique_ptr<smt::AbstractValues> d_absValues;
diff --git a/src/smt/smt_engine_state.cpp b/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
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".