Extended rewriter for string equalities (#2427)

1 files changed, 11 insertions, 1 deletions

diff --git a/src/theory/quantifiers/extended_rewrite.h b/src/theory/quantifiers/extended_rewrite.h
index 29f3b7bb3..da77bda51 100644
--- a/src/theory/quantifiers/extended_rewrite.h
+++ b/src/theory/quantifiers/extended_rewrite.h
@@ -231,8 +231,18 @@ class ExtendedRewriter
   //--------------------------------------end generic utilities
 
   //--------------------------------------theory-specific top-level calls
-  /** extended rewrite arith */
+  /** extended rewrite arith
+   *
+   * If this method returns a non-null node ret', then ret is equivalent to
+   * ret'.
+   */
   Node extendedRewriteArith(Node ret);
+  /** extended rewrite strings
+   *
+   * If this method returns a non-null node ret', then ret is equivalent to
+   * ret'.
+   */
+  Node extendedRewriteStrings(Node ret);
   //--------------------------------------end theory-specific top-level calls
 };