diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-06-11 18:25:07 -0700 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-06-11 18:25:07 -0700 |
commit | 3f489edfc287678dd2f8c70eea1356b92eb1fa1c (patch) | |
tree | b4a53294816afcbf1b2f1e89c17ae95503aaec65 /src/theory/strings/theory_strings.cpp | |
parent | 2907e3b429abfa334e219dbbbaa0641ea1b7bf7b (diff) |
replace lemmaaddLemmas
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; } |