From 4d8e954c952db015e28d218b4c23f038155797ad Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 7 Oct 2021 15:10:26 -0500 Subject: [PATCH] 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). --- .../preprocessing_pass_context.cpp | 11 ++++---- .../preprocessing_pass_context.h | 10 ++++--- src/smt/preprocessor.cpp | 6 ++--- src/smt/preprocessor.h | 8 ++++-- src/smt/process_assertions.cpp | 2 +- src/smt/smt_solver.cpp | 8 ++++-- src/smt/smt_solver.h | 8 +++--- src/smt/solver_engine.cpp | 26 +++++++------------ src/smt/solver_engine.h | 4 --- src/smt/sygus_solver.cpp | 13 +++++----- src/smt/sygus_solver.h | 5 +--- .../preprocessing/pass_bv_gauss_white.cpp | 5 +++- 12 files changed, 53 insertions(+), 53 deletions(-) diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp index a0d607032..91f83c56e 100644 --- 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 ec9d39920..fc3faa7ab 100644 --- 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 e66269f71..a4eacbfab 100644 --- 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 35eb5d35a..b455fb3ca 100644 --- 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 76059ac72..f269bfb53 100644 --- 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 cf2ecf387..0f98c5866 100644 --- 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 9baaea302..04093443e 100644 --- a/src/smt/smt_solver.h +++ b/src/smt/smt_solver.h @@ -21,6 +21,7 @@ #include #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 b458c421f..52f47f037 100644 --- 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 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 SolverEngine::getExpandedAssertions() { std::vector 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 2a922914e..0cb83cb0b 100644 --- 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 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 ce98b820d..65ede41b8 100644 --- 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 aa0355fb8..0c742fbd4 100644 --- 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 aef461173..aca4239d5 100644 --- 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())); -- 2.30.2