Working on rewrites for sequences

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**

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.

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)
+)

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.

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

src/smt/proof_final_callback.cpp

@@ -48,7 +48,10 @@ ProofFinalCallback::ProofFinalCallback(Env& env)
           "finalProof::trustCount")),
       d_trustTheoryIdCount(
           statisticsRegistry().registerHistogram<theory::TheoryId>(
-              "finalProof::trustTheoryIdCount")),
+              "finalProof::trustTheoryRewriteCount")),
+      d_trustTheoryLemmaCount(
+          statisticsRegistry().registerHistogram<theory::TheoryId>(
+              "finalProof::trustTheoryLemmaCount")),
       d_totalRuleCount(
           statisticsRegistry().registerInt("finalProof::totalRuleCount")),
       d_minPedanticLevel(
@@ -137,6 +140,16 @@ bool ProofFinalCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
     {
       d_trustIds << id;
       Trace("final-pf-hole") << " " << id;
+      if (id == TrustId::THEORY_LEMMA)
+      {
+        const std::vector<Node>& 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<ProofNode> 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<Node>& args = pn->getArguments();
+              if (args.size() >= 3)
+              {
+                builtin::BuiltinProofRuleChecker::getTheoryId(args[2], tid);
+              }
+            }
+          }
+        }
+        else if (r == ProofRule::TRUST_THEORY_REWRITE)
+        {
+          const std::vector<Node>& 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)
       {

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<theory::TheoryId> d_trustTheoryIdCount;
+  /**
+   * Counts number of theory ids in TRUST / THEORY_LEMMA steps.
+   */
+  HistogramStat<theory::TheoryId> d_trustTheoryLemmaCount;
   /** Total number of postprocessed rule applications */
   IntStat d_totalRuleCount;
   /** The minimum pedantic level of any rule encountered */

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();