Split infer info data structure in strings (#3107)

1 files changed, 16 insertions, 83 deletions

diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index a83a6ad12..e3bb2e719 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -24,6 +24,7 @@
 #include "expr/attribute.h"
 #include "expr/node_trie.h"
 #include "theory/decision_manager.h"
+#include "theory/strings/infer_info.h"
 #include "theory/strings/inference_manager.h"
 #include "theory/strings/normal_form.h"
 #include "theory/strings/regexp_elim.h"
@@ -46,55 +47,6 @@ 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);
-
 /** inference steps
  *
  * Corresponds to a step in the overall strategy of the strings solver. For
@@ -448,13 +400,6 @@ private:
   };
 
  private:
-  /** Length status, used for the registerLength function below */
-  enum LengthStatus
-  {
-    LENGTH_SPLIT,
-    LENGTH_ONE,
-    LENGTH_GEQ_ONE
-  };
 
   /** register length
    *
@@ -473,30 +418,6 @@ private:
    */
   void registerLength(Node n, LengthStatus s);
 
-  //------------------------- candidate inferences
-  class InferInfo
-  {
-   public:
-    /** for debugging
-     *
-     * The base pair of strings d_i/d_j that led to the inference, and whether
-     * (d_rev) we were processing the normal forms of these strings in reverse
-     * direction.
-     */
-    Node d_i;
-    Node d_j;
-    bool d_rev;
-    std::vector<Node> d_ant;
-    std::vector<Node> d_antn;
-    std::map<LengthStatus, std::vector<Node> > d_new_skolem;
-    Node d_conc;
-    Inference d_id;
-    std::map<Node, bool> d_pending_phase;
-    unsigned d_index;
-    Node d_nf_pair[2];
-    bool sendAsLemma();
-  };
-  //------------------------- end candidate inferences
   /** cache of all skolems */
   SkolemCache d_sk_cache;
 
@@ -739,6 +660,12 @@ private:
    */
   void assertPendingFact(Node atom, bool polarity, Node exp);
   /**
+   * This processes the infer info ii as an inference. In more detail, it calls
+   * the inference manager to process the inference, it introduces Skolems, and
+   * updates the set of normal form pairs.
+   */
+  void doInferInfo(const InferInfo& ii);
+  /**
    * Adds equality a = b to the vector exp if a and b are distinct terms. It
    * must be the case that areEqual( a, b ) holds in this context.
    */
@@ -778,9 +705,15 @@ private:
   inline Node mkConcat(const std::vector<Node>& c);
   inline Node mkLength(Node n);
 
-  /** mkExplain **/
-  Node mkExplain(std::vector<Node>& a);
-  Node mkExplain(std::vector<Node>& a, std::vector<Node>& an);
+  /** make explanation
+   *
+   * This returns a node corresponding to the explanation of formulas in a,
+   * interpreted conjunctively. The returned node is a conjunction of literals
+   * that have been asserted to the equality engine.
+   */
+  Node mkExplain(const std::vector<Node>& a);
+  /** Same as above, but the new literals an are append to the result */
+  Node mkExplain(const std::vector<Node>& a, const std::vector<Node>& an);
 
  protected: