diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-07-05 17:22:53 +0100 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-07-05 09:22:53 -0700 |
commit | ceba90a89f878cda01067042ca9a0dfee555b7cd (patch) | |
tree | fc1aaecc4eae3a83edaa5bcc7a254cd3ef65d205 /src/theory/strings/theory_strings.h | |
parent | dc8cbd0728630db5a3bc566a9cd627bcb122dda2 (diff) |
Make string length lemmas more robust to rewriting (#2150)
Diffstat (limited to 'src/theory/strings/theory_strings.h')
-rw-r--r-- | src/theory/strings/theory_strings.h | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 0d4b1f282..de505f262 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -532,6 +532,15 @@ private: void sendLemma(Node ant, Node conc, const char* c); void sendInfer(Node eq_exp, Node eq, const char* c); bool sendSplit(Node a, Node b, const char* c, bool preq = true); + /** send length lemma + * + * This method is called on non-constant string terms n. It sends a lemma + * on the output channel that ensures that len( n ) >= 0. In particular, the + * this lemma is typically of the form: + * ( n = "" ^ len( n ) = 0 ) OR len( n ) > 0 + * This method also ensures that, when applicable, the left branch is taken + * first via calls to requirePhase. + */ void sendLengthLemma(Node n); /** mkConcat **/ inline Node mkConcat(Node n1, Node n2); |