diff options
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
| -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, |