From 77415ff440424e1071c538f13ec1684feffad7d6 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 7 Dec 2021 08:56:12 -0600 Subject: [PATCH] Eliminate more static calls to Rewriter::rewrite (#7740) --- src/preprocessing/passes/apply_substs.cpp | 5 +++-- src/preprocessing/passes/non_clausal_simp.cpp | 14 ++++++++------ src/smt/abduction_solver.cpp | 1 + src/smt/check_models.cpp | 2 +- src/smt/interpolation_solver.cpp | 1 + src/smt/preprocessor.cpp | 4 ++-- src/smt/solver_engine.cpp | 2 +- .../quantifiers/cegqi/inst_strategy_cegqi.cpp | 2 +- src/theory/quantifiers/cegqi/vts_term_cache.cpp | 5 +++-- src/theory/quantifiers/cegqi/vts_term_cache.h | 6 ++++-- src/theory/quantifiers/quantifiers_rewriter.cpp | 6 ++---- src/theory/quantifiers/single_inv_partition.cpp | 3 --- src/theory/quantifiers/skolemize.cpp | 1 - src/theory/quantifiers/sygus/sygus_abduct.cpp | 3 --- src/theory/substitutions.cpp | 8 ++++---- src/theory/substitutions.h | 11 +++++++---- src/theory/theory_model.cpp | 1 + src/theory/trust_substitutions.cpp | 8 ++++---- src/theory/trust_substitutions.h | 7 ++++--- 19 files changed, 47 insertions(+), 43 deletions(-) diff --git a/src/preprocessing/passes/apply_substs.cpp b/src/preprocessing/passes/apply_substs.cpp index 99bded47a..82122fa7f 100644 --- a/src/preprocessing/passes/apply_substs.cpp +++ b/src/preprocessing/passes/apply_substs.cpp @@ -21,7 +21,7 @@ #include "context/cdo.h" #include "preprocessing/assertion_pipeline.h" #include "preprocessing/preprocessing_pass_context.h" -#include "theory/rewriter.h" +#include "smt/env.h" #include "theory/substitutions.h" namespace cvc5 { @@ -55,7 +55,8 @@ PreprocessingPassResult ApplySubsts::applyInternal( << std::endl; d_preprocContext->spendResource(Resource::PreprocessStep); assertionsToPreprocess->replaceTrusted( - i, tlsm.applyTrusted((*assertionsToPreprocess)[i])); + i, + tlsm.applyTrusted((*assertionsToPreprocess)[i], d_env.getRewriter())); Trace("apply-substs") << " got " << (*assertionsToPreprocess)[i] << std::endl; } diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp index 4bf29157e..247a8b72e 100644 --- a/src/preprocessing/passes/non_clausal_simp.cpp +++ b/src/preprocessing/passes/non_clausal_simp.cpp @@ -120,6 +120,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal( << " learned literals." << std::endl; // No conflict, go through the literals and solve them context::Context* u = userContext(); + Rewriter* rw = d_env.getRewriter(); TrustSubstitutionMap& ttls = d_preprocContext->getTopLevelSubstitutions(); CVC5_UNUSED SubstitutionMap& top_level_substs = ttls.get(); // constant propagations @@ -228,7 +229,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal( c = learnedLiteral[1]; } Assert(!t.isConst()); - Assert(cps.apply(t, true) == t); + Assert(rewrite(cps.apply(t)) == t); Assert(top_level_substs.apply(t) == t); Assert(nss.apply(t) == t); // also add to learned literal @@ -293,7 +294,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal( for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i) { Node assertion = (*assertionsToPreprocess)[i]; - TrustNode assertionNew = newSubstitutions->applyTrusted(assertion); + TrustNode assertionNew = newSubstitutions->applyTrusted(assertion, rw); Trace("non-clausal-simplify") << "assertion = " << assertion << std::endl; if (!assertionNew.isNull()) { @@ -305,7 +306,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal( } for (;;) { - assertionNew = constantPropagations->applyTrusted(assertion); + assertionNew = constantPropagations->applyTrusted(assertion, rw); if (assertionNew.isNull()) { break; @@ -340,7 +341,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal( if (d_preprocContext->getSymsInAssertions().contains(lhs)) { // if it has, the substitution becomes an assertion - TrustNode trhs = newSubstitutions->applyTrusted(lhs); + TrustNode trhs = newSubstitutions->applyTrusted(lhs, rw); Assert(!trhs.isNull()); Trace("non-clausal-simplify") << "substitute: will notify SAT layer of substitution: " @@ -446,10 +447,11 @@ Node NonClausalSimp::processLearnedLit(Node lit, theory::TrustSubstitutionMap* subs, theory::TrustSubstitutionMap* cp) { + Rewriter* rw = d_env.getRewriter(); TrustNode tlit; if (subs != nullptr) { - tlit = subs->applyTrusted(lit); + tlit = subs->applyTrusted(lit, rw); if (!tlit.isNull()) { lit = processRewrittenLearnedLit(tlit); @@ -462,7 +464,7 @@ Node NonClausalSimp::processLearnedLit(Node lit, { for (;;) { - tlit = cp->applyTrusted(lit); + tlit = cp->applyTrusted(lit, rw); if (tlit.isNull()) { break; diff --git a/src/smt/abduction_solver.cpp b/src/smt/abduction_solver.cpp index ce11c5718..063ffe09b 100644 --- a/src/smt/abduction_solver.cpp +++ b/src/smt/abduction_solver.cpp @@ -50,6 +50,7 @@ bool AbductionSolver::getAbduct(const std::vector& axioms, std::vector asserts(axioms.begin(), axioms.end()); // must expand definitions Node conjn = d_env.getTopLevelSubstitutions().apply(goal); + conjn = rewrite(conjn); // now negate conjn = conjn.negate(); d_abdConj = conjn; diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp index 7d546eae7..f3393caae 100644 --- a/src/smt/check_models.cpp +++ b/src/smt/check_models.cpp @@ -71,7 +71,7 @@ void CheckModels::checkModel(TheoryModel* m, // evaluate e.g. divide-by-zero. This is intentional since the evaluation // is not trustworthy, since the UF introduced by expanding definitions may // not be properly constrained. - Node n = sm.apply(assertion, false); + Node n = sm.apply(assertion); verbose(1) << "SolverEngine::checkModel(): -- substitutes to " << n << std::endl; diff --git a/src/smt/interpolation_solver.cpp b/src/smt/interpolation_solver.cpp index 36f8e2a8d..20be53e85 100644 --- a/src/smt/interpolation_solver.cpp +++ b/src/smt/interpolation_solver.cpp @@ -51,6 +51,7 @@ bool InterpolationSolver::getInterpol(const std::vector& axioms, << std::endl; // must expand definitions Node conjn = d_env.getTopLevelSubstitutions().apply(conj); + conjn = rewrite(conjn); std::string name("__internal_interpol"); quantifiers::SygusInterpol interpolSolver(d_env); diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp index 41653b6ee..0fdb569c8 100644 --- a/src/smt/preprocessor.cpp +++ b/src/smt/preprocessor.cpp @@ -125,8 +125,8 @@ Node Preprocessor::expandDefinitions(const Node& node, // Ensure node is type-checked at this point. n.getType(true); } - // we apply substitutions here, before expanding definitions - n = d_env.getTopLevelSubstitutions().apply(n, false); + // apply substitutions here (without rewriting), before expanding definitions + n = d_env.getTopLevelSubstitutions().apply(n); // now call expand definitions n = d_exDefs.expandDefinitions(n, cache); return n; diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index 2cf4862a9..52fdaf74b 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -1386,7 +1386,7 @@ void SolverEngine::checkUnsatCore() theory::TrustSubstitutionMap& tls = d_env->getTopLevelSubstitutions(); for (UnsatCore::iterator i = core.begin(); i != core.end(); ++i) { - Node assertionAfterExpansion = tls.apply(*i, false); + Node assertionAfterExpansion = tls.apply(*i); d_env->verbose(1) << "SolverEngine::checkUnsatCore(): pushing core member " << *i << ", expanded to " << assertionAfterExpansion << std::endl; diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 65ad79e29..e08f89218 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -56,7 +56,7 @@ InstStrategyCegqi::InstStrategyCegqi(Env& env, d_cbqi_set_quant_inactive(false), d_incomplete_check(false), d_added_cbqi_lemma(userContext()), - d_vtsCache(new VtsTermCache(qim)), + d_vtsCache(new VtsTermCache(env, qim)), d_bv_invert(nullptr), d_small_const_multiplier(NodeManager::currentNM()->mkConst( CONST_RATIONAL, Rational(1) / Rational(1000000))), diff --git a/src/theory/quantifiers/cegqi/vts_term_cache.cpp b/src/theory/quantifiers/cegqi/vts_term_cache.cpp index 37ded9b7f..f405da345 100644 --- a/src/theory/quantifiers/cegqi/vts_term_cache.cpp +++ b/src/theory/quantifiers/cegqi/vts_term_cache.cpp @@ -28,7 +28,8 @@ namespace cvc5 { namespace theory { namespace quantifiers { -VtsTermCache::VtsTermCache(QuantifiersInferenceManager& qim) : d_qim(qim) +VtsTermCache::VtsTermCache(Env& env, QuantifiersInferenceManager& qim) + : EnvObj(env), d_qim(qim) { d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0)); } @@ -155,7 +156,7 @@ Node VtsTermCache::rewriteVtsSymbols(Node n) subs_lhs.end(), subs_rhs.begin(), subs_rhs.end()); - n = Rewriter::rewrite(n); + n = rewrite(n); // may have cancelled if (!expr::hasSubterm(n, rew_vts_inf)) { diff --git a/src/theory/quantifiers/cegqi/vts_term_cache.h b/src/theory/quantifiers/cegqi/vts_term_cache.h index d3a6558cf..60c8f28f3 100644 --- a/src/theory/quantifiers/cegqi/vts_term_cache.h +++ b/src/theory/quantifiers/cegqi/vts_term_cache.h @@ -19,8 +19,10 @@ #define CVC5__THEORY__QUANTIFIERS__CEGQI__VTS_TERM_CACHE_H #include + #include "expr/attribute.h" #include "expr/node.h" +#include "smt/env_obj.h" namespace cvc5 { namespace theory { @@ -68,10 +70,10 @@ class QuantifiersInferenceManager; * that combine instantiating quantified formulas with nested quantifiers * with terms containing virtual terms. */ -class VtsTermCache +class VtsTermCache : protected EnvObj { public: - VtsTermCache(QuantifiersInferenceManager& qim); + VtsTermCache(Env& env, QuantifiersInferenceManager& qim); ~VtsTermCache() {} /** * Get vts delta. The argument isFree indicates if we are getting the diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index c38d0aa91..ba10a2efc 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -443,7 +443,7 @@ Node QuantifiersRewriter::computeProcessTerms(Node body, { Node r = computeProcessTerms2(fbody, cache, new_vars, new_conds); Assert(new_vars.size() == h.getNumChildren()); - return Rewriter::rewrite(NodeManager::currentNM()->mkNode(EQUAL, h, r)); + return NodeManager::currentNM()->mkNode(EQUAL, h, r); } // It can happen that we can't infer the shape of the function definition, // for example: forall xy. f( x, y ) = 1 + f( x, y ), this is rewritten to @@ -1028,12 +1028,11 @@ bool QuantifiersRewriter::getVarElimInternal(Node body, std::vector& subs) const { Kind nk = n.getKind(); - if (nk == NOT) + while (nk == NOT) { n = n[0]; pol = !pol; nk = n.getKind(); - Assert(nk != NOT); } if ((nk == AND && pol) || (nk == OR && !pol)) { @@ -1326,7 +1325,6 @@ Node QuantifiersRewriter::computeVarElimination(Node body, // remake with eliminated nodes body = body.substitute(vars.begin(), vars.end(), subs.begin(), subs.end()); - body = Rewriter::rewrite(body); if (!qa.d_ipl.isNull()) { qa.d_ipl = qa.d_ipl.substitute( diff --git a/src/theory/quantifiers/single_inv_partition.cpp b/src/theory/quantifiers/single_inv_partition.cpp index 73bcad535..2725e1826 100644 --- a/src/theory/quantifiers/single_inv_partition.cpp +++ b/src/theory/quantifiers/single_inv_partition.cpp @@ -19,7 +19,6 @@ #include "expr/node_algorithm.h" #include "expr/skolem_manager.h" #include "theory/quantifiers/term_util.h" -#include "theory/rewriter.h" using namespace cvc5; using namespace cvc5::kind; @@ -336,7 +335,6 @@ bool SingleInvocationPartition::init(std::vector& funcs, cr = cr.substitute( termsNs.begin(), termsNs.end(), subsNs.begin(), subsNs.end()); } - cr = Rewriter::rewrite(cr); Trace("si-prt") << ".....got si=" << singleInvocation << ", result : " << cr << std::endl; d_conjuncts[2].push_back(cr); @@ -349,7 +347,6 @@ bool SingleInvocationPartition::init(std::vector& funcs, Assert(si_terms.size() == si_subs.size()); cr = cr.substitute( si_terms.begin(), si_terms.end(), si_subs.begin(), si_subs.end()); - cr = Rewriter::rewrite(cr); Trace("si-prt") << ".....si version=" << cr << std::endl; d_conjuncts[0].push_back(cr); } diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp index 4dea0dc22..f116b2f3c 100644 --- a/src/theory/quantifiers/skolemize.cpp +++ b/src/theory/quantifiers/skolemize.cpp @@ -309,7 +309,6 @@ Node Skolemize::mkSkolemizedBody(Node f, { Node bvl = nm->mkNode(BOUND_VAR_LIST, rem_ind_vars); nret = nm->mkNode(FORALL, bvl, nret); - nret = Rewriter::rewrite(nret); sub = nret; sub_vars.insert( sub_vars.end(), ind_var_indicies.begin() + 1, ind_var_indicies.end()); diff --git a/src/theory/quantifiers/sygus/sygus_abduct.cpp b/src/theory/quantifiers/sygus/sygus_abduct.cpp index fc7e7a1b9..3da55ff50 100644 --- a/src/theory/quantifiers/sygus/sygus_abduct.cpp +++ b/src/theory/quantifiers/sygus/sygus_abduct.cpp @@ -28,7 +28,6 @@ #include "theory/quantifiers/sygus/sygus_grammar_cons.h" #include "theory/quantifiers/sygus/sygus_utils.h" #include "theory/quantifiers/term_util.h" -#include "theory/rewriter.h" using namespace std; using namespace cvc5::kind; @@ -184,8 +183,6 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name, res = SygusUtils::mkSygusConjecture({abd}, res, {instAttr}); Trace("sygus-abduct-debug") << "...finish" << std::endl; - res = theory::Rewriter::rewrite(res); - Trace("sygus-abduct") << "Generate: " << res << std::endl; return res; diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp index 70e3deb63..f91094481 100644 --- a/src/theory/substitutions.cpp +++ b/src/theory/substitutions.cpp @@ -184,8 +184,8 @@ void SubstitutionMap::addSubstitutions(SubstitutionMap& subMap, bool invalidateC } } -Node SubstitutionMap::apply(TNode t, bool doRewrite) { - +Node SubstitutionMap::apply(TNode t, Rewriter* r) +{ Debug("substitution") << "SubstitutionMap::apply(" << t << ")" << endl; // Setup the cache @@ -199,9 +199,9 @@ Node SubstitutionMap::apply(TNode t, bool doRewrite) { Node result = internalSubstitute(t, d_substitutionCache); Debug("substitution") << "SubstitutionMap::apply(" << t << ") => " << result << endl; - if (doRewrite) + if (r != nullptr) { - result = Rewriter::rewrite(result); + result = r->rewrite(result); } return result; diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h index 1de636fb3..7a3afcb11 100644 --- a/src/theory/substitutions.h +++ b/src/theory/substitutions.h @@ -32,6 +32,8 @@ namespace cvc5 { namespace theory { +class Rewriter; + /** * The type for the Substitutions mapping output by * Theory::simplify(), TheoryEngine::simplify(), and @@ -125,16 +127,17 @@ class SubstitutionMap } /** - * Apply the substitutions to the node. + * Apply the substitutions to the node, optionally rewrite if a non-null + * Rewriter pointer is passed. */ - Node apply(TNode t, bool doRewrite = false); + Node apply(TNode t, Rewriter* r = nullptr); /** * Apply the substitutions to the node. */ - Node apply(TNode t, bool doRewrite = false) const + Node apply(TNode t, Rewriter* r = nullptr) const { - return const_cast(this)->apply(t, doRewrite); + return const_cast(this)->apply(t, r); } iterator begin() { return d_substitutions.begin(); } diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 079683116..33ec5b23b 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -135,6 +135,7 @@ Node TheoryModel::getValue(TNode n) const { //apply substitutions Node nn = d_env.getTopLevelSubstitutions().apply(n); + nn = rewrite(nn); Debug("model-getvalue-debug") << "[model-getvalue] getValue : substitute " << n << " to " << nn << std::endl; //get value in model nn = getModelValue(nn); diff --git a/src/theory/trust_substitutions.cpp b/src/theory/trust_substitutions.cpp index c73265095..ea87829a9 100644 --- a/src/theory/trust_substitutions.cpp +++ b/src/theory/trust_substitutions.cpp @@ -145,11 +145,11 @@ void TrustSubstitutionMap::addSubstitutions(TrustSubstitutionMap& t) } } -TrustNode TrustSubstitutionMap::applyTrusted(Node n, bool doRewrite) +TrustNode TrustSubstitutionMap::applyTrusted(Node n, Rewriter* r) { Trace("trust-subs") << "TrustSubstitutionMap::addSubstitution: apply " << n << std::endl; - Node ns = d_subs.apply(n, doRewrite); + Node ns = d_subs.apply(n, r); Trace("trust-subs") << "...subs " << ns << std::endl; if (n == ns) { @@ -172,9 +172,9 @@ TrustNode TrustSubstitutionMap::applyTrusted(Node n, bool doRewrite) return TrustNode::mkTrustRewrite(n, ns, this); } -Node TrustSubstitutionMap::apply(Node n, bool doRewrite) +Node TrustSubstitutionMap::apply(Node n, Rewriter* r) { - return d_subs.apply(n, doRewrite); + return d_subs.apply(n, r); } std::shared_ptr TrustSubstitutionMap::getProofFor(Node eq) diff --git a/src/theory/trust_substitutions.h b/src/theory/trust_substitutions.h index cc08c870d..abcf039ba 100644 --- a/src/theory/trust_substitutions.h +++ b/src/theory/trust_substitutions.h @@ -87,11 +87,12 @@ class TrustSubstitutionMap : public ProofGenerator /** * Apply substitutions in this class to node n. Returns a trust node * proving n = n*sigma, where the proof generator is provided by this class - * (when proofs are enabled). + * (when proofs are enabled). If a non-null rewriter is provided, the result + * of the substitution is rewritten. */ - TrustNode applyTrusted(Node n, bool doRewrite = true); + TrustNode applyTrusted(Node n, Rewriter* r = nullptr); /** Same as above, without proofs */ - Node apply(Node n, bool doRewrite = true); + Node apply(Node n, Rewriter* r = nullptr); /** Get the proof for formula f */ std::shared_ptr getProofFor(Node f) override; -- 2.30.2