(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.

diff --git a/src/theory/strings/rewrites.cpp b/src/theory/strings/rewrites.cpp
index c62c1253d3370d331b6733de7d191ea2ecea0211..0c4e35df747bcd8e5e5c064529f3f28c0698c273 100644 (file)
--- 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 0173d309a850780701bf31c6b861641f2bc1a27e..482666faa386b5e43a70682f981eb293175809a6 100644 (file)
--- 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 d3c7501853ec2557b534c7b61d7b02ab37f68158..a0e627423582515b7148bd593d9ea7934ab297a5 100644 (file)
--- 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 d7a0a055466c9898c143d4f175e0a15834a166f8..ced2c7dae9199a898debfd823bb0dc80ea753ade 100644 (file)
--- 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 1cc0736fb615009d6eb072237ed313f9866f122f..d83c326c79894b63e30ad4cb916095e770c9d30f 100644 (file)
--- 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 7f7799b2522dbc31832972738c67790aea691640..a7e891d86ced8b1681e5363c167212982aaed1ab 100644 (file)
--- 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();
 }