From 09c6f9514b993c78c662ff6d3f46acce97286068 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 20 Oct 2021 16:07:09 -0500 Subject: [PATCH] Eliminate last static calls to rewriter from smt layer (#7355) --- src/proof/proof_node_manager.cpp | 7 ++++--- src/proof/proof_node_manager.h | 8 +++++++- src/smt/check_models.cpp | 5 ++--- src/smt/check_models.h | 10 ++-------- src/smt/model_blocker.cpp | 2 ++ src/smt/model_blocker.h | 6 ++++-- src/smt/preprocessor.cpp | 2 +- src/smt/proof_manager.cpp | 2 +- src/smt/proof_post_processor.cpp | 2 +- src/smt/solver_engine.cpp | 8 +++++--- src/smt/sygus_solver.cpp | 2 +- src/smt/witness_form.cpp | 18 ++++++++++++------ src/smt/witness_form.h | 11 ++++++++++- 13 files changed, 52 insertions(+), 31 deletions(-) diff --git a/src/proof/proof_node_manager.cpp b/src/proof/proof_node_manager.cpp index a3ef944e0..8b4b332a1 100644 --- a/src/proof/proof_node_manager.cpp +++ b/src/proof/proof_node_manager.cpp @@ -28,7 +28,8 @@ using namespace cvc5::kind; namespace cvc5 { -ProofNodeManager::ProofNodeManager(ProofChecker* pc) : d_checker(pc) +ProofNodeManager::ProofNodeManager(theory::Rewriter* rr, ProofChecker* pc) + : d_rewriter(rr), d_checker(pc) { d_true = NodeManager::currentNM()->mkConst(true); // we always allocate a proof checker, regardless of the proof checking mode @@ -160,14 +161,14 @@ std::shared_ptr ProofNodeManager::mkScope( computedAcr = true; for (const Node& acc : ac) { - Node accr = theory::Rewriter::rewrite(acc); + Node accr = d_rewriter->rewrite(acc); if (accr != acc) { acr[accr] = acc; } } } - Node ar = theory::Rewriter::rewrite(a); + Node ar = d_rewriter->rewrite(a); std::unordered_map::iterator itr = acr.find(ar); if (itr != acr.end()) { diff --git a/src/proof/proof_node_manager.h b/src/proof/proof_node_manager.h index 928aabb76..533f6d173 100644 --- a/src/proof/proof_node_manager.h +++ b/src/proof/proof_node_manager.h @@ -28,6 +28,10 @@ namespace cvc5 { class ProofChecker; class ProofNode; +namespace theory { +class Rewriter; +} + /** * A manager for proof node objects. This is a trusted interface for creating * and updating ProofNode objects. @@ -54,7 +58,7 @@ class ProofNode; class ProofNodeManager { public: - ProofNodeManager(ProofChecker* pc = nullptr); + ProofNodeManager(theory::Rewriter* rr, ProofChecker* pc = nullptr); ~ProofNodeManager() {} /** * This constructs a ProofNode with the given arguments. The expected @@ -184,6 +188,8 @@ class ProofNodeManager static ProofNode* cancelDoubleSymm(ProofNode* pn); private: + /** The rewriter */ + theory::Rewriter* d_rewriter; /** The (optional) proof checker */ ProofChecker* d_checker; /** the true node */ diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp index f148d1018..36d107429 100644 --- a/src/smt/check_models.cpp +++ b/src/smt/check_models.cpp @@ -31,8 +31,7 @@ using namespace cvc5::theory; namespace cvc5 { namespace smt { -CheckModels::CheckModels(Env& e) : d_env(e) {} -CheckModels::~CheckModels() {} +CheckModels::CheckModels(Env& e) : EnvObj(e) {} void CheckModels::checkModel(TheoryModel* m, const context::CDList& al, @@ -71,7 +70,7 @@ void CheckModels::checkModel(TheoryModel* m, Notice() << "SolverEngine::checkModel(): -- substitutes to " << n << std::endl; - n = Rewriter::rewrite(n); + n = rewrite(n); Notice() << "SolverEngine::checkModel(): -- rewrites to " << n << std::endl; // We look up the value before simplifying. If n contains quantifiers, diff --git a/src/smt/check_models.h b/src/smt/check_models.h index d785b53d5..2b3447010 100644 --- a/src/smt/check_models.h +++ b/src/smt/check_models.h @@ -20,11 +20,10 @@ #include "context/cdlist.h" #include "expr/node.h" +#include "smt/env_obj.h" namespace cvc5 { -class Env; - namespace theory { class TheoryModel; } @@ -34,11 +33,10 @@ namespace smt { /** * This utility is responsible for checking the current model. */ -class CheckModels +class CheckModels : protected EnvObj { public: CheckModels(Env& e); - ~CheckModels(); /** * Check model m against the current set of input assertions al. * @@ -48,10 +46,6 @@ class CheckModels void checkModel(theory::TheoryModel* m, const context::CDList& al, bool hardFailure); - - private: - /** Reference to the environment */ - Env& d_env; }; } // namespace smt diff --git a/src/smt/model_blocker.cpp b/src/smt/model_blocker.cpp index cbc388331..e8c1ff07f 100644 --- a/src/smt/model_blocker.cpp +++ b/src/smt/model_blocker.cpp @@ -25,6 +25,8 @@ using namespace cvc5::kind; namespace cvc5 { +ModelBlocker::ModelBlocker(Env& e) : EnvObj(e) {} + Node ModelBlocker::getModelBlocker(const std::vector& assertions, theory::TheoryModel* m, options::BlockModelsMode mode, diff --git a/src/smt/model_blocker.h b/src/smt/model_blocker.h index 42219e220..5e41de6a3 100644 --- a/src/smt/model_blocker.h +++ b/src/smt/model_blocker.h @@ -22,6 +22,7 @@ #include "expr/node.h" #include "options/smt_options.h" +#include "smt/env_obj.h" namespace cvc5 { @@ -32,9 +33,10 @@ class TheoryModel; /** * A utility for blocking the current model. */ -class ModelBlocker +class ModelBlocker : protected EnvObj { public: + ModelBlocker(Env& e); /** get model blocker * * This returns a disjunction of literals ~L1 V ... V ~Ln with the following @@ -63,7 +65,7 @@ class ModelBlocker * our input. In other words, we do not return ~(x < 0) V ~(w < 0) since the * left disjunct is always false. */ - static Node getModelBlocker( + Node getModelBlocker( const std::vector& assertions, theory::TheoryModel* m, options::BlockModelsMode mode, diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp index 4b16b9391..3aed58b30 100644 --- a/src/smt/preprocessor.cpp +++ b/src/smt/preprocessor.cpp @@ -150,7 +150,7 @@ Node Preprocessor::simplify(const Node& node) d_env.getPrinter().toStreamCmdSimplify(d_env.getDumpOut(), node); } Node ret = expandDefinitions(node); - ret = theory::Rewriter::rewrite(ret); + ret = rewrite(ret); return ret; } diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index 2e08ab2df..4b4291075 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -41,7 +41,7 @@ PfManager::PfManager(Env& env) d_pchecker(new ProofChecker( options().proof.proofCheck == options::ProofCheckMode::EAGER, options().proof.proofPedantic)), - d_pnm(new ProofNodeManager(d_pchecker.get())), + d_pnm(new ProofNodeManager(env.getRewriter(), d_pchecker.get())), d_pppg(new PreprocessProofGenerator( d_pnm.get(), env.getUserContext(), "smt::PreprocessProofGenerator")), d_pfpp(nullptr), diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index a547c4362..04a36c1c0 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -42,7 +42,7 @@ ProofPostprocessCallback::ProofPostprocessCallback(Env& env, : d_env(env), d_pnm(env.getProofNodeManager()), d_pppg(pppg), - d_wfpm(env.getProofNodeManager()), + d_wfpm(env), d_updateScopedAssumptions(updateScopedAssumptions) { d_true = NodeManager::currentNM()->mkConst(true); diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index e928dcade..fc6ec3915 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -1081,7 +1081,7 @@ Node SolverEngine::getValue(const Node& ex) const // AJR : necessary? if (!n.getType().isFunction()) { - n = Rewriter::rewrite(n); + n = d_env->getRewriter()->rewrite(n); } Trace("smt") << "--- getting value of " << n << endl; @@ -1224,7 +1224,8 @@ Result SolverEngine::blockModel() // get expanded assertions std::vector eassertsProc = getExpandedAssertions(); - Node eblocker = ModelBlocker::getModelBlocker( + ModelBlocker mb(*d_env.get()); + Node eblocker = mb.getModelBlocker( eassertsProc, m, d_env->getOptions().smt.blockModelsMode); Trace("smt") << "Block formula: " << eblocker << std::endl; return assertFormula(eblocker); @@ -1247,7 +1248,8 @@ Result SolverEngine::blockModelValues(const std::vector& exprs) // get expanded assertions std::vector eassertsProc = getExpandedAssertions(); // we always do block model values mode here - Node eblocker = ModelBlocker::getModelBlocker( + ModelBlocker mb(*d_env.get()); + Node eblocker = mb.getModelBlocker( eassertsProc, m, options::BlockModelsMode::VALUES, exprs); return assertFormula(eblocker); } diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp index 2a1d4e6c6..5db9804c6 100644 --- a/src/smt/sygus_solver.cpp +++ b/src/smt/sygus_solver.cpp @@ -377,7 +377,7 @@ void SygusSolver::checkSynthSolution(Assertions& as) // problem are rewritten to true. If this is not the case, then the // assertions module of the subsolver will complain about assertions // with free variables. - Node ar = theory::Rewriter::rewrite(a); + Node ar = rewrite(a); solChecker->assertFormula(ar); } Result r = solChecker->checkSat(); diff --git a/src/smt/witness_form.cpp b/src/smt/witness_form.cpp index 8e998b9cf..16d297495 100644 --- a/src/smt/witness_form.cpp +++ b/src/smt/witness_form.cpp @@ -16,21 +16,27 @@ #include "smt/witness_form.h" #include "expr/skolem_manager.h" +#include "smt/env.h" #include "theory/rewriter.h" namespace cvc5 { namespace smt { -WitnessFormGenerator::WitnessFormGenerator(ProofNodeManager* pnm) - : d_tcpg(pnm, +WitnessFormGenerator::WitnessFormGenerator(Env& env) + : d_rewriter(env.getRewriter()), + d_tcpg(env.getProofNodeManager(), nullptr, TConvPolicy::FIXPOINT, TConvCachePolicy::NEVER, "WfGenerator::TConvProofGenerator", nullptr, true), - d_wintroPf(pnm, nullptr, nullptr, "WfGenerator::LazyCDProof"), - d_pskPf(pnm, nullptr, "WfGenerator::PurifySkolemProof") + d_wintroPf(env.getProofNodeManager(), + nullptr, + nullptr, + "WfGenerator::LazyCDProof"), + d_pskPf( + env.getProofNodeManager(), nullptr, "WfGenerator::PurifySkolemProof") { } @@ -114,12 +120,12 @@ Node WitnessFormGenerator::convertToWitnessForm(Node t) bool WitnessFormGenerator::requiresWitnessFormTransform(Node t, Node s) const { - return theory::Rewriter::rewrite(t) != theory::Rewriter::rewrite(s); + return d_rewriter->rewrite(t) != d_rewriter->rewrite(s); } bool WitnessFormGenerator::requiresWitnessFormIntro(Node t) const { - Node tr = theory::Rewriter::rewrite(t); + Node tr = d_rewriter->rewrite(t); return !tr.isConst() || !tr.getConst(); } diff --git a/src/smt/witness_form.h b/src/smt/witness_form.h index 8522d41f0..06d60c1ed 100644 --- a/src/smt/witness_form.h +++ b/src/smt/witness_form.h @@ -25,6 +25,13 @@ #include "proof/proof_generator.h" namespace cvc5 { + +class Env; + +namespace theory { +class Rewriter; +} + namespace smt { /** @@ -37,7 +44,7 @@ namespace smt { class WitnessFormGenerator : public ProofGenerator { public: - WitnessFormGenerator(ProofNodeManager* pnm); + WitnessFormGenerator(Env& env); ~WitnessFormGenerator() {} /** * Get proof for, which expects an equality of the form t = toWitness(t). @@ -85,6 +92,8 @@ class WitnessFormGenerator : public ProofGenerator * Return a proof generator that can prove the given axiom exists. */ ProofGenerator* convertExistsInternal(Node exists); + /** The rewriter we are using */ + theory::Rewriter* d_rewriter; /** The term conversion proof generator */ TConvProofGenerator d_tcpg; /** The nodes we have already added rewrite steps for in d_tcpg */ -- 2.30.2