Rename SmtEngine to SolverEngine. (#7282)

14 files changed, 31 insertions, 29 deletions

diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp
index 27deebe2f..ab1efe728 100644
--- a/src/theory/quantifiers/candidate_rewrite_database.cpp
+++ b/src/theory/quantifiers/candidate_rewrite_database.cpp
@@ -140,9 +140,9 @@ Node CandidateRewriteDatabase::addTerm(Node sol,
         Trace("rr-check") << "Check candidate rewrite : " << crr << std::endl;
 
         // Notice we don't set produce-models. rrChecker takes the same
-        // options as the SmtEngine we belong to, where we ensure that
+        // options as the SolverEngine we belong to, where we ensure that
         // produce-models is set.
-        std::unique_ptr<SmtEngine> rrChecker;
+        std::unique_ptr<SolverEngine> rrChecker;
         initializeChecker(rrChecker, crr);
         Result r = rrChecker->checkSat();
         Trace("rr-check") << "...result : " << r << std::endl;
diff --git a/src/theory/quantifiers/candidate_rewrite_database.h b/src/theory/quantifiers/candidate_rewrite_database.h
index c0e783fc1..f81bcfd7b 100644
--- a/src/theory/quantifiers/candidate_rewrite_database.h
+++ b/src/theory/quantifiers/candidate_rewrite_database.h
@@ -36,7 +36,7 @@ namespace quantifiers {
  * of this class are to perform the "equivalence checking" and "congruence
  * and matching filtering" in Figure 1. The equivalence checking is done
  * through a combination of the sygus sampler object owned by this class
- * and the calls made to copies of the SmtEngine in ::addTerm. The rewrite
+ * and the calls made to copies of the SolverEngine in ::addTerm. The rewrite
  * rule filtering (based on congruence, matching, variable ordering) is also
  * managed by the sygus sampler object.
  */
diff --git a/src/theory/quantifiers/cegqi/nested_qe.cpp b/src/theory/quantifiers/cegqi/nested_qe.cpp
index 869ebe036..0d01efba7 100644
--- a/src/theory/quantifiers/cegqi/nested_qe.cpp
+++ b/src/theory/quantifiers/cegqi/nested_qe.cpp
@@ -137,7 +137,7 @@ Node NestedQe::doQe(Env& env, Node q)
   Trace("cegqi-nested-qe") << "  Apply qe to " << q << std::endl;
   NodeManager* nm = NodeManager::currentNM();
   q = nm->mkNode(kind::EXISTS, q[0], q[1].negate());
-  std::unique_ptr<SmtEngine> smt_qe;
+  std::unique_ptr<SolverEngine> smt_qe;
   initializeSubsolver(smt_qe, env);
   Node qqe = smt_qe->getQuantifierElimination(q, true, false);
   if (expr::hasBoundVar(qqe))
diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp
index 49b1d56fa..d648a7a29 100644
--- a/src/theory/quantifiers/expr_miner.cpp
+++ b/src/theory/quantifiers/expr_miner.cpp
@@ -50,7 +50,7 @@ Node ExprMiner::convertToSkolem(Node n)
       d_vars.begin(), d_vars.end(), d_skolems.begin(), d_skolems.end());
 }
 
-void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker,
+void ExprMiner::initializeChecker(std::unique_ptr<SolverEngine>& checker,
                                   Node query)
 {
   Assert (!query.isNull());
@@ -88,7 +88,7 @@ Result ExprMiner::doCheck(Node query)
       return Result(Result::SAT);
     }
   }
-  std::unique_ptr<SmtEngine> smte;
+  std::unique_ptr<SolverEngine> smte;
   initializeChecker(smte, query);
   return smte->checkSat();
 }
diff --git a/src/theory/quantifiers/expr_miner.h b/src/theory/quantifiers/expr_miner.h
index 56eaccd7c..3933b9635 100644
--- a/src/theory/quantifiers/expr_miner.h
+++ b/src/theory/quantifiers/expr_miner.h
@@ -30,7 +30,7 @@
 namespace cvc5 {
 
 class Env;
-class SmtEngine;
+class SolverEngine;
 
 namespace theory {
 namespace quantifiers {
@@ -85,7 +85,7 @@ class ExprMiner : protected EnvObj
    * of the argument "query", which is a formula whose free variables (of
    * kind BOUND_VARIABLE) are a subset of d_vars.
    */
-  void initializeChecker(std::unique_ptr<SmtEngine>& smte, Node query);
+  void initializeChecker(std::unique_ptr<SolverEngine>& smte, Node query);
   /**
    * Run the satisfiability check on query and return the result
    * (sat/unsat/unknown).
diff --git a/src/theory/quantifiers/query_generator.cpp b/src/theory/quantifiers/query_generator.cpp
index 31d8c3c22..f7c9aa37b 100644
--- a/src/theory/quantifiers/query_generator.cpp
+++ b/src/theory/quantifiers/query_generator.cpp
@@ -157,7 +157,7 @@ void QueryGenerator::checkQuery(Node qy, unsigned spIndex)
   {
     Trace("sygus-qgen-check") << "  query: check " << qy << "..." << std::endl;
     // make the satisfiability query
-    std::unique_ptr<SmtEngine> queryChecker;
+    std::unique_ptr<SolverEngine> queryChecker;
     initializeChecker(queryChecker, qy);
     Result r = queryChecker->checkSat();
     Trace("sygus-qgen-check") << "  query: ...got : " << r << std::endl;
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index d039eb855..ad9da816b 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -226,7 +226,7 @@ bool CegSingleInv::solve()
     siq = nm->mkNode(FORALL, siq[0], siq[1], n_attr);
   }
   // solve the single invocation conjecture using a fresh copy of SMT engine
-  std::unique_ptr<SmtEngine> siSmt;
+  std::unique_ptr<SolverEngine> siSmt;
   initializeSubsolver(siSmt, d_env);
   // do not use shared selectors in subsolver, since this leads to solutions
   // with non-user symbols
diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
index b9066b079..936310e4e 100644
--- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
@@ -595,7 +595,7 @@ bool CegisCoreConnective::Component::addToAsserts(CegisCoreConnective* p,
   return true;
 }
 
-void CegisCoreConnective::getModel(SmtEngine& smt,
+void CegisCoreConnective::getModel(SolverEngine& smt,
                                    std::vector<Node>& vals) const
 {
   for (const Node& v : d_vars)
@@ -607,7 +607,7 @@ void CegisCoreConnective::getModel(SmtEngine& smt,
 }
 
 bool CegisCoreConnective::getUnsatCore(
-    SmtEngine& smt,
+    SolverEngine& smt,
     const std::unordered_set<Node>& queryAsserts,
     std::vector<Node>& uasserts) const
 {
@@ -733,7 +733,7 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck,
   {
     addSuccess = false;
     // try a new core
-    std::unique_ptr<SmtEngine> checkSol;
+    std::unique_ptr<SolverEngine> checkSol;
     initializeSubsolver(checkSol, d_env);
     Trace("sygus-ccore") << "----- Check candidate " << an << std::endl;
     std::vector<Node> rasserts = asserts;
@@ -773,7 +773,7 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck,
         {
           // In terms of Variant #2, this is the check "if S ^ U is unsat"
           Trace("sygus-ccore") << "----- Check side condition" << std::endl;
-          std::unique_ptr<SmtEngine> checkSc;
+          std::unique_ptr<SolverEngine> checkSc;
           initializeSubsolver(checkSc, d_env);
           std::vector<Node> scasserts;
           scasserts.insert(scasserts.end(), uasserts.begin(), uasserts.end());
diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.h b/src/theory/quantifiers/sygus/cegis_core_connective.h
index ebcd871aa..3ee631dea 100644
--- a/src/theory/quantifiers/sygus/cegis_core_connective.h
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.h
@@ -28,7 +28,7 @@
 
 namespace cvc5 {
 
-class SmtEngine;
+class SolverEngine;
 
 namespace theory {
 namespace quantifiers {
@@ -339,7 +339,7 @@ class CegisCoreConnective : public Cegis
    * Assuming smt has just been called to check-sat and returned "SAT", this
    * method adds the model for d_vars to mvs.
    */
-  void getModel(SmtEngine& smt, std::vector<Node>& mvs) const;
+  void getModel(SolverEngine& smt, std::vector<Node>& mvs) const;
   /**
    * Assuming smt has just been called to check-sat and returned "UNSAT", this
    * method get the unsat core and adds it to uasserts.
@@ -349,7 +349,7 @@ class CegisCoreConnective : public Cegis
    * If one of the formulas in queryAsserts was in the unsat core, then this
    * method returns true. Otherwise, this method returns false.
    */
-  bool getUnsatCore(SmtEngine& smt,
+  bool getUnsatCore(SolverEngine& smt,
                     const std::unordered_set<Node>& queryAsserts,
                     std::vector<Node>& uasserts) const;
   /**
diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp
index 7e20f56c3..1a42ec337 100644
--- a/src/theory/quantifiers/sygus/sygus_interpol.cpp
+++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp
@@ -260,7 +260,9 @@ void SygusInterpol::mkSygusConjecture(Node itp,
   Trace("sygus-interpol") << "Generate: " << d_sygusConj << std::endl;
 }
 
-bool SygusInterpol::findInterpol(SmtEngine* subSolver, Node& interpol, Node itp)
+bool SygusInterpol::findInterpol(SolverEngine* subSolver,
+                                 Node& interpol,
+                                 Node itp)
 {
   // get the synthesis solution
   std::map<Node, Node> sols;
@@ -270,12 +272,12 @@ bool SygusInterpol::findInterpol(SmtEngine* subSolver, Node& interpol, Node itp)
   if (its == sols.end())
   {
     Trace("sygus-interpol")
-        << "SmtEngine::getInterpol: could not find solution!" << std::endl;
+        << "SolverEngine::getInterpol: could not find solution!" << std::endl;
     throw RecoverableModalException(
         "Could not find solution for get-interpol.");
     return false;
   }
-  Trace("sygus-interpol") << "SmtEngine::getInterpol: solution is "
+  Trace("sygus-interpol") << "SolverEngine::getInterpol: solution is "
                           << its->second << std::endl;
   interpol = its->second;
   // replace back the created variables to original symbols.
@@ -323,7 +325,7 @@ bool SygusInterpol::solveInterpolation(const std::string& name,
   Node itp = mkPredicate(name);
   mkSygusConjecture(itp, axioms, conj);
 
-  std::unique_ptr<SmtEngine> subSolver;
+  std::unique_ptr<SolverEngine> subSolver;
   initializeSubsolver(subSolver, d_env);
   // get the logic
   LogicInfo l = subSolver->getLogicInfo().getUnlockedCopy();
@@ -337,15 +339,15 @@ bool SygusInterpol::solveInterpolation(const std::string& name,
   }
   std::vector<Node> vars_empty;
   subSolver->declareSynthFun(itp, grammarType, false, vars_empty);
-  Trace("sygus-interpol") << "SmtEngine::getInterpol: made conjecture : "
+  Trace("sygus-interpol") << "SolverEngine::getInterpol: made conjecture : "
                           << d_sygusConj << ", solving for "
                           << d_sygusConj[0][0] << std::endl;
   subSolver->assertSygusConstraint(d_sygusConj);
 
-  Trace("sygus-interpol") << "  SmtEngine::getInterpol check sat..."
+  Trace("sygus-interpol") << "  SolverEngine::getInterpol check sat..."
                           << std::endl;
   Result r = subSolver->checkSynth();
-  Trace("sygus-interpol") << "  SmtEngine::getInterpol result: " << r
+  Trace("sygus-interpol") << "  SolverEngine::getInterpol result: " << r
                           << std::endl;
   if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
   {
diff --git a/src/theory/quantifiers/sygus/sygus_interpol.h b/src/theory/quantifiers/sygus/sygus_interpol.h
index 8f91d921b..924426365 100644
--- a/src/theory/quantifiers/sygus/sygus_interpol.h
+++ b/src/theory/quantifiers/sygus/sygus_interpol.h
@@ -27,7 +27,7 @@
 namespace cvc5 {
 
 class Env;
-class SmtEngine;
+class SolverEngine;
 
 namespace theory {
 namespace quantifiers {
@@ -174,7 +174,7 @@ class SygusInterpol : protected EnvObj
    * @param interpol the solution to the sygus conjecture.
    * @param itp the interpolation predicate.
    */
-  bool findInterpol(SmtEngine* subsolver, Node& interpol, Node itp);
+  bool findInterpol(SolverEngine* subsolver, Node& interpol, Node itp);
   /**
    * symbols from axioms and conjecture.
    */
diff --git a/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp b/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp
index 0dfa0141f..2400e0e56 100644
--- a/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp
+++ b/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp
@@ -51,7 +51,7 @@ Node SygusQePreproc::preprocess(Node q)
     return Node::null();
   }
   // create new smt engine to do quantifier elimination
-  std::unique_ptr<SmtEngine> smt_qe;
+  std::unique_ptr<SolverEngine> smt_qe;
   initializeSubsolver(smt_qe, d_env);
   Trace("cegqi-qep") << "Property is non-ground single invocation, run "
                         "QE to obtain single invocation."
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
index b7611784d..44269eb6f 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
@@ -228,7 +228,7 @@ bool SygusRepairConst::repairSolution(Node sygusBody,
 
   Trace("sygus-engine") << "Repairing previous solution..." << std::endl;
   // make the satisfiability query
-  std::unique_ptr<SmtEngine> repcChecker;
+  std::unique_ptr<SolverEngine> repcChecker;
   // initialize the subsolver using the standard method
   initializeSubsolver(
       repcChecker,
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.h b/src/theory/quantifiers/sygus/sygus_repair_const.h
index e6a1ee514..7797f7fa9 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.h
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.h
@@ -44,7 +44,7 @@ class TermDbSygus;
  *   forall x. P( (\x. t[x,c']), x )  [***]
  * is satisfiable, where notice that the above formula after beta-reduction may
  * be one in pure first-order logic in a decidable theory (say linear
- * arithmetic). To check this, we invoke a separate instance of the SmtEngine
+ * arithmetic). To check this, we invoke a separate instance of the SolverEngine
  * within repairSolution(...) below, which if satisfiable gives us the
  * valuation for c'.
  */