From 89024b9d8ef08f58de22943ea1756610c394d7bc Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Mon, 21 Oct 2024 15:27:43 -0500
Subject: [PATCH] More

---
 src/proof/alf/alf_printer.cpp             |  1 +
 src/theory/strings/rewrites               | 23 ++++++++++++-----------
 src/theory/strings/sequences_rewriter.cpp | 23 +++++++++++++++++++----
 3 files changed, 32 insertions(+), 15 deletions(-)

diff --git a/src/proof/alf/alf_printer.cpp b/src/proof/alf/alf_printer.cpp
index 435a767e4cd..9018f796143 100644
--- a/src/proof/alf/alf_printer.cpp
+++ b/src/proof/alf/alf_printer.cpp
@@ -259,6 +259,7 @@ bool AlfPrinter::isHandledTheoryRewrite(ProofRewriteRule id,
     case ProofRewriteRule::STR_IN_RE_SIGMA:
     case ProofRewriteRule::STR_IN_RE_SIGMA_STAR:
     case ProofRewriteRule::STR_IN_RE_CONSUME:
+    case ProofRewriteRule::SEQ_LENGTH_EVAL:
     case ProofRewriteRule::RE_INTER_UNION_INCLUSION:
     case ProofRewriteRule::BV_BITWISE_SLICING: return true;
     case ProofRewriteRule::STR_IN_RE_EVAL:
diff --git a/src/theory/strings/rewrites b/src/theory/strings/rewrites
index 94ede9b8588..1158ede47bf 100644
--- a/src/theory/strings/rewrites
+++ b/src/theory/strings/rewrites
@@ -39,14 +39,18 @@
   (= (str.++ x2 (str.++ x1 x)) y)
   (= y (str.++ x2 x1 x)))
 
-(define-rule str-substr-empty-str ((n Int) (m Int)) (str.substr "" n m) "")
+(define-cond-rule str-substr-empty-str ((r ?Seq) (n Int) (m Int))
+  (= (str.len r) 0)
+  (str.substr r n m)
+  r
+)
 (define-cond-rule str-substr-empty-range ((x String) (n Int) (m Int)) (>= 0 m) (str.substr x n m) "")
 (define-cond-rule str-substr-empty-start ((x String) (n Int) (m Int)) (>= n (str.len x)) (str.substr x n m) "")
 (define-cond-rule str-substr-empty-start-neg ((x String) (n Int) (m Int)) (< n 0) (str.substr x n m) "")
-(define-cond-rule str-substr-eq-empty ((s String) (n Int) (m Int))
-  (and (= n 0) (> m n))
-  (= (str.substr s n m) "")
-  (= s ""))
+(define-cond-rule str-substr-eq-empty ((s ?Seq) (r ?Seq) (n Int) (m Int))
+  (and (= n 0) (> m n) (= (str.len r) 0))
+  (= (str.substr s n m) r)
+  (= s r))
 
 (define-cond-rule str-len-replace-inv ((t ?Seq) (s ?Seq) (r ?Seq)) 
   (= (str.len s) (str.len r))
@@ -203,10 +207,6 @@
   (str.contains x y)
   (= x y))
 
-(define-rule str-concat-emp ((xs String :list) (ys String :list)) 
-  (str.++ xs "" ys) 
-  (str.++ xs ys))
-
 (define-rule str-at-elim ((x ?Seq) (n Int)) (str.at x n) (str.substr x n 1))
 
 ; not effective since due to not proving inequalities on length
@@ -224,8 +224,9 @@
   (str.replace t s r)
   t)
 
-(define-rule str-replace-empty ((t ?Seq) (s ?Seq))
-  (str.replace t "" s)
+(define-cond-rule str-replace-empty ((t ?Seq) (s ?Seq) (r ?Seq))
+  (= (str.len r) 0)
+  (str.replace t r s)
   (str.++ s t))
 
 (define-rule* str-len-concat-rec ((s1 ?Seq) (s2 ?Seq) (s3 ?Seq :list))
diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index f3e6c5cc8a6..075a1662914 100644
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -65,8 +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);
+  registerProofRewriteRule(ProofRewriteRule::SEQ_LENGTH_EVAL,
+                           TheoryRewriteCtx::DSL_SUBCALL);
 }
 
 Node SequencesRewriter::rewriteViaRule(ProofRewriteRule id, const Node& n)
@@ -95,9 +95,24 @@ Node SequencesRewriter::rewriteViaRule(ProofRewriteRule id, const Node& n)
     }
     case ProofRewriteRule::SEQ_LENGTH_EVAL:
     {
-      if (n.getKind()==Kind::STRING_LENGTH && n[0].getKind()==Kind::CONST_SEQUENCE)
+      if (n.getKind()==Kind::STRING_LENGTH)
       {
-        return nm->mkConstInt(Rational(Word::getLength(node[0])));
+        if (n[0].getKind()==Kind::CONST_SEQUENCE)
+        {
+          return nodeManager()->mkConstInt(Rational(Word::getLength(n[0])));
+        }
+        // maybe after converting to its node form
+        if (n[0].getKind()==Kind::STRING_CONCAT)
+        {
+          for (const Node& nc : n[0])
+          {
+            if (nc.getKind()!=Kind::SEQ_UNIT)
+            {
+              return Node::null();
+            }
+          }
+          return nodeManager()->mkConstInt(Rational(n[0].getNumChildren()));
+        }
       }
     }
     default: break;