Make string length lemmas more robust to rewriting (#2150)

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