From 89641ef6aae22610cf544f1e7545178ee6418597 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 7 May 2021 14:09:58 -0500 Subject: [PATCH] Simplifications to expand definitions (#6487) This removes the expandOnly flag from expandDefinitions. The use of expandOnly = true is equivalent to applying top-level substitutions only, which should be done explicitly via Env::getTopLevelSubstitutions. It updates the trust substitutions utility to distinguish apply vs applyTrusted for convenience for this purpose. This also breaks several dependencies in e.g. expand definitions module. --- src/preprocessing/passes/apply_substs.cpp | 2 +- src/preprocessing/passes/non_clausal_simp.cpp | 18 +++--- .../preprocessing_pass_context.cpp | 4 +- src/smt/abduction_solver.cpp | 4 +- src/smt/check_models.cpp | 18 ++---- src/smt/check_models.h | 10 ++-- src/smt/expand_definitions.cpp | 54 +++++++++--------- src/smt/expand_definitions.h | 16 +----- src/smt/interpolation_solver.cpp | 4 +- src/smt/preprocessor.cpp | 25 +++------ src/smt/preprocessor.h | 8 +-- src/smt/smt_engine.cpp | 22 +++++--- src/smt/smt_engine.h | 10 +++- src/theory/datatypes/sygus_datatype_utils.cpp | 56 +------------------ src/theory/datatypes/sygus_datatype_utils.h | 5 -- .../ematching/candidate_generator.cpp | 5 +- src/theory/rewriter.cpp | 5 ++ src/theory/rewriter.h | 3 + src/theory/trust_substitutions.cpp | 7 ++- src/theory/trust_substitutions.h | 4 +- 20 files changed, 111 insertions(+), 169 deletions(-) diff --git a/src/preprocessing/passes/apply_substs.cpp b/src/preprocessing/passes/apply_substs.cpp index 20c173316..2e40cbd5b 100644 --- a/src/preprocessing/passes/apply_substs.cpp +++ b/src/preprocessing/passes/apply_substs.cpp @@ -55,7 +55,7 @@ PreprocessingPassResult ApplySubsts::applyInternal( << std::endl; d_preprocContext->spendResource(Resource::PreprocessStep); assertionsToPreprocess->replaceTrusted( - i, tlsm.apply((*assertionsToPreprocess)[i])); + i, tlsm.applyTrusted((*assertionsToPreprocess)[i])); 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 af1e09eca..2fcc6f76f 100644 --- a/src/preprocessing/passes/non_clausal_simp.cpp +++ b/src/preprocessing/passes/non_clausal_simp.cpp @@ -298,7 +298,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal( for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i) { Node assertion = (*assertionsToPreprocess)[i]; - TrustNode assertionNew = newSubstitutions->apply(assertion); + TrustNode assertionNew = newSubstitutions->applyTrusted(assertion); Trace("non-clausal-simplify") << "assertion = " << assertion << std::endl; if (!assertionNew.isNull()) { @@ -310,7 +310,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal( } for (;;) { - assertionNew = constantPropagations->apply(assertion); + assertionNew = constantPropagations->applyTrusted(assertion); if (assertionNew.isNull()) { break; @@ -332,7 +332,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal( for (SubstitutionMap::iterator pos = nss.begin(); pos != nss.end(); ++pos) { Node lhs = (*pos).first; - TrustNode trhs = newSubstitutions->apply((*pos).second); + TrustNode trhs = newSubstitutions->applyTrusted((*pos).second); Node rhs = trhs.isNull() ? (*pos).second : trhs.getNode(); // If using incremental, we must check whether this variable has occurred // before now. If it hasn't we can add this as a substitution. @@ -351,10 +351,10 @@ PreprocessingPassResult NonClausalSimp::applyInternal( Trace("non-clausal-simplify") << "substitute: will notify SAT layer of substitution: " << eq << std::endl; - trhs = newSubstitutions->apply((*pos).first); - Assert(!trhs.isNull()); - assertionsToPreprocess->addSubstitutionNode(trhs.getProven(), - trhs.getGenerator()); + trhs = newSubstitutions->applyTrusted((*pos).first); + Assert(!trhs.isNull()); + assertionsToPreprocess->addSubstitutionNode(trhs.getProven(), + trhs.getGenerator()); } } @@ -450,7 +450,7 @@ Node NonClausalSimp::processLearnedLit(Node lit, TrustNode tlit; if (subs != nullptr) { - tlit = subs->apply(lit); + tlit = subs->applyTrusted(lit); if (!tlit.isNull()) { lit = processRewrittenLearnedLit(tlit); @@ -463,7 +463,7 @@ Node NonClausalSimp::processLearnedLit(Node lit, { for (;;) { - tlit = cp->apply(lit); + tlit = cp->applyTrusted(lit); if (tlit.isNull()) { break; diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp index 99798e7d7..139fa4153 100644 --- a/src/preprocessing/preprocessing_pass_context.cpp +++ b/src/preprocessing/preprocessing_pass_context.cpp @@ -70,8 +70,8 @@ void PreprocessingPassContext::recordSymbolsInAssertions( void PreprocessingPassContext::addModelSubstitution(const Node& lhs, const Node& rhs) { - getTheoryEngine()->getModel()->addSubstitution( - lhs, d_smt->expandDefinitions(rhs, false)); + getTheoryEngine()->getModel()->addSubstitution(lhs, + d_smt->expandDefinitions(rhs)); } void PreprocessingPassContext::addSubstitution(const Node& lhs, diff --git a/src/smt/abduction_solver.cpp b/src/smt/abduction_solver.cpp index 23f46cc58..6be05c6b7 100644 --- a/src/smt/abduction_solver.cpp +++ b/src/smt/abduction_solver.cpp @@ -19,11 +19,13 @@ #include "base/modal_exception.h" #include "options/smt_options.h" +#include "smt/env.h" #include "smt/smt_engine.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/sygus/sygus_abduct.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" #include "theory/smt_engine_subsolver.h" +#include "theory/trust_substitutions.h" using namespace cvc5::theory; @@ -46,7 +48,7 @@ bool AbductionSolver::getAbduct(const Node& goal, std::vector axioms = d_parent->getExpandedAssertions(); std::vector asserts(axioms.begin(), axioms.end()); // must expand definitions - Node conjn = d_parent->expandDefinitions(goal); + Node conjn = d_parent->getEnv().getTopLevelSubstitutions().apply(goal); // now negate conjn = conjn.negate(); d_abdConj = conjn; diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp index f6d1da345..3d5429635 100644 --- a/src/smt/check_models.cpp +++ b/src/smt/check_models.cpp @@ -17,6 +17,7 @@ #include "base/modal_exception.h" #include "options/smt_options.h" +#include "smt/env.h" #include "smt/model.h" #include "smt/node_command.h" #include "smt/preprocessor.h" @@ -30,7 +31,7 @@ using namespace cvc5::theory; namespace cvc5 { namespace smt { -CheckModels::CheckModels(SmtSolver& s) : d_smt(s) {} +CheckModels::CheckModels(Env& e) : d_env(e) {} CheckModels::~CheckModels() {} void CheckModels::checkModel(Model* m, @@ -50,16 +51,7 @@ void CheckModels::checkModel(Model* m, "Cannot run check-model on a model with approximate values."); } - // Check individual theory assertions - if (options::debugCheckModels()) - { - TheoryEngine* te = d_smt.getTheoryEngine(); - Assert(te != nullptr); - te->checkTheoryAssertionsWithModel(hardFailure); - } - - Preprocessor* pp = d_smt.getPreprocessor(); - + theory::SubstitutionMap& sm = d_env.getTopLevelSubstitutions().get(); Trace("check-model") << "checkModel: Check assertions..." << std::endl; std::unordered_map cache; // the list of assertions that did not rewrite to true @@ -75,8 +67,8 @@ void CheckModels::checkModel(Model* 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 = pp->expandDefinitions(assertion, cache, true); - Notice() << "SmtEngine::checkModel(): -- expands to " << n << std::endl; + Node n = sm.apply(assertion, false); + Notice() << "SmtEngine::checkModel(): -- substitutes to " << n << std::endl; n = Rewriter::rewrite(n); Notice() << "SmtEngine::checkModel(): -- rewrites to " << n << std::endl; diff --git a/src/smt/check_models.h b/src/smt/check_models.h index 9b6780ddf..ce06bae07 100644 --- a/src/smt/check_models.h +++ b/src/smt/check_models.h @@ -22,10 +22,12 @@ #include "expr/node.h" namespace cvc5 { + +class Env; + namespace smt { class Model; -class SmtSolver; /** * This utility is responsible for checking the current model. @@ -33,7 +35,7 @@ class SmtSolver; class CheckModels { public: - CheckModels(SmtSolver& s); + CheckModels(Env& e); ~CheckModels(); /** * Check model m against the current set of input assertions al. @@ -44,8 +46,8 @@ class CheckModels void checkModel(Model* m, context::CDList* al, bool hardFailure); private: - /** Reference to the SMT solver */ - SmtSolver& d_smt; + /** Reference to the environment */ + Env& d_env; }; } // namespace smt diff --git a/src/smt/expand_definitions.cpp b/src/smt/expand_definitions.cpp index 14182a46d..349736d15 100644 --- a/src/smt/expand_definitions.cpp +++ b/src/smt/expand_definitions.cpp @@ -19,11 +19,14 @@ #include #include "expr/node_manager_attributes.h" +#include "expr/term_conversion_proof_generator.h" #include "preprocessing/assertion_pipeline.h" #include "smt/env.h" #include "smt/smt_engine.h" #include "smt/smt_engine_stats.h" -#include "theory/theory_engine.h" +#include "theory/rewriter.h" +#include "theory/theory.h" +#include "util/resource_manager.h" using namespace cvc5::preprocessing; using namespace cvc5::theory; @@ -32,26 +35,23 @@ using namespace cvc5::kind; namespace cvc5 { namespace smt { -ExpandDefs::ExpandDefs(SmtEngine& smt, Env& env, SmtEngineStatistics& stats) - : d_smt(smt), d_env(env), d_smtStats(stats), d_tpg(nullptr) +ExpandDefs::ExpandDefs(Env& env, SmtEngineStatistics& stats) + : d_env(env), d_smtStats(stats), d_tpg(nullptr) { } ExpandDefs::~ExpandDefs() {} Node ExpandDefs::expandDefinitions( - TNode n, - std::unordered_map& cache, - bool expandOnly) + TNode n, std::unordered_map& cache) { - TrustNode trn = expandDefinitions(n, cache, expandOnly, nullptr); + TrustNode trn = expandDefinitions(n, cache, nullptr); return trn.isNull() ? Node(n) : trn.getNode(); } TrustNode ExpandDefs::expandDefinitions( TNode n, std::unordered_map& cache, - bool expandOnly, TConvProofGenerator* tpg) { const TNode orig = n; @@ -62,9 +62,11 @@ TrustNode ExpandDefs::expandDefinitions( // output / rewritten node and finally a flag tracking whether the children // have been explored (i.e. if this is a downward or upward pass). + ResourceManager* rm = d_env.getResourceManager(); + Rewriter* rr = d_env.getRewriter(); do { - d_env.getResourceManager()->spendResource(Resource::PreprocessStep); + rm->spendResource(Resource::PreprocessStep); // n is the input / original // node is the output / result @@ -93,30 +95,24 @@ TrustNode ExpandDefs::expandDefinitions( result.push(ret.isNull() ? n : ret); continue; } - if (!expandOnly) - { - // do not do any theory stuff if expandOnly is true + theory::TheoryId tid = theory::Theory::theoryOf(node); + theory::TheoryRewriter* tr = rr->getTheoryRewriter(tid); - theory::Theory* t = d_smt.getTheoryEngine()->theoryOf(node); - theory::TheoryRewriter* tr = t->getTheoryRewriter(); - - Assert(t != NULL); - TrustNode trn = tr->expandDefinition(n); - if (!trn.isNull()) - { - node = trn.getNode(); - if (tpg != nullptr) - { - tpg->addRewriteStep( - n, node, trn.getGenerator(), true, PfRule::THEORY_EXPAND_DEF); - } - } - else + Assert(tr != NULL); + TrustNode trn = tr->expandDefinition(n); + if (!trn.isNull()) + { + node = trn.getNode(); + if (tpg != nullptr) { - node = n; + tpg->addRewriteStep( + n, node, trn.getGenerator(), true, PfRule::THEORY_EXPAND_DEF); } } - + else + { + node = n; + } // the partial functions can fall through, in which case we still // consider their children worklist.push(std::make_tuple( diff --git a/src/smt/expand_definitions.h b/src/smt/expand_definitions.h index d6fe8ba0d..d4e591c31 100644 --- a/src/smt/expand_definitions.h +++ b/src/smt/expand_definitions.h @@ -27,13 +27,8 @@ namespace cvc5 { class Env; class ProofNodeManager; -class SmtEngine; class TConvProofGenerator; -namespace preprocessing { -class AssertionPipeline; -} - namespace smt { struct SmtEngineStatistics; @@ -47,21 +42,17 @@ struct SmtEngineStatistics; class ExpandDefs { public: - ExpandDefs(SmtEngine& smt, Env& env, SmtEngineStatistics& stats); + ExpandDefs(Env& env, SmtEngineStatistics& stats); ~ExpandDefs(); /** * Expand definitions in term n. Return the expanded form of n. * * @param n The node to expand * @param cache Cache of previous results - * @param expandOnly if true, then the expandDefinitions function of - * TheoryEngine is not called on subterms of n. * @return The expanded term. */ Node expandDefinitions( - TNode n, - std::unordered_map& cache, - bool expandOnly = false); + TNode n, std::unordered_map& cache); /** * Set proof node manager, which signals this class to enable proofs using the @@ -77,10 +68,7 @@ class ExpandDefs theory::TrustNode expandDefinitions( TNode n, std::unordered_map& cache, - bool expandOnly, TConvProofGenerator* tpg); - /** Reference to the SMT engine */ - SmtEngine& d_smt; /** Reference to the environment. */ Env& d_env; /** Reference to the SMT stats */ diff --git a/src/smt/interpolation_solver.cpp b/src/smt/interpolation_solver.cpp index 813fc45cf..fbbdb1b90 100644 --- a/src/smt/interpolation_solver.cpp +++ b/src/smt/interpolation_solver.cpp @@ -19,11 +19,13 @@ #include "base/modal_exception.h" #include "options/smt_options.h" +#include "smt/env.h" #include "smt/smt_engine.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" #include "theory/quantifiers/sygus/sygus_interpol.h" #include "theory/smt_engine_subsolver.h" +#include "theory/trust_substitutions.h" using namespace cvc5::theory; @@ -50,7 +52,7 @@ bool InterpolationSolver::getInterpol(const Node& conj, << std::endl; std::vector axioms = d_parent->getExpandedAssertions(); // must expand definitions - Node conjn = d_parent->expandDefinitions(conj); + Node conjn = d_parent->getEnv().getTopLevelSubstitutions().apply(conj); std::string name("A"); quantifiers::SygusInterpol interpolSolver; diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp index f434e13ca..a222568d3 100644 --- a/src/smt/preprocessor.cpp +++ b/src/smt/preprocessor.cpp @@ -43,8 +43,8 @@ Preprocessor::Preprocessor(SmtEngine& smt, d_absValues(abs), d_propagator(true, true), d_assertionsProcessed(env.getUserContext(), false), - d_exDefs(smt, d_env, stats), - d_processor(smt, *smt.getResourceManager(), stats), + d_exDefs(env, stats), + d_processor(smt, *env.getResourceManager(), stats), d_pnm(nullptr) { } @@ -110,16 +110,14 @@ void Preprocessor::clearLearnedLiterals() void Preprocessor::cleanup() { d_processor.cleanup(); } -Node Preprocessor::expandDefinitions(const Node& n, bool expandOnly) +Node Preprocessor::expandDefinitions(const Node& n) { std::unordered_map cache; - return expandDefinitions(n, cache, expandOnly); + return expandDefinitions(n, cache); } Node Preprocessor::expandDefinitions( - const Node& node, - std::unordered_map& cache, - bool expandOnly) + const Node& node, std::unordered_map& cache) { Trace("smt") << "SMT expandDefinitions(" << node << ")" << endl; // Substitute out any abstract values in node. @@ -130,13 +128,9 @@ Node Preprocessor::expandDefinitions( n.getType(true); } // we apply substitutions here, before expanding definitions - theory::SubstitutionMap& sm = d_env.getTopLevelSubstitutions().get(); - n = sm.apply(n); - if (!expandOnly) - { - // expand only = true - n = d_exDefs.expandDefinitions(n, cache, expandOnly); - } + n = d_env.getTopLevelSubstitutions().apply(n, false); + // now call expand definitions + n = d_exDefs.expandDefinitions(n, cache); return n; } @@ -148,8 +142,7 @@ Node Preprocessor::simplify(const Node& node) d_smt.getOutputManager().getPrinter().toStreamCmdSimplify( d_smt.getOutputManager().getDumpOut(), node); } - std::unordered_map cache; - Node ret = expandDefinitions(node, cache, false); + Node ret = expandDefinitions(node); ret = theory::Rewriter::rewrite(ret); return ret; } diff --git a/src/smt/preprocessor.h b/src/smt/preprocessor.h index e0ad2cc14..4c60a2898 100644 --- a/src/smt/preprocessor.h +++ b/src/smt/preprocessor.h @@ -85,16 +85,12 @@ class Preprocessor * simplification or normalization is done. * * @param n The node to expand - * @param expandOnly if true, then the expandDefinitions function of - * TheoryEngine is not called on subterms of n. * @return The expanded term. */ - Node expandDefinitions(const Node& n, bool expandOnly = false); + Node expandDefinitions(const Node& n); /** Same as above, with a cache of previous results. */ Node expandDefinitions( - const Node& n, - std::unordered_map& cache, - bool expandOnly = false); + const Node& n, std::unordered_map& cache); /** * Set proof node manager. Enables proofs in this preprocessor. */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index cccb4f544..780ed78ce 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -243,7 +243,7 @@ void SmtEngine::finishInit() { d_model.reset(new Model(tm)); // make the check models utility - d_checkModels.reset(new CheckModels(*d_smtSolver.get())); + d_checkModels.reset(new CheckModels(*d_env.get())); } // global push/pop around everything, to ensure proper destruction @@ -1129,15 +1129,13 @@ Node SmtEngine::simplify(const Node& ex) return d_pp->simplify(ex); } -Node SmtEngine::expandDefinitions(const Node& ex, bool expandOnly) +Node SmtEngine::expandDefinitions(const Node& ex) { - getResourceManager()->spendResource( - Resource::PreprocessStep); - + getResourceManager()->spendResource(Resource::PreprocessStep); SmtScope smts(this); finishInit(); d_state->doPendingPops(); - return d_pp->expandDefinitions(ex, expandOnly); + return d_pp->expandDefinitions(ex); } // TODO(#1108): Simplify the error reporting of this method. @@ -1340,6 +1338,7 @@ std::vector SmtEngine::getExpandedAssertions() } return eassertsProc; } +Env& SmtEngine::getEnv() { return *d_env.get(); } void SmtEngine::declareSepHeap(TypeNode locT, TypeNode dataT) { @@ -1455,8 +1454,9 @@ void SmtEngine::checkUnsatCore() { Notice() << "SmtEngine::checkUnsatCore(): pushing core assertions" << std::endl; + theory::TrustSubstitutionMap& tls = d_env->getTopLevelSubstitutions(); for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) { - Node assertionAfterExpansion = expandDefinitions(*i); + Node assertionAfterExpansion = tls.apply(*i, false); Notice() << "SmtEngine::checkUnsatCore(): pushing core member " << *i << ", expanded to " << assertionAfterExpansion << "\n"; coreChecker->assertFormula(assertionAfterExpansion); @@ -1493,6 +1493,14 @@ void SmtEngine::checkModel(bool hardFailure) { Model* m = getAvailableModel("check model"); Assert(m != nullptr); + // check the model with the theory engine for debugging + if (options::debugCheckModels()) + { + TheoryEngine* te = getTheoryEngine(); + Assert(te != nullptr); + te->checkTheoryAssertionsWithModel(hardFailure); + } + // check the model with the check models utility Assert(d_checkModels != nullptr); d_checkModels->checkModel(m, al, hardFailure); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index a7e39e004..22316b872 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -512,12 +512,10 @@ class CVC5_EXPORT SmtEngine * Expand the definitions in a term or formula. * * @param n The node to expand - * @param expandOnly if true, then the expandDefinitions function of - * TheoryEngine is not called on subterms of n. * * @throw TypeCheckingException, LogicException, UnsafeInterruptException */ - Node expandDefinitions(const Node& n, bool expandOnly = true); + Node expandDefinitions(const Node& n); /** * Get the assigned value of an expr (only if immediately preceded by a SAT @@ -887,6 +885,12 @@ class CVC5_EXPORT SmtEngine * Return the set of assertions, after expanding definitions. */ std::vector getExpandedAssertions(); + + /** + * !!!!! temporary, until the environment is passsed to all classes that + * require it. + */ + Env& getEnv(); /* ....................................................................... */ private: /* ....................................................................... */ diff --git a/src/theory/datatypes/sygus_datatype_utils.cpp b/src/theory/datatypes/sygus_datatype_utils.cpp index 008e9c015..4b0c17bee 100644 --- a/src/theory/datatypes/sygus_datatype_utils.cpp +++ b/src/theory/datatypes/sygus_datatype_utils.cpp @@ -21,6 +21,7 @@ #include "expr/dtype_cons.h" #include "expr/node_algorithm.h" #include "expr/sygus_datatype.h" +#include "smt/env.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "theory/evaluator.h" @@ -138,60 +139,6 @@ Kind getEliminateKind(Kind ok) return nk; } -Node eliminatePartialOperators(Node n) -{ - NodeManager* nm = NodeManager::currentNM(); - std::unordered_map visited; - std::unordered_map::iterator it; - std::vector visit; - TNode cur; - visit.push_back(n); - do - { - cur = visit.back(); - visit.pop_back(); - it = visited.find(cur); - - if (it == visited.end()) - { - visited[cur] = Node::null(); - visit.push_back(cur); - for (const Node& cn : cur) - { - visit.push_back(cn); - } - } - else if (it->second.isNull()) - { - Node ret = cur; - bool childChanged = false; - std::vector children; - if (cur.getMetaKind() == metakind::PARAMETERIZED) - { - children.push_back(cur.getOperator()); - } - for (const Node& cn : cur) - { - it = visited.find(cn); - Assert(it != visited.end()); - Assert(!it->second.isNull()); - childChanged = childChanged || cn != it->second; - children.push_back(it->second); - } - Kind ok = cur.getKind(); - Kind nk = getEliminateKind(ok); - if (nk != ok || childChanged) - { - ret = nm->mkNode(nk, children); - } - visited[cur] = ret; - } - } while (!visit.empty()); - Assert(visited.find(n) != visited.end()); - Assert(!visited.find(n)->second.isNull()); - return visited[n]; -} - Node mkSygusTerm(const DType& dt, unsigned i, const std::vector& children, @@ -235,7 +182,6 @@ Node mkSygusTerm(const DType& dt, // expandDefinitions. opn = smt::currentSmtEngine()->expandDefinitions(op); opn = Rewriter::rewrite(opn); - opn = eliminatePartialOperators(opn); SygusOpRewrittenAttribute sora; op.setAttribute(sora, opn); } diff --git a/src/theory/datatypes/sygus_datatype_utils.h b/src/theory/datatypes/sygus_datatype_utils.h index 77aa7ac54..63e8a057a 100644 --- a/src/theory/datatypes/sygus_datatype_utils.h +++ b/src/theory/datatypes/sygus_datatype_utils.h @@ -86,11 +86,6 @@ Kind getOperatorKindForSygusBuiltin(Node op); * otherwise k itself. */ Kind getEliminateKind(Kind k); -/** - * Returns a version of n where all partial functions such as bvudiv - * have been replaced by their total versions like bvudiv_total. - */ -Node eliminatePartialOperators(Node n); /** make sygus term * * This function returns a builtin term f( children[0], ..., children[n] ) diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp index 93ef072fa..5295302c4 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.cpp +++ b/src/theory/quantifiers/ematching/candidate_generator.cpp @@ -289,7 +289,10 @@ CandidateGeneratorSelector::CandidateGeneratorSelector(QuantifiersState& qs, { Trace("sel-trigger") << "Selector trigger: " << mpat << std::endl; Assert(mpat.getKind() == APPLY_SELECTOR); - Node mpatExp = smt::currentSmtEngine()->expandDefinitions(mpat, false); + // NOTE: could use qs.getValuation().getPreprocessedTerm(mpat); when + // expand definitions is eliminated, however, this also requires avoiding + // term formula removal. + Node mpatExp = smt::currentSmtEngine()->expandDefinitions(mpat); Trace("sel-trigger") << "Expands to: " << mpatExp << std::endl; if (mpatExp.getKind() == ITE) { diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 5cea6592c..2b2604593 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -179,6 +179,11 @@ void Rewriter::registerPostRewriteEqual( d_postRewritersEqual[tid] = fn; } +TheoryRewriter* Rewriter::getTheoryRewriter(theory::TheoryId theoryId) +{ + return d_theoryRewriters[theoryId]; +} + Rewriter* Rewriter::getInstance() { return smt::currentSmtEngine()->getRewriter(); diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h index 3f4676fa0..b3ea3b542 100644 --- a/src/theory/rewriter.h +++ b/src/theory/rewriter.h @@ -147,6 +147,9 @@ class Rewriter { theory::TheoryId tid, std::function fn); + /** Get the theory rewriter for the given id */ + TheoryRewriter* getTheoryRewriter(theory::TheoryId theoryId); + private: /** * Get the rewriter associated with the SmtEngine in scope. diff --git a/src/theory/trust_substitutions.cpp b/src/theory/trust_substitutions.cpp index 47507bfe0..7a2fb19bd 100644 --- a/src/theory/trust_substitutions.cpp +++ b/src/theory/trust_substitutions.cpp @@ -146,7 +146,7 @@ void TrustSubstitutionMap::addSubstitutions(TrustSubstitutionMap& t) } } -TrustNode TrustSubstitutionMap::apply(Node n, bool doRewrite) +TrustNode TrustSubstitutionMap::applyTrusted(Node n, bool doRewrite) { Trace("trust-subs") << "TrustSubstitutionMap::addSubstitution: apply " << n << std::endl; @@ -169,6 +169,11 @@ TrustNode TrustSubstitutionMap::apply(Node n, bool doRewrite) return TrustNode::mkTrustRewrite(n, ns, this); } +Node TrustSubstitutionMap::apply(Node n, bool doRewrite) +{ + return d_subs.apply(n, doRewrite); +} + std::shared_ptr TrustSubstitutionMap::getProofFor(Node eq) { Assert(eq.getKind() == kind::EQUAL); diff --git a/src/theory/trust_substitutions.h b/src/theory/trust_substitutions.h index ec5b2ffb5..b7b526205 100644 --- a/src/theory/trust_substitutions.h +++ b/src/theory/trust_substitutions.h @@ -89,7 +89,9 @@ class TrustSubstitutionMap : public ProofGenerator * proving n = n*sigma, where the proof generator is provided by this class * (when proofs are enabled). */ - TrustNode apply(Node n, bool doRewrite = true); + TrustNode applyTrusted(Node n, bool doRewrite = true); + /** Same as above, without proofs */ + Node apply(Node n, bool doRewrite = true); /** Get the proof for formula f */ std::shared_ptr getProofFor(Node f) override; -- 2.30.2