diff options
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); |