diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-06-13 18:39:10 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-06-13 18:39:10 -0700 |
| commit | 2d478849d704f44f2a1f584dbc98d3731ca4e6ee (patch) | |
| tree | 69b4559ecf894a939c6b333f76eb2d4df340a120 | |
| parent | f61ad6919fc80cbc19fde9c295beb5082a6e0d79 (diff) | |
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)`.
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 9 |
1 files changed, 9 insertions, 0 deletions
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, |