From 9f7d01fa038ffeacd06bfcfad49e3cbab720dabb Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 21 Oct 2024 15:04:13 -0500 Subject: [PATCH] Working on rewrites for sequences --- include/cvc5/cvc5_proof_rule.h | 12 ++++++ proofs/eo/cpc/programs/Strings.eo | 12 ++++++ proofs/eo/cpc/rules/Strings.eo | 12 ++++++ proofs/eo/cpc/theories/Strings.eo | 2 +- src/api/cpp/cvc5_proof_rule_template.cpp | 2 + src/smt/proof_final_callback.cpp | 52 +++++++++++++++++++++-- src/smt/proof_final_callback.h | 4 ++ src/theory/strings/sequences_rewriter.cpp | 9 ++++ 8 files changed, 101 insertions(+), 4 deletions(-) diff --git a/include/cvc5/cvc5_proof_rule.h b/include/cvc5/cvc5_proof_rule.h index 00aecd89d91..fedb027599e 100644 --- a/include/cvc5/cvc5_proof_rule.h +++ b/include/cvc5/cvc5_proof_rule.h @@ -2738,6 +2738,18 @@ enum ENUM(ProofRewriteRule) * \endverbatim */ EVALUE(MACRO_SUBSTR_STRIP_SYM_LENGTH), + /** + * \verbatim embed:rst:leading-asterisk + * **Sequences - sequence length eval** + * + * .. math:: + * \mathit{len}(c) = n + * + * where :math:`c` is concatenation of :math:`seq.unit` terms of length :math:`n`. + * + * \endverbatim + */ + EVALUE(SEQ_LENGTH_EVAL), /** * \verbatim embed:rst:leading-asterisk * **Sets - empty tester evaluation** diff --git a/proofs/eo/cpc/programs/Strings.eo b/proofs/eo/cpc/programs/Strings.eo index 772dd60a9e8..5c0a84f558d 100644 --- a/proofs/eo/cpc/programs/Strings.eo +++ b/proofs/eo/cpc/programs/Strings.eo @@ -22,6 +22,18 @@ ) ) +; program: $seq_is_units_concat +; args: +; - s (Seq U): a sequence term +; return: true if s is a concatenation of units. +(program $seq_is_units_concat ((U Type) (s (Seq U) :list) (u U)) + (U) Bool + ( + (($seq_is_units_concat (seq.++ (seq.unit u) s)) ($seq_is_units_concat s)) + (($seq_is_units_concat (seq.empty U)) true) + ) +) + ; define: $char_type_of ; args: ; - T Type: The string-like type to check. diff --git a/proofs/eo/cpc/rules/Strings.eo b/proofs/eo/cpc/rules/Strings.eo index 33ff694c9ad..2fb778f7286 100644 --- a/proofs/eo/cpc/rules/Strings.eo +++ b/proofs/eo/cpc/rules/Strings.eo @@ -567,3 +567,15 @@ :requires ((($str_mk_str_in_re_sigma_star s r) b)) :conclusion (= (str.in_re s (re.* r)) b) ) +; rule: seq-length-eval +; implements: ProofRewriteRule::SEQ_LENGTH_EVAL +; args: +; - eq Bool: The equality between the length of a sequence and a constant integer. +; requires: > +; The right hand side of the equality is a concatenation of units having length n. +; conclusion: The given equality. +(declare-rule seq-length-eval ((T Type) (s (Seq T)) (n Int)) + :args ((= (seq.len s) n)) + :requires ((($seq_is_units_concat s) true) ((eo::list_len seq.++ s) n)) + :conclusion (= (seq.len s) n) +) diff --git a/proofs/eo/cpc/theories/Strings.eo b/proofs/eo/cpc/theories/Strings.eo index 3cb12a508ec..fc6b3d8dcc8 100644 --- a/proofs/eo/cpc/theories/Strings.eo +++ b/proofs/eo/cpc/theories/Strings.eo @@ -134,7 +134,7 @@ ; disclaimer: This function is not in SMT-LIB. (declare-const seq.unit (-> (! Type :var T :implicit) T (Seq T))) ; disclaimer: This function is not in SMT-LIB. -(declare-const seq.nth (-> (! Type :var T :implicit) (Seq T) Int (eo::ite (eo::is_eq T Char) Int T))) +(declare-const seq.nth (-> (! Type :var T :implicit) (Seq T) Int T)) ; Sequence operators are automatically translated to the string operators. ; disclaimer: This function is not in SMT-LIB. diff --git a/src/api/cpp/cvc5_proof_rule_template.cpp b/src/api/cpp/cvc5_proof_rule_template.cpp index 053f0b58d80..63af8b0e24f 100644 --- a/src/api/cpp/cvc5_proof_rule_template.cpp +++ b/src/api/cpp/cvc5_proof_rule_template.cpp @@ -263,6 +263,8 @@ const char* toString(cvc5::ProofRewriteRule rule) case ProofRewriteRule::STR_IN_RE_SIGMA_STAR: return "str-in-re-sigma-star"; case ProofRewriteRule::MACRO_SUBSTR_STRIP_SYM_LENGTH: return "macro-substr-strip-sym-length"; + case ProofRewriteRule::SEQ_LENGTH_EVAL: + return "seq-length-eval"; case ProofRewriteRule::SETS_IS_EMPTY_EVAL: return "sets-is-empty-eval"; //================================================= RARE rules diff --git a/src/smt/proof_final_callback.cpp b/src/smt/proof_final_callback.cpp index f4f72e8bfe3..bf5fc63a74e 100644 --- a/src/smt/proof_final_callback.cpp +++ b/src/smt/proof_final_callback.cpp @@ -48,7 +48,10 @@ ProofFinalCallback::ProofFinalCallback(Env& env) "finalProof::trustCount")), d_trustTheoryIdCount( statisticsRegistry().registerHistogram( - "finalProof::trustTheoryIdCount")), + "finalProof::trustTheoryRewriteCount")), + d_trustTheoryLemmaCount( + statisticsRegistry().registerHistogram( + "finalProof::trustTheoryLemmaCount")), d_totalRuleCount( statisticsRegistry().registerInt("finalProof::totalRuleCount")), d_minPedanticLevel( @@ -137,6 +140,16 @@ bool ProofFinalCallback::shouldUpdate(std::shared_ptr pn, { d_trustIds << id; Trace("final-pf-hole") << " " << id; + if (id == TrustId::THEORY_LEMMA) + { + const std::vector& args = pn->getArguments(); + TheoryId tid = THEORY_BUILTIN; + if (args.size() >= 3) + { + builtin::BuiltinProofRuleChecker::getTheoryId(args[2], tid); + } + d_trustTheoryLemmaCount << tid; + } } Trace("final-pf-hole") << ": " << pn->getResult() << std::endl; } @@ -178,11 +191,44 @@ bool ProofFinalCallback::shouldUpdate(std::shared_ptr pn, premises.push_back(pncc->getResult()); } NodeManager* nm = nodeManager(); - Node query = nm->mkNode(Kind::IMPLIES, nm->mkAnd(premises), conc); + Node query = conc; + if (!premises.empty()) + { + query = nm->mkNode(Kind::IMPLIES, nm->mkAnd(premises), query); + } + // print the trusted step information if (isOutputOn(OutputTag::TRUSTED_PROOF_STEPS)) { output(OutputTag::TRUSTED_PROOF_STEPS) - << "(trusted-proof-step " << query << ")" << std::endl; + << "(trusted-proof-step " << query; + output(OutputTag::TRUSTED_PROOF_STEPS) << " :rule " << r; + TheoryId tid = THEORY_LAST; + if (r == ProofRule::TRUST) + { + TrustId id; + if (getTrustId(pn->getArguments()[0], id)) + { + output(OutputTag::TRUSTED_PROOF_STEPS) << " :trust-id " << id; + if (id == TrustId::THEORY_LEMMA) + { + const std::vector& args = pn->getArguments(); + if (args.size() >= 3) + { + builtin::BuiltinProofRuleChecker::getTheoryId(args[2], tid); + } + } + } + } + else if (r == ProofRule::TRUST_THEORY_REWRITE) + { + const std::vector& args = pn->getArguments(); + builtin::BuiltinProofRuleChecker::getTheoryId(args[1], tid); + } + if (tid != THEORY_LAST) + { + output(OutputTag::TRUSTED_PROOF_STEPS) << " :theory " << tid; + } + output(OutputTag::TRUSTED_PROOF_STEPS) << ")" << std::endl; } if (options().proof.checkProofSteps) { diff --git a/src/smt/proof_final_callback.h b/src/smt/proof_final_callback.h index 7e80a346bfc..cee7343310a 100644 --- a/src/smt/proof_final_callback.h +++ b/src/smt/proof_final_callback.h @@ -74,6 +74,10 @@ class ProofFinalCallback : protected EnvObj, public ProofNodeUpdaterCallback * Counts number of theory ids in TRUST_THEORY_REWRITE steps. */ HistogramStat d_trustTheoryIdCount; + /** + * Counts number of theory ids in TRUST / THEORY_LEMMA steps. + */ + HistogramStat d_trustTheoryLemmaCount; /** Total number of postprocessed rule applications */ IntStat d_totalRuleCount; /** The minimum pedantic level of any rule encountered */ diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index b57f0e59d11..f3e6c5cc8a6 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -65,6 +65,8 @@ SequencesRewriter::SequencesRewriter(NodeManager* nm, TheoryRewriteCtx::PRE_DSL); registerProofRewriteRule(ProofRewriteRule::MACRO_SUBSTR_STRIP_SYM_LENGTH, TheoryRewriteCtx::POST_DSL); + registerProofRewriteRule(ProofRewriteRule::SEQ_EMPTY_LEN_EVAL, + TheoryRewriteCtx::PRE_DSL); } Node SequencesRewriter::rewriteViaRule(ProofRewriteRule id, const Node& n) @@ -91,6 +93,13 @@ Node SequencesRewriter::rewriteViaRule(ProofRewriteRule id, const Node& n) StringsEntail sent(nullptr, ae, nullptr); return rewriteViaMacroSubstrStripSymLength(n, rule, sent); } + case ProofRewriteRule::SEQ_LENGTH_EVAL: + { + if (n.getKind()==Kind::STRING_LENGTH && n[0].getKind()==Kind::CONST_SEQUENCE) + { + return nm->mkConstInt(Rational(Word::getLength(node[0]))); + } + } default: break; } return Node::null();