From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Fri, 14 Jun 2019 01:39:10 +0000 (-0700)
Subject: Add lemma for the range of values of str.indexof (#3054)
X-Git-Tag: cvc5-1.0.0~4110
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2d478849d704f44f2a1f584dbc98d3731ca4e6ee;p=cvc5.git

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 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,