diff --git a/include/cvc5/cvc5_proof_rule.h b/include/cvc5/cvc5_proof_rule.h index 6897a231643..46217c2dcbe 100644 --- a/include/cvc5/cvc5_proof_rule.h +++ b/include/cvc5/cvc5_proof_rule.h @@ -2658,6 +2658,18 @@ enum ENUM(ProofRewriteRule) * \endverbatim */ EVALUE(MACRO_QUANT_VAR_ELIM_INEQ), + /** + * \verbatim embed:rst:leading-asterisk + * **Quantifiers -- Macro quantifiers rewrite body** + * + * .. math:: + * \forall X.\> F = \forall X.\> G + * + * where :math:`G` is semantically equivalent to :math:`F`. + * + * \endverbatim + */ + EVALUE(MACRO_QUANT_REWRITE_BODY), /** * \verbatim embed:rst:leading-asterisk * **Datatypes -- Instantiation** @@ -3085,6 +3097,8 @@ enum ENUM(ProofRewriteRule) EVALUE(ARRAY_STORE_OVERWRITE), /** Auto-generated from RARE rule array-store-self */ EVALUE(ARRAY_STORE_SELF), + /** Auto-generated from RARE rule array-read-over-write-split */ + EVALUE(ARRAY_READ_OVER_WRITE_SPLIT), /** Auto-generated from RARE rule bool-double-not-elim */ EVALUE(BOOL_DOUBLE_NOT_ELIM), /** Auto-generated from RARE rule bool-not-true */ @@ -3853,6 +3867,8 @@ enum ENUM(ProofRewriteRule) EVALUE(EQ_SYMM), /** Auto-generated from RARE rule eq-cond-deq */ EVALUE(EQ_COND_DEQ), + /** Auto-generated from RARE rule eq-ite-lift */ + EVALUE(EQ_ITE_LIFT), /** Auto-generated from RARE rule distinct-binary-elim */ EVALUE(DISTINCT_BINARY_ELIM), /** Auto-generated from RARE rule uf-bv2nat-int2bv */ diff --git a/proofs/eo/cpc/rules/Rewrites.eo b/proofs/eo/cpc/rules/Rewrites.eo index 865f5efaf75..36115644868 100644 --- a/proofs/eo/cpc/rules/Rewrites.eo +++ b/proofs/eo/cpc/rules/Rewrites.eo @@ -208,6 +208,10 @@ :args (t1 i1) :conclusion (= (store t1 i1 (select t1 i1)) t1) ) +(declare-rule array-read-over-write-split ((@T0 Type) (@T1 Type) (@T2 Type) (@T3 Type) (@T4 Type) (t1 (Array @T0 @T1)) (i1 @T2) (e1 @T3) (j1 @T4)) + :args (t1 i1 e1 j1) + :conclusion (= (select (store t1 j1 e1) i1) (ite (= i1 j1) e1 (select t1 i1))) +) (declare-rule bool-double-not-elim ((t1 Bool)) :args (t1) :conclusion (= (not (not t1)) t1) @@ -1908,6 +1912,10 @@ :args (t1 s1 r1) :conclusion (= (= (= t1 s1) (= t1 r1)) (and (not (= t1 s1)) (not (= t1 r1)))) ) +(declare-rule eq-ite-lift ((@T0 Type) (@T1 Type) (@T2 Type) (C1 Bool) (t1 @T0) (s1 @T1) (r1 @T2)) + :args (C1 t1 s1 r1) + :conclusion (= (= (ite C1 t1 s1) r1) (ite C1 (= t1 r1) (= s1 r1))) +) (declare-rule distinct-binary-elim ((@T0 Type) (@T1 Type) (t1 @T0) (s1 @T1)) :args (t1 s1) :conclusion (= (distinct t1 s1) (not (= t1 s1))) diff --git a/src/api/cpp/cvc5_proof_rule_template.cpp b/src/api/cpp/cvc5_proof_rule_template.cpp index 9f9235795c3..fcf658bbf53 100644 --- a/src/api/cpp/cvc5_proof_rule_template.cpp +++ b/src/api/cpp/cvc5_proof_rule_template.cpp @@ -256,6 +256,8 @@ const char* toString(cvc5::ProofRewriteRule rule) case ProofRewriteRule::MACRO_QUANT_VAR_ELIM_INEQ: return "macro-quant-var-elim-ineq"; case ProofRewriteRule::QUANT_VAR_ELIM_EQ: return "quant-var-elim-eq"; + case ProofRewriteRule::MACRO_QUANT_REWRITE_BODY: + return "macro-quant-rewrite-body"; case ProofRewriteRule::DT_INST: return "dt-inst"; case ProofRewriteRule::DT_COLLAPSE_SELECTOR: return "dt-collapse-selector"; case ProofRewriteRule::DT_COLLAPSE_TESTER: return "dt-collapse-tester"; diff --git a/src/rewriter/basic_rewrite_rcons.cpp b/src/rewriter/basic_rewrite_rcons.cpp index 466996c3490..31377c0a07d 100644 --- a/src/rewriter/basic_rewrite_rcons.cpp +++ b/src/rewriter/basic_rewrite_rcons.cpp @@ -65,8 +65,6 @@ bool BasicRewriteRCons::prove(CDProof* cdp, { Node eq = a.eqNode(b); Trace("trewrite-rcons") << "Reconstruct " << eq << std::endl; - Node lhs = eq[0]; - Node rhs = eq[1]; // this probably should never happen if (eq[0] == eq[1]) { @@ -218,6 +216,12 @@ void BasicRewriteRCons::ensureProofForTheoryRewrite( handledMacro = true; } break; + case ProofRewriteRule::MACRO_QUANT_REWRITE_BODY: + if (ensureProofMacroQuantRewriteBody(cdp, eq)) + { + handledMacro = true; + } + break; default: break; } if (handledMacro) @@ -799,6 +803,14 @@ bool BasicRewriteRCons::ensureProofMacroQuantVarElimEq(CDProof* cdp, for (size_t i = 0, nchild = body1r.getNumChildren(); i < nchild; i++) { Node eql = body1r[i].eqNode(body1re[i]); + // must ensure that this is indeed an equivalence, otherwise this trust + // step will be unsound. this is the case e.g. when + // a != (str.++ b x) is turned into x != (str.substr a (str.len b) ...) + // where the latter implies the former, but they are not equivalent + if (rewrite(body1r[i]) != rewrite(body1re[i])) + { + return false; + } if (body1r[i] == body1re[i]) { cdp->addStep(eql, ProofRule::REFL, {}, {eql[0]}); @@ -912,6 +924,28 @@ bool BasicRewriteRCons::ensureProofMacroQuantMiniscope(CDProof* cdp, return true; } +bool BasicRewriteRCons::ensureProofMacroQuantRewriteBody(CDProof* cdp, + const Node& eq) +{ + Trace("brc-macro") << "Expand quant rewrite body " << eq[0] << " == " << eq[1] + << std::endl; + // Call the utility again with proof tracking and construct the term + // conversion proof. This proof itself may have trust steps in it. + TConvProofGenerator tcpg(d_env, nullptr); + theory::quantifiers::QuantifiersRewriter qrew( + nodeManager(), d_env.getRewriter(), options()); + Node qr = qrew.computeRewriteBody(eq[0], &tcpg); + if (qr != eq[1]) + { + Assert(false) << "Failed to rewrite " << eq[0] << " to " << qr + << " != " << eq[1]; + return false; + } + std::shared_ptr pfn = tcpg.getProofFor(eq); + cdp->addProof(pfn); + return true; +} + bool BasicRewriteRCons::ensureProofArithPolyNormRel(CDProof* cdp, const Node& eq) { diff --git a/src/rewriter/basic_rewrite_rcons.h b/src/rewriter/basic_rewrite_rcons.h index 93c0ff97903..949e4cd3c00 100644 --- a/src/rewriter/basic_rewrite_rcons.h +++ b/src/rewriter/basic_rewrite_rcons.h @@ -210,6 +210,16 @@ class BasicRewriteRCons : protected EnvObj * @return true if added a closed proof of eq to cdp. */ bool ensureProofMacroQuantMiniscope(CDProof* cdp, const Node& eq); + /** + * Elaborate a rewrite eq that was proven by + * ProofRewriteRule::MACRO_QUANT_REWRITE_BODY. + * + * @param cdp The proof to add to. + * @param eq The rewrite proven by + * ProofRewriteRule::MACRO_QUANT_REWRITE_BODY. + * @return true if added a closed proof of eq to cdp. + */ + bool ensureProofMacroQuantRewriteBody(CDProof* cdp, const Node& eq); /** * @param cdp The proof to add to. * @param eq The rewrite that can be proven by ProofRule::ARITH_POLY_NORM_REL. diff --git a/src/theory/arrays/rewrites b/src/theory/arrays/rewrites index cd9f3be87f6..d1c96153648 100644 --- a/src/theory/arrays/rewrites +++ b/src/theory/arrays/rewrites @@ -11,3 +11,6 @@ (define-rule array-store-self ((t ?Array) (i ?)) (store t i (select t i)) t) + +(define-rule array-read-over-write-split ((t ?Array) (i ?) (e ?) (j ?)) + (select (store t j e) i) (ite (= i j) e (select t i))) diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 459402d498a..4e5e484a386 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -23,6 +23,7 @@ #include "expr/node_algorithm.h" #include "expr/skolem_manager.h" #include "options/quantifiers_options.h" +#include "proof/conv_proof_generator.h" #include "theory/arith/arith_msum.h" #include "theory/booleans/theory_bool_rewriter.h" #include "theory/datatypes/theory_datatypes_utils.h" @@ -118,6 +119,8 @@ QuantifiersRewriter::QuantifiersRewriter(NodeManager* nm, TheoryRewriteCtx::PRE_DSL); registerProofRewriteRule(ProofRewriteRule::MACRO_QUANT_VAR_ELIM_INEQ, TheoryRewriteCtx::PRE_DSL); + registerProofRewriteRule(ProofRewriteRule::MACRO_QUANT_REWRITE_BODY, + TheoryRewriteCtx::PRE_DSL); } Node QuantifiersRewriter::rewriteViaRule(ProofRewriteRule id, const Node& n) @@ -363,6 +366,19 @@ Node QuantifiersRewriter::rewriteViaRule(ProofRewriteRule id, const Node& n) } } break; + case ProofRewriteRule::MACRO_QUANT_REWRITE_BODY: + { + if (n.getKind() != Kind::FORALL) + { + return Node::null(); + } + Node nr = computeRewriteBody(n); + if (nr != n) + { + return nr; + } + } + break; default: break; } return Node::null(); @@ -712,22 +728,16 @@ void QuantifiersRewriter::computeDtTesterIteSplit( Node QuantifiersRewriter::computeProcessTerms(const Node& q, const std::vector& args, Node body, - QAttributes& qa) const + QAttributes& qa, + TConvProofGenerator* pg) const { options::IteLiftQuantMode iteLiftMode = options::IteLiftQuantMode::NONE; if (qa.isStandard()) { iteLiftMode = d_opts.quantifiers.iteLiftQuant; } - std::vector new_conds; std::map cache; - Node n = computeProcessTerms2(q, args, body, cache, new_conds, iteLiftMode); - if (!new_conds.empty()) - { - new_conds.push_back(n); - n = nodeManager()->mkNode(Kind::OR, new_conds); - } - return n; + return computeProcessTerms2(q, args, body, cache, iteLiftMode, pg); } Node QuantifiersRewriter::computeProcessTerms2( @@ -735,8 +745,8 @@ Node QuantifiersRewriter::computeProcessTerms2( const std::vector& args, Node body, std::map& cache, - std::vector& new_conds, - options::IteLiftQuantMode iteLiftMode) const + options::IteLiftQuantMode iteLiftMode, + TConvProofGenerator* pg) const { NodeManager* nm = nodeManager(); Trace("quantifiers-rewrite-term-debug2") @@ -745,40 +755,12 @@ Node QuantifiersRewriter::computeProcessTerms2( if( iti!=cache.end() ){ return iti->second; } - if (body.isClosure()) - { - // Ensure no shadowing. If this term is a closure quantifying a variable - // in args, then we introduce fresh variable(s) and replace this closure - // to be over the fresh variables instead. - std::vector oldVars; - std::vector newVars; - for (size_t i = 0, nvars = body[0].getNumChildren(); i < nvars; i++) - { - const Node& v = body[0][i]; - if (std::find(args.begin(), args.end(), v) != args.end()) - { - Trace("quantifiers-rewrite-unshadow") - << "Found shadowed variable " << v << " in " << q << std::endl; - oldVars.push_back(v); - Node nv = ElimShadowNodeConverter::getElimShadowVar(q, body, i); - newVars.push_back(nv); - } - } - if (!oldVars.empty()) - { - Assert(oldVars.size() == newVars.size()); - Node sbody = body.substitute( - oldVars.begin(), oldVars.end(), newVars.begin(), newVars.end()); - cache[body] = sbody; - return sbody; - } - } bool changed = false; std::vector children; for (const Node& bc : body) { // do the recursive call on children - Node nn = computeProcessTerms2(q, args, bc, cache, new_conds, iteLiftMode); + Node nn = computeProcessTerms2(q, args, bc, cache, iteLiftMode, pg); children.push_back(nn); changed = changed || nn != bc; } @@ -798,11 +780,39 @@ Node QuantifiersRewriter::computeProcessTerms2( ret = body; } + Node retOrig = ret; Trace("quantifiers-rewrite-term-debug2") << "Returning " << ret << " for " << body << std::endl; // do context-independent rewriting - if (ret.getKind() == Kind::EQUAL - && iteLiftMode != options::IteLiftQuantMode::NONE) + if (ret.isClosure()) + { + // Ensure no shadowing. If this term is a closure quantifying a variable + // in args, then we introduce fresh variable(s) and replace this closure + // to be over the fresh variables instead. + std::vector oldVars; + std::vector newVars; + for (size_t i = 0, nvars = ret[0].getNumChildren(); i < nvars; i++) + { + const Node& v = ret[0][i]; + if (std::find(args.begin(), args.end(), v) != args.end()) + { + Trace("quantifiers-rewrite-unshadow") + << "Found shadowed variable " << v << " in " << q << std::endl; + oldVars.push_back(v); + Node nv = ElimShadowNodeConverter::getElimShadowVar(q, ret, i); + newVars.push_back(nv); + } + } + if (!oldVars.empty()) + { + Assert(oldVars.size() == newVars.size()); + Node sbody = ret.substitute( + oldVars.begin(), oldVars.end(), newVars.begin(), newVars.end()); + ret = sbody; + } + } + else if (ret.getKind() == Kind::EQUAL + && iteLiftMode != options::IteLiftQuantMode::NONE) { for (size_t i = 0; i < 2; i++) { @@ -863,6 +873,17 @@ Node QuantifiersRewriter::computeProcessTerms2( ret = fullApp; } } + if (pg != nullptr) + { + if (retOrig != ret) + { + pg->addRewriteStep(retOrig, + ret, + nullptr, + false, + TrustId::MACRO_THEORY_REWRITE_RCONS_SIMPLE); + } + } cache[body] = ret; return ret; } @@ -2154,6 +2175,28 @@ bool QuantifiersRewriter::isStandard(QAttributes& qa, const Options& opts) return qa.isStandard() && !is_strict_trigger; } +Node QuantifiersRewriter::computeRewriteBody(const Node& n, + TConvProofGenerator* pg) const +{ + Assert(n.getKind() == Kind::FORALL); + QAttributes qa; + QuantAttributes::computeQuantAttributes(n, qa); + std::vector args(n[0].begin(), n[0].end()); + Node body = computeProcessTerms(n, args, n[1], qa, pg); + if (body != n[1]) + { + std::vector children; + children.push_back(n[0]); + children.push_back(body); + if (n.getNumChildren() == 3) + { + children.push_back(n[2]); + } + return d_nm->mkNode(Kind::FORALL, children); + } + return n; +} + bool QuantifiersRewriter::doOperation(Node q, RewriteStep computeOption, QAttributes& qa) const diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index c71b58a06b9..981bb63ac48 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -25,6 +25,7 @@ namespace cvc5::internal { class Options; +class TConvProofGenerator; namespace theory { @@ -227,6 +228,14 @@ class QuantifiersRewriter : public TheoryRewriter */ static bool isStandard(QAttributes& qa, const Options& opts); + /** + * @param q The quantified formula to rewrite. + * @param pg If provided, stores a set of small step rewrites that suffice + * to show that q rewrites to the returned quantified formula. + */ + Node computeRewriteBody(const Node& q, + TConvProofGenerator* pg = nullptr) const; + private: /** * Do trivial merging of the prenex of quantified formula q, e.g. @@ -263,25 +272,23 @@ class QuantifiersRewriter : public TheoryRewriter Node n, Node ipl); /** - * It may introduce new conditions C into new_conds. It returns a node retBody - * such that q of the form + * Returns a node retBody such that q of the form * forall args. body * is equivalent to: - * forall args. ( C V retBody ) + * forall args. retBody * * @param q The original quantified formula we are processing * @param args The bound variables of q * @param body The subformula of the body of q we are processing * @param cache Cache from terms to their processed form - * @param new_conds New conditions to add as disjunctions to the return * @param iteLiftMode The mode for lifting ITEs from body. */ Node computeProcessTerms2(const Node& q, const std::vector& args, Node body, std::map& cache, - std::vector& new_conds, - options::IteLiftQuantMode iteLiftMode) const; + options::IteLiftQuantMode iteLiftMode, + TConvProofGenerator* pg) const; void computeDtTesterIteSplit(Node n, std::map& pcons, std::map >& ncons, @@ -331,7 +338,8 @@ class QuantifiersRewriter : public TheoryRewriter Node computeProcessTerms(const Node& q, const std::vector& args, Node body, - QAttributes& qa) const; + QAttributes& qa, + TConvProofGenerator* pg = nullptr) const; //------------------------------------- end process terms //------------------------------------- extended rewrite /** compute extended rewrite diff --git a/src/theory/uf/rewrites b/src/theory/uf/rewrites index 6ac90c34642..eba7d938013 100644 --- a/src/theory/uf/rewrites +++ b/src/theory/uf/rewrites @@ -8,6 +8,10 @@ (= (= t s) (= t r)) (and (not (= t s)) (not (= t r)))) +(define-rule eq-ite-lift ((C Bool) (t ?) (s ?) (r ?)) + (= (ite C t s) r) + (ite C (= t r) (= s r))) + (define-rule distinct-binary-elim ((t ?) (s ?)) (distinct t s) (not (= t s))) ; bv to arith conversions