Eliminate SmtSolver dependency on SolverEngineState (#8581)

This is in preparation for making SmtSolver able to be deep reset (reconstructed) within in a SolverEngine instance.

diff --git a/src/proof/proof_checker.cpp b/src/proof/proof_checker.cpp
index 4b9fb40ce82f7a2a3614d411c7fefaec48cebc26..fe68e418c821d04ad328fa57e909efebf175849c 100644 (file)
--- a/src/proof/proof_checker.cpp
+++ b/src/proof/proof_checker.cpp
@@ -93,6 +93,12 @@ ProofChecker::ProofChecker(bool eagerCheck,
 {
 }
 
+void ProofChecker::reset()
+{
+  d_checker.clear();
+  d_plevel.clear();
+}
+
 Node ProofChecker::check(ProofNode* pn, Node expected)
 {
   return check(pn->getRule(), pn->getChildren(), pn->getArguments(), expected);

diff --git a/src/proof/proof_checker.h b/src/proof/proof_checker.h
index 2c69588abdcd8e43e3a5caf5d77ff739327e4982..652ec0cf1be5cd2a0bcf154e0518d5b8fbf0cc51 100644 (file)
--- a/src/proof/proof_checker.h
+++ b/src/proof/proof_checker.h
@@ -109,6 +109,8 @@ class ProofChecker
                uint32_t pclevel = 0,
                rewriter::RewriteDb* rdb = nullptr);
   ~ProofChecker() {}
+  /** Reset, which clears the rule checkers */
+  void reset();
   /**
    * Return the formula that is proven by proof node pn, or null if pn is not
    * well-formed. If expected is non-null, then we return null if pn does not

diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index f1670cc924e7294a8bf6fc30702b39acf24f603e..bd23ff3530ee8a88c4823b94d4a9b45e66cc7a6d 100644 (file)
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -15,6 +15,7 @@
 
 #include "smt/smt_solver.h"
 
+#include "options/base_options.h"
 #include "options/main_options.h"
 #include "options/smt_options.h"
 #include "prop/prop_engine.h"
@@ -35,11 +36,9 @@ namespace cvc5::internal {
 namespace smt {
 
 SmtSolver::SmtSolver(Env& env,
-                     SolverEngineState& state,
                      AbstractValues& abs,
                      SolverEngineStatistics& stats)
-    : d_env(env),
-      d_state(state),
+    : EnvObj(env),
       d_pp(env, abs, stats),
       d_stats(stats),
       d_theoryEngine(nullptr),
@@ -65,6 +64,9 @@ void SmtSolver::finishInit()
   ProofNodeManager* pnm = d_env.getProofNodeManager();
   if (pnm)
   {
+    // reset the rule checkers
+    pnm->getChecker()->reset();
+    // add rule checkers from the theory engine
     d_theoryEngine->initializeProofChecker(pnm->getChecker());
   }
   Trace("smt-debug") << "Making prop engine..." << std::endl;
@@ -116,13 +118,8 @@ Result SmtSolver::checkSatisfiability(Assertions& as,
                                       const std::vector<Node>& assumptions)
 {
   Result result;
-
-  bool hasAssumptions = !assumptions.empty();
-
   try
   {
-    // update the state to indicate we are about to run a check-sat
-    d_state.notifyCheckSat(hasAssumptions);
 
     // then, initialize the assertions
     as.initializeCheckSat(assumptions);
@@ -208,19 +205,13 @@ Result SmtSolver::checkSatisfiability(Assertions& as,
 
   // set the filename on the result
   const std::string& filename = d_env.getOptions().driver.filename;
-  result = Result(result, filename);
-
-  // notify our state of the check-sat result
-  d_state.notifyCheckSatResult(hasAssumptions, result);
-
-  return result;
+  return Result(result, filename);
 }
 
 void SmtSolver::processAssertions(Assertions& as)
 {
   TimerStat::CodeTimer paTimer(d_stats.d_processAssertionsTime);
   d_env.getResourceManager()->spendResource(Resource::PreprocessStep);
-  Assert(d_state.isFullyReady());
 
   preprocessing::AssertionPipeline& ap = as.getAssertionPipeline();
 

diff --git a/src/smt/smt_solver.h b/src/smt/smt_solver.h
index 429d7ee21e453d97abb1a4d833f2f44ae327165e..78d11ef2a53761968f176cd85d3f319ba51b525f 100644 (file)
--- a/src/smt/smt_solver.h
+++ b/src/smt/smt_solver.h
@@ -21,6 +21,8 @@
 #include <vector>
 
 #include "expr/node.h"
+#include "smt/assertions.h"
+#include "smt/env_obj.h"
 #include "smt/preprocessor.h"
 #include "theory/logic_info.h"
 #include "util/result.h"
@@ -43,7 +45,6 @@ class QuantifiersEngine;
 
 namespace smt {
 
-class Assertions;
 class SolverEngineState;
 struct SolverEngineStatistics;
 
@@ -61,11 +62,10 @@ struct SolverEngineStatistics;
  * models) can be queries using other classes that examine the state of the
  * TheoryEngine directly, which can be accessed via getTheoryEngine.
  */
-class SmtSolver
+class SmtSolver : protected EnvObj
 {
  public:
   SmtSolver(Env& env,
-            SolverEngineState& state,
             AbstractValues& abs,
             SolverEngineStatistics& stats);
   ~SmtSolver();
@@ -114,10 +114,6 @@ class SmtSolver
   //------------------------------------------ end access methods
 
  private:
-  /** Reference to the environment */
-  Env& d_env;
-  /** Reference to the state of the SolverEngine */
-  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 46b30206bf422749010cd2444c42d973722d7940..5ae8bd08f4413ce0610232aee48e8841a04d55ae 100644 (file)
--- a/src/smt/solver_engine.cpp
+++ b/src/smt/solver_engine.cpp
@@ -117,7 +117,7 @@ SolverEngine::SolverEngine(NodeManager* nm, const Options* optr)
   // make statistics
   d_stats.reset(new SolverEngineStatistics());
   // make the SMT solver
-  d_smtSolver.reset(new SmtSolver(*d_env, *d_state, *d_absValues, *d_stats));
+  d_smtSolver.reset(new SmtSolver(*d_env, *d_absValues, *d_stats));
   // make the SyGuS solver
   d_sygusSolver.reset(new SygusSolver(*d_env.get(), *d_smtSolver));
   // make the quantifier elimination solver
@@ -750,17 +750,24 @@ Result SolverEngine::checkSat(const std::vector<Node>& assumptions)
 
 Result SolverEngine::checkSatInternal(const std::vector<Node>& assumptions)
 {
-  Result r;
-
   SolverEngineScope smts(this);
   finishInit();
 
   Trace("smt") << "SolverEngine::checkSat(" << assumptions << ")" << endl;
+  // update the state to indicate we are about to run a check-sat
+  bool hasAssumptions = !assumptions.empty();
+  d_state->notifyCheckSat(hasAssumptions);
+
+  // state should be fully ready now
+  Assert(d_state->isFullyReady());
+
   // check the satisfiability with the solver object
-  r = d_smtSolver->checkSatisfiability(*d_asserts.get(), assumptions);
+  Result r = d_smtSolver->checkSatisfiability(*d_asserts.get(), assumptions);
 
   Trace("smt") << "SolverEngine::checkSat(" << assumptions << ") => " << r
                << endl;
+  // notify our state of the check-sat result
+  d_state->notifyCheckSatResult(hasAssumptions, r);
 
   // Check that SAT results generate a model correctly.
   if (d_env->getOptions().smt.checkModels)