Add lemma for the range of values of str.indexof (#3054)

This commit adds a lemma that the value of `str.indexof(x, y, n)` must
be between -1 and `str.len(x)`.

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index ba0c16d025f875f2f0d7b1996748ee9a3508288d..d37d4f9048709c32b40f2beed08818c7fa646c09 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -4022,6 +4022,15 @@ void TheoryStrings::registerTerm( Node n, int effort ) {
     Trace("strings-assert") << "(assert " << lem << ")" << std::endl;
     d_out->lemma(lem);
   }
+  else if (n.getKind() == STRING_STRIDOF)
+  {
+    Node len = mkLength(n[0]);
+    Node lem = nm->mkNode(
+        AND,
+        nm->mkNode(GEQ, n, nm->mkConst(Rational(-1))),
+        nm->mkNode(LT, n, len));
+    d_out->lemma(lem);
+  }
 }
 
 bool TheoryStrings::sendInternalInference(std::vector<Node>& exp,