Rename SmtEngine to SolverEngine. (#7282)

4 files changed, 10 insertions, 10 deletions

diff --git a/src/preprocessing/passes/apply_substs.cpp b/src/preprocessing/passes/apply_substs.cpp
index 2e40cbd5b..90685b9c7 100644
--- a/src/preprocessing/passes/apply_substs.cpp
+++ b/src/preprocessing/passes/apply_substs.cpp
@@ -37,7 +37,7 @@ PreprocessingPassResult ApplySubsts::applyInternal(
     AssertionPipeline* assertionsToPreprocess)
 {
   Chat() << "applying substitutions..." << std::endl;
-  Trace("apply-substs") << "SmtEnginePrivate::processAssertions(): "
+  Trace("apply-substs") << "ApplySubsts::processAssertions(): "
                         << "applying substitutions" << std::endl;
   // TODO(#1255): Substitutions in incremental mode should be managed with a
   // proper data structure.
diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp
index 9a35c2909..16ecc2d6a 100644
--- a/src/preprocessing/passes/sygus_inference.cpp
+++ b/src/preprocessing/passes/sygus_inference.cpp
@@ -295,7 +295,7 @@ bool SygusInference::solveSygus(const std::vector<Node>& assertions,
   Trace("sygus-infer") << "*** Return sygus inference : " << body << std::endl;
 
   // make a separate smt call
-  std::unique_ptr<SmtEngine> rrSygus;
+  std::unique_ptr<SolverEngine> rrSygus;
   theory::initializeSubsolver(rrSygus, options(), logicInfo());
   rrSygus->assertFormula(body);
   Trace("sygus-infer") << "*** Check sat..." << std::endl;
diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp
index 9d7c80812..a0d607032 100644
--- a/src/preprocessing/preprocessing_pass_context.cpp
+++ b/src/preprocessing/preprocessing_pass_context.cpp
@@ -25,11 +25,11 @@ namespace cvc5 {
 namespace preprocessing {
 
 PreprocessingPassContext::PreprocessingPassContext(
-    SmtEngine* smt,
+    SolverEngine* slv,
     Env& env,
     theory::booleans::CircuitPropagator* circuitPropagator)
     : EnvObj(env),
-      d_smt(smt),
+      d_slv(slv),
       d_circuitPropagator(circuitPropagator),
       d_llm(
           env.getTopLevelSubstitutions(), userContext(), getProofNodeManager()),
@@ -45,11 +45,11 @@ PreprocessingPassContext::getTopLevelSubstitutions() const
 
 TheoryEngine* PreprocessingPassContext::getTheoryEngine() const
 {
-  return d_smt->getTheoryEngine();
+  return d_slv->getTheoryEngine();
 }
 prop::PropEngine* PreprocessingPassContext::getPropEngine() const
 {
-  return d_smt->getPropEngine();
+  return d_slv->getPropEngine();
 }
 
 void PreprocessingPassContext::spendResource(Resource r)
diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h
index 79b89dda8..ec9d39920 100644
--- a/src/preprocessing/preprocessing_pass_context.h
+++ b/src/preprocessing/preprocessing_pass_context.h
@@ -31,7 +31,7 @@
 namespace cvc5 {
 
 class Env;
-class SmtEngine;
+class SolverEngine;
 class TheoryEngine;
 
 namespace theory::booleans {
@@ -49,7 +49,7 @@ class PreprocessingPassContext : protected EnvObj
  public:
   /** Constructor. */
   PreprocessingPassContext(
-      SmtEngine* smt,
+      SolverEngine* smt,
       Env& env,
       theory::booleans::CircuitPropagator* circuitPropagator);
 
@@ -120,8 +120,8 @@ class PreprocessingPassContext : protected EnvObj
   ProofNodeManager* getProofNodeManager() const;
 
  private:
-  /** Pointer to the SmtEngine that this context was created in. */
-  SmtEngine* d_smt;
+  /** Pointer to the SolverEngine that this context was created in. */
+  SolverEngine* d_slv;
   /** Instance of the circuit propagator */
   theory::booleans::CircuitPropagator* d_circuitPropagator;
   /**