(proof-new) Miscellaneous updates to strings from proof-new (#6557)

This includes:
(1) The type rule for `re.range` no longer insists on constant arguments, or a non-empty range. This is required for LFSC proof conversion, where re.range terms take arguments that are not (cvc5 internal) constants. 
(2) Simplifications to reductions for indexof, which fixes proof checking errors in LFSC.

6 files changed, 38 insertions, 29 deletions

diff --git a/src/theory/strings/rewrites.cpp b/src/theory/strings/rewrites.cpp
index c62c1253d..0c4e35df7 100644
--- a/src/theory/strings/rewrites.cpp
+++ b/src/theory/strings/rewrites.cpp
@@ -201,6 +201,7 @@ const char* toString(Rewrite r)
     case Rewrite::SUF_PREFIX_ELIM: return "SUF_PREFIX_ELIM";
     case Rewrite::STR_LT_ELIM: return "STR_LT_ELIM";
     case Rewrite::RE_RANGE_SINGLE: return "RE_RANGE_SINGLE";
+    case Rewrite::RE_RANGE_EMPTY: return "RE_RANGE_EMPTY";
     case Rewrite::RE_OPT_ELIM: return "RE_OPT_ELIM";
     case Rewrite::RE_PLUS_ELIM: return "RE_PLUS_ELIM";
     case Rewrite::RE_DIFF_ELIM: return "RE_DIFF_ELIM";
diff --git a/src/theory/strings/rewrites.h b/src/theory/strings/rewrites.h
index 0173d309a..482666faa 100644
--- a/src/theory/strings/rewrites.h
+++ b/src/theory/strings/rewrites.h
@@ -204,6 +204,7 @@ enum class Rewrite : uint32_t
   SUF_PREFIX_ELIM,
   STR_LT_ELIM,
   RE_RANGE_SINGLE,
+  RE_RANGE_EMPTY,
   RE_OPT_ELIM,
   RE_PLUS_ELIM,
   RE_DIFF_ELIM,
diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index d3c750185..a0e627423 100644
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -1129,13 +1129,31 @@ Node SequencesRewriter::rewriteDifferenceRegExp(TNode node)
 Node SequencesRewriter::rewriteRangeRegExp(TNode node)
 {
   Assert(node.getKind() == REGEXP_RANGE);
+  NodeManager* nm = NodeManager::currentNM();
   if (node[0] == node[1])
   {
-    NodeManager* nm = NodeManager::currentNM();
     Node retNode = nm->mkNode(STRING_TO_REGEXP, node[0]);
     // re.range( "A", "A" ) ---> str.to_re( "A" )
     return returnRewrite(node, retNode, Rewrite::RE_RANGE_SINGLE);
   }
+
+  bool appliedCh = true;
+  unsigned ch[2];
+  for (size_t i = 0; i < 2; ++i)
+  {
+    if (node[i].isConst() || node[i].getConst<String>().size() != 1)
+    {
+      appliedCh = false;
+      break;
+    }
+    ch[i] = node[i].getConst<String>().front();
+  }
+  if (appliedCh && ch[0] > ch[1])
+  {
+    // re.range( "B", "A" ) ---> re.none
+    Node retNode = nm->mkNode(REGEXP_EMPTY, {});
+    return returnRewrite(node, retNode, Rewrite::RE_RANGE_EMPTY);
+  }
   return node;
 }
 
diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp
index d7a0a0554..ced2c7dae 100644
--- a/src/theory/strings/term_registry.cpp
+++ b/src/theory/strings/term_registry.cpp
@@ -90,7 +90,7 @@ Node TermRegistry::eagerReduce(Node t, SkolemCache* sc)
   {
     // (and (>= (str.indexof x y n) (- 1)) (<= (str.indexof x y n) (str.len
     // x)))
-    Node l = utils::mkNLength(t[0]);
+    Node l = nm->mkNode(STRING_LENGTH, t[0]);
     lemma = nm->mkNode(AND,
                        nm->mkNode(GEQ, t, nm->mkConst(Rational(-1))),
                        nm->mkNode(LEQ, t, l));
@@ -176,6 +176,22 @@ void TermRegistry::preRegisterTerm(TNode n)
   {
     d_hasStrCode = true;
   }
+  else if (k == REGEXP_RANGE)
+  {
+    for (const Node& nc : n)
+    {
+      if (!nc.isConst())
+      {
+        throw LogicException(
+            "expecting a constant string term in regexp range");
+      }
+      if (nc.getConst<String>().size() != 1)
+      {
+        throw LogicException(
+            "expecting a single constant string term in regexp range");
+      }
+    }
+  }
   registerTerm(n, 0);
   TypeNode tn = n.getType();
   if (tn.isRegExp() && n.isVar())
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 1cc0736fb..d83c326c7 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -190,12 +190,6 @@ Node StringsPreprocess::reduce(Node t,
         nm->integerType(), t, SkolemCache::SK_PURIFY, "iok");
 
     Node negone = nm->mkConst(Rational(-1));
-    Node krange = nm->mkNode(GEQ, skk, negone);
-    // assert:   indexof( x, y, n ) >= -1
-    asserts.push_back(krange);
-    krange = nm->mkNode(GEQ, nm->mkNode(STRING_LENGTH, x), skk);
-    // assert:   len( x ) >= indexof( x, y, z )
-    asserts.push_back(krange);
 
     // substr( x, n, len( x ) - n )
     Node st = nm->mkNode(STRING_SUBSTR,
diff --git a/src/theory/strings/theory_strings_type_rules.cpp b/src/theory/strings/theory_strings_type_rules.cpp
index 7f7799b25..a7e891d86 100644
--- a/src/theory/strings/theory_strings_type_rules.cpp
+++ b/src/theory/strings/theory_strings_type_rules.cpp
@@ -277,8 +277,6 @@ TypeNode RegExpRangeTypeRule::computeType(NodeManager* nodeManager,
   if (check)
   {
     TNode::iterator it = n.begin();
-    unsigned ch[2];
-
     for (int i = 0; i < 2; ++i)
     {
       TypeNode t = (*it).getType(check);
@@ -287,27 +285,8 @@ TypeNode RegExpRangeTypeRule::computeType(NodeManager* nodeManager,
         throw TypeCheckingExceptionPrivate(
             n, "expecting a string term in regexp range");
       }
-      if (!(*it).isConst())
-      {
-        throw TypeCheckingExceptionPrivate(
-            n, "expecting a constant string term in regexp range");
-      }
-      if ((*it).getConst<String>().size() != 1)
-      {
-        throw TypeCheckingExceptionPrivate(
-            n, "expecting a single constant string term in regexp range");
-      }
-      unsigned ci = (*it).getConst<String>().front();
-      ch[i] = ci;
       ++it;
     }
-    if (ch[0] > ch[1])
-    {
-      throw TypeCheckingExceptionPrivate(
-          n,
-          "expecting the first constant is less or equal to the second one in "
-          "regexp range");
-    }
   }
   return nodeManager->regExpType();
 }