Move notifications about context to SMT driver (cvc5#9274)

In preparation for cvc5#9268.

src/smt/context_manager.cpp

@@ -21,18 +21,16 @@
 #include "options/option_exception.h"
 #include "options/smt_options.h"
 #include "smt/env.h"
-#include "smt/smt_solver.h"
+#include "smt/smt_driver.h"
 #include "smt/solver_engine_state.h"
 
 namespace cvc5::internal {
 namespace smt {
 
-ContextManager::ContextManager(Env& env,
-                               SolverEngineState& state,
-                               SmtSolver& smt)
+ContextManager::ContextManager(Env& env, SolverEngineState& state)
     : EnvObj(env),
       d_state(state),
-      d_smt(smt),
+      d_smt(nullptr),
       d_pendingPops(0),
       d_needPostsolve(false)
 {
@@ -70,8 +68,9 @@ void ContextManager::notifyCheckSatResult(bool hasAssumptions)
   }
 }
 
-void ContextManager::setup()
+void ContextManager::setup(SmtDriver* smt)
 {
+  d_smt = smt;
   // push a context
   push();
 }
@@ -148,10 +147,10 @@ void ContextManager::internalPush()
   if (options().base.incrementalSolving)
   {
     // notifies the SolverEngine to process the assertions immediately
-    d_smt.notifyPushPre();
+    d_smt->notifyPushPre();
     userContext()->push();
     // the context push is done inside of the SAT solver
-    d_smt.notifyPushPost();
+    d_smt->notifyPushPost();
   }
 }
 
@@ -175,13 +174,13 @@ void ContextManager::doPendingPops()
   // check to see if a postsolve() is pending
   if (d_needPostsolve)
   {
-    d_smt.notifyPostSolve();
+    d_smt->notifyPostSolve();
     d_needPostsolve = false;
   }
   while (d_pendingPops > 0)
   {
     // the context pop is done inside of the SAT solver
-    d_smt.notifyPopPre();
+    d_smt->notifyPopPre();
     // pop the context
     userContext()->pop();
     --d_pendingPops;

src/smt/context_manager.h

@@ -29,7 +29,7 @@
 namespace cvc5::internal {
 namespace smt {
 
-class SmtSolver;
+class SmtDriver;
 class SolverEngineState;
 
 /**
@@ -39,7 +39,7 @@ class SolverEngineState;
 class ContextManager : protected EnvObj
 {
  public:
-  ContextManager(Env& env, SolverEngineState& state, SmtSolver& smt);
+  ContextManager(Env& env, SolverEngineState& state);
   ~ContextManager() {}
   /**
    * Notify that we are resetting the assertions, called when a reset-assertions
@@ -67,8 +67,11 @@ class ContextManager : protected EnvObj
   /**
    * Setup the context, which makes a single push to maintain a global
    * context around everything.
+   *
+   * @param smt The driver that handles notifications from this context
+   * manager
    */
-  void setup();
+  void setup(SmtDriver* smt);
   /**
    * Prepare for a shutdown of the SolverEngine, which does pending pops and
    * pops the user context to zero.
@@ -123,8 +126,8 @@ class ContextManager : protected EnvObj
   void internalPop(bool immediate = false);
   /** Reference to the SolverEngineState */
   SolverEngineState& d_state;
-  /** Reference to the SmtSolver */
-  SmtSolver& d_smt;
+  /** Pointer to the SmtDriver */
+  SmtDriver* d_smt;
   /** The context levels of user pushes */
   std::vector<int> d_userLevels;
   /** Number of internal pops that have been deferred. */

src/smt/smt_driver.cpp

@@ -74,7 +74,7 @@ Result SmtDriver::checkSat(const std::vector<Node>& assumptions)
           // finish init to construct new theory/prop engine
           d_smt.finishInit();
           // setup
-          d_ctx->setup();
+          d_ctx->setup(this);
         }
         else
         {
@@ -109,6 +109,24 @@ Result SmtDriver::checkSat(const std::vector<Node>& assumptions)
   return result;
 }
 
+void SmtDriver::refreshAssertions()
+{
+  d_smt.refreshAssertions();
+}
+
+void SmtDriver::notifyPushPre()
+{
+  // must preprocess the assertions and push them to the SAT solver, to make
+  // the state accurate prior to pushing
+  d_smt.refreshAssertions();
+}
+
+void SmtDriver::notifyPushPost() { d_smt.pushPropContext(); }
+
+void SmtDriver::notifyPopPre() { d_smt.popPropContext(); }
+
+void SmtDriver::notifyPostSolve() { d_smt.postsolve(); }
+
 SmtDriverSingleCall::SmtDriverSingleCall(Env& env, SmtSolver& smt)
     : SmtDriver(env, smt, nullptr)
 {
@@ -125,5 +143,6 @@ Result SmtDriverSingleCall::checkSatNext()
 
 void SmtDriverSingleCall::getNextAssertions(Assertions& as) { Unreachable(); }
 
+
 }  // namespace smt
 }  // namespace cvc5::internal

src/smt/smt_driver.h

@@ -21,6 +21,7 @@
 #include <vector>
 
 #include "expr/node.h"
+#include "preprocessing/assertion_pipeline.h"
 #include "smt/assertions.h"
 #include "smt/env_obj.h"
 #include "util/result.h"
@@ -53,6 +54,38 @@ class SmtDriver : protected EnvObj
    */
   Result checkSat(const std::vector<Node>& assumptions);
 
+  /**
+   * Refresh the assertions that have been asserted to the underlying SMT
+   * solver. This gets the set of unprocessed assertions of the underlying
+   * SMT solver, preprocesses them, pushes them into the SMT solver.
+   *
+   * We ensure that assertions are refreshed eagerly during user pushes to
+   * ensure that assertions are only preprocessed in one context.
+   */
+  void refreshAssertions();
+  // --------------------------------------- callbacks from the context manager
+  /**
+   * Notify push pre, which is called just before the user context of the state
+   * pushes. This processes all pending assertions.
+   */
+  void notifyPushPre();
+  /**
+   * Notify push post, which is called just after the user context of the state
+   * pushes. This performs a push on the underlying prop engine.
+   */
+  void notifyPushPost();
+  /**
+   * Notify pop pre, which is called just before the user context of the state
+   * pops. This performs a pop on the underlying prop engine.
+   */
+  void notifyPopPre();
+  /**
+   * Notify post solve, which is called once per check-sat query. It is
+   * triggered when the first d_state.doPendingPops() is issued after the
+   * check-sat. This calls the postsolve method of the underlying TheoryEngine.
+   */
+  void notifyPostSolve();
+  // ----------------------------------- end callbacks from the context manager
  protected:
   /**
    * Check satisfiability next, return the result.

src/smt/smt_solver.cpp

@@ -266,28 +266,21 @@ Preprocessor* SmtSolver::getPreprocessor() { return &d_pp; }
 
 Assertions& SmtSolver::getAssertions() { return d_asserts; }
 
-void SmtSolver::notifyPushPre()
-{
-  // must preprocess the assertions and push them to the SAT solver, to make
-  // the state accurate prior to pushing
-  refreshAssertions();
-}
-
-void SmtSolver::notifyPushPost()
+void SmtSolver::pushPropContext()
 {
   TimerStat::CodeTimer pushPopTimer(d_stats.d_pushPopTime);
   Assert(d_propEngine != nullptr);
   d_propEngine->push();
 }
 
-void SmtSolver::notifyPopPre()
+void SmtSolver::popPropContext()
 {
   TimerStat::CodeTimer pushPopTimer(d_stats.d_pushPopTime);
   Assert(d_propEngine != nullptr);
   d_propEngine->pop();
 }
 
-void SmtSolver::notifyPostSolve()
+void SmtSolver::postsolve()
 {
   Assert(d_propEngine != nullptr);
   d_propEngine->resetTrail();

src/smt/smt_solver.h

@@ -98,29 +98,15 @@ class SmtSolver : protected EnvObj
    * if trackPreprocessedAssertions is true.
    */
   const std::unordered_map<size_t, Node>& getPreprocessedSkolemMap() const;
-  // --------------------------------------- callbacks from the context manager
+  /** Performs a push on the underlying prop engine. */
+  void pushPropContext();
+  /** Performs a pop on the underlying prop engine. */
+  void popPropContext();
   /**
-   * Notify push pre, which is called just before the user context of the state
-   * pushes. This processes all pending assertions.
+   * Reset the prop engine trail and call the postsolve method of the
+   * underlying TheoryEngine.
    */
-  void notifyPushPre();
-  /**
-   * Notify push post, which is called just after the user context of the state
-   * pushes. This performs a push on the underlying prop engine.
-   */
-  void notifyPushPost();
-  /**
-   * Notify pop pre, which is called just before the user context of the state
-   * pops. This performs a pop on the underlying prop engine.
-   */
-  void notifyPopPre();
-  /**
-   * Notify post solve, which is called once per check-sat query. It is
-   * triggered when the first d_state.doPendingPops() is issued after the
-   * check-sat. This calls the postsolve method of the underlying TheoryEngine.
-   */
-  void notifyPostSolve();
-  // ----------------------------------- end callbacks from the context manager
+  void postsolve();
   //------------------------------------------ access methods
   /** Get a pointer to the TheoryEngine owned by this solver. */
   TheoryEngine* getTheoryEngine();

src/smt/solver_engine.cpp

@@ -112,7 +112,7 @@ SolverEngine::SolverEngine(const Options* optr)
   // make the SMT solver
   d_smtSolver.reset(new SmtSolver(*d_env, *d_absValues, *d_stats));
   // make the context manager
-  d_ctxManager.reset(new ContextManager(*d_env.get(), *d_state, *d_smtSolver));
+  d_ctxManager.reset(new ContextManager(*d_env.get(), *d_state));
   // make the SyGuS solver
   d_sygusSolver.reset(new SygusSolver(*d_env.get(), *d_smtSolver));
   // make the quantifier elimination solver
@@ -177,6 +177,9 @@ void SolverEngine::finishInit()
   // enable proof support in the environment/rewriter
   d_env->finishInit(pnm);
 
+  Trace("smt-debug") << "SolverEngine::finishInit" << std::endl;
+  d_smtSolver->finishInit();
+
   // make SMT solver driver based on options
   if (options().smt.deepRestartMode != options::DeepRestartMode::NONE)
   {
@@ -190,12 +193,9 @@ void SolverEngine::finishInit()
         new SmtDriverSingleCall(*d_env.get(), *d_smtSolver.get()));
   }
 
-  Trace("smt-debug") << "SolverEngine::finishInit" << std::endl;
-  d_smtSolver->finishInit();
-
   // global push/pop around everything, to ensure proper destruction
   // of context-dependent data structures
-  d_ctxManager->setup();
+  d_ctxManager->setup(d_smtDriver.get());
 
   // subsolvers
   if (d_env->getOptions().smt.produceAbducts)
@@ -942,7 +942,7 @@ Node SolverEngine::simplify(const Node& t)
   finishInit();
   d_ctxManager->doPendingPops();
   // ensure we've processed assertions
-  d_smtSolver->refreshAssertions();
+  d_smtDriver->refreshAssertions();
   // Substitute out any abstract values in node.
   Node tt = d_absValues->substituteAbstractValues(t);
   // apply substitutions
@@ -1836,7 +1836,7 @@ void SolverEngine::push()
   finishInit();
   d_ctxManager->doPendingPops();
   Trace("smt") << "SMT push()" << endl;
-  d_smtSolver->refreshAssertions();
+  d_smtDriver->refreshAssertions();
   d_ctxManager->userPush();
 }
 
@@ -1873,7 +1873,7 @@ void SolverEngine::resetAssertions()
   d_smtSolver->getAssertions().getAssertionPipeline().clear();
   d_ctxManager->notifyResetAssertions();
   // push the state to maintain global context around everything
-  d_ctxManager->setup();
+  d_ctxManager->setup(d_smtDriver.get());
 
   // reset SmtSolver, which will construct a new prop engine
   d_smtSolver->resetAssertions();