From 2d478849d704f44f2a1f584dbc98d3731ca4e6ee Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Thu, 13 Jun 2019 18:39:10 -0700
Subject: [PATCH] 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)`.
---
 src/theory/strings/theory_strings.cpp | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index ba0c16d02..d37d4f904 100644
--- 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,
-- 
2.30.2