diff options
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index afdf6821f..5adae11e2 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -3953,6 +3953,23 @@ void TheoryStrings::registerTerm( Node n, int effort ) { // can register length term if it does not rewrite if (lsum == lsumb) { + if (n.getKind() == STRING_STRREPL) + { + Node len = mkLength(n[0]); + Node cond = nm->mkNode(GEQ, mkLength(n[1]), mkLength(n[2])); + Node lem = nm->mkNode( + ITE, + cond, + nm->mkNode(LEQ, lsum, len), + nm->mkNode( + LEQ, + lsum, + nm->mkNode( + PLUS, + len, + nm->mkNode(MINUS, mkLength(n[2]), mkLength(n[1]))))); + d_out->lemma(lem); + } registerLength(n, LENGTH_SPLIT); return; } |