Rename files smt_engine.(cpp|h) to solver_engine.(cpp|h). (#7279)

This is in preparation for renaming SmtEngine to SolverEngine.

46 files changed, 136 insertions, 107 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 18312f7c0..fe9267bed 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -343,8 +343,8 @@ libcvc5_add_sources(
   smt/proof_post_processor.h
   smt/set_defaults.cpp
   smt/set_defaults.h
-  smt/smt_engine.cpp
-  smt/smt_engine.h
+  smt/solver_engine.cpp
+  smt/solver_engine.h
   smt/smt_engine_scope.cpp
   smt/smt_engine_scope.h
   smt/smt_engine_state.cpp
diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 42690586a..a8b60a94d 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -64,8 +64,8 @@
 #include "proof/unsat_core.h"
 #include "smt/env.h"
 #include "smt/model.h"
-#include "smt/smt_engine.h"
 #include "smt/smt_mode.h"
+#include "smt/solver_engine.h"
 #include "theory/datatypes/tuple_project_op.h"
 #include "theory/logic_info.h"
 #include "theory/theory_model.h"
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 2c5741491..6a6ae4658 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -27,7 +27,7 @@
 
 #include "main/main.h"
 #include "smt/command.h"
-#include "smt/smt_engine.h"
+#include "smt/solver_engine.h"
 
 namespace cvc5 {
 namespace main {
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index de7566b1f..ee610757b 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -36,7 +36,7 @@
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
 #include "smt/command.h"
-#include "smt/smt_engine.h"
+#include "smt/solver_engine.h"
 #include "util/result.h"
 
 using namespace std;
diff --git a/src/omt/bitvector_optimizer.cpp b/src/omt/bitvector_optimizer.cpp
index 01cb6da42..72219d995 100644
--- a/src/omt/bitvector_optimizer.cpp
+++ b/src/omt/bitvector_optimizer.cpp
@@ -16,7 +16,7 @@
 #include "omt/bitvector_optimizer.h"
 
 #include "options/smt_options.h"
-#include "smt/smt_engine.h"
+#include "smt/solver_engine.h"
 #include "util/bitvector.h"
 
 using namespace cvc5::smt;
diff --git a/src/omt/integer_optimizer.cpp b/src/omt/integer_optimizer.cpp
index 379b0cd43..b3047b390 100644
--- a/src/omt/integer_optimizer.cpp
+++ b/src/omt/integer_optimizer.cpp
@@ -16,7 +16,7 @@
 #include "omt/integer_optimizer.h"
 
 #include "options/smt_options.h"
-#include "smt/smt_engine.h"
+#include "smt/solver_engine.h"
 
 using namespace cvc5::smt;
 namespace cvc5::omt {
diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp
index 8abd77a27..9a35c2909 100644
--- a/src/preprocessing/passes/sygus_inference.cpp
+++ b/src/preprocessing/passes/sygus_inference.cpp
@@ -17,9 +17,9 @@
 
 #include "preprocessing/assertion_pipeline.h"
 #include "preprocessing/preprocessing_pass_context.h"
-#include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
+#include "smt/solver_engine.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/quantifiers_preprocess.h"
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp
index a0894351d..9d7c80812 100644
--- a/src/preprocessing/preprocessing_pass_context.cpp
+++ b/src/preprocessing/preprocessing_pass_context.cpp
@@ -17,7 +17,7 @@
 
 #include "expr/node_algorithm.h"
 #include "smt/env.h"
-#include "smt/smt_engine.h"
+#include "smt/solver_engine.h"
 #include "theory/theory_engine.h"
 #include "theory/theory_model.h"
 
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 0c107573f..507937b2d 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -41,7 +41,7 @@
 #include "proof/unsat_core.h"
 #include "smt/command.h"
 #include "smt/node_command.h"
-#include "smt/smt_engine.h"
+#include "smt/solver_engine.h"
 #include "smt_util/boolean_simplification.h"
 #include "theory/arrays/theory_arrays_rewriter.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
diff --git a/src/printer/tptp/tptp_printer.cpp b/src/printer/tptp/tptp_printer.cpp
index 6c8746706..e5f2ea55d 100644
--- a/src/printer/tptp/tptp_printer.cpp
+++ b/src/printer/tptp/tptp_printer.cpp
@@ -25,7 +25,7 @@
 #include "proof/unsat_core.h"
 #include "smt/command.h"
 #include "smt/node_command.h"
-#include "smt/smt_engine.h"
+#include "smt/solver_engine.h"
 
 using namespace std;
 
diff --git a/src/smt/abduction_solver.cpp b/src/smt/abduction_solver.cpp
index 3bdf13efb..0c6ff5a68 100644
--- a/src/smt/abduction_solver.cpp
+++ b/src/smt/abduction_solver.cpp
@@ -20,7 +20,7 @@
 #include "base/modal_exception.h"
 #include "options/smt_options.h"
 #include "smt/env.h"
-#include "smt/smt_engine.h"
+#include "smt/solver_engine.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/sygus/sygus_abduct.h"
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp
index b78659d39..02ae86317 100644
--- a/src/smt/assertions.cpp
+++ b/src/smt/assertions.cpp
@@ -25,7 +25,7 @@
 #include "options/smt_options.h"
 #include "smt/abstract_values.h"
 #include "smt/env.h"
-#include "smt/smt_engine.h"
+#include "smt/solver_engine.h"
 #include "theory/trust_substitutions.h"
 
 using namespace cvc5::theory;
diff --git a/src/smt/expand_definitions.cpp b/src/smt/expand_definitions.cpp
index 293c46906..3ee08848d 100644
--- a/src/smt/expand_definitions.cpp
+++ b/src/smt/expand_definitions.cpp
@@ -22,8 +22,8 @@
 #include "preprocessing/assertion_pipeline.h"
 #include "proof/conv_proof_generator.h"
 #include "smt/env.h"
-#include "smt/smt_engine.h"
 #include "smt/smt_engine_stats.h"
+#include "smt/solver_engine.h"
 #include "theory/rewriter.h"
 #include "theory/theory.h"
 #include "util/resource_manager.h"
diff --git a/src/smt/interpolation_solver.cpp b/src/smt/interpolation_solver.cpp
index ff8e14e9b..923f14272 100644
--- a/src/smt/interpolation_solver.cpp
+++ b/src/smt/interpolation_solver.cpp
@@ -20,7 +20,7 @@
 #include "base/modal_exception.h"
 #include "options/smt_options.h"
 #include "smt/env.h"
-#include "smt/smt_engine.h"
+#include "smt/solver_engine.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
 #include "theory/quantifiers/sygus/sygus_interpol.h"
diff --git a/src/smt/listeners.cpp b/src/smt/listeners.cpp
index a0a3962ac..816a49a85 100644
--- a/src/smt/listeners.cpp
+++ b/src/smt/listeners.cpp
@@ -23,8 +23,8 @@
 #include "smt/dump.h"
 #include "smt/dump_manager.h"
 #include "smt/node_command.h"
-#include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
+#include "smt/solver_engine.h"
 
 namespace cvc5 {
 namespace smt {
diff --git a/src/smt/optimization_solver.cpp b/src/smt/optimization_solver.cpp
index 67de9728c..a62a315c1 100644
--- a/src/smt/optimization_solver.cpp
+++ b/src/smt/optimization_solver.cpp
@@ -23,7 +23,7 @@
 #include "options/smt_options.h"
 #include "smt/assertions.h"
 #include "smt/env.h"
-#include "smt/smt_engine.h"
+#include "smt/solver_engine.h"
 #include "theory/smt_engine_subsolver.h"
 
 using namespace cvc5::theory;
diff --git a/src/smt/output_manager.cpp b/src/smt/output_manager.cpp
index aa91bb184..03995fdc5 100644
--- a/src/smt/output_manager.cpp
+++ b/src/smt/output_manager.cpp
@@ -16,7 +16,7 @@
 #include "smt/output_manager.h"
 
 #include "options/base_options.h"
-#include "smt/smt_engine.h"
+#include "smt/solver_engine.h"
 
 namespace cvc5 {
 
diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp
index c36ff1bce..e63877c22 100644
--- a/src/smt/preprocessor.cpp
+++ b/src/smt/preprocessor.cpp
@@ -25,7 +25,7 @@
 #include "smt/dump.h"
 #include "smt/env.h"
 #include "smt/preprocess_proof_generator.h"
-#include "smt/smt_engine.h"
+#include "smt/solver_engine.h"
 #include "theory/rewriter.h"
 
 using namespace std;
diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index a9426d5bd..1fd47352e 100644
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -33,8 +33,8 @@
 #include "smt/assertions.h"
 #include "smt/dump.h"
 #include "smt/expand_definitions.h"
-#include "smt/smt_engine.h"
 #include "smt/smt_engine_stats.h"
+#include "smt/solver_engine.h"
 #include "theory/logic_info.h"
 #include "theory/theory_engine.h"
 
diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index f5db349e1..d6a5f7652 100644
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -19,7 +19,7 @@
 #include "options/proof_options.h"
 #include "preprocessing/assertion_pipeline.h"
 #include "proof/proof_node_manager.h"
-#include "smt/smt_engine.h"
+#include "smt/solver_engine.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/builtin/proof_checker.h"
 #include "theory/bv/bitblast/bitblast_proof_generator.h"
diff --git a/src/smt/smt_engine_scope.cpp b/src/smt/smt_engine_scope.cpp
index ebaa73b03..2dcb4fa23 100644
--- a/src/smt/smt_engine_scope.cpp
+++ b/src/smt/smt_engine_scope.cpp
@@ -21,7 +21,7 @@
 #include "base/check.h"
 #include "base/configuration_private.h"
 #include "base/output.h"
-#include "smt/smt_engine.h"
+#include "smt/solver_engine.h"
 
 namespace cvc5 {
 namespace smt {
diff --git a/src/smt/smt_engine_state.cpp b/src/smt/smt_engine_state.cpp
index 2206b29cd..6fb997c95 100644
--- a/src/smt/smt_engine_state.cpp
+++ b/src/smt/smt_engine_state.cpp
@@ -21,7 +21,7 @@
 #include "options/option_exception.h"
 #include "options/smt_options.h"
 #include "smt/env.h"
-#include "smt/smt_engine.h"
+#include "smt/solver_engine.h"
 
 namespace cvc5 {
 namespace smt {
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index e509eafcf..48db0c45f 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -21,9 +21,9 @@
 #include "smt/assertions.h"
 #include "smt/env.h"
 #include "smt/preprocessor.h"
-#include "smt/smt_engine.h"
 #include "smt/smt_engine_state.h"
 #include "smt/smt_engine_stats.h"
+#include "smt/solver_engine.h"
 #include "theory/logic_info.h"
 #include "theory/theory_engine.h"
 #include "theory/theory_traits.h"
diff --git a/src/smt/smt_engine.cpp b/src/smt/solver_engine.cpp
index 99410593c..1a03aea0a 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/solver_engine.cpp
@@ -13,7 +13,7 @@
  * The main entry point into the cvc5 library's SMT interface.
  */
 
-#include "smt/smt_engine.h"
+#include "smt/solver_engine.h"
 
 #include "base/check.h"
 #include "base/exception.h"
@@ -233,16 +233,16 @@ void SmtEngine::finishInit()
   // dumping the command twice.
   if (Dump.isOn("benchmark"))
   {
-      LogicInfo everything;
-      everything.lock();
-      getPrinter().toStreamCmdSetInfo(
-          d_env->getDumpOut(),
-          "notes",
-          "cvc5 always dumps the most general, all-supported logic (below), as "
-          "some internals might require the use of a logic more general than "
-          "the input.");
-      getPrinter().toStreamCmdSetBenchmarkLogic(d_env->getDumpOut(),
-                                                everything.getLogicString());
+    LogicInfo everything;
+    everything.lock();
+    getPrinter().toStreamCmdSetInfo(
+        d_env->getDumpOut(),
+        "notes",
+        "cvc5 always dumps the most general, all-supported logic (below), as "
+        "some internals might require the use of a logic more general than "
+        "the input.");
+    getPrinter().toStreamCmdSetBenchmarkLogic(d_env->getDumpOut(),
+                                              everything.getLogicString());
   }
 
   // initialize the dump manager
@@ -272,7 +272,8 @@ void SmtEngine::finishInit()
   Trace("smt-debug") << "SmtEngine::finishInit done" << std::endl;
 }
 
-void SmtEngine::shutdown() {
+void SmtEngine::shutdown()
+{
   d_state->shutdown();
 
   d_smtSolver->shutdown();
@@ -284,14 +285,15 @@ SmtEngine::~SmtEngine()
 {
   SmtScope smts(this);
 
-  try {
+  try
+  {
     shutdown();
 
     // global push/pop around everything, to ensure proper destruction
     // of context-dependent data structures
     d_state->cleanup();
 
-    //destroy all passes before destroying things that they refer to
+    // destroy all passes before destroying things that they refer to
     d_pp->cleanup();
 
     d_pfManager.reset(nullptr);
@@ -315,7 +317,9 @@ SmtEngine::~SmtEngine()
     d_state.reset(nullptr);
     // destroy the environment
     d_env.reset(nullptr);
-  } catch(Exception& e) {
+  }
+  catch (Exception& e)
+  {
     Warning() << "cvc5 threw an exception during cleanup." << endl << e << endl;
   }
 }
@@ -325,8 +329,9 @@ void SmtEngine::setLogic(const LogicInfo& logic)
   SmtScope smts(this);
   if (d_state->isFullyInited())
   {
-    throw ModalException("Cannot set logic in SmtEngine after the engine has "
-                         "finished initializing.");
+    throw ModalException(
+        "Cannot set logic in SmtEngine after the engine has "
+        "finished initializing.");
   }
   d_env->d_logic = logic;
   d_userLogic = logic;
@@ -389,7 +394,8 @@ void SmtEngine::setInfo(const std::string& key, const std::string& value)
     d_env->getStatisticsRegistry().registerValue<std::string>(
         "driver::filename", value);
   }
-  else if (key == "smt-lib-version" && !getOptions().base.inputLanguageWasSetByUser)
+  else if (key == "smt-lib-version"
+           && !getOptions().base.inputLanguageWasSetByUser)
   {
     Language ilang = Language::LANG_SMTLIB_V2_6;
 
@@ -436,7 +442,8 @@ std::string SmtEngine::getInfo(const std::string& key) const
   Trace("smt") << "SMT getInfo(" << key << ")" << endl;
   if (key == "all-statistics")
   {
-    return toSExpr(d_env->getStatisticsRegistry().begin(), d_env->getStatisticsRegistry().end());
+    return toSExpr(d_env->getStatisticsRegistry().begin(),
+                   d_env->getStatisticsRegistry().end());
   }
   if (key == "error-behavior")
   {
@@ -500,9 +507,10 @@ std::string SmtEngine::getInfo(const std::string& key) const
   Assert(key == "all-options");
   // get the options, like all-statistics
   std::vector<std::vector<std::string>> res;
-  for (const auto& opt: options::getNames())
+  for (const auto& opt : options::getNames())
   {
-    res.emplace_back(std::vector<std::string>{opt, options::get(getOptions(), opt)});
+    res.emplace_back(
+        std::vector<std::string>{opt, options::get(getOptions(), opt)});
   }
   return toSExpr(res);
 }
@@ -513,9 +521,11 @@ void SmtEngine::debugCheckFormals(const std::vector<Node>& formals, Node func)
        i != formals.end();
        ++i)
   {
-    if((*i).getKind() != kind::BOUND_VARIABLE) {
+    if ((*i).getKind() != kind::BOUND_VARIABLE)
+    {
       stringstream ss;
-      ss << "All formal arguments to defined functions must be BOUND_VARIABLEs, but in the\n"
+      ss << "All formal arguments to defined functions must be "
+            "BOUND_VARIABLEs, but in the\n"
          << "definition of function " << func << ", formal\n"
          << "  " << *i << "\n"
          << "has kind " << (*i).getKind();
@@ -528,17 +538,18 @@ void SmtEngine::debugCheckFunctionBody(Node formula,
                                        const std::vector<Node>& formals,
                                        Node func)
 {
-  TypeNode formulaType =
-      formula.getType(d_env->getOptions().expr.typeChecking);
+  TypeNode formulaType = formula.getType(d_env->getOptions().expr.typeChecking);
   TypeNode funcType = func.getType();
   // We distinguish here between definitions of constants and functions,
   // because the type checking for them is subtly different.  Perhaps we
   // should instead have SmtEngine::defineFunction() and
   // SmtEngine::defineConstant() for better clarity, although then that
   // doesn't match the SMT-LIBv2 standard...
-  if(formals.size() > 0) {
+  if (formals.size() > 0)
+  {
     TypeNode rangeType = funcType.getRangeType();
-    if(! formulaType.isComparableTo(rangeType)) {
+    if (!formulaType.isComparableTo(rangeType))
+    {
       stringstream ss;
       ss << "Type of defined function does not match its declaration\n"
          << "The function  : " << func << "\n"
@@ -547,8 +558,11 @@ void SmtEngine::debugCheckFunctionBody(Node formula,
          << "Body type     : " << formulaType;
       throw TypeCheckingExceptionPrivate(func, ss.str());
     }
-  } else {
-    if(! formulaType.isComparableTo(funcType)) {
+  }
+  else
+  {
+    if (!formulaType.isComparableTo(funcType))
+    {
       stringstream ss;
       ss << "Declared type of defined constant does not match its definition\n"
          << "The constant   : " << func << "\n"
@@ -573,7 +587,7 @@ void SmtEngine::defineFunction(Node func,
 
   stringstream ss;
   ss << language::SetLanguage(
-            language::SetLanguage::getLanguage(Dump.getStream()))
+      language::SetLanguage::getLanguage(Dump.getStream()))
      << func;
 
   DefineFunctionNodeCommand nc(ss.str(), func, formals, formula);
@@ -679,7 +693,8 @@ void SmtEngine::defineFunctionRec(Node func,
   defineFunctionsRec(funcs, formals_multi, formulas, global);
 }
 
-Result SmtEngine::quickCheck() {
+Result SmtEngine::quickCheck()
+{
   Assert(d_state->isFullyInited());
   Trace("smt") << "SMT quickCheck()" << endl;
   const std::string& filename = d_env->getOptions().driver.filename;
@@ -900,7 +915,8 @@ Result SmtEngine::checkSatInternal(const std::vector<Node>& assumptions,
     {
       printStatisticsDiff();
     }
-    return Result(Result::SAT_UNKNOWN, why, d_env->getOptions().driver.filename);
+    return Result(
+        Result::SAT_UNKNOWN, why, d_env->getOptions().driver.filename);
   }
 }
 
@@ -951,7 +967,7 @@ Result SmtEngine::assertFormula(const Node& formula)
 
   d_asserts->assertFormula(n);
   return quickCheck().asEntailmentResult();
-}/* SmtEngine::assertFormula() */
+} /* SmtEngine::assertFormula() */
 
 /*
    --------------------------------------------------------------------------
@@ -1063,8 +1079,9 @@ Node SmtEngine::getValue(const Node& ex) const
   // two are different, but they need to be unified.  This ugly hack here
   // is to fix bug 554 until we can revamp boolean-terms and models [MGD]
 
-  //AJR : necessary?
-  if(!n.getType().isFunction()) {
+  // AJR : necessary?
+  if (!n.getType().isFunction())
+  {
     n = Rewriter::rewrite(n);
   }
 
@@ -1088,8 +1105,7 @@ Node SmtEngine::getValue(const Node& ex) const
   Assert(m->hasApproximations() || resultNode.getKind() == kind::LAMBDA
          || resultNode.isConst());
 
-  if (d_env->getOptions().smt.abstractValues
-      && resultNode.getType().isArray())
+  if (d_env->getOptions().smt.abstractValues && resultNode.getType().isArray())
   {
     resultNode = d_absValues->mkAbstractValue(resultNode);
     Trace("smt") << "--- abstract value >> " << resultNode << endl;
@@ -1200,8 +1216,7 @@ Result SmtEngine::blockModel()
 
   TheoryModel* m = getAvailableModel("block model");
 
-  if (d_env->getOptions().smt.blockModelsMode
-      == options::BlockModelsMode::NONE)
+  if (d_env->getOptions().smt.blockModelsMode == options::BlockModelsMode::NONE)
   {
     std::stringstream ss;
     ss << "Cannot block model when block-models is set to none.";
@@ -1435,7 +1450,8 @@ std::vector<Node> SmtEngine::reduceUnsatCore(const std::vector<Node>& core)
   }
 }
 
-void SmtEngine::checkUnsatCore() {
+void SmtEngine::checkUnsatCore()
+{
   Assert(d_env->getOptions().smt.unsatCores)
       << "cannot check unsat core if unsat cores are turned off";
 
@@ -1460,20 +1476,25 @@ void SmtEngine::checkUnsatCore() {
   Notice() << "SmtEngine::checkUnsatCore(): pushing core assertions"
            << std::endl;
   theory::TrustSubstitutionMap& tls = d_env->getTopLevelSubstitutions();
-  for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) {
+  for (UnsatCore::iterator i = core.begin(); i != core.end(); ++i)
+  {
     Node assertionAfterExpansion = tls.apply(*i, false);
     Notice() << "SmtEngine::checkUnsatCore(): pushing core member " << *i
              << ", expanded to " << assertionAfterExpansion << "\n";
     coreChecker->assertFormula(assertionAfterExpansion);
   }
   Result r;
-  try {
+  try
+  {
     r = coreChecker->checkSat();
-  } catch(...) {
+  }
+  catch (...)
+  {
     throw;
   }
   Notice() << "SmtEngine::checkUnsatCore(): result is " << r << endl;
-  if(r.asSatisfiabilityResult().isUnknown()) {
+  if (r.asSatisfiabilityResult().isUnknown())
+  {
     Warning()
         << "SmtEngine::checkUnsatCore(): could not check core result unknown."
         << std::endl;
@@ -1485,7 +1506,8 @@ void SmtEngine::checkUnsatCore() {
   }
 }
 
-void SmtEngine::checkModel(bool hardFailure) {
+void SmtEngine::checkModel(bool hardFailure)
+{
   context::CDList<Node>* al = d_asserts->getAssertionList();
   // --check-model implies --produce-assertions, which enables the
   // assertion list, so we should be ok.
@@ -1511,7 +1533,8 @@ void SmtEngine::checkModel(bool hardFailure) {
   d_checkModels->checkModel(m, al, hardFailure);
 }
 
-UnsatCore SmtEngine::getUnsatCore() {
+UnsatCore SmtEngine::getUnsatCore()
+{
   Trace("smt") << "SMT getUnsatCore()" << std::endl;
   SmtScope smts(this);
   finishInit();
@@ -1564,7 +1587,8 @@ std::string SmtEngine::getProof()
   return ss.str();
 }
 
-void SmtEngine::printInstantiations( std::ostream& out ) {
+void SmtEngine::printInstantiations(std::ostream& out)
+{
   SmtScope smts(this);
   finishInit();
   QuantifiersEngine* qe = getAvailableQuantifiersEngine("printInstantiations");
@@ -1633,7 +1657,8 @@ void SmtEngine::printInstantiations( std::ostream& out ) {
       continue;
     }
     // must have a name
-    if (d_env->getOptions().printer.printInstMode == options::PrintInstMode::NUM)
+    if (d_env->getOptions().printer.printInstMode
+        == options::PrintInstMode::NUM)
     {
       out << "(num-instantiations " << name << " " << i.second.d_inst.size()
           << ")" << std::endl;
@@ -1758,7 +1783,8 @@ std::vector<Node> SmtEngine::getAssertions()
   if (!d_env->getOptions().smt.produceAssertions)
   {
     const char* msg =
-      "Cannot query the current assertion list when not in produce-assertions mode.";
+        "Cannot query the current assertion list when not in "
+        "produce-assertions mode.";
     throw ModalException(msg);
   }
   return getAssertionsInternal();
@@ -1794,13 +1820,15 @@ void SmtEngine::push()
   d_state->doPendingPops();
   Trace("smt") << "SMT push()" << endl;
   d_smtSolver->processAssertions(*d_asserts);
-  if(Dump.isOn("benchmark")) {
+  if (Dump.isOn("benchmark"))
+  {
     getPrinter().toStreamCmdPush(d_env->getDumpOut());
   }
   d_state->userPush();
 }
 
-void SmtEngine::pop() {
+void SmtEngine::pop()
+{
   SmtScope smts(this);
   finishInit();
   Trace("smt") << "SMT pop()" << endl;
@@ -1835,7 +1863,6 @@ void SmtEngine::resetAssertions()
     return;
   }
 
-
   Trace("smt") << "SMT resetAssertions()" << endl;
   if (Dump.isOn("benchmark"))
   {
@@ -1958,7 +1985,8 @@ std::string SmtEngine::getOption(const std::string& key) const
 
   if (key.find("command-verbosity:") == 0)
   {
-    auto it = d_commandVerbosity.find(key.substr(std::strlen("command-verbosity:")));
+    auto it =
+        d_commandVerbosity.find(key.substr(std::strlen("command-verbosity:")));
     if (it != d_commandVerbosity.end())
     {
       return std::to_string(it->second);
@@ -1980,7 +2008,7 @@ std::string SmtEngine::getOption(const std::string& key) const
   {
     vector<Node> result;
     Node defaultVerbosity;
-    for (const auto& verb: d_commandVerbosity)
+    for (const auto& verb : d_commandVerbosity)
     {
       // treat the command name as a variable name as opposed to a string
       // constant to avoid printing double quotes around the name
diff --git a/src/smt/smt_engine.h b/src/smt/solver_engine.h
index a06b2fd61..92fe30fa1 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/solver_engine.h
@@ -33,7 +33,8 @@
 
 namespace cvc5 {
 
-template <bool ref_count> class NodeTemplate;
+template <bool ref_count>
+class NodeTemplate;
 typedef NodeTemplate<true> Node;
 typedef NodeTemplate<false> TNode;
 class TypeNode;
@@ -56,9 +57,9 @@ class Solver;
 /* -------------------------------------------------------------------------- */
 
 namespace context {
-  class Context;
-  class UserContext;
-  }  // namespace context
+class Context;
+class UserContext;
+}  // namespace context
 
 /* -------------------------------------------------------------------------- */
 
@@ -69,8 +70,8 @@ class PreprocessingPassContext;
 /* -------------------------------------------------------------------------- */
 
 namespace prop {
-  class PropEngine;
-  }  // namespace prop
+class PropEngine;
+}  // namespace prop
 
 /* -------------------------------------------------------------------------- */
 
@@ -121,8 +122,8 @@ class CVC5_EXPORT SmtEngine
 
   /**
    * Construct an SmtEngine with the given expression manager.
-   * If provided, optr is a pointer to a set of options that should initialize the values
-   * of the options object owned by this class.
+   * If provided, optr is a pointer to a set of options that should initialize
+   * the values of the options object owned by this class.
    */
   SmtEngine(NodeManager* nm, const Options* optr = nullptr);
   /** Destruct the SMT engine.  */
diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp
index 37758ad4a..1c4633b5a 100644
--- a/src/theory/bv/abstraction.cpp
+++ b/src/theory/bv/abstraction.cpp
@@ -19,9 +19,9 @@
 #include "options/bv_options.h"
 #include "printer/printer.h"
 #include "smt/dump.h"
-#include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
+#include "smt/solver_engine.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
 #include "util/bitvector.h"
diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp
index dd3a3e9ce..9e3efa3bf 100644
--- a/src/theory/bv/bitblast/eager_bitblaster.cpp
+++ b/src/theory/bv/bitblast/eager_bitblaster.cpp
@@ -21,8 +21,8 @@
 #include "options/smt_options.h"
 #include "prop/cnf_stream.h"
 #include "prop/sat_solver_factory.h"
-#include "smt/smt_engine.h"
 #include "smt/smt_statistics_registry.h"
+#include "smt/solver_engine.h"
 #include "theory/bv/bv_solver_layered.h"
 #include "theory/bv/theory_bv.h"
 #include "theory/theory_model.h"
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp
index 3eb2eebe7..a61c7a9ab 100644
--- a/src/theory/bv/bitblast/lazy_bitblaster.cpp
+++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp
@@ -20,8 +20,8 @@
 #include "prop/cnf_stream.h"
 #include "prop/sat_solver.h"
 #include "prop/sat_solver_factory.h"
-#include "smt/smt_engine.h"
 #include "smt/smt_statistics_registry.h"
+#include "smt/solver_engine.h"
 #include "theory/bv/abstraction.h"
 #include "theory/bv/bv_solver_layered.h"
 #include "theory/bv/theory_bv.h"
diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index d6e60d1f4..27afdbbaa 100644
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -20,9 +20,9 @@
 #include "options/bv_options.h"
 #include "printer/printer.h"
 #include "smt/dump.h"
-#include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
+#include "smt/solver_engine.h"
 #include "smt_util/boolean_simplification.h"
 #include "theory/bv/bv_quick_check.h"
 #include "theory/bv/bv_solver_layered.h"
diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index 7553bcbb6..da2a8b3ce 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -25,8 +25,8 @@
 #include "context/context.h"
 #include "printer/printer.h"
 #include "smt/dump.h"
-#include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
+#include "smt/solver_engine.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/theory.h"
 #include "util/statistics_stats.h"
diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp
index 475df0b43..27deebe2f 100644
--- a/src/theory/quantifiers/candidate_rewrite_database.cpp
+++ b/src/theory/quantifiers/candidate_rewrite_database.cpp
@@ -17,9 +17,9 @@
 
 #include "options/base_options.h"
 #include "printer/printer.h"
-#include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
+#include "smt/solver_engine.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp
index 0fd5c21d5..f891b0e99 100644
--- a/src/theory/quantifiers/ematching/candidate_generator.cpp
+++ b/src/theory/quantifiers/ematching/candidate_generator.cpp
@@ -18,8 +18,8 @@
 #include "expr/dtype.h"
 #include "expr/dtype_cons.h"
 #include "options/quantifiers_options.h"
-#include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
+#include "smt/solver_engine.h"
 #include "theory/datatypes/datatypes_rewriter.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/quantifiers_state.h"
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index 4e571a66b..30f283dc2 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -17,9 +17,9 @@
 
 #include "options/theory_options.h"
 #include "proof/conv_proof_generator.h"
-#include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
+#include "smt/solver_engine.h"
 #include "theory/builtin/proof_checker.h"
 #include "theory/evaluator.h"
 #include "theory/quantifiers/extended_rewrite.h"
diff --git a/src/theory/smt_engine_subsolver.cpp b/src/theory/smt_engine_subsolver.cpp
index dda065d7b..108d59800 100644
--- a/src/theory/smt_engine_subsolver.cpp
+++ b/src/theory/smt_engine_subsolver.cpp
@@ -17,8 +17,8 @@
 #include "theory/smt_engine_subsolver.h"
 
 #include "smt/env.h"
-#include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
+#include "smt/solver_engine.h"
 #include "theory/rewriter.h"
 
 namespace cvc5 {
diff --git a/src/theory/smt_engine_subsolver.h b/src/theory/smt_engine_subsolver.h
index 028c35cd8..f46f29fc1 100644
--- a/src/theory/smt_engine_subsolver.h
+++ b/src/theory/smt_engine_subsolver.h
@@ -22,7 +22,7 @@
 #include <vector>
 
 #include "expr/node.h"
-#include "smt/smt_engine.h"
+#include "smt/solver_engine.h"
 
 namespace cvc5 {
 namespace theory {
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 528e093aa..8c1a17fe1 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -20,7 +20,7 @@
 #include "options/theory_options.h"
 #include "options/uf_options.h"
 #include "smt/env.h"
-#include "smt/smt_engine.h"
+#include "smt/solver_engine.h"
 #include "theory/trust_substitutions.h"
 #include "util/rational.h"
 
diff --git a/test/api/smt2_compliance.cpp b/test/api/smt2_compliance.cpp
index 83c3833d1..2a39b1d0b 100644
--- a/test/api/smt2_compliance.cpp
+++ b/test/api/smt2_compliance.cpp
@@ -22,7 +22,7 @@
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
 #include "smt/command.h"
-#include "smt/smt_engine.h"
+#include "smt/solver_engine.h"
 
 using namespace cvc5;
 using namespace cvc5::parser;
diff --git a/test/unit/node/attribute_white.cpp b/test/unit/node/attribute_white.cpp
index 4b0f1892f..fef1184a2 100644
--- a/test/unit/node/attribute_white.cpp
+++ b/test/unit/node/attribute_white.cpp
@@ -22,8 +22,8 @@
 #include "expr/node_manager.h"
 #include "expr/node_manager_attributes.h"
 #include "expr/node_value.h"
-#include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
+#include "smt/solver_engine.h"
 #include "test_node.h"
 #include "theory/theory.h"
 #include "theory/theory_engine.h"
diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp
index d083c9fb0..df78061a0 100644
--- a/test/unit/node/node_black.cpp
+++ b/test/unit/node/node_black.cpp
@@ -30,7 +30,7 @@
 #include "options/base_options.h"
 #include "options/language.h"
 #include "options/options_public.h"
-#include "smt/smt_engine.h"
+#include "smt/solver_engine.h"
 #include "test_node.h"
 #include "theory/rewriter.h"
 #include "util/bitvector.h"
diff --git a/test/unit/node/type_node_white.cpp b/test/unit/node/type_node_white.cpp
index d3d05040f..d4e86608d 100644
--- a/test/unit/node/type_node_white.cpp
+++ b/test/unit/node/type_node_white.cpp
@@ -19,7 +19,7 @@
 
 #include "expr/node_manager.h"
 #include "expr/type_node.h"
-#include "smt/smt_engine.h"
+#include "smt/solver_engine.h"
 #include "test_node.h"
 #include "util/rational.h"
 
diff --git a/test/unit/preprocessing/pass_bv_gauss_white.cpp b/test/unit/preprocessing/pass_bv_gauss_white.cpp
index 329c565ea..ad3c1b0d1 100644
--- a/test/unit/preprocessing/pass_bv_gauss_white.cpp
+++ b/test/unit/preprocessing/pass_bv_gauss_white.cpp
@@ -22,8 +22,8 @@
 #include "preprocessing/assertion_pipeline.h"
 #include "preprocessing/passes/bv_gauss.h"
 #include "preprocessing/preprocessing_pass_context.h"
-#include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
+#include "smt/solver_engine.h"
 #include "test_smt.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
diff --git a/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp b/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp
index c10d8f363..254c4b5e9 100644
--- a/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp
+++ b/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp
@@ -15,7 +15,7 @@
 
 #include "expr/node_manager.h"
 #include "preprocessing/passes/foreign_theory_rewrite.h"
-#include "smt/smt_engine.h"
+#include "smt/solver_engine.h"
 #include "test_smt.h"
 #include "util/rational.h"
 
diff --git a/test/unit/printer/smt2_printer_black.cpp b/test/unit/printer/smt2_printer_black.cpp
index 3d9c3ca2c..66304ec01 100644
--- a/test/unit/printer/smt2_printer_black.cpp
+++ b/test/unit/printer/smt2_printer_black.cpp
@@ -19,7 +19,7 @@
 #include "expr/node.h"
 #include "expr/node_manager.h"
 #include "options/language.h"
-#include "smt/smt_engine.h"
+#include "smt/solver_engine.h"
 #include "test_smt.h"
 #include "util/regexp.h"
 #include "util/string.h"
diff --git a/test/unit/test_env.h b/test/unit/test_env.h
index b3f60a98a..4b4fb72e9 100644
--- a/test/unit/test_env.h
+++ b/test/unit/test_env.h
@@ -20,8 +20,8 @@
 #include "expr/skolem_manager.h"
 #include "options/options.h"
 #include "smt/env.h"
-#include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
+#include "smt/solver_engine.h"
 #include "test.h"
 
 namespace cvc5 {
diff --git a/test/unit/test_node.h b/test/unit/test_node.h
index a6a85b1b1..08fa8eb30 100644
--- a/test/unit/test_node.h
+++ b/test/unit/test_node.h
@@ -18,8 +18,8 @@
 
 #include "expr/node_manager.h"
 #include "expr/skolem_manager.h"
-#include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
+#include "smt/solver_engine.h"
 #include "test.h"
 
 namespace cvc5 {
diff --git a/test/unit/test_smt.h b/test/unit/test_smt.h
index 92701d60c..5dd4137aa 100644
--- a/test/unit/test_smt.h
+++ b/test/unit/test_smt.h
@@ -21,8 +21,8 @@
 #include "expr/node_manager.h"
 #include "expr/skolem_manager.h"
 #include "proof/proof_checker.h"
-#include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
+#include "smt/solver_engine.h"
 #include "test.h"
 #include "theory/output_channel.h"
 #include "theory/rewriter.h"