Move preprocessor to smt solver (#7321)

This breaks the circular dependency of preprocessing pass context of solver engine.

It also moves the preprocessor to be owned by SMT solver, instead of Solver engine.

It also changes the behavior of reset assertions: now, the preprocessing pass context is reset, whereas previously it was not. I believe this is the right behavior, as it eliminates stale data (e.g. learned literals, symbols in assertion cache).

diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp
index a0d6070323887cfdd1f793f2ef843801613681b9..91f83c56e16299ea10b109ac5b47f7bf01210815 100644 (file)
--- a/src/preprocessing/preprocessing_pass_context.cpp
+++ b/src/preprocessing/preprocessing_pass_context.cpp
@@ -17,7 +17,6 @@
 
 #include "expr/node_algorithm.h"
 #include "smt/env.h"
-#include "smt/solver_engine.h"
 #include "theory/theory_engine.h"
 #include "theory/theory_model.h"
 
@@ -25,11 +24,13 @@ namespace cvc5 {
 namespace preprocessing {
 
 PreprocessingPassContext::PreprocessingPassContext(
-    SolverEngine* slv,
     Env& env,
+    TheoryEngine* te,
+    prop::PropEngine* pe,
     theory::booleans::CircuitPropagator* circuitPropagator)
     : EnvObj(env),
-      d_slv(slv),
+      d_theoryEngine(te),
+      d_propEngine(pe),
       d_circuitPropagator(circuitPropagator),
       d_llm(
           env.getTopLevelSubstitutions(), userContext(), getProofNodeManager()),
@@ -45,11 +46,11 @@ PreprocessingPassContext::getTopLevelSubstitutions() const
 
 TheoryEngine* PreprocessingPassContext::getTheoryEngine() const
 {
-  return d_slv->getTheoryEngine();
+  return d_theoryEngine;
 }
 prop::PropEngine* PreprocessingPassContext::getPropEngine() const
 {
-  return d_slv->getPropEngine();
+  return d_propEngine;
 }
 
 void PreprocessingPassContext::spendResource(Resource r)

diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h
index ec9d399208fe7dbe66feeb5969e3b292114b0f1f..fc3faa7abada04a455e841cfebe0a3e065be444c 100644 (file)
--- a/src/preprocessing/preprocessing_pass_context.h
+++ b/src/preprocessing/preprocessing_pass_context.h
@@ -31,7 +31,6 @@
 namespace cvc5 {
 
 class Env;
-class SolverEngine;
 class TheoryEngine;
 
 namespace theory::booleans {
@@ -49,8 +48,9 @@ class PreprocessingPassContext : protected EnvObj
  public:
   /** Constructor. */
   PreprocessingPassContext(
-      SolverEngine* smt,
       Env& env,
+      TheoryEngine* te,
+      prop::PropEngine* pe,
       theory::booleans::CircuitPropagator* circuitPropagator);
 
   /** Get the associated Environment. */
@@ -120,8 +120,10 @@ class PreprocessingPassContext : protected EnvObj
   ProofNodeManager* getProofNodeManager() const;
 
  private:
-  /** Pointer to the SolverEngine that this context was created in. */
-  SolverEngine* d_slv;
+  /** Pointer to the theory engine associated with this context. */
+  TheoryEngine* d_theoryEngine;
+  /** Pointer to the prop engine associated with this context. */
+  prop::PropEngine* d_propEngine;
   /** Instance of the circuit propagator */
   theory::booleans::CircuitPropagator* d_circuitPropagator;
   /**

diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp
index e66269f718d78359f2b5f4009252752cc1461afc..a4eacbfabef68ed097eab2c8ba2d0b5cef739cef 100644 (file)
--- a/src/smt/preprocessor.cpp
+++ b/src/smt/preprocessor.cpp
@@ -57,10 +57,10 @@ Preprocessor::~Preprocessor()
   }
 }
 
-void Preprocessor::finishInit(SolverEngine* slv)
+void Preprocessor::finishInit(TheoryEngine* te, prop::PropEngine* pe)
 {
-  d_ppContext.reset(
-      new preprocessing::PreprocessingPassContext(slv, d_env, &d_propagator));
+  d_ppContext.reset(new preprocessing::PreprocessingPassContext(
+      d_env, te, pe, &d_propagator));
 
   // initialize the preprocessing passes
   d_processor.finishInit(d_ppContext.get());

diff --git a/src/smt/preprocessor.h b/src/smt/preprocessor.h
index 35eb5d35af81ba9d15f613e3f6a2707c0a50c93a..b455fb3ca6f7ab71891c71bb3b95436ca1fd4a44 100644 (file)
--- a/src/smt/preprocessor.h
+++ b/src/smt/preprocessor.h
@@ -27,11 +27,15 @@
 
 namespace cvc5 {
 
-class SolverEngine;
+class TheoryEngine;
 
 namespace preprocessing {
 class PreprocessingPassContext;
 }
+namespace prop {
+class PropEngine;
+}
+
 namespace smt {
 
 class AbstractValues;
@@ -54,7 +58,7 @@ class Preprocessor : protected EnvObj
   /**
    * Finish initialization
    */
-  void finishInit(SolverEngine* slv);
+  void finishInit(TheoryEngine* te, prop::PropEngine* pe);
   /**
    * Process the assertions that have been asserted in argument as. Returns
    * true if no conflict was discovered while preprocessing them.

diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index 76059ac72b996d5b3b7be6a6cdea6724b5f40c90..f269bfb53631776f1cf308fc1d122bb2ef5084b2 100644 (file)
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -69,7 +69,7 @@ ProcessAssertions::~ProcessAssertions()
 
 void ProcessAssertions::finishInit(PreprocessingPassContext* pc)
 {
-  Assert(d_preprocessingPassContext == nullptr);
+  // note that we may be replacing a stale preprocessing pass context here
   d_preprocessingPassContext = pc;
 
   PreprocessingPassRegistry& ppReg = PreprocessingPassRegistry::getInstance();

diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index cf2ecf3871230338463da33e4fd2720b67947241..0f98c58664f7eab94fa438aede0cda6bfecb0c54 100644 (file)
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -35,11 +35,11 @@ namespace smt {
 
 SmtSolver::SmtSolver(Env& env,
                      SmtEngineState& state,
-                     Preprocessor& pp,
+                     AbstractValues& abs,
                      SmtEngineStatistics& stats)
     : d_env(env),
       d_state(state),
-      d_pp(pp),
+      d_pp(env, abs, stats),
       d_stats(stats),
       d_theoryEngine(nullptr),
       d_propEngine(nullptr)
@@ -78,6 +78,8 @@ void SmtSolver::finishInit()
   Trace("smt-debug") << "Finishing init for theory engine..." << std::endl;
   d_theoryEngine->finishInit();
   d_propEngine->finishInit();
+
+  d_pp.finishInit(d_theoryEngine.get(), d_propEngine.get());
 }
 
 void SmtSolver::resetAssertions()
@@ -93,6 +95,8 @@ void SmtSolver::resetAssertions()
   // finishInit again. In particular, TheoryEngine::finishInit does not
   // depend on knowing the associated PropEngine.
   d_propEngine->finishInit();
+  // must reset the preprocessor as well
+  d_pp.finishInit(d_theoryEngine.get(), d_propEngine.get());
 }
 
 void SmtSolver::interrupt()

diff --git a/src/smt/smt_solver.h b/src/smt/smt_solver.h
index 9baaea3024f9203ca2e60cfc1a80628695d55580..04093443eeee398bdecf9e48a817f570365a311a 100644 (file)
--- a/src/smt/smt_solver.h
+++ b/src/smt/smt_solver.h
@@ -21,6 +21,7 @@
 #include <vector>
 
 #include "expr/node.h"
+#include "smt/preprocessor.h"
 #include "theory/logic_info.h"
 #include "util/result.h"
 
@@ -44,7 +45,6 @@ namespace smt {
 
 class Assertions;
 class SmtEngineState;
-class Preprocessor;
 struct SmtEngineStatistics;
 
 /**
@@ -66,7 +66,7 @@ class SmtSolver
  public:
   SmtSolver(Env& env,
             SmtEngineState& state,
-            Preprocessor& pp,
+            AbstractValues& abs,
             SmtEngineStatistics& stats);
   ~SmtSolver();
   /**
@@ -128,8 +128,8 @@ class SmtSolver
   Env& d_env;
   /** Reference to the state of the SolverEngine */
   SmtEngineState& d_state;
-  /** Reference to the preprocessor of SolverEngine */
-  Preprocessor& d_pp;
+  /** The preprocessor of this SMT solver */
+  Preprocessor d_pp;
   /** Reference to the statistics of SolverEngine */
   SmtEngineStatistics& d_stats;
   /** The theory engine */

diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp
index b458c421f1e6704c660857f3242e7400cd82fe20..52f47f037294da7cb70c94a588095e89dac9f355 100644 (file)
--- a/src/smt/solver_engine.cpp
+++ b/src/smt/solver_engine.cpp
@@ -102,7 +102,6 @@ SolverEngine::SolverEngine(NodeManager* nm, const Options* optr)
       d_isInternalSubsolver(false),
       d_stats(nullptr),
       d_outMgr(this),
-      d_pp(nullptr),
       d_scope(nullptr)
 {
   // !!!!!!!!!!!!!!!!!!!!!! temporary hack: this makes the current SolverEngine
@@ -123,12 +122,10 @@ SolverEngine::SolverEngine(NodeManager* nm, const Options* optr)
   getResourceManager()->registerListener(d_routListener.get());
   // make statistics
   d_stats.reset(new SmtEngineStatistics());
-  // reset the preprocessor
-  d_pp.reset(new smt::Preprocessor(*d_env, *d_absValues, *d_stats));
   // make the SMT solver
-  d_smtSolver.reset(new SmtSolver(*d_env, *d_state, *d_pp, *d_stats));
+  d_smtSolver.reset(new SmtSolver(*d_env, *d_state, *d_absValues, *d_stats));
   // make the SyGuS solver
-  d_sygusSolver.reset(new SygusSolver(*d_env.get(), *d_smtSolver, *d_pp));
+  d_sygusSolver.reset(new SygusSolver(*d_env.get(), *d_smtSolver));
   // make the quantifier elimination solver
   d_quantElimSolver.reset(new QuantElimSolver(*d_env.get(), *d_smtSolver));
 }
@@ -204,7 +201,7 @@ void SolverEngine::finishInit()
     // enable it in the assertions pipeline
     d_asserts->setProofGenerator(pppg);
     // enabled proofs in the preprocessor
-    d_pp->setProofGenerator(pppg);
+    d_smtSolver->getPreprocessor()->setProofGenerator(pppg);
   }
 
   Trace("smt-debug") << "SolverEngine::finishInit" << std::endl;
@@ -257,8 +254,6 @@ void SolverEngine::finishInit()
     d_interpolSolver.reset(new InterpolationSolver(*d_env));
   }
 
-  d_pp->finishInit(this);
-
   AlwaysAssert(getPropEngine()->getAssertionLevel() == 0)
       << "The PropEngine has pushed but the SolverEngine "
          "hasn't finished initializing!";
@@ -292,7 +287,7 @@ SolverEngine::~SolverEngine()
     d_state->cleanup();
 
     // destroy all passes before destroying things that they refer to
-    d_pp->cleanup();
+    d_smtSolver->getPreprocessor()->cleanup();
 
     d_pfManager.reset(nullptr);
     d_ucManager.reset(nullptr);
@@ -310,7 +305,6 @@ SolverEngine::~SolverEngine()
     getNodeManager()->unsubscribeEvents(d_snmListener.get());
     d_snmListener.reset(nullptr);
     d_routListener.reset(nullptr);
-    d_pp.reset(nullptr);
     // destroy the state
     d_state.reset(nullptr);
     // destroy the environment
@@ -1050,7 +1044,7 @@ Node SolverEngine::simplify(const Node& ex)
   d_state->doPendingPops();
   // ensure we've processed assertions
   d_smtSolver->processAssertions(*d_asserts);
-  return d_pp->simplify(ex);
+  return d_smtSolver->getPreprocessor()->simplify(ex);
 }
 
 Node SolverEngine::expandDefinitions(const Node& ex)
@@ -1059,7 +1053,7 @@ Node SolverEngine::expandDefinitions(const Node& ex)
   SmtScope smts(this);
   finishInit();
   d_state->doPendingPops();
-  return d_pp->expandDefinitions(ex);
+  return d_smtSolver->getPreprocessor()->expandDefinitions(ex);
 }
 
 // TODO(#1108): Simplify the error reporting of this method.
@@ -1075,7 +1069,7 @@ Node SolverEngine::getValue(const Node& ex) const
   TypeNode expectedType = ex.getType();
 
   // Substitute out any abstract values in ex and expand
-  Node n = d_pp->expandDefinitions(ex);
+  Node n = d_smtSolver->getPreprocessor()->expandDefinitions(ex);
 
   Trace("smt") << "--- getting value of " << n << endl;
   // There are two ways model values for terms are computed (for historical
@@ -1155,7 +1149,7 @@ bool SolverEngine::isModelCoreSymbol(Node n)
     // we get the assertions using the getAssertionsInternal, which does not
     // impact whether we are in "sat" mode
     std::vector<Node> asserts = getAssertionsInternal();
-    d_pp->expandDefinitions(asserts);
+    d_smtSolver->getPreprocessor()->expandDefinitions(asserts);
     ModelCoreBuilder mcb(*d_env.get());
     mcb.setModelCore(asserts, tm, opts.smt.modelCoresMode);
   }
@@ -1296,7 +1290,7 @@ std::vector<Node> SolverEngine::getExpandedAssertions()
 {
   std::vector<Node> easserts = getAssertions();
   // must expand definitions
-  d_pp->expandDefinitions(easserts);
+  d_smtSolver->getPreprocessor()->expandDefinitions(easserts);
   return easserts;
 }
 Env& SolverEngine::getEnv() { return *d_env.get(); }
@@ -1846,7 +1840,7 @@ void SolverEngine::pop()
   // Clear out assertion queues etc., in case anything is still in there
   d_asserts->clearCurrent();
   // clear the learned literals from the preprocessor
-  d_pp->clearLearnedLiterals();
+  d_smtSolver->getPreprocessor()->clearLearnedLiterals();
 
   Trace("userpushpop") << "SolverEngine: popped to level "
                        << getUserContext()->getLevel() << endl;

diff --git a/src/smt/solver_engine.h b/src/smt/solver_engine.h
index 2a922914e53918827a678fe473c16465b083e952..0cb83cb0b6bfcc6f22fc372d7224e00cc4407a44 100644 (file)
--- a/src/smt/solver_engine.h
+++ b/src/smt/solver_engine.h
@@ -1106,10 +1106,6 @@ class CVC5_EXPORT SolverEngine
 
   /** the output manager for commands */
   mutable OutputManager d_outMgr;
-  /**
-   * The preprocessor.
-   */
-  std::unique_ptr<smt::Preprocessor> d_pp;
   /**
    * The global scope object. Upon creation of this SolverEngine, it becomes the
    * SolverEngine in scope. It says the SolverEngine in scope until it is

diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp
index ce98b820d1dde45bfef2164465af7eed185a39c5..65ede41b86b86d135d2574e384074743289b82f5 100644 (file)
--- a/src/smt/sygus_solver.cpp
+++ b/src/smt/sygus_solver.cpp
@@ -41,11 +41,8 @@ using namespace cvc5::kind;
 namespace cvc5 {
 namespace smt {
 
-SygusSolver::SygusSolver(Env& env, SmtSolver& sms, Preprocessor& pp)
-    : EnvObj(env),
-      d_smtSolver(sms),
-      d_pp(pp),
-      d_sygusConjectureStale(userContext(), true)
+SygusSolver::SygusSolver(Env& env, SmtSolver& sms)
+    : EnvObj(env), d_smtSolver(sms), d_sygusConjectureStale(userContext(), true)
 {
 }
 
@@ -315,7 +312,7 @@ void SygusSolver::checkSynthSolution(Assertions& as)
              << assertion << std::endl;
     Trace("check-synth-sol") << "Retrieving assertion " << assertion << "\n";
     // Apply any define-funs from the problem.
-    Node n = d_pp.expandDefinitions(assertion, cache);
+    Node n = d_smtSolver.getPreprocessor()->expandDefinitions(assertion, cache);
     Notice() << "SygusSolver::checkSynthSolution(): -- expands to " << n
              << std::endl;
     Trace("check-synth-sol") << "Expanded assertion " << n << "\n";
@@ -435,7 +432,9 @@ void SygusSolver::expandDefinitionsSygusDt(TypeNode tn) const
       // ensures we don't try to expand e.g. bitvector extract operators,
       // whose type is undefined, and thus should not be passed to
       // expandDefinitions.
-      Node eop = op.isConst() ? op : d_pp.expandDefinitions(op);
+      Node eop = op.isConst()
+                     ? op
+                     : d_smtSolver.getPreprocessor()->expandDefinitions(op);
       datatypes::utils::setExpandedDefinitionForm(op, eop);
       // also must consider the arguments
       for (unsigned j = 0, nargs = c->getNumArgs(); j < nargs; ++j)

diff --git a/src/smt/sygus_solver.h b/src/smt/sygus_solver.h
index aa0355fb83ff3df9d8d1fbdfd50c8328af30272f..0c742fbd408118a422ee646584509d0be110b4a8 100644 (file)
--- a/src/smt/sygus_solver.h
+++ b/src/smt/sygus_solver.h
@@ -31,7 +31,6 @@ class OutputManager;
 
 namespace smt {
 
-class Preprocessor;
 class SmtSolver;
 
 /**
@@ -46,7 +45,7 @@ class SmtSolver;
 class SygusSolver : protected EnvObj
 {
  public:
-  SygusSolver(Env& env, SmtSolver& sms, Preprocessor& pp);
+  SygusSolver(Env& env, SmtSolver& sms);
   ~SygusSolver();
 
   /**
@@ -173,8 +172,6 @@ class SygusSolver : protected EnvObj
   void expandDefinitionsSygusDt(TypeNode tn) const;
   /** The SMT solver, which is used during checkSynth. */
   SmtSolver& d_smtSolver;
-  /** The preprocessor, used for checkSynthSolution. */
-  Preprocessor& d_pp;
   /**
    * sygus variables declared (from "declare-var" and "declare-fun" commands)
    *

diff --git a/test/unit/preprocessing/pass_bv_gauss_white.cpp b/test/unit/preprocessing/pass_bv_gauss_white.cpp
index aef46117365e011fde3e7424cb0dfa84af1e8e6e..aca4239d561afab3e2f5f8e46b0ffe40d5994386 100644 (file)
--- a/test/unit/preprocessing/pass_bv_gauss_white.cpp
+++ b/test/unit/preprocessing/pass_bv_gauss_white.cpp
@@ -46,7 +46,10 @@ class TestPPWhiteBVGauss : public TestSmt
     TestSmt::SetUp();
 
     d_preprocContext.reset(new preprocessing::PreprocessingPassContext(
-        d_slvEngine.get(), d_slvEngine->getEnv(), nullptr));
+        d_slvEngine->getEnv(),
+        d_slvEngine->getTheoryEngine(),
+        d_slvEngine->getPropEngine(),
+        nullptr));
 
     d_bv_gauss.reset(new BVGauss(d_preprocContext.get()));