Document inferences for strings (#1642)

1 files changed, 50 insertions, 15 deletions

diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 5dbbb93d6..2dcb3ebc8 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -44,6 +44,55 @@ namespace strings {
  *
  */
 
+/** Types of inferences used in the procedure
+ *
+ * These are variants of the inference rules in Figures 3-5 of Liang et al.
+ * "A DPLL(T) Solver for a Theory of Strings and Regular Expressions", CAV 2014.
+ */
+enum Inference
+{
+  INFER_NONE,
+  // string split constant propagation, for example:
+  //     x = y, x = "abc", y = y1 ++ "b" ++ y2
+  //       implies y1 = "a" ++ y1'
+  INFER_SSPLIT_CST_PROP,
+  // string split variable propagation, for example:
+  //     x = y, x = x1 ++ x2, y = y1 ++ y2, len( x1 ) >= len( y1 )
+  //       implies x1 = y1 ++ x1'
+  // This is inspired by Zheng et al CAV 2015.
+  INFER_SSPLIT_VAR_PROP,
+  // length split, for example:
+  //     len( x1 ) = len( y1 ) V len( x1 ) != len( y1 )
+  // This is inferred when e.g. x = y, x = x1 ++ x2, y = y1 ++ y2.
+  INFER_LEN_SPLIT,
+  // length split empty, for example:
+  //     z = "" V z != ""
+  // This is inferred when, e.g. x = y, x = z ++ x1, y = y1 ++ z
+  INFER_LEN_SPLIT_EMP,
+  // string split constant binary, for example:
+  //     x1 = "aaaa" ++ x1' V "aaaa" = x1 ++ x1'
+  // This is inferred when, e.g. x = y, x = x1 ++ x2, y = "aaaaaaaa" ++ y2.
+  // This inference is disabled by default and is enabled by stringBinaryCsp().
+  INFER_SSPLIT_CST_BINARY,
+  // string split constant
+  //    x = y, x = "c" ++ x2, y = y1 ++ y2, y1 != ""
+  //      implies y1 = "c" ++ y1'
+  // This is a special case of F-Split in Figure 5 of Liang et al CAV 2014.
+  INFER_SSPLIT_CST,
+  // string split variable, for example:
+  //    x = y, x = x1 ++ x2, y = y1 ++ y2
+  //      implies x1 = y1 ++ x1' V y1 = x1 ++ y1'
+  // This is rule F-Split in Figure 5 of Liang et al CAV 2014.
+  INFER_SSPLIT_VAR,
+  // flat form loop, for example:
+  //    x = y, x = x1 ++ z, y = z ++ y2
+  //      implies z = u2 ++ u1, u in ( u1 ++ u2 )*, x1 = u2 ++ u, y2 = u ++ u1
+  //        for fresh u, u1, u2.
+  // This is the rule F-Loop from Figure 5 of Liang et al CAV 2014.
+  INFER_FLOOP,
+};
+std::ostream& operator<<(std::ostream& out, Inference i);
+
 struct StringsProxyVarAttributeId {};
 typedef expr::Attribute< StringsProxyVarAttributeId, bool > StringsProxyVarAttribute;
 
@@ -300,23 +349,9 @@ private:
     std::vector< Node > d_antn;
     std::map< int, std::vector< Node > > d_new_skolem;
     Node d_conc;
-    unsigned d_id;
+    Inference d_id;
     std::map< Node, bool > d_pending_phase;
     unsigned d_index;
-    const char * getId() { 
-      switch( d_id ){
-      case 1:return "S-Split(CST-P)-prop";break;
-      case 2:return "S-Split(VAR)-prop";break;
-      case 3:return "Len-Split(Len)";break;
-      case 4:return "Len-Split(Emp)";break;
-      case 5:return "S-Split(CST-P)-binary";break;
-      case 6:return "S-Split(CST-P)";break;
-      case 7:return "S-Split(VAR)";break;
-      case 8:return "F-Loop";break;
-      default:break;
-      }
-      return "";
-    }
     Node d_nf_pair[2];
     bool sendAsLemma();
   };