diff --git a/include/cvc5/cvc5_proof_rule.h b/include/cvc5/cvc5_proof_rule.h index 7e6a6e758bc..f377bd8ed2d 100644 --- a/include/cvc5/cvc5_proof_rule.h +++ b/include/cvc5/cvc5_proof_rule.h @@ -1142,21 +1142,6 @@ enum ENUM(ProofRule) : uint32_t * \endverbatim */ EVALUE(HO_CONG), - /** - * \verbatim embed:rst:leading-asterisk - * **Equality -- Beta reduction** - * - * .. math:: - * - * \inferrule{\mid \lambda x_1\dots x_n.\> t, t_1,\dots,t_n} - * {((\lambda x_1\dots x_n.\> t) t_1 \ldots t_n)=t\{x_1\mapsto t_1,\dots,x_n\mapsto t_n\}} - * - * The right hand side of the equality in the conclusion is computed using - * standard substitution via Node::substitute. - * \endverbatim - */ - EVALUE(BETA_REDUCE), - /** * \verbatim embed:rst:leading-asterisk * **Arrays -- Read over write** @@ -1204,19 +1189,6 @@ enum ENUM(ProofRule) : uint32_t * \endverbatim */ EVALUE(ARRAYS_EXT), - /** - * \verbatim embed:rst:leading-asterisk - * **Arrays -- Expansion of array range equality** - * - * .. math:: - * - * \inferrule{-\mid \mathit{eqrange}(a,b,i,j)} - * {\mathit{eqrange}(a,b,i,j)= - * \forall x.\> i \leq x \leq j \rightarrow - * \mathit{select}(a,x)=\mathit{select}(b,x)} - * \endverbatim - */ - EVALUE(ARRAYS_EQ_RANGE_EXPAND), /** * \verbatim embed:rst:leading-asterisk @@ -2296,6 +2268,31 @@ enum ENUM(ProofRewriteRule) : uint32_t * \endverbatim */ EVALUE(DISTINCT_ELIM), + /** + * \verbatim embed:rst:leading-asterisk + * **Equality -- Beta reduction** + * + * .. math:: + * + * ((\lambda x_1\dots x_n.\> t) t_1 \ldots t_n)=t\{x_1\mapsto + * t_1,\dots,x_n\mapsto t_n\} + * + * The right hand side of the equality in the conclusion is computed using + * standard substitution via Node::substitute. + * \endverbatim + */ + EVALUE(BETA_REDUCE), + /** + * \verbatim embed:rst:leading-asterisk + * **Arrays -- Expansion of array range equality** + * + * .. math:: + * \mathit{eqrange}(a,b,i,j)= + * \forall x.\> i \leq x \leq j \rightarrow + * \mathit{select}(a,x)=\mathit{select}(b,x) + * \endverbatim + */ + EVALUE(ARRAYS_EQ_RANGE_EXPAND), /** * \verbatim embed:rst:leading-asterisk * **Quantifiers -- Exists elimination** diff --git a/src/api/cpp/cvc5_proof_rule_template.cpp b/src/api/cpp/cvc5_proof_rule_template.cpp index d9cd839bccc..9dcba613b32 100644 --- a/src/api/cpp/cvc5_proof_rule_template.cpp +++ b/src/api/cpp/cvc5_proof_rule_template.cpp @@ -111,14 +111,12 @@ const char* toString(ProofRule rule) case ProofRule::FALSE_ELIM: return "FALSE_ELIM"; case ProofRule::HO_APP_ENCODE: return "HO_APP_ENCODE"; case ProofRule::HO_CONG: return "HO_CONG"; - case ProofRule::BETA_REDUCE: return "BETA_REDUCE"; //================================================= Array rules case ProofRule::ARRAYS_READ_OVER_WRITE: return "ARRAYS_READ_OVER_WRITE"; case ProofRule::ARRAYS_READ_OVER_WRITE_CONTRA: return "ARRAYS_READ_OVER_WRITE_CONTRA"; case ProofRule::ARRAYS_READ_OVER_WRITE_1: return "ARRAYS_READ_OVER_WRITE_1"; case ProofRule::ARRAYS_EXT: return "ARRAYS_EXT"; - case ProofRule::ARRAYS_EQ_RANGE_EXPAND: return "ARRAYS_EQ_RANGE_EXPAND"; //================================================= Bit-Vector rules case ProofRule::MACRO_BV_BITBLAST: return "MACRO_BV_BITBLAST"; case ProofRule::BV_BITBLAST_STEP: return "BV_BITBLAST_STEP"; @@ -222,6 +220,9 @@ const char* toString(cvc5::ProofRewriteRule rule) case ProofRewriteRule::NONE: return "NONE"; //================================================= ad-hoc rules case ProofRewriteRule::DISTINCT_ELIM: return "distinct-elim"; + case ProofRewriteRule::BETA_REDUCE: return "beta-reduce"; + case ProofRewriteRule::ARRAYS_EQ_RANGE_EXPAND: + return "arrays-eq-range-expand"; case ProofRewriteRule::EXISTS_ELIM: return "exists-elim"; case ProofRewriteRule::DT_COLLAPSE_SELECTOR: return "dt-collapse-selector"; case ProofRewriteRule::DT_COLLAPSE_TESTER: return "dt-collapse-tester"; diff --git a/src/proof/eager_proof_generator.cpp b/src/proof/eager_proof_generator.cpp index e6cf21d4e0d..45354e861e2 100644 --- a/src/proof/eager_proof_generator.cpp +++ b/src/proof/eager_proof_generator.cpp @@ -18,6 +18,7 @@ #include "proof/proof.h" #include "proof/proof_node.h" #include "proof/proof_node_manager.h" +#include "rewriter/rewrites.h" #include "smt/env.h" namespace cvc5::internal { @@ -125,6 +126,16 @@ TrustNode EagerProofGenerator::mkTrustNode(Node conc, return mkTrustNode(pfs->getResult(), pfs, isConflict); } +TrustNode EagerProofGenerator::mkTrustNodeRewrite(const Node& a, + const Node& b, + ProofRewriteRule id) +{ + std::vector args; + args.push_back(rewriter::mkRewriteRuleNode(id)); + args.push_back(a); + return mkTrustedRewrite(a, b, ProofRule::THEORY_REWRITE, args); +} + TrustNode EagerProofGenerator::mkTrustedRewrite(Node a, Node b, std::shared_ptr pf) diff --git a/src/proof/eager_proof_generator.h b/src/proof/eager_proof_generator.h index 329f1f1a975..51bd086e5ee 100644 --- a/src/proof/eager_proof_generator.h +++ b/src/proof/eager_proof_generator.h @@ -137,6 +137,21 @@ class EagerProofGenerator : protected EnvObj, public ProofGenerator const std::vector& exp, const std::vector& args, bool isConflict = false); + /** + * Make trust node from a single step proof of a rewrite. This is a + * convenience function that avoids the need to explictly construct ProofNode + * by the caller. + * + * @param a the original + * @param b what is rewrites to + * @param id The rewrite rule of the proof concluding conc based on rewriting + * the term a. + * @return The trust node corresponding to the fact that this generator has + * a proof of a=b. + */ + TrustNode mkTrustNodeRewrite(const Node& a, + const Node& b, + ProofRewriteRule id); /** * Make trust node: wrap `exp => n` in a trust node with this generator, and * have it store the proof `pf` too. diff --git a/src/proof/lfsc/lfsc_post_processor.cpp b/src/proof/lfsc/lfsc_post_processor.cpp index cdcd7c4066d..cd987c96e68 100644 --- a/src/proof/lfsc/lfsc_post_processor.cpp +++ b/src/proof/lfsc/lfsc_post_processor.cpp @@ -22,6 +22,7 @@ #include "proof/proof_node_algorithm.h" #include "proof/proof_node_manager.h" #include "proof/proof_node_updater.h" +#include "rewriter/rewrites.h" #include "smt/env.h" #include "theory/strings/theory_strings_utils.h" @@ -430,11 +431,20 @@ bool LfscProofPostprocessCallback::update(Node res, } } break; - case ProofRule::BETA_REDUCE: + case ProofRule::THEORY_REWRITE: { - // get the term to beta-reduce - Node termToReduce = nm->mkNode(Kind::APPLY_UF, args); - addLfscRule(cdp, res, {}, LfscRule::BETA_REDUCE, {termToReduce}); + Assert(args.size() >= 2); + ProofRewriteRule idr; + if (!rewriter::getRewriteRule(args[0], idr)) + { + return false; + } + if (idr == ProofRewriteRule::BETA_REDUCE) + { + // get the term to beta-reduce + Node termToReduce = nm->mkNode(Kind::APPLY_UF, args[1]); + addLfscRule(cdp, res, {}, LfscRule::BETA_REDUCE, {termToReduce}); + } } break; default: return false; break; diff --git a/src/rewriter/basic_rewrite_rcons.cpp b/src/rewriter/basic_rewrite_rcons.cpp index c0716784796..d32ede86b2f 100644 --- a/src/rewriter/basic_rewrite_rcons.cpp +++ b/src/rewriter/basic_rewrite_rcons.cpp @@ -64,19 +64,6 @@ bool BasicRewriteRCons::prove( return true; } } - - if (eq[0].getKind() == Kind::APPLY_UF - && eq[0].getOperator().getKind() == Kind::LAMBDA) - { - std::vector args; - args.push_back(eq[0].getOperator()); - args.insert(args.end(), eq[0].begin(), eq[0].end()); - if (tryRule(cdp, eq, ProofRule::BETA_REDUCE, args)) - { - Trace("trewrite-rcons") << "...BETA_REDUCE" << std::endl; - return true; - } - } Trace("trewrite-rcons") << "...(fail)" << std::endl; return false; } diff --git a/src/theory/arrays/proof_checker.cpp b/src/theory/arrays/proof_checker.cpp index 097c75c1af2..8bda0feb0a4 100644 --- a/src/theory/arrays/proof_checker.cpp +++ b/src/theory/arrays/proof_checker.cpp @@ -34,7 +34,6 @@ void ArraysProofRuleChecker::registerTo(ProofChecker* pc) pc->registerChecker(ProofRule::ARRAYS_READ_OVER_WRITE_CONTRA, this); pc->registerChecker(ProofRule::ARRAYS_READ_OVER_WRITE_1, this); pc->registerChecker(ProofRule::ARRAYS_EXT, this); - pc->registerChecker(ProofRule::ARRAYS_EQ_RANGE_EXPAND, this); } Node ArraysProofRuleChecker::checkInternal(ProofRule id, @@ -108,11 +107,6 @@ Node ArraysProofRuleChecker::checkInternal(ProofRule id, Node bs = nm->mkNode(Kind::SELECT, b, k); return as.eqNode(bs).notNode(); } - if (id == ProofRule::ARRAYS_EQ_RANGE_EXPAND) - { - Node expandedEqRange = TheoryArraysRewriter::expandEqRange(args[0]); - return args[0].eqNode(expandedEqRange); - } // no rule return Node::null(); } diff --git a/src/theory/arrays/theory_arrays_rewriter.cpp b/src/theory/arrays/theory_arrays_rewriter.cpp index 059116f03f0..d7f39a62c2b 100644 --- a/src/theory/arrays/theory_arrays_rewriter.cpp +++ b/src/theory/arrays/theory_arrays_rewriter.cpp @@ -64,6 +64,25 @@ TheoryArraysRewriter::TheoryArraysRewriter(NodeManager* nm, EagerProofGenerator* epg) : TheoryRewriter(nm), d_rewriter(r), d_epg(epg) { + registerProofRewriteRule(ProofRewriteRule::ARRAYS_EQ_RANGE_EXPAND, + TheoryRewriteCtx::PRE_DSL); +} + +Node TheoryArraysRewriter::rewriteViaRule(ProofRewriteRule id, const Node& n) +{ + switch (id) + { + case ProofRewriteRule::ARRAYS_EQ_RANGE_EXPAND: + { + if (n.getKind() == Kind::EQ_RANGE) + { + return expandEqRange(n); + } + break; + } + default: break; + } + return Node::null(); } Node TheoryArraysRewriter::normalizeConstant(TNode node) @@ -692,11 +711,8 @@ TrustNode TheoryArraysRewriter::expandDefinition(Node node) Node expandedEqRange = expandEqRange(node); if (d_epg) { - TrustNode tn = d_epg->mkTrustNode(node.eqNode(expandedEqRange), - ProofRule::ARRAYS_EQ_RANGE_EXPAND, - {}, - {node}); - return TrustNode::mkTrustRewrite(node, expandedEqRange, d_epg); + return d_epg->mkTrustNodeRewrite( + node, expandedEqRange, ProofRewriteRule::ARRAYS_EQ_RANGE_EXPAND); } return TrustNode::mkTrustRewrite(node, expandedEqRange, nullptr); } diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h index 86c4e5206f1..2a7414c2f1e 100644 --- a/src/theory/arrays/theory_arrays_rewriter.h +++ b/src/theory/arrays/theory_arrays_rewriter.h @@ -63,6 +63,15 @@ class TheoryArraysRewriter : public TheoryRewriter RewriteResponse preRewrite(TNode node) override; + /** + * Rewrite n based on the proof rewrite rule id. + * @param id The rewrite rule. + * @param n The node to rewrite. + * @return The rewritten version of n based on id, or Node::null() if n + * cannot be rewritten. + */ + Node rewriteViaRule(ProofRewriteRule id, const Node& n) override; + TrustNode expandDefinition(Node node) override; /** diff --git a/src/theory/uf/proof_checker.cpp b/src/theory/uf/proof_checker.cpp index 1a5e6f3ceae..50b174299dd 100644 --- a/src/theory/uf/proof_checker.cpp +++ b/src/theory/uf/proof_checker.cpp @@ -37,7 +37,6 @@ void UfProofRuleChecker::registerTo(ProofChecker* pc) pc->registerChecker(ProofRule::FALSE_ELIM, this); pc->registerChecker(ProofRule::HO_CONG, this); pc->registerChecker(ProofRule::HO_APP_ENCODE, this); - pc->registerChecker(ProofRule::BETA_REDUCE, this); } Node UfProofRuleChecker::checkInternal(ProofRule id, @@ -205,29 +204,6 @@ Node UfProofRuleChecker::checkInternal(ProofRule id, Node ret = TheoryUfRewriter::getHoApplyForApplyUf(args[0]); return args[0].eqNode(ret); } - else if (id == ProofRule::BETA_REDUCE) - { - Assert(args.size() >= 2); - Node lambda = args[0]; - if (lambda.getKind() != Kind::LAMBDA) - { - return Node::null(); - } - std::vector vars(lambda[0].begin(), lambda[0].end()); - std::vector subs(args.begin() + 1, args.end()); - if (vars.size() != subs.size()) - { - return Node::null(); - } - NodeManager* nm = nodeManager(); - std::vector appArgs; - appArgs.push_back(lambda); - appArgs.insert(appArgs.end(), subs.begin(), subs.end()); - Node app = nm->mkNode(Kind::APPLY_UF, appArgs); - Node ret = lambda[1].substitute( - vars.begin(), vars.end(), subs.begin(), subs.end()); - return app.eqNode(ret); - } // no rule return Node::null(); } diff --git a/src/theory/uf/theory_uf_rewriter.cpp b/src/theory/uf/theory_uf_rewriter.cpp index 65277b45bf6..190327c729f 100644 --- a/src/theory/uf/theory_uf_rewriter.cpp +++ b/src/theory/uf/theory_uf_rewriter.cpp @@ -29,7 +29,11 @@ namespace cvc5::internal { namespace theory { namespace uf { -TheoryUfRewriter::TheoryUfRewriter(NodeManager* nm) : TheoryRewriter(nm) {} +TheoryUfRewriter::TheoryUfRewriter(NodeManager* nm) : TheoryRewriter(nm) +{ + registerProofRewriteRule(ProofRewriteRule::BETA_REDUCE, + TheoryRewriteCtx::PRE_DSL); +} RewriteResponse TheoryUfRewriter::postRewrite(TNode node) { @@ -153,6 +157,34 @@ RewriteResponse TheoryUfRewriter::preRewrite(TNode node) return RewriteResponse(REWRITE_DONE, node); } +Node TheoryUfRewriter::rewriteViaRule(ProofRewriteRule id, const Node& n) +{ + switch (id) + { + case ProofRewriteRule::BETA_REDUCE: + { + if (n.getKind() != Kind::APPLY_UF + || n.getOperator().getKind() != Kind::LAMBDA) + { + return Node::null(); + } + Node lambda = n.getOperator(); + std::vector vars(lambda[0].begin(), lambda[0].end()); + std::vector subs(n.begin(), n.end()); + if (vars.size() != subs.size()) + { + return Node::null(); + } + Node ret = lambda[1].substitute( + vars.begin(), vars.end(), subs.begin(), subs.end()); + return ret; + } + break; + default: break; + } + return Node::null(); +} + Node TheoryUfRewriter::getHoApplyForApplyUf(TNode n) { Assert(n.getKind() == Kind::APPLY_UF); diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h index 65269a7d3d0..981ef3e2143 100644 --- a/src/theory/uf/theory_uf_rewriter.h +++ b/src/theory/uf/theory_uf_rewriter.h @@ -39,6 +39,14 @@ class TheoryUfRewriter : public TheoryRewriter RewriteResponse postRewrite(TNode node) override; /** pre-rewrite */ RewriteResponse preRewrite(TNode node) override; + /** + * Rewrite n based on the proof rewrite rule id. + * @param id The rewrite rule. + * @param n The node to rewrite. + * @return The rewritten version of n based on id, or Node::null() if n + * cannot be rewritten. + */ + Node rewriteViaRule(ProofRewriteRule id, const Node& n) override; // conversion between HO_APPLY AND APPLY_UF /** * converts an APPLY_UF to a curried HO_APPLY e.g.