From 2dcbe617a3a2bab9167717eb7e13b94183bc14d1 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 19 Feb 2025 20:41:50 -0600 Subject: [PATCH 1/5] 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))) ) From a09cf821a0e1f706e76b2db78d0371a7aaca00ca Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 20 Feb 2025 06:14:22 -0600 Subject: [PATCH 2/5] Add elaboration for MACRO_STR_EQ_LEN_UNIFY (#11659) Note this elaboration depends on CONCAT_UNIFY, which due its simplifications from https://github.com/cvc5/cvc5/pull/11594 now can be applied to non-flat terms. This also relies on the RARE rewrite introduced in https://github.com/cvc5/cvc5/pull/11658. --- src/rewriter/basic_rewrite_rcons.cpp | 100 +++++++++++++++++++++++++++ src/rewriter/basic_rewrite_rcons.h | 10 +++ 2 files changed, 110 insertions(+) diff --git a/src/rewriter/basic_rewrite_rcons.cpp b/src/rewriter/basic_rewrite_rcons.cpp index ae658bf541e..d673b3cd3f4 100644 --- a/src/rewriter/basic_rewrite_rcons.cpp +++ b/src/rewriter/basic_rewrite_rcons.cpp @@ -224,6 +224,12 @@ void BasicRewriteRCons::ensureProofForTheoryRewrite(CDProof* cdp, handledMacro = true; } break; + case ProofRewriteRule::MACRO_STR_EQ_LEN_UNIFY: + if (ensureProofMacroStrEqLenUnify(cdp, eq)) + { + handledMacro = true; + } + break; case ProofRewriteRule::MACRO_STR_STRIP_ENDPOINTS: case ProofRewriteRule::MACRO_STR_SPLIT_CTN: if (ensureProofMacroOverlap(id, cdp, eq)) @@ -920,6 +926,100 @@ bool BasicRewriteRCons::ensureProofMacroSubstrStripSymLength(CDProof* cdp, return true; } +bool BasicRewriteRCons::ensureProofMacroStrEqLenUnify(CDProof* cdp, + const Node& eq) +{ + NodeManager* nm = nodeManager(); + Trace("brc-macro") << "Expand macro str eq len unify for " << eq << std::endl; + Assert(eq[1].getKind() == Kind::AND && eq[1].getNumChildren() == 2); + // This proves e.g. (= (= (str.++ x y) (str.++ z w)) (and (= x z) (= y w))). + // We prove this in two phases + Node falsen = nodeManager()->mkConst(false); + std::vector elhs; + std::vector erhs; + std::vector cpremises(eq[1].begin(), eq[1].end()); + for (const Node& eq1e : cpremises) + { + Assert(eq1e.getKind() == Kind::EQUAL && eq1e[0].getType().isStringLike()); + elhs.push_back(eq1e[0]); + erhs.push_back(eq1e[1]); + } + // the proper grouped equality + CDProof cdfwd(d_env); + Node clhs = nm->mkNode(Kind::STRING_CONCAT, elhs); + Node crhs = nm->mkNode(Kind::STRING_CONCAT, erhs); + Node ceq = clhs.eqNode(crhs); + // NOTE: ceq could be proven equivalent to eq[0] + + Node llhs0 = nm->mkNode(Kind::STRING_LENGTH, elhs[0]); + Node lrhs0 = nm->mkNode(Kind::STRING_LENGTH, erhs[0]); + Node leq = llhs0.eqNode(lrhs0); + // should be provable as a subgoal + Trace("brc-macro") << "- subgoal " << leq << std::endl; + cdfwd.addTrustedStep(leq, TrustId::MACRO_THEORY_REWRITE_RCONS, {}, {}); + // prove first component by CONCAT_UNIFY + cdfwd.addStep(cpremises[0], ProofRule::CONCAT_UNIFY, {ceq, leq}, {falsen}); + + elhs[0] = erhs[0]; + Node clhs2 = nm->mkNode(Kind::STRING_CONCAT, elhs); + std::vector cargs; + ProofRule ccr = expr::getCongRule(clhs2, cargs); + Node equiv = clhs2.eqNode(clhs); + Node cp0s = cpremises[0][1].eqNode(cpremises[0][0]); + Node reflEq = elhs[1].eqNode(elhs[1]); + cdfwd.addStep(cp0s, ProofRule::SYMM, {cpremises[0]}, {}); + cdfwd.addStep(reflEq, ProofRule::REFL, {}, {elhs[1]}); + cdfwd.addStep(equiv, ccr, {cp0s, reflEq}, cargs); + Node equiv2 = clhs2.eqNode(crhs); + cdfwd.addStep(equiv2, ProofRule::TRANS, {equiv, ceq}, {}); + // prove second component by CONCAT_EQ after congruence above + cdfwd.addStep(cpremises[1], ProofRule::CONCAT_EQ, {equiv2}, {falsen}); + // combine two equalities + cdfwd.addStep(eq[1], ProofRule::AND_INTRO, cpremises, {}); + // prove the implication and add to main proof + Node impl = nm->mkNode(Kind::IMPLIES, ceq, eq[1]); + cdfwd.addStep(impl, ProofRule::SCOPE, {eq[1]}, {ceq}); + cdp->addProof(cdfwd.getProofFor(impl)); + + // reverse proof is easy + CDProof cdrev(d_env); + cdrev.addStep( + cpremises[0], ProofRule::AND_ELIM, {eq[1]}, {nm->mkConstInt(0)}); + cdrev.addStep( + cpremises[1], ProofRule::AND_ELIM, {eq[1]}, {nm->mkConstInt(1)}); + cargs.clear(); + ccr = expr::getCongRule(ceq[0], cargs); + cdrev.addStep(ceq, ccr, cpremises, cargs); + // prove the implication and add to main proof + Node implrev = nm->mkNode(Kind::IMPLIES, eq[1], ceq); + cdrev.addStep(implrev, ProofRule::SCOPE, {ceq}, {eq[1]}); + cdp->addProof(cdrev.getProofFor(implrev)); + + // now prove dual implication is the same as equality + Node eqfinal = proveDualImplication(cdp, impl, implrev); + + // prove eq[0] is equal to the grouped concatenation terms, if necessary + if (eq[0] != ceq) + { + Node eqs1 = eq[0][0].eqNode(clhs); + Trace("brc-macro") << "- subgoal " << eqs1 << std::endl; + cdp->addTrustedStep(eqs1, TrustId::MACRO_THEORY_REWRITE_RCONS, {}, {}); + Node eqs2 = eq[0][1].eqNode(crhs); + Trace("brc-macro") << "- subgoal " << eqs2 << std::endl; + cdp->addTrustedStep(eqs2, TrustId::MACRO_THEORY_REWRITE_RCONS, {}, {}); + Node equivSetup = eq[0].eqNode(ceq); + cargs.clear(); + ccr = expr::getCongRule(eq[0], cargs); + cdp->addStep(equivSetup, ccr, {eqs1, eqs2}, cargs); + cdp->addStep(eq, ProofRule::TRANS, {equivSetup, eqfinal}, {}); + } + else + { + Assert(eqfinal == eq); + } + return true; +} + bool BasicRewriteRCons::ensureProofMacroOverlap(ProofRewriteRule id, CDProof* cdp, const Node& eq) diff --git a/src/rewriter/basic_rewrite_rcons.h b/src/rewriter/basic_rewrite_rcons.h index 17f9deea9a7..3f958b847de 100644 --- a/src/rewriter/basic_rewrite_rcons.h +++ b/src/rewriter/basic_rewrite_rcons.h @@ -191,6 +191,16 @@ 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_EQ_LEN_UNIFY. + * + * @param cdp The proof to add to. + * @param eq The rewrite proven by + * ProofRewriteRule::MACRO_STR_EQ_LEN_UNIFY. + * @return true if added a closed proof of eq to cdp. + */ + bool ensureProofMacroStrEqLenUnify(CDProof* cdp, const Node& eq); /** * Elaborate a rewrite eq that was proven by * ProofRewriteRule::MACRO_STR_SPLIT_CTN or From cecff59b21c30968d10fd19719ca9d81944c7cac Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 20 Feb 2025 06:52:46 -0600 Subject: [PATCH 3/5] Add proof rewrite rule SEQ_EVAL_OP (#11657) Also fixes the side condition for converting sequences to strings based on further tests, a regression is added. Review https://github.com/cvc5/cvc5/pull/11603 first. --- include/cvc5/cvc5_proof_rule.h | 13 +++++ proofs/eo/cpc/Cpc.eo | 14 ++++++ proofs/eo/cpc/programs/SeqToString.eo | 3 +- proofs/eo/cpc/programs/Utils.eo | 13 +++++ proofs/eo/cpc/rules/Quantifiers.eo | 1 + proofs/eo/cpc/rules/Strings.eo | 43 ++++++++++++++++ src/api/cpp/cvc5_proof_rule_template.cpp | 1 + src/proof/alf/alf_printer.cpp | 3 +- src/theory/strings/sequences_rewriter.cpp | 53 +++++++++++++++++--- src/theory/strings/theory_strings.cpp | 3 ++ src/theory/strings/theory_strings_utils.cpp | 3 +- test/regress/cli/CMakeLists.txt | 1 + test/regress/cli/regress0/seq/seq-evals.smt2 | 11 ++++ 13 files changed, 150 insertions(+), 12 deletions(-) create mode 100644 test/regress/cli/regress0/seq/seq-evals.smt2 diff --git a/include/cvc5/cvc5_proof_rule.h b/include/cvc5/cvc5_proof_rule.h index e270802ebb1..71268226d0f 100644 --- a/include/cvc5/cvc5_proof_rule.h +++ b/include/cvc5/cvc5_proof_rule.h @@ -3234,6 +3234,19 @@ enum ENUM(ProofRewriteRule) * \endverbatim */ EVALUE(STR_OVERLAP_ENDPOINTS_REPLACE), + /** + * \verbatim embed:rst:leading-asterisk + * **Strings -- Sequence evaluate operator** + * + * .. math:: + * f(s_1, \ldots, s_n) = t + * + * where :math:`f` is an operator over sequences and :math:`s_1, \ldots, s_n` + * are values, that is, the Node::isConst method returns true for each, and + * :math:`t` is the result of evaluating :math:`f` on them. + * \endverbatim + */ + EVALUE(SEQ_EVAL_OP), /** * \verbatim embed:rst:leading-asterisk * **Strings -- string indexof regex evaluation** diff --git a/proofs/eo/cpc/Cpc.eo b/proofs/eo/cpc/Cpc.eo index 27f0bb01912..bc9cde9f662 100644 --- a/proofs/eo/cpc/Cpc.eo +++ b/proofs/eo/cpc/Cpc.eo @@ -92,6 +92,8 @@ ; @var is an alias of eo::var to ensure the cpc proof does not use eo::var. (define @var ((s String) (T Type)) (eo::var s T)) +;;;;; ProofRule::EVALUATE + ; program: $run_evaluate ; args: ; - t S: The term to evaluate. @@ -297,6 +299,18 @@ ) ) +; program: $evaluate_list +; args: +; - ts @List: The list of terms to evaluate. +; return: The list containing the result of evaluating the terms in ts. +(program $evaluate_list ((U Type) (t U) (ts @List :list)) + (@List) @List + ( + (($evaluate_list (@list t ts)) (eo::cons @list ($run_evaluate t) ($evaluate_list ts))) + (($evaluate_list @list.nil) @list.nil) + ) +) + ; rule: evaluate ; implements: ProofRule::EVALUATE ; args: diff --git a/proofs/eo/cpc/programs/SeqToString.eo b/proofs/eo/cpc/programs/SeqToString.eo index 6a9d8b55da3..89bce1b039c 100644 --- a/proofs/eo/cpc/programs/SeqToString.eo +++ b/proofs/eo/cpc/programs/SeqToString.eo @@ -57,7 +57,7 @@ ; already allocated ($seq_to_string_rec ss - (eo::concat s (eo::to_str id)) + (eo::concat s (eo::to_str (eo::add (eo::list_len @list units) (eo::neg id) -1))) units chars n))))) @@ -89,7 +89,6 @@ (program $seq_to_string_op_rec ((U Type) (T Type) (f (-> T U)) (b T) (units @List) (chars @List) (S Type) (V Type) (u V) (ts (Seq V) :list)) (T @List @List) (Tuple S @List @List) ( - (($seq_to_string_op_rec (seq.++ (seq.unit u) ts) units chars) ($seq_to_string_rec (seq.++ (seq.unit u) ts) "" units chars (eo::list_len @list units))) (($seq_to_string_op_rec (seq.unit u) units chars) ($seq_to_string_rec (seq.unit u) "" units chars (eo::list_len @list units))) (($seq_to_string_op_rec (@seq.empty (Seq V)) units chars) (tuple "" units chars)) (($seq_to_string_op_rec (f b) units chars) (eo::match ((S1 Type) (fs S1) (nunits1 @List) (nchars1 @List)) diff --git a/proofs/eo/cpc/programs/Utils.eo b/proofs/eo/cpc/programs/Utils.eo index 4a30f539b02..e160da2de43 100644 --- a/proofs/eo/cpc/programs/Utils.eo +++ b/proofs/eo/cpc/programs/Utils.eo @@ -21,6 +21,19 @@ (declare-const @list.nil @List) (declare-const @list (-> (! Type :var T :implicit) T @List @List) :right-assoc-nil @list.nil) +; note: This is a forward declaration of $evaluate_list defined in Cpc.eo. +(program $evaluate_list () (@List) @List) + +; define: $evaluate +; args: +; - t S: The term to evaluate. +; return: The result of evaluating t. +; note: > +; This method is defined in terms of the forward declaration $evaluate_list here. +; The implementation of this method depends on defining the evaluation for all +; theories and thus is contained in Cpc.eo. +(define $evaluate ((T Type :implicit) (t T)) (eo::list_nth @list ($evaluate_list (@list t)) 0)) + ; program: $get_fun ; args: ; - t S: The term to inspect. diff --git a/proofs/eo/cpc/rules/Quantifiers.eo b/proofs/eo/cpc/rules/Quantifiers.eo index 67ecf3ecb4d..5c37acf6aa3 100644 --- a/proofs/eo/cpc/rules/Quantifiers.eo +++ b/proofs/eo/cpc/rules/Quantifiers.eo @@ -1,6 +1,7 @@ (include "../programs/Quantifiers.eo") (include "../programs/Datatypes.eo") (include "../theories/Quantifiers.eo") +(include "../theories/BitVectors.eo") ; rule: instantiate ; implements: ProofRule::INSTANTIATE. diff --git a/proofs/eo/cpc/rules/Strings.eo b/proofs/eo/cpc/rules/Strings.eo index 090fee79ee3..cf388c9f894 100644 --- a/proofs/eo/cpc/rules/Strings.eo +++ b/proofs/eo/cpc/rules/Strings.eo @@ -1,5 +1,8 @@ (include "../theories/Strings.eo") (include "../theories/Quantifiers.eo") + +(include "../programs/Quantifiers.eo") +(include "../programs/SeqToString.eo") (include "../programs/Strings.eo") ;;-------------------- Core @@ -867,3 +870,43 @@ :requires ((($str_eval_replace_re_all s r t) u)) :conclusion (= (str.replace_re_all s r t) u) ) + + +;;;;; ProofRewriteRule::SEQ_EVAL_OP + +; program: $seq_eval +; args: +; - t T: the term to evaluate, expected to be an operator applied to values, including at least one sequence value. +; return: The result of evaluating t. +(program $seq_eval ((T Type :implicit) (t T) (n Int)) + (T) T + ( + ; handle sequence-specific operators here + (($seq_eval (seq.nth t n)) (eo::match ((e T)) + (eo::list_nth str.++ ($str_to_nary_form t false) n) + (((seq.unit e) e)))) + ; otherwise, we rely on the strings evaluator + (($seq_eval t) (eo::match ((S Type) (u S) (units @List) (chars @List)) + ($seq_to_string_op_rec t @list.nil @list.nil) ; convert to string + (((tuple u units chars) (eo::define ((ue ($evaluate u))) ; evaluate on string + (eo::ite (eo::is_eq (eo::typeof ue) String) + ($singleton_elim + ($substitute_simul ($str_flatten_word ue) ; convert back to sequence + (eo::cons @list "" chars) + (eo::cons @list (@seq.empty (eo::typeof t)) units))) + ue)))))) ; otherwise just return self + ) +) + +; rule: seq-eval-op +; implements: ProofRewriteRule::SEQ_EVAL_OP +; args: +; - eq Bool: The equality between term involving sequences and its evaluation. +; requires: > +; Evaluating the left hand side gives the right hand side. +; conclusion: The given equality. +(declare-rule seq-eval-op ((T Type) (t T) (u T)) + :args ((= t u)) + :requires ((($seq_eval t) u)) + :conclusion (= t u) +) diff --git a/src/api/cpp/cvc5_proof_rule_template.cpp b/src/api/cpp/cvc5_proof_rule_template.cpp index f7516f46ce0..f4d2ba69578 100644 --- a/src/api/cpp/cvc5_proof_rule_template.cpp +++ b/src/api/cpp/cvc5_proof_rule_template.cpp @@ -310,6 +310,7 @@ const char* toString(cvc5::ProofRewriteRule rule) return "str-overlap-endpoints-indexof"; case ProofRewriteRule::STR_OVERLAP_ENDPOINTS_REPLACE: return "str-overlap-endpoints-replace"; + case ProofRewriteRule::SEQ_EVAL_OP: return "seq-eval-op"; case ProofRewriteRule::STR_INDEXOF_RE_EVAL: return "str-indexof-re-eval"; case ProofRewriteRule::STR_REPLACE_RE_EVAL: return "str-replace-re-eval"; case ProofRewriteRule::STR_REPLACE_RE_ALL_EVAL: diff --git a/src/proof/alf/alf_printer.cpp b/src/proof/alf/alf_printer.cpp index 30f4dc9d464..cbb8367b16b 100644 --- a/src/proof/alf/alf_printer.cpp +++ b/src/proof/alf/alf_printer.cpp @@ -333,7 +333,8 @@ bool AlfPrinter::isHandledTheoryRewrite(ProofRewriteRule id, const Node& n) case ProofRewriteRule::STR_OVERLAP_ENDPOINTS_CTN: case ProofRewriteRule::STR_OVERLAP_ENDPOINTS_INDEXOF: case ProofRewriteRule::STR_OVERLAP_ENDPOINTS_REPLACE: - case ProofRewriteRule::STR_CTN_MULTISET_SUBSET: return true; + case ProofRewriteRule::STR_CTN_MULTISET_SUBSET: + case ProofRewriteRule::SEQ_EVAL_OP: return true; case ProofRewriteRule::STR_IN_RE_EVAL: Assert(n[0].getKind() == Kind::STRING_IN_REGEXP && n[0][0].isConst()); return canEvaluateRegExp(n[0][1]); diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index fd469622186..ff0a0cd255f 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -81,6 +81,8 @@ SequencesRewriter::SequencesRewriter(NodeManager* nm, TheoryRewriteCtx::POST_DSL); registerProofRewriteRule(ProofRewriteRule::MACRO_STR_SPLIT_CTN, TheoryRewriteCtx::POST_DSL); + registerProofRewriteRule(ProofRewriteRule::SEQ_EVAL_OP, + TheoryRewriteCtx::PRE_DSL); // make back pointer to this (for rewriting contains) se.d_rewriter = this; } @@ -114,7 +116,9 @@ Node SequencesRewriter::rewriteViaRule(ProofRewriteRule id, const Node& n) } case ProofRewriteRule::STR_CTN_MULTISET_SUBSET: { - if (n.getKind() == Kind::STRING_CONTAINS) + // don't use this just for evaluation + if (n.getKind() == Kind::STRING_CONTAINS + && (!n[0].isConst() || !n[1].isConst())) { if (d_stringsEntail.checkMultisetSubset(n[0], n[1])) { @@ -162,6 +166,29 @@ Node SequencesRewriter::rewriteViaRule(ProofRewriteRule id, const Node& n) std::vector nb, nrem, ne; return rewriteViaMacroStrStripEndpoints(n, nb, nrem, ne); } + case ProofRewriteRule::SEQ_EVAL_OP: + { + // this is a catchall rule for evaluation of operations on constant + // sequences + TypeNode tn = utils::getOwnerStringType(n); + if (tn.isSequence()) + { + for (const Node& nc : n) + { + if (!nc.isConst()) + { + return Node::null(); + } + } + RewriteResponse response = postRewrite(n); + Node ret = response.d_node; + if (ret.isConst()) + { + return ret; + } + } + } + break; case ProofRewriteRule::STR_OVERLAP_SPLIT_CTN: case ProofRewriteRule::STR_OVERLAP_ENDPOINTS_CTN: case ProofRewriteRule::STR_OVERLAP_ENDPOINTS_INDEXOF: @@ -3185,11 +3212,6 @@ Node SequencesRewriter::rewriteReplace(Node node) Assert(node.getKind() == Kind::STRING_REPLACE); NodeManager* nm = nodeManager(); - if (node[1].isConst() && Word::isEmpty(node[1])) - { - Node ret = nm->mkNode(Kind::STRING_CONCAT, node[2], node[0]); - return returnRewrite(node, ret, Rewrite::RPL_RPL_EMPTY); - } // the string type TypeNode stype = node.getType(); @@ -3223,11 +3245,28 @@ Node SequencesRewriter::rewriteReplace(Node node) children.push_back(s3); } children.insert(children.end(), children0.begin() + 1, children0.end()); - Node ret = utils::mkConcat(children, stype); + Node ret; + if (children0.size() == 1 && node[2].isConst()) + { + // evaluate the constant, this ensures that we always immediately + // evaluate constants immediately, which is important for proof + // reconstruction. + ret = Word::mkWordFlatten(children); + } + else + { + ret = utils::mkConcat(children, stype); + } return returnRewrite(node, ret, Rewrite::RPL_CONST_FIND); } } + if (node[1].isConst() && Word::isEmpty(node[1])) + { + Node ret = nm->mkNode(Kind::STRING_CONCAT, node[2], node[0]); + return returnRewrite(node, ret, Rewrite::RPL_RPL_EMPTY); + } + // rewrites that apply to both replace and replaceall Node rri = rewriteReplaceInternal(node); if (!rri.isNull()) diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 2fa0ef43781..2cc1a141f8e 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -1105,6 +1105,9 @@ void TheoryStrings::computeCareGraph() } if( has_trigger_arg ){ TypeNode ft = utils::getOwnerStringType(f1); + AlwaysAssert(ft.isStringLike()) + << "Unexpected term in getOwnerStringType : " << f1 << ", type " + << ft; std::pair ikey = std::pair(ft, op); index[ikey].addTerm(f1, reps); arity[op] = reps.size(); diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp index 828ac89859b..f32ac3b05a0 100644 --- a/src/theory/strings/theory_strings_utils.cpp +++ b/src/theory/strings/theory_strings_utils.cpp @@ -452,8 +452,7 @@ TypeNode getOwnerStringType(Node n) { tn = n.getType(); } - AlwaysAssert(tn.isStringLike()) - << "Unexpected term in getOwnerStringType : " << n << ", type " << tn; + // otherwise return null return tn; } diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index 2e83cfc29c9..52d5c3ccebb 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -1735,6 +1735,7 @@ set(regress_0_tests regress0/seq/array/update-word-eq.smt2 regress0/seq/issue6005-no-strings-exp.smt2 regress0/seq/seq-2var.smt2 + regress0/seq/seq-evals.smt2 regress0/seq/seq-ex1.smt2 regress0/seq/seq-ex2.smt2 regress0/seq/seq-ex3.smt2 diff --git a/test/regress/cli/regress0/seq/seq-evals.smt2 b/test/regress/cli/regress0/seq/seq-evals.smt2 new file mode 100644 index 00000000000..cf4911d4e2f --- /dev/null +++ b/test/regress/cli/regress0/seq/seq-evals.smt2 @@ -0,0 +1,11 @@ +; EXPECT: unsat +(set-logic ALL) +(assert (or +(not (= (seq.replace (seq.++ (seq.unit 0) (seq.unit 1) (seq.unit 2)) (seq.++ (seq.unit 1) (seq.unit 2)) (as seq.empty (Seq Int))) (seq.unit 0))) +(not (= (seq.contains (seq.++ (seq.unit 0) (seq.unit 1) (seq.unit 2)) (seq.++ (seq.unit 1) (seq.unit 3))) false)) +(not (= (seq.nth (seq.++ (seq.unit 0) (seq.unit 1) (seq.unit 2) (seq.unit 5)) 3) 5)) +(not (= (seq.contains (seq.++ (seq.unit (set.singleton 0)) (seq.unit (set.union (set.singleton 2) (set.singleton 1))) (seq.unit (set.singleton 0))) + (seq.unit (set.union (set.singleton 1) (set.singleton 3)))) false)) + +)) +(check-sat) From 348845e3f43b84733e3d5523ee3aa08828ccec24 Mon Sep 17 00:00:00 2001 From: Kartik Sabharwal <12889896+kartik-sabharwal@users.noreply.github.com> Date: Thu, 20 Feb 2025 07:10:08 -0600 Subject: [PATCH 4/5] Documentation for OpArgIndex in conjecture generator (#11665) --- src/theory/quantifiers/conjecture_generator.h | 136 +++++++++++++++++- 1 file changed, 135 insertions(+), 1 deletion(-) diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index cc49c905636..547f084181a 100644 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -33,7 +33,141 @@ namespace quantifiers { class ConjectureGenerator; -// operator independent index of arguments for an EQC +/** operator independent index of arguments for an EQC + * + * The (almost) inductive definition of the set of irrelevant terms suggests + * the following algorithm to compute I, the set of irrelevant equivalence + * classes. It is a standard algorithm that starts from the empty set and + * iterates up to a fixed point. + * + * declare I and set its value to the empty set + * + * for each equivalence class e: + * if the sort of e is not an inductive datatype sort: + * add e to I + * + * declare I_old + * + * do: + * set I_old to the current value of I + * for each equivalence class e: + * if e is not in I: + * for each term t in e: + * if t has the form f(t_1, ..., t_n) where f is an atomic + * trigger that is not a skolem function and the equivalence class + * of each t_i is in I: + * add e to I + * continue to the next equivalence class + * else + * continue to the next term in e + * while I_old is different from I + * + * Note the three nested loops in the second phase of the algorithm above. + * We can avoid inspecting each element of each equivalence class that is not + * already in I by preparing a family of indices, which can be described + * abstractly as follows. + * + * _Definitions_ + * + * - 'E' is the set of representatives of equivalence classes. + * - 'F' is the set of function symbols. + * - 'T' is the set of terms. + * - For a set 'X', X* denotes the set of all strings over X. + * - For a set 'X', X+ denotes the set of non-empty strings over X. + * - For sets 'X' and 'Y', X x Y denotes their cartesian product. + * - 't = u' means the terms t and u are syntactically equal. + * - 't ~ u' means the terms t and u are in the same equivalence class according + * to the current model + * + * _Declarations_ + * + * - 'OpArgIndex' is a subset of E+, we intend that OpArgIndex(e e_1 ... e_n) is + * true iff the string e e_1 ... e_n denotes an instance of the C++ class named + * OpArgIndex + * + * - '[[e e_1 ... e_n]]' is the instance of the OpArgIndex class denoted by the + * string e e_1 ... e_n when OpArgIndex(e e_1 ... e_n) is true, and it is + * equal to d_op_arg_index[e].d_child[e_1].(...).d_child[e_n] + * + * - 'child' is a subset of E+ x E, we intend that child(e e_1 ... e_n, e^) is + * true iff the map [[e e_1 ... e_n]].d_child contains e^ as a key. + * + * - 'ops' : OpArgIndex -> F* is a function where we intend ops(e e_1 ... e_n) + * to be the same sequence of function symbols as the vector + * [[e e_1 ... e_n]].d_ops + * + * - 'op_terms' : OpArgIndex -> T* is a function where we intend + * op_terms(e e_1 ... e_n) to be the same sequence of terms as the vector + * [[e e_1 ... e_n]].d_op_terms + * + * - 'added' is a subset of E x T where we intend added(e, t) to be true iff + * d_op_arg_index[e].addTerm(t) executes successfully. + * + * _Invariants_ + * + * (i) child(e e_1 ... e_n, e^) + * <==> OpArgIndex(e e_1 ... e_n e^) + * + * (ii) OpArgIndex(e e_1 ... e_n) + * ==> for all 0 <= i < n. OpArgIndex(e e_1 ... e_i) + * + * (iii) added(e, f(t_1, ..., t_n)) + * <==> OpArgIndex(e e_1 ... e_n) + * /\ there exists j. ops(e e_1 ... e_n)(j) = f + * /\ op_terms(e e_1 ... e_n)(j) = f(t_1, ..., t_n) + * + * (iv) d_ops(e e_1 ... e_n) has the same length as |d_op_terms(e e_1 ... e_n)| + * + * _Additional guarantees_ + * + * In the implementation of getEquivalenceClasses, note that we add + * f(t_1, ..., t_n) to d_op_terms[e] when, among satisfying certain other + * properties, it is in e's equivalence class. This guarantees that + * added(e, f(t_1, ..., t_n)) ==> f(t_1, ..., t_n) ~ e. + * + * Furthermore the implementation of addTerm ensures that for any equivalence + * class representative e and for any two terms t = f(t_1, ..., t_n) and + * u = f(u_1, ..., u_n) such that t != u, t ~ e, u ~ e, + * and t_i ~ u_i for each i, we that at most one of added(e, t) and + * added(e, u) is true. + * + * _Take-away_ + * + * The problem of deciding whether the equivalence class represented by e is + * irrelevant (see comment for computeIrrelevantEqcs) falls to searching for + * a string e e_1 ... e_n such that + * + * - OpArgIndex(e e_1 ... e_n), and + * - for all 1 <= i < n. e_i is irrelevant, and + * - ops(e e_1 ... e_n) is non-empty. + * + * as implemented in 'getGroundTerms'. + * + * We hope is that searching for such a string is more efficient than the + * naive approach of iterating over all terms in e's equivalence class and + * checking if any one of these terms is irrelevant. + * + * _Example_ + * + * Let e, e_1, e_2 and e_3 be representatives of equivalence classes. + * Suppose we're given that + * + * - f(t_1,t_2) ~ g(t_3) ~ f(t_4,t_5) ~ f(t_6,t_7) ~ e, and + * - t_1 ~ t_3 ~ t_4 ~ t_6 ~ e_1, and + * - t_2 ~ t_5 ~ e_2, and + * - t_7 ~ e_3 + * + * Suppose also that we add f(t_1,t_2), g(t_3), f(t_4,t_5), and f(t_6,t_7) + * to d_op_arg_index[e] in sequence. The resulting data structure looks like + * + * [[e]], d_ops = [], d_op_terms = [] + * | + * e_1 '-- [[e e_1]], d_ops = [ g ], d_op_terms = [ g(t_3) ] + * | + * e_2 |-- [[e e_1 e_2]], d_ops = [ f ], d_op_terms = [ f(t_4,t_5) ] + * | + * e_3 '-- [[e e_1 e_3]], d_ops = [ f ], d_op_terms = [ f(t_6,t_7) ] + */ class OpArgIndex { public: From 0ab0f2de41b0777c3c8bc23bb64213c0d85a4543 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 20 Feb 2025 07:16:47 -0600 Subject: [PATCH 5/5] Add elaboration for MACRO_STR_EQ_LEN_UNIFY_PREFIX (#11658) This adds proof elaboration for MACRO_STR_EQ_LEN_UNIFY_PREFIX. It does not require any new rules, apart from a RARE rewrite for turning a dual implicaition into an equality. --- include/cvc5/cvc5_proof_rule.h | 2 + proofs/eo/cpc/rules/Rewrites.eo | 4 + src/rewriter/basic_rewrite_rcons.cpp | 229 +++++++++++++++++++++++++++ src/rewriter/basic_rewrite_rcons.h | 10 ++ src/theory/booleans/rewrites | 3 + 5 files changed, 248 insertions(+) diff --git a/include/cvc5/cvc5_proof_rule.h b/include/cvc5/cvc5_proof_rule.h index 71268226d0f..01cee0d5478 100644 --- a/include/cvc5/cvc5_proof_rule.h +++ b/include/cvc5/cvc5_proof_rule.h @@ -3636,6 +3636,8 @@ enum ENUM(ProofRewriteRule) EVALUE(BOOL_IMPL_TRUE2), /** Auto-generated from RARE rule bool-impl-elim */ EVALUE(BOOL_IMPL_ELIM), + /** Auto-generated from RARE rule bool-dual-impl-eq */ + EVALUE(BOOL_DUAL_IMPL_EQ), /** Auto-generated from RARE rule bool-or-true */ EVALUE(BOOL_OR_TRUE), /** Auto-generated from RARE rule bool-or-flatten */ diff --git a/proofs/eo/cpc/rules/Rewrites.eo b/proofs/eo/cpc/rules/Rewrites.eo index 19d47fd554e..1e826c725ea 100644 --- a/proofs/eo/cpc/rules/Rewrites.eo +++ b/proofs/eo/cpc/rules/Rewrites.eo @@ -291,6 +291,10 @@ :args (t1 s1) :conclusion (= (=> t1 s1) (or (not t1) s1)) ) +(declare-rule bool-dual-impl-eq ((t1 Bool) (s1 Bool)) + :args (t1 s1) + :conclusion (= (and (=> t1 s1) (=> s1 t1)) (= t1 s1)) +) (declare-rule bool-or-true ((xs1 Bool :list) (ys1 Bool :list)) :args (xs1 ys1) :conclusion (= ($singleton_elim (or xs1 true ys1)) true) diff --git a/src/rewriter/basic_rewrite_rcons.cpp b/src/rewriter/basic_rewrite_rcons.cpp index d673b3cd3f4..53dd84985d9 100644 --- a/src/rewriter/basic_rewrite_rcons.cpp +++ b/src/rewriter/basic_rewrite_rcons.cpp @@ -224,6 +224,12 @@ void BasicRewriteRCons::ensureProofForTheoryRewrite(CDProof* cdp, handledMacro = true; } break; + case ProofRewriteRule::MACRO_STR_EQ_LEN_UNIFY_PREFIX: + if (ensureProofMacroStrEqLenUnifyPrefix(cdp, eq)) + { + handledMacro = true; + } + break; case ProofRewriteRule::MACRO_STR_EQ_LEN_UNIFY: if (ensureProofMacroStrEqLenUnify(cdp, eq)) { @@ -926,6 +932,229 @@ bool BasicRewriteRCons::ensureProofMacroSubstrStripSymLength(CDProof* cdp, return true; } + +bool BasicRewriteRCons::ensureProofMacroStrEqLenUnifyPrefix(CDProof* cdp, + const Node& eq) +{ + Trace("brc-macro") << "Expand macro str eq len unify prefix " << eq + << std::endl; + NodeManager* nm = nodeManager(); + theory::strings::ArithEntail ae(nullptr); + theory::strings::StringsEntail sent(nullptr, ae); + + Assert(eq[1].getKind() == Kind::AND); + Node eq1p = eq[1]; + // get the equations equal empty + // we group (and (= s t) (= t1 "") ... (= tn "")) to + // (and (= s t) (and (= t1 "") ... (= tn ""))) and store in eq1p. + std::vector empeqs; + if (eq[1].getNumChildren() > 2) + { + empeqs.insert(empeqs.end(), eq[1].begin() + 1, eq[1].end()); + Node eq1g = nm->mkAnd(empeqs); + eq1p = nm->mkNode(Kind::AND, eq[1][0], eq1g); + Node eqg = eq1p.eqNode(eq[1]); + cdp->addStep(eqg, ProofRule::ACI_NORM, {}, {eqg}); + } + else + { + empeqs.push_back(eq[1][1]); + } + + // prove eq[0] => eq1p in cdfwd + CDProof cdfwd(d_env); + Node eqsrc = eq[0]; + Node ret = sent.inferEqsFromContains(eqsrc[0], eqsrc[1]); + Trace("brc-macro") << "[1] setup forward implication" << std::endl; + bool eqFlipped = false; + if (ret.isNull()) + { + Trace("brc-macro") << "...failed " << ret << ", try flip" << std::endl; + eqsrc = eq[0][1].eqNode(eq[0][0]); + ret = sent.inferEqsFromContains(eqsrc[0], eqsrc[1]); + if (ret.isNull()) + { + Trace("brc-macro") << "... failed to replicate " << ret << std::endl; + return false; + } + eqFlipped = true; + cdfwd.addStep(eqsrc, ProofRule::SYMM, {eq[0]}, {}); + } + Node len1 = nm->mkNode(Kind::STRING_LENGTH, eqsrc[0]); + Node len2 = nm->mkNode(Kind::STRING_LENGTH, eqsrc[1]); + Node leneq = proveCong(&cdfwd, len1, {eqsrc}); + Node li[2]; + std::vector eqi; + eqi.resize(2); + for (size_t i = 0; i < 2; i++) + { + Node l = i == 0 ? len1 : len2; + TConvProofGenerator tcpg(d_env, nullptr); + li[i] = ae.rewriteLengthIntro(l, &tcpg); + if (li[i] != l) + { + Node equiv = l.eqNode(li[i]); + std::shared_ptr pfn = tcpg.getProofFor(equiv); + cdfwd.addProof(pfn); + eqi[i] = pfn->getResult(); + } + } + Node leneqi = li[0].eqNode(li[1]); + if (leneqi != leneq) + { + Node equiv = proveCong(&cdfwd, leneq, eqi); + cdfwd.addStep(leneqi, ProofRule::EQ_RESOLVE, {leneq, equiv}, {}); + } + Trace("brc-macro") << "...length: " << li[0] << " == " << li[1] << std::endl; + // based on swapping above, we should have len1i >= len2i + Node diff = nm->mkNode(Kind::SUB, li[1], li[0]); + Node diffn = theory::arith::PolyNorm::getPolyNorm(diff); + Trace("brc-macro") << "...norm diff " << diffn << std::endl; + Node diffneqz = diffn.eqNode(nm->mkConstInt(Rational(0))); + Node equiv = leneqi.eqNode(diffneqz); + if (!ensureProofArithPolyNormRel(&cdfwd, equiv)) + { + Trace("brc-macro") << "... failed poly norm rel" << std::endl; + return false; + } + cdfwd.addStep(diffneqz, ProofRule::EQ_RESOLVE, {leneqi, equiv}, {}); + Trace("brc-macro") << "...have " << diffneqz << std::endl; + + // get the concatenation term corresponding to the components equated to empty + std::vector concat; + std::map empMap; + Assert(eq1p.getKind() == Kind::AND && eq1p.getNumChildren() == 2); + for (const Node& ee : empeqs) + { + Assert(ee.getKind() == Kind::EQUAL && ee[0].getType().isStringLike()); + concat.push_back(ee[0]); + empMap[ee[0]] = ee; + } + TypeNode stype = concat[0].getType(); + Node cc = theory::strings::utils::mkConcat(concat, stype); + Node lcc = nm->mkNode(Kind::STRING_LENGTH, cc); + TConvProofGenerator tcpg(d_env, nullptr); + Node lcci = ae.rewriteLengthIntro(lcc, &tcpg); + Trace("brc-macro") << "...normalized concat length " << lcci << std::endl; + Node lcceq = lcc.eqNode(lcci); + std::shared_ptr pfn = tcpg.getProofFor(lcceq); + cdfwd.addProof(pfn); + + // the length of the empty components should be equal to the difference + // the length of the equality before and after removing empty components + Node pnEq = lcci.eqNode(diffneqz[0]); + if (!cdfwd.addStep(pnEq, ProofRule::ARITH_POLY_NORM, {}, {pnEq})) + { + Trace("brc-macro") << "...fail poly norm " << pnEq << std::endl; + return false; + } + Node pnEq2 = lcc.eqNode(diffneqz[1]); + cdfwd.addStep(pnEq2, ProofRule::TRANS, {lcceq, pnEq, diffneqz}, {}); + // now have proven (str.len (str.++ t1 ... tn)) = 0, + // need t1 = "" ^ ... ^ tn = "" + Trace("brc-macro") << "...have " << pnEq2 << std::endl; + Node eqconv = pnEq2.eqNode(eq1p[1]); + Trace("brc-macro") << "- subgoal " << eqconv << std::endl; + // subgoal, which can be filled with RARE rules + // str-len-eq-zero-concat-rec and str-len-eq-zero-base + cdfwd.addTrustedStep(eqconv, TrustId::MACRO_THEORY_REWRITE_RCONS, {}, {}); + cdfwd.addStep(eq1p[1], ProofRule::EQ_RESOLVE, {pnEq2, eqconv}, {}); + + // proves (=> (and t="") (= (= (str.++ s t) r) (= s r))) + CDProof cdmid(d_env); + Node srcRew = eqsrc[1]; + Trace("brc-macro") << "[2] source term to rewrite " << srcRew << std::endl; + Assert(srcRew.getKind() == Kind::STRING_CONCAT); + std::vector eqe; + std::map::iterator it; + for (const Node& tc : srcRew) + { + it = empMap.find(tc); + if (it != empMap.end()) + { + eqe.push_back(it->second); + } + else + { + eqe.push_back(Node::null()); + } + } + Node cres = proveCong(&cdmid, srcRew, eqe); + if (cres.isNull()) + { + Trace("brc-macro") << "...fail cong" << std::endl; + return false; + } + Trace("brc-macro") << "...cong to " << cres[1] << std::endl; + Node tgtRew = eq1p[0][eqFlipped ? 0 : 1]; + Trace("brc-macro") << "...target is " << tgtRew << std::endl; + + Node eqacin = cres[1].eqNode(tgtRew); + if (!cdmid.addStep(eqacin, ProofRule::ACI_NORM, {}, {eqacin})) + { + Trace("brc-macro") << "...fail aci norm" << std::endl; + return false; + } + Trace("brc-macro") << "...proved subs empty " << eqacin << std::endl; + Node teq = srcRew.eqNode(tgtRew); + cdmid.addStep(teq, ProofRule::TRANS, {cres, eqacin}, {}); + + Node eqqeq = eq[0].eqNode(eq1p[0]); + std::vector eqee; + for (size_t i = 0; i < 2; i++) + { + Node eee = eq[0][i].eqNode(eq1p[0][i]); + eqee.push_back(eee); + if (eee[0] == eee[1]) + { + Node refl = eee[0].eqNode(eee[0]); + cdmid.addStep(refl, ProofRule::REFL, {}, {eee[0]}); + } + } + std::vector cargs; + ProofRule cr = expr::getCongRule(eq[0], cargs); + cdmid.addStep(eqqeq, cr, eqee, cargs); + Node implMid = nm->mkNode(Kind::IMPLIES, eq1p[1], eqqeq); + cdmid.addStep(implMid, ProofRule::SCOPE, {eqqeq}, empeqs); + Trace("brc-macro") << "...intermediate result: " << implMid << std::endl; + std::shared_ptr pfmid = cdmid.getProofFor(implMid); + Assert(implMid[1][0] == eq[0]); + Assert(implMid[1][1] == eq1p[0]); + + // finish the forward proof + cdfwd.addProof(pfmid); + cdfwd.addStep(implMid[1], ProofRule::MODUS_PONENS, {eq1p[1], implMid}, {}); + cdfwd.addStep(eq1p[0], ProofRule::EQ_RESOLVE, {eq[0], implMid[1]}, {}); + cdfwd.addStep(eq1p, ProofRule::AND_INTRO, {eq1p[0], eq1p[1]}, {}); + Node impl = nm->mkNode(Kind::IMPLIES, eq[0], eq1p); + cdfwd.addStep(impl, ProofRule::SCOPE, {eq1p}, {eq[0]}); + cdp->addProof(cdfwd.getProofFor(impl)); + + // reverse proof is easy + CDProof cdrev(d_env); + cdrev.addProof(pfmid); + cdrev.addStep(implMid[1], ProofRule::MODUS_PONENS, {eq1p[1], implMid}, {}); + Node equivs = implMid[1][1].eqNode(implMid[1][0]); + cdrev.addStep(equivs, ProofRule::SYMM, {implMid[1]}, {}); + cdrev.addStep( + implMid[1][0], ProofRule::EQ_RESOLVE, {implMid[1][1], equivs}, {}); + Node implrev = nm->mkNode(Kind::IMPLIES, eq1p, eq[0]); + cdrev.addStep(implrev, ProofRule::SCOPE, {eq[0]}, {eq1p[0], eq1p[1]}); + cdp->addProof(cdrev.getProofFor(implrev)); + + // dual implication + Node eqfinal = proveDualImplication(cdp, impl, implrev); + + // if we grouped the empty equations, we close with a transitive step + // which we added via ACI_NORM above + if (eq1p != eq[1]) + { + cdp->addStep(eq, ProofRule::TRANS, {eqfinal, eq1p.eqNode(eq[1])}, {}); + } + + return true; +} + bool BasicRewriteRCons::ensureProofMacroStrEqLenUnify(CDProof* cdp, const Node& eq) { diff --git a/src/rewriter/basic_rewrite_rcons.h b/src/rewriter/basic_rewrite_rcons.h index 3f958b847de..441756e2657 100644 --- a/src/rewriter/basic_rewrite_rcons.h +++ b/src/rewriter/basic_rewrite_rcons.h @@ -191,6 +191,16 @@ 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_EQ_LEN_UNIFY_PREFIX. + * + * @param cdp The proof to add to. + * @param eq The rewrite proven by + * ProofRewriteRule::MACRO_STR_EQ_LEN_UNIFY_PREFIX. + * @return true if added a closed proof of eq to cdp. + */ + bool ensureProofMacroStrEqLenUnifyPrefix(CDProof* cdp, const Node& eq); /** * Elaborate a rewrite eq that was proven by * ProofRewriteRule::MACRO_STR_EQ_LEN_UNIFY. diff --git a/src/theory/booleans/rewrites b/src/theory/booleans/rewrites index 555198a9f2c..7ef8e110fd0 100644 --- a/src/theory/booleans/rewrites +++ b/src/theory/booleans/rewrites @@ -14,6 +14,9 @@ (define-rule bool-impl-true2 ((t Bool)) (=> true t) t) (define-rule bool-impl-elim ((t Bool) (s Bool)) (=> t s) (or (not t) s)) +; used in proof elaboration +(define-rule bool-dual-impl-eq ((t Bool) (s Bool)) (and (=> t s) (=> s t)) (= t s)) + (define-rule bool-or-true ((xs Bool :list) (ys Bool :list)) (or xs true ys) true) (define-rule* bool-or-flatten ((xs Bool :list) (b Bool) (ys Bool :list) (zs Bool :list)) (or xs (or b ys) zs) (or xs b ys zs))