1 files changed, 70 insertions, 2 deletions
diff --git a/src/theory/strings/infer_info.h b/src/theory/strings/infer_info.h
index 3ce673967..7fce2eaf2 100644
--- a/src/theory/strings/infer_info.h
+++ b/src/theory/strings/infer_info.h
@@ -59,10 +59,39 @@ enum class Inference : uint32_t
   // equal after e.g. removing strings that are currently empty. For example:
   //   y = "" ^ z = "" => x ++ y = z ++ x
   I_NORM,
+  // A split due to cardinality
+  CARD_SP,
   // The cardinality inference for strings, see Liang et al CAV 2014.
   CARDINALITY,
   //-------------------------------------- end base solver
   //-------------------------------------- core solver
+  // A cycle in the empty string equivalence class, e.g.:
+  //   x ++ y = "" => x = ""
+  // This is typically not applied due to length constraints implying emptiness.
+  I_CYCLE_E,
+  // A cycle in the containment ordering.
+  //   x = y ++ x => y = "" or
+  //   x = y ++ z ^ y = x ++ w => z = "" ^ w = ""
+  // This is typically not applied due to length constraints implying emptiness.
+  I_CYCLE,
+  // Flat form constant
+  //   x = y ^ x = z ++ c ... ^ y = z ++ d => false
+  // where c and d are distinct constants.
+  F_CONST,
+  // Flat form unify
+  //   x = y ^ x = z ++ x' ... ^ y = z ++ y' ^ len(x') = len(y') => x' = y'
+  // Notice flat form instances are similar to normal form inferences but do
+  // not involve recursive explanations.
+  F_UNIFY,
+  // Flat form endpoint empty
+  //   x = y ^ x = z ^ y = z ++ y' => y' = ""
+  F_ENDPOINT_EMP,
+  // Flat form endpoint equal
+  //   x = y ^ x = z ++ x' ^ y = z ++ y' => x' = y'
+  F_ENDPOINT_EQ,
+  // Flat form not contained
+  // x = c ^ x = y => false when rewrite( contains( y, c ) ) = false
+  F_NCTN,
   // Given two normal forms, infers that the remainder one of them has to be
   // empty. For example:
   //    If x1 ++ x2 = y1 and x1 = y1, then x2 = ""
@@ -119,6 +148,18 @@ enum class Inference : uint32_t
   //        for fresh u, u1, u2.
   // This is the rule F-Loop from Figure 5 of Liang et al CAV 2014.
   FLOOP,
+  // loop conflict ???
+  FLOOP_CONFLICT,
+  // Normal form inference
+  // x = y ^ z = y => x = z
+  // This is applied when y is the normal form of both x and z.
+  NORMAL_FORM,
+  // Normal form not contained, same as FFROM_NCTN but for normal forms
+  N_NCTN,
+  // Length normalization
+  //   x = y => len( x ) = len( y )
+  // Typically applied when y is the normal form of x.
+  LEN_NORM,
   // When x ++ x' ++ ... != "abc" ++ y' ++ ... ^ len(x) != len(y), we apply the
   // inference:
   //   x = "" v x != ""
@@ -152,7 +193,18 @@ enum class Inference : uint32_t
   //   ni = px ++ x ++ ... ^ nj = py ^ len(ni) = len(nj) --->
   //     x = "" ^ ...
   DEQ_NORM_EMP,
+  // When two strings are disequal s != t and the comparison of their lengths
+  // is unknown, we apply the inference:
+  //   len(s) != len(t) V len(s) = len(t)
+  DEQ_LENGTH_SP,
   //-------------------------------------- end core solver
+  //-------------------------------------- codes solver
+  // str.to_code( v ) = rewrite( str.to_code(c) )
+  // where v is the proxy variable for c.
+  CODE_PROXY,
+  // str.code(x) = -1 V str.code(x) != str.code(y) V x = y
+  CODE_INJ,
+  //-------------------------------------- end codes solver
   //-------------------------------------- regexp solver
   // regular expression normal form conflict
   //   ( x in R ^ x = y ^ rewrite((str.in_re y R)) = false ) => false
@@ -190,14 +242,30 @@ enum class Inference : uint32_t
   RE_DERIVE,
   //-------------------------------------- end regexp solver
   //-------------------------------------- extended function solver
-  // All extended function inferences from context-dependent rewriting produced
-  // by constant substitutions. See Reynolds et al CAV 2017. These are
+  // Standard extended function inferences from context-dependent rewriting
+  // produced by constant substitutions. See Reynolds et al CAV 2017. These are
   // inferences of the form:
   //   X = Y => f(X) = t   when   rewrite( f(Y) ) = t
   // where X = Y is a vector of equalities, where some of Y may be constants.
   EXTF,
   // Same as above, for normal form substitutions.
   EXTF_N,
+  // Decompositions based on extended function inferences from context-dependent
+  // rewriting produced by constant substitutions. This is like the above, but
+  // handles cases where the inferred predicate is not necessarily an equality
+  // involving f(X). For example:
+  //   x = "A" ^ contains( y ++ x, "B" ) => contains( y, "B" )
+  // This is generally only inferred if contains( y, "B" ) is a known term in
+  // the current context.
+  EXTF_D,
+  // Same as above, for normal form substitutions.
+  EXTF_D_N,
+  // Extended function equality rewrite. This is an inference of the form:
+  //   t = s => P
+  // where P is a predicate implied by rewrite( t = s ).
+  // Typically, t is an application of an extended function and s is a constant.
+  // It is generally only inferred if P is a predicate over known terms.
+  EXTF_EQ_REW,
   // contain transitive
   //   ( str.contains( s, t ) ^ ~contains( s, r ) ) => ~contains( t, r ).
   CTN_TRANS,