From 228f749173ffd03c3dca662b9ab6e44a58d544fe Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 19 Feb 2025 13:34:48 -0600 Subject: [PATCH 1/3] Add proof elaboration for string overlap macro rules (#11650) This adds proof elaboration for the macros in https://github.com/cvc5/cvc5/pull/11618 and https://github.com/cvc5/cvc5/pull/11591. --- src/rewriter/basic_rewrite_rcons.cpp | 208 +++++++++++++++++++++++++++ src/rewriter/basic_rewrite_rcons.h | 15 ++ 2 files changed, 223 insertions(+) diff --git a/src/rewriter/basic_rewrite_rcons.cpp b/src/rewriter/basic_rewrite_rcons.cpp index 191836d27a8..ae658bf541e 100644 --- a/src/rewriter/basic_rewrite_rcons.cpp +++ b/src/rewriter/basic_rewrite_rcons.cpp @@ -36,8 +36,10 @@ #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/rewriter.h" #include "theory/strings/arith_entail.h" +#include "theory/strings/sequences_rewriter.h" #include "theory/strings/strings_entail.h" #include "theory/strings/theory_strings_utils.h" +#include "theory/strings/word.h" #include "util/rational.h" using namespace cvc5::internal::kind; @@ -222,6 +224,13 @@ void BasicRewriteRCons::ensureProofForTheoryRewrite(CDProof* cdp, handledMacro = true; } break; + case ProofRewriteRule::MACRO_STR_STRIP_ENDPOINTS: + case ProofRewriteRule::MACRO_STR_SPLIT_CTN: + if (ensureProofMacroOverlap(id, cdp, eq)) + { + handledMacro = true; + } + break; case ProofRewriteRule::MACRO_QUANT_MERGE_PRENEX: if (ensureProofMacroQuantMergePrenex(cdp, eq)) { @@ -911,6 +920,205 @@ bool BasicRewriteRCons::ensureProofMacroSubstrStripSymLength(CDProof* cdp, return true; } +bool BasicRewriteRCons::ensureProofMacroOverlap(ProofRewriteRule id, + CDProof* cdp, + const Node& eq) +{ + Trace("brc-macro") << "Expand macro overlap (" << id << ") for " << eq + << std::endl; + NodeManager* nm = nodeManager(); + Assert(eq[0].getNumChildren() >= 2); + Node concat = eq[0][0]; + TypeNode stype = concat.getType(); + Node emp = theory::strings::Word::mkEmptyWord(stype); + size_t nchildpre = 0; + ProofRewriteRule rule; + std::vector premises; + if (id == ProofRewriteRule::MACRO_STR_SPLIT_CTN) + { + Assert(concat.getKind() == Kind::STRING_CONCAT); + rule = ProofRewriteRule::STR_OVERLAP_SPLIT_CTN; + Assert(eq[1].getKind() == Kind::OR + && eq[1][0].getKind() == Kind::STRING_CONTAINS); + if (eq[1][0][0].getKind() == Kind::STRING_CONCAT) + { + nchildpre = eq[1][0][0].getNumChildren(); + } + else if (eq[1][0][0] != emp) + { + nchildpre = 1; + } + // partition into three children + std::vector childpre(concat.begin(), concat.begin() + nchildpre); + Node cpre = theory::strings::utils::mkConcat(childpre, stype); + Node cmid = concat[nchildpre]; + std::vector childpost(concat.begin() + nchildpre + 1, concat.end()); + Node cpost = theory::strings::utils::mkConcat(childpost, stype); + Node cgroup = nm->mkNode(Kind::STRING_CONCAT, cpre, cmid, cpost); + if (concat != cgroup) + { + Node eqc = concat.eqNode(cgroup); + if (!cdp->addStep(eqc, ProofRule::ACI_NORM, {}, {eqc})) + { + Assert(false); + return false; + } + premises.push_back(eqc); + } + } + else + { + Assert(id == ProofRewriteRule::MACRO_STR_STRIP_ENDPOINTS); + theory::strings::ArithEntail ae(nullptr); + theory::strings::StringsEntail se(nullptr, ae); + theory::strings::SequencesRewriter srew(nm, ae, se, nullptr); + std::vector nb, nc1, ne; + // replay the strip endpoint operation + Kind k = eq[0].getKind(); + Node res = srew.rewriteViaMacroStrStripEndpoints(eq[0], nb, nc1, ne); + if (res != eq[1]) + { + Assert(false); + return false; + } + std::vector nc2; + theory::strings::utils::getConcat(eq[0][1], nc2); + std::vector newChildren[2]; + for (size_t i = 0; i < 2; i++) + { + std::vector& vec = i == 0 ? nb : ne; + if (i == 0 && k == Kind::STRING_INDEXOF) + { + Assert(vec.empty()); + continue; + } + else if (i == 1) + { + // placeholder for the middle term + newChildren[0].push_back(emp); + newChildren[1].push_back(emp); + } + if (vec.empty()) + { + newChildren[0].push_back(emp); + newChildren[1].push_back(emp); + continue; + } + if (vec.size() != 1) + { + Trace("brc-macro") << "...fail due to multiple stripped components" + << std::endl; + Assert(false); + return false; + } + newChildren[0].push_back(vec[0]); + // should be the case since we don't rewrite from both sides if + // the second term is a constant. + Assert(!nc2.empty()); + size_t index2 = (i == 0 ? 0 : nc2.size() - 1); + if (i == 0) + { + newChildren[1].push_back(nc2[index2]); + nc2.erase(nc2.begin(), nc2.begin() + 1); + } + else + { + newChildren[1].push_back(nc2[index2]); + nc2.pop_back(); + } + } + size_t remIndex = k == Kind::STRING_INDEXOF ? 0 : 1; + newChildren[0][remIndex] = theory::strings::utils::mkConcat(nc1, stype); + newChildren[1][remIndex] = theory::strings::utils::mkConcat(nc2, stype); + Trace("brc-macro") << "First child processed to : " << eq[0][0] + << " == " << newChildren[0] << std::endl; + Trace("brc-macro") << "Second child processed to : " << eq[0][1] + << " == " << newChildren[1] << std::endl; + // now, check if the children changed, if so add to premises + Node g1 = theory::strings::utils::mkConcat(newChildren[0], stype); + Node g2 = theory::strings::utils::mkConcat(newChildren[1], stype); + // the first may involve more than ACI_NORM, we use a subgoal + if (g1 != eq[0][0]) + { + Node eqc = eq[0][0].eqNode(g1); + cdp->addTrustedStep( + eqc, TrustId::MACRO_THEORY_REWRITE_RCONS_SIMPLE, {}, {}); + premises.push_back(eqc); + } + // the second should just be ACI_NORM + if (g2 != eq[0][1]) + { + // add the REFL step if we didnt change above + if (g1 == eq[0][0]) + { + Node refl = eq[0][0].eqNode(eq[0][0]); + cdp->addStep(refl, ProofRule::REFL, {}, {eq[0][0]}); + premises.push_back(refl); + } + Node eqc = eq[0][1].eqNode(g2); + if (!cdp->addStep(eqc, ProofRule::ACI_NORM, {}, {eqc})) + { + Assert(false); + Trace("brc-macro") << "...failed ACI_NORM" << std::endl; + return false; + } + premises.push_back(eqc); + } + switch (k) + { + case Kind::STRING_CONTAINS: + rule = ProofRewriteRule::STR_OVERLAP_ENDPOINTS_CTN; + break; + case Kind::STRING_INDEXOF: + rule = ProofRewriteRule::STR_OVERLAP_ENDPOINTS_INDEXOF; + break; + case Kind::STRING_REPLACE: + rule = ProofRewriteRule::STR_OVERLAP_ENDPOINTS_REPLACE; + break; + default: return false; + } + } + // cgroup is now the proper version of concat and we have proved (if + // necessary) that concat = cgroup. + Node input = eq[0]; + // if we rewrote children above + std::vector transEq; + if (!premises.empty()) + { + // prove input = inputRew by congruence given the premises + Node ceq = proveCong(cdp, input, premises); + transEq.push_back(ceq); + input = ceq[1]; + } + Trace("brc-macro") << "Run " << rule << " on " << input << std::endl; + theory::Rewriter* rr = d_env.getRewriter(); + Node ret = rr->rewriteViaRule(rule, input); + if (ret.isNull()) + { + Trace("brc-macro") << "...failed rewrite" << std::endl; + return false; + } + // add the rewrite + Node equiv = input.eqNode(ret); + cdp->addTheoryRewriteStep(equiv, rule); + transEq.push_back(equiv); + if (ret != eq[1]) + { + // should rewrite e.g. via ACI_NORM + Node eqpost = ret.eqNode(eq[1]); + Trace("brc-macro") << "- post-process subgoal " << eqpost << std::endl; + cdp->addTrustedStep( + eqpost, TrustId::MACRO_THEORY_REWRITE_RCONS_SIMPLE, {}, {}); + transEq.push_back(eqpost); + } + // apply transitivity if necessary + if (transEq.size() > 1) + { + cdp->addStep(eq, ProofRule::TRANS, transEq, {}); + } + return true; +} + bool BasicRewriteRCons::ensureProofMacroQuantMergePrenex(CDProof* cdp, const Node& eq) { diff --git a/src/rewriter/basic_rewrite_rcons.h b/src/rewriter/basic_rewrite_rcons.h index 110c5d61533..17f9deea9a7 100644 --- a/src/rewriter/basic_rewrite_rcons.h +++ b/src/rewriter/basic_rewrite_rcons.h @@ -191,6 +191,21 @@ class BasicRewriteRCons : protected EnvObj * @return true if added a closed proof of eq to cdp. */ bool ensureProofMacroSubstrStripSymLength(CDProof* cdp, const Node& eq); + /** + * Elaborate a rewrite eq that was proven by + * ProofRewriteRule::MACRO_STR_SPLIT_CTN or + * ProofRewriteRule::MACRO_STR_STRIP_ENDPOINTS. + * + * @param id The macro rule we are expanding. + * @param cdp The proof to add to. + * @param eq The rewrite proven by + * ProofRewriteRule::MACRO_STR_SPLIT_CTN or + * ProofRewriteRule::MACRO_STR_STRIP_ENDPOINTS. + * @return true if added a closed proof of eq to cdp. + */ + bool ensureProofMacroOverlap(ProofRewriteRule id, + CDProof* cdp, + const Node& eq); /** * Elaborate a rewrite eq that was proven by * ProofRewriteRule::MACRO_QUANT_MERGE_PRENEX. From d0e7209cba17b445e3f490cf652393f9fece7811 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 19 Feb 2025 14:26:14 -0600 Subject: [PATCH 2/3] Fixes for BV RARE rules (#11642) This corrects several BV rare rules which made them fail to match existing rules. This is work towards filling the remaining BV rewrite rules. It also restores and reformulates 2 rules deleted in https://github.com/cvc5/cvc5/pull/10904 so that they do not contain evaluatable terms in index positions. FYI @Lachnitt --- include/cvc5/cvc5_proof_rule.h | 4 ++++ proofs/eo/cpc/rules/Rewrites.eo | 33 +++++++++++++++++---------- src/theory/bv/rewrites | 13 ++++++----- src/theory/bv/rewrites-elimination | 22 ++++++++++-------- src/theory/bv/rewrites-simplification | 32 +++++++++++++++++++++----- 5 files changed, 70 insertions(+), 34 deletions(-) diff --git a/include/cvc5/cvc5_proof_rule.h b/include/cvc5/cvc5_proof_rule.h index 367d853ab19..e270802ebb1 100644 --- a/include/cvc5/cvc5_proof_rule.h +++ b/include/cvc5/cvc5_proof_rule.h @@ -4021,6 +4021,10 @@ enum ENUM(ProofRewriteRule) EVALUE(BV_ZERO_EXTEND_EQ_CONST_1), /** Auto-generated from RARE rule bv-zero-extend-eq-const-2 */ EVALUE(BV_ZERO_EXTEND_EQ_CONST_2), + /** Auto-generated from RARE rule bv-zero-extend-ult-const-1 */ + EVALUE(BV_ZERO_EXTEND_ULT_CONST_1), + /** Auto-generated from RARE rule bv-zero-extend-ult-const-2 */ + EVALUE(BV_ZERO_EXTEND_ULT_CONST_2), /** Auto-generated from RARE rule bv-sign-extend-ult-const-1 */ EVALUE(BV_SIGN_EXTEND_ULT_CONST_1), /** Auto-generated from RARE rule bv-sign-extend-ult-const-2 */ diff --git a/proofs/eo/cpc/rules/Rewrites.eo b/proofs/eo/cpc/rules/Rewrites.eo index 4fbfae8a4d5..19d47fd554e 100644 --- a/proofs/eo/cpc/rules/Rewrites.eo +++ b/proofs/eo/cpc/rules/Rewrites.eo @@ -603,10 +603,10 @@ :args (xs1 ys1 zs1 x1) :conclusion (= (bvxor xs1 (bvnot x1) ys1 x1 zs1) (bvnot ($singleton_elim (bvxor xs1 ys1 zs1)))) ) -(declare-rule bv-ult-add-one ((@n0 Int) (@n1 Int) (@n2 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1)) (c1 (BitVec @n2)) (w1 Int)) - :premises ((= c1 (@bv 1 w1)) (= w1 (@bvsize y1))) - :args (x1 y1 c1 w1) - :conclusion (= (bvult x1 (bvadd y1 c1)) (and (not (= y1 (bvnot (@bv 0 w1)))) (not (bvult y1 x1)))) +(declare-rule bv-ult-add-one ((@n0 Int) (@n1 Int) (@n2 Int) (@n3 Int) (x1 (BitVec @n0)) (ys1 (BitVec @n1) :list) (zs1 (BitVec @n2) :list) (c1 (BitVec @n3)) (w1 Int)) + :premises ((= c1 (@bv 1 w1)) (= w1 (@bvsize x1))) + :args (x1 ys1 zs1 c1 w1) + :conclusion (= (bvult x1 ($singleton_elim (bvadd ys1 c1 zs1))) (eo::define ((_let_1 ($singleton_elim (bvadd ys1 zs1)))) (and (not (= _let_1 (bvnot (@bv 0 w1)))) (not (bvult _let_1 x1))))) ) (declare-rule bv-concat-to-mult ((@n0 Int) (x1 (BitVec @n0)) (i1 Int) (m1 Int) (n1 Int) (w1 Int)) :premises ((= (+ 1 i1 m1) (@bvsize x1)) (= n1 0) (= w1 (@bvsize x1))) @@ -830,7 +830,7 @@ (declare-rule bv-smod-eliminate ((@n0 Int) (@n1 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1)) (w1 Int) (wm1 Int)) :premises ((= w1 (@bvsize x1)) (= wm1 (- (@bvsize x1) 1))) :args (x1 y1 w1 wm1) - :conclusion (= (bvsmod x1 y1) (eo::define ((_let_1 (@bv 1 1))) (eo::define ((_let_2 (= (extract wm1 wm1 y1) _let_1))) (eo::define ((_let_3 (= (extract wm1 wm1 x1) _let_1))) (eo::define ((_let_4 (bvurem (ite _let_3 (bvneg x1) x1) (ite _let_2 (bvneg y1) y1)))) (eo::define ((_let_5 (bvneg _let_4))) (eo::define ((_let_6 (not _let_3))) (eo::define ((_let_7 (not _let_2))) (ite (= _let_4 (@bv 0 w1)) _let_4 (ite (and _let_6 _let_7) _let_4 (ite (and _let_3 _let_7) (bvadd _let_5 y1) (ite (and _let_6 _let_2) (bvadd _let_4 y1) _let_5)))))))))))) + :conclusion (= (bvsmod x1 y1) (eo::define ((_let_1 (@bv 0 1))) (eo::define ((_let_2 (extract wm1 wm1 y1))) (eo::define ((_let_3 (= _let_2 _let_1))) (eo::define ((_let_4 (extract wm1 wm1 x1))) (eo::define ((_let_5 (= _let_4 _let_1))) (eo::define ((_let_6 (bvurem (ite _let_5 x1 (bvneg x1)) (ite _let_3 y1 (bvneg y1))))) (eo::define ((_let_7 (bvneg _let_6))) (eo::define ((_let_8 (@bv 1 1))) (ite (= _let_6 (@bv 0 w1)) _let_6 (ite (and _let_5 _let_3) _let_6 (ite (and (= _let_4 _let_8) _let_3) (bvadd _let_7 y1) (ite (and _let_5 (= _let_2 _let_8)) (bvadd _let_6 y1) _let_7))))))))))))) ) (declare-rule bv-smod-eliminate-fewer-bitwise-ops ((@n0 Int) (@n1 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1)) (w1 Int) (wm1 Int)) :premises ((= w1 (@bvsize x1)) (= wm1 (- (@bvsize x1) 1))) @@ -840,7 +840,7 @@ (declare-rule bv-srem-eliminate ((@n0 Int) (@n1 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1)) (nm1 Int)) :premises ((= nm1 (- (@bvsize x1) 1))) :args (x1 y1 nm1) - :conclusion (= (bvsrem x1 y1) (eo::define ((_let_1 (extract nm1 nm1 x1))) (eo::define ((_let_2 (bvurem (bvite _let_1 (bvneg x1) x1) (bvite (extract nm1 nm1 y1) (bvneg y1) y1)))) (bvite _let_1 (bvneg _let_2) _let_2)))) + :conclusion (= (bvsrem x1 y1) (eo::define ((_let_1 (@bv 1 1))) (eo::define ((_let_2 (= (extract nm1 nm1 x1) _let_1))) (eo::define ((_let_3 (bvurem (ite _let_2 (bvneg x1) x1) (ite (= (extract nm1 nm1 y1) _let_1) (bvneg y1) y1)))) (ite _let_2 (bvneg _let_3) _let_3))))) ) (declare-rule bv-srem-eliminate-fewer-bitwise-ops ((@n0 Int) (@n1 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1)) (nm1 Int)) :premises ((= nm1 (- (@bvsize x1) 1))) @@ -891,7 +891,7 @@ ) (declare-rule bv-ite-merge-then-else ((@n0 Int) (@n1 Int) (c1 (_ BitVec 1)) (c2 (_ BitVec 1)) (t1 (BitVec @n0)) (e1 (BitVec @n1))) :args (c1 c2 t1 e1) - :conclusion (= (bvite c1 t1 (bvite c2 t1 e1)) (bvite (bvnor c1 c2) e1 t1)) + :conclusion (= (bvite c1 t1 (bvite c2 t1 e1)) (bvite (bvand (bvnot c1) (bvnot c2)) e1 t1)) ) (declare-rule bv-ite-merge-else-else ((@n0 Int) (@n1 Int) (c1 (_ BitVec 1)) (c2 (_ BitVec 1)) (t1 (BitVec @n0)) (t2 (BitVec @n1))) :args (c1 c2 t1 t2) @@ -1136,14 +1136,13 @@ :conclusion (= (sign_extend i1 (sign_extend j1 x1)) (sign_extend k1 x1)) ) (declare-rule bv-merge-sign-extend-2 ((@n0 Int) (x1 (BitVec @n0)) (i1 Int) (j1 Int) (k1 Int)) - :premises ((= (> j1 1) true) (= k1 (+ i1 j1))) + :premises ((= (> j1 0) true) (= k1 (+ i1 j1))) :args (x1 i1 j1 k1) :conclusion (= (sign_extend i1 (zero_extend j1 x1)) (zero_extend k1 x1)) ) -(declare-rule bv-merge-sign-extend-3 ((@n0 Int) (x1 (BitVec @n0)) (i1 Int) (n1 Int)) - :premises ((= n1 0)) - :args (x1 i1 n1) - :conclusion (= (sign_extend i1 (zero_extend n1 x1)) (sign_extend i1 x1)) +(declare-rule bv-merge-sign-extend-3 ((@n0 Int) (x1 (BitVec @n0)) (i1 Int)) + :args (x1 i1) + :conclusion (= (sign_extend i1 (zero_extend 0 x1)) (sign_extend i1 x1)) ) (declare-rule bv-sign-extend-eq-const-1 ((@n0 Int) (x1 (BitVec @n0)) (m1 Int) (c1 Int) (nm1 Int) (mp1 Int) (nm2 Int) (nmm1 Int)) :premises ((= mp1 (+ m1 1)) (= nm2 (- (@bvsize x1) 1)) (= nmm1 (- nm1 1))) @@ -1165,6 +1164,16 @@ :args (x1 m1 c1 nm1 nm2 nmm1) :conclusion (= (= (@bv c1 nm1) (zero_extend m1 x1)) (eo::define ((_let_1 (@bv c1 nm1))) (and (= (extract nmm1 nm2 _let_1) (@bv 0 m1)) (= x1 (extract nm2 0 _let_1))))) ) +(declare-rule bv-zero-extend-ult-const-1 ((@n0 Int) (x1 (BitVec @n0)) (m1 Int) (c1 Int) (nm1 Int) (nm2 Int)) + :premises ((= nm2 (- (@bvsize x1) 1)) (eo::define ((_let_1 (@bv c1 nm1))) (= _let_1 (zero_extend m1 (extract nm2 0 _let_1))))) + :args (x1 m1 c1 nm1 nm2) + :conclusion (= (bvult (zero_extend m1 x1) (@bv c1 nm1)) (bvult x1 (extract nm2 0 (@bv c1 nm1)))) +) +(declare-rule bv-zero-extend-ult-const-2 ((@n0 Int) (x1 (BitVec @n0)) (m1 Int) (c1 Int) (nm1 Int) (nm2 Int)) + :premises ((= nm2 (- (@bvsize x1) 1)) (eo::define ((_let_1 (@bv c1 nm1))) (= _let_1 (zero_extend m1 (extract nm2 0 _let_1))))) + :args (x1 m1 c1 nm1 nm2) + :conclusion (= (bvult (@bv c1 nm1) (zero_extend m1 x1)) (bvult (extract nm2 0 (@bv c1 nm1)) x1)) +) (declare-rule bv-sign-extend-ult-const-1 ((@n0 Int) (x1 (BitVec @n0)) (m1 Int) (c1 Int) (nm1 Int) (nm2 Int)) :premises ((eo::define ((_let_1 (@bv (- (@bvsize x1) 1) nm1))) (eo::define ((_let_2 (@bv c1 nm1))) (= (or (bvule _let_2 (bvshl (@bv 1 nm1) _let_1)) (bvuge _let_2 (bvshl (bvnot (@bv 0 nm1)) _let_1))) true))) (= nm2 (- (@bvsize x1) 1))) :args (x1 m1 c1 nm1 nm2) diff --git a/src/theory/bv/rewrites b/src/theory/bv/rewrites index 163d44ec0b0..a219030c6ec 100644 --- a/src/theory/bv/rewrites +++ b/src/theory/bv/rewrites @@ -192,14 +192,15 @@ ; -- Simplify Bitblasting -- -; x < y + 1 <=> (not y < x) and y != 1...1 +; x < ys + 1 + zs <=> (not (ys + zs) < x) and (ys + zs) != 1...1 +; we use ys, zs as lists so that 1 may appear on the left or the right of the bvadd term. (define-cond-rule bv-ult-add-one - ((x ?BitVec) (y ?BitVec) (c1 ?BitVec) (w Int)) - (and (= c1 (@bv 1 w)) (= w (@bvsize y))) - (bvult x (bvadd y c1)) + ((x ?BitVec) (ys ?BitVec :list) (zs ?BitVec :list) (c1 ?BitVec) (w Int)) + (and (= c1 (@bv 1 w)) (= w (@bvsize x))) + (bvult x (bvadd ys c1 zs)) (and - (not (= y (bvnot (@bv 0 w)))) - (not (bvult y x)))) + (not (= (bvadd ys zs) (bvnot (@bv 0 w)))) + (not (bvult (bvadd ys zs) x)))) (define-cond-rule bv-concat-to-mult ((x ?BitVec) (i Int) (m Int) (n0 Int) (w Int)) (and (= (+ 1 i m) (@bvsize x)) (= n0 0) (= w (@bvsize x))) diff --git a/src/theory/bv/rewrites-elimination b/src/theory/bv/rewrites-elimination index a7fc398dde4..1f36bb72c69 100644 --- a/src/theory/bv/rewrites-elimination +++ b/src/theory/bv/rewrites-elimination @@ -155,19 +155,21 @@ (def (xLt0 (= (extract wm1 wm1 x) (@bv 1 1))) (yLt0 (= (extract wm1 wm1 y) (@bv 1 1))) - (xAbs (ite xLt0 (bvneg x) x)) - (yAbs (ite yLt0 (bvneg y) y)) + (nxLt0 (= (extract wm1 wm1 x) (@bv 0 1))) + (nyLt0 (= (extract wm1 wm1 y) (@bv 0 1))) + (xAbs (ite nxLt0 x (bvneg x))) + (yAbs (ite nyLt0 y (bvneg y))) (u (bvurem xAbs yAbs)) ) (and (= w (@bvsize x)) (= wm1 (- (@bvsize x) 1))) (bvsmod x y) (ite (= u (@bv 0 w)) u - (ite (and (not xLt0) (not yLt0)) + (ite (and nxLt0 nyLt0) u - (ite (and xLt0 (not yLt0)) + (ite (and xLt0 nyLt0) (bvadd (bvneg u) y) - (ite (and (not xLt0) yLt0) + (ite (and nxLt0 yLt0) (bvadd u y) (bvneg u)))))) (define-cond-rule bv-smod-eliminate-fewer-bitwise-ops @@ -194,15 +196,15 @@ (define-cond-rule bv-srem-eliminate ((x ?BitVec) (y ?BitVec) (nm1 Int)) (def - (xLt0 (extract nm1 nm1 x)) - (yLt0 (extract nm1 nm1 y)) - (xAbs (bvite xLt0 (bvneg x) x)) - (yAbs (bvite yLt0 (bvneg y) y)) + (xLt0 (= (extract nm1 nm1 x) (@bv 1 1))) + (yLt0 (= (extract nm1 nm1 y) (@bv 1 1))) + (xAbs (ite xLt0 (bvneg x) x)) + (yAbs (ite yLt0 (bvneg y) y)) (u (bvurem xAbs yAbs)) ) (= nm1 (- (@bvsize x) 1)) (bvsrem x y) - (bvite xLt0 (bvneg u) u)) + (ite xLt0 (bvneg u) u)) (define-cond-rule bv-srem-eliminate-fewer-bitwise-ops ((x ?BitVec) (y ?BitVec) (nm1 Int)) (def diff --git a/src/theory/bv/rewrites-simplification b/src/theory/bv/rewrites-simplification index 73246369ce9..888513a3d4c 100644 --- a/src/theory/bv/rewrites-simplification +++ b/src/theory/bv/rewrites-simplification @@ -59,7 +59,7 @@ (e1 ?BitVec) ) (bvite c0 t0 (bvite c1 t0 e1)) - (bvite (bvnor c0 c1) e1 t0)) + (bvite (bvand (bvnot c0) (bvnot c1)) e1 t0)) (define-rule bv-ite-merge-else-else ( (c0 (_ BitVec 1)) (c1 (_ BitVec 1)) @@ -364,14 +364,13 @@ ) (define-cond-rule bv-merge-sign-extend-2 ((x ?BitVec) (i Int) (j Int) (k Int)) - (and (> j 1) (= k (+ i j))) + (and (> j 0) (= k (+ i j))) (sign_extend i (zero_extend j x)) (zero_extend k x) ) -(define-cond-rule bv-merge-sign-extend-3 - ((x ?BitVec) (i Int) (n0 Int)) - (= n0 0) - (sign_extend i (zero_extend n0 x)) +(define-rule bv-merge-sign-extend-3 + ((x ?BitVec) (i Int)) + (sign_extend i (zero_extend 0 x)) (sign_extend i x) ) (define-cond-rule bv-sign-extend-eq-const-1 @@ -424,6 +423,27 @@ (and (= chi (@bv 0 m)) (= x clo))) + +(define-cond-rule bv-zero-extend-ult-const-1 + ((x ?BitVec) (m Int) (c Int) (nm Int) (nm1 Int)) + (def + (n (@bvsize x)) + (clo (extract nm1 0 (@bv c nm))) + ) + (and (= nm1 (- n 1)) (= (@bv c nm) (zero_extend m clo))) + (bvult (zero_extend m x) (@bv c nm)) + (bvult x clo)) + +(define-cond-rule bv-zero-extend-ult-const-2 + ((x ?BitVec) (m Int) (c Int) (nm Int) (nm1 Int)) + (def + (n (@bvsize x)) + (clo (extract nm1 0 (@bv c nm))) + ) + (and (= nm1 (- n 1)) (= (@bv c nm) (zero_extend m clo))) + (bvult (@bv c nm) (zero_extend m x)) + (bvult clo x)) + (define-cond-rule bv-sign-extend-ult-const-1 ((x ?BitVec) (m Int) (c Int) (nm Int) (nm1 Int)) (def From 2dcbe617a3a2bab9167717eb7e13b94183bc14d1 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 19 Feb 2025 20:41:50 -0600 Subject: [PATCH 3/3] Improvements and optimizations for Eunoia quantifiers signature (#11603) Notably substitutions are now proper substitutions and not computed as term substitutions, similarly searching for free variables is simplified by looking for atomic terms only. Also, substitutions for multiple variables are made significantly faster by leveraging eo::list operators. --- proofs/eo/cpc/programs/Quantifiers.eo | 36 +++++++++++---------------- proofs/eo/cpc/rules/Quantifiers.eo | 14 +++++------ 2 files changed, 22 insertions(+), 28 deletions(-) diff --git a/proofs/eo/cpc/programs/Quantifiers.eo b/proofs/eo/cpc/programs/Quantifiers.eo index 1871b9d7c9a..80a3e2741e4 100644 --- a/proofs/eo/cpc/programs/Quantifiers.eo +++ b/proofs/eo/cpc/programs/Quantifiers.eo @@ -11,29 +11,12 @@ ((T Type) (U Type) (S Type) (x S) (y S) (f (-> T U)) (a T) (z U) (w T)) (S S U) U ( - (($substitute x y x) y) (($substitute x y (f a)) (_ ($substitute x y f) ($substitute x y a))) + (($substitute x y x) y) (($substitute x y z) z) ) ) -; program: $substitute_list -; args: -; - arg1 @List: The list of domains of the substitution. -; - arg2 @List: The list of ranges of the substitution. -; - arg3 U: The term to process. -; return: > -; The result of applying the substitutions specified by arg1 -; and arg2 in order to arg3. In particular, the first element in the lists arg1 -; and arg2 are processed first. -(program $substitute_list ((T Type) (U Type) (F U) (x T) (xs @List :list) (t T) (ts @List :list)) - (@List @List U) U - ( - (($substitute_list (@list x xs) (@list t ts) F) ($substitute_list xs ts ($substitute x t F))) - (($substitute_list @list.nil @list.nil F) F) - ) -) - ; program: $contains_subterm ; args: ; - arg1 S: The term to process. @@ -62,6 +45,18 @@ ) ) +; program: $contains_aterm_list +; args: +; - t T: The term to process. +; - xs @List: The list of terms to find. +; return: true if any atomic (0-ary) subterm of t is in xs. +(program $contains_aterm_list ((T Type) (U Type) (S Type) (x U) (f (-> T S)) (a T) (xs @List)) + (T @List) Bool + ( + (($contains_aterm_list (f a) xs) (eo::ite ($contains_aterm_list f xs) true ($contains_aterm_list a xs))) + (($contains_aterm_list x xs) (eo::not (eo::is_neg (eo::list_find @list xs x)))) + ) +) ; program: $substitute_simul ; args: @@ -74,9 +69,8 @@ (S @List @List) S ( (($substitute_simul (f a) xs ss) (_ ($substitute_simul f xs ss) ($substitute_simul a xs ss))) - (($substitute_simul x @list.nil @list.nil) x) - (($substitute_simul x (@list x xs) (@list s ss)) s) ; note that we do not substitute further since this is a simultaneous substitution. - (($substitute_simul x (@list y xs) (@list s ss)) ($substitute_simul x xs ss)) + (($substitute_simul x xs ss) (eo::define ((i (eo::list_find @list xs x))) + (eo::ite (eo::is_neg i) x (eo::list_nth @list ss i)))) ) ) diff --git a/proofs/eo/cpc/rules/Quantifiers.eo b/proofs/eo/cpc/rules/Quantifiers.eo index b755495adcf..67ecf3ecb4d 100644 --- a/proofs/eo/cpc/rules/Quantifiers.eo +++ b/proofs/eo/cpc/rules/Quantifiers.eo @@ -12,7 +12,7 @@ (declare-rule instantiate ((F Bool) (xs @List) (ts @List)) :premises ((forall xs F)) :args (ts) - :conclusion ($substitute_list xs ts F)) + :conclusion ($substitute_simul F xs ts)) ; program: $mk_skolems ; args: @@ -39,7 +39,7 @@ ; introduced via $mk_skolems. (declare-rule skolemize ((x @List) (G Bool)) :premises ((not (forall x G))) - :conclusion ($substitute_list x ($mk_skolems x (forall x G) 0) (not G)) + :conclusion ($substitute_simul (not G) x ($mk_skolems x (forall x G) 0)) ) ; rule: skolem_intro @@ -66,8 +66,8 @@ ; B. The substitution is valid renaming due to the requirement check. (declare-rule alpha_equiv ((B Bool) (vs @List) (ts @List)) :args (B vs ts) - :requires ((($contains_subterm_list B ts) false)) - :conclusion (= B ($substitute_list vs ts B)) + :requires ((($contains_aterm_list B ts) false)) + :conclusion (= B ($substitute_simul B vs ts)) ) ; rule: beta-reduce @@ -235,9 +235,9 @@ (program $is_quant_miniscope_or ((x @List) (xs @List :list) (ys @List :list) (f Bool) (fs Bool :list) (g Bool) (gs Bool :list)) (@List Bool Bool) Bool ( - (($is_quant_miniscope_or x (or f fs) (or f gs)) (eo::requires ($contains_subterm_list f x) false + (($is_quant_miniscope_or x (or f fs) (or f gs)) (eo::requires ($contains_aterm_list f x) false ($is_quant_miniscope_or x fs gs))) - (($is_quant_miniscope_or x (or f fs) (or (forall @list.nil f) gs)) (eo::requires ($contains_subterm_list f x) false + (($is_quant_miniscope_or x (or f fs) (or (forall @list.nil f) gs)) (eo::requires ($contains_aterm_list f x) false ($is_quant_miniscope_or x fs gs))) (($is_quant_miniscope_or (@list x xs) (or f fs) (or (forall (@list x ys) f) gs)) (eo::requires ($contains_subterm gs x) false @@ -273,7 +273,7 @@ ; conclusion: The given equality. (declare-rule quant-miniscope-ite ((x @List) (A Bool) (F1 Bool) (F2 Bool) (G Bool)) :args ((= (forall x (ite A F1 F2)) (ite A (forall x F1) (forall x F2)))) - :requires ((($contains_subterm_list A x) false)) + :requires ((($contains_aterm_list A x) false)) :conclusion (= (forall x (ite A F1 F2)) (ite A (forall x F1) (forall x F2))) )