Refactor strings extended functions inferences (#2480)

This refactors the extended function inference step of TheoryStrings. It also generalizes a data member (d_pol) so that we track extended functions that are equal to constants for any type.

This is in preparation for working on solving equations and further inferences in this style.

1 files changed, 70 insertions, 19 deletions

diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 73906d029..2fd7b3525 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -289,6 +289,25 @@ private:
   NodeList d_ee_disequalities;
 private:
   NodeSet d_congruent;
+  /**
+   * The following three vectors are used for tracking constants that each
+   * equivalence class is entailed to be equal to.
+   * - The map d_eqc_to_const maps (representatives) r of equivalence classes to
+   * the constant that that equivalence class is entailed to be equal to,
+   * - The term d_eqc_to_const_base[r] is the term in the equivalence class r
+   * that is entailed to be equal to the constant d_eqc_to_const[r],
+   * - The term d_eqc_to_const_exp[r] is the explanation of why
+   * d_eqc_to_const_base[r] is equal to d_eqc_to_const[r].
+   *
+   * For example, consider the equivalence class { r, x++"a"++y, x++z }, and
+   * assume x = "" and y = "bb" in the current context. We have that
+   *   d_eqc_to_const[r] = "abb",
+   *   d_eqc_to_const_base[r] = x++"a"++y
+   *   d_eqc_to_const_exp[r] = ( x = "" AND y = "bb" )
+   *
+   * This information is computed during checkInit and is used during various
+   * inference schemas for deriving inferences.
+   */
   std::map< Node, Node > d_eqc_to_const;
   std::map< Node, Node > d_eqc_to_const_base;
   std::map< Node, Node > d_eqc_to_const_exp;
@@ -375,24 +394,6 @@ private:
     //all variables in this term
     std::vector< Node > d_vars;
   };
-  // non-static information about extf
-  class ExtfInfoTmp {
-  public:
-    void init(){
-      d_pol = 0;
-      d_model_active = true;
-    }
-    // list of terms that something (does not) contain and their explanation
-    std::map< bool, std::vector< Node > > d_ctn;
-    std::map< bool, std::vector< Node > > d_ctn_from;
-    //polarity
-    int d_pol;
-    //explanation
-    std::vector< Node > d_exp;
-    //false if it is reduced in the model
-    bool d_model_active;
-  };
-  std::map< Node, ExtfInfoTmp > d_extf_info_tmp;
 
  private:
   /** Length status, used for the registerLength function below */
@@ -441,9 +442,59 @@ private:
   SkolemCache d_sk_cache;
 
   void checkConstantEquivalenceClasses( TermIndex* ti, std::vector< Node >& vecc );
-  void checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int effort );
   Node getSymbolicDefinition( Node n, std::vector< Node >& exp );
 
+  //--------------------------for checkExtfEval
+  /**
+   * Non-static information about an extended function t. This information is
+   * constructed and used during the check extended function evaluation
+   * inference schema.
+   *
+   * In the following, we refer to the "context-dependent simplified form"
+   * of a term t to be the result of rewriting t * sigma, where sigma is a
+   * derivable substitution in the current context. For example, the
+   * context-depdendent simplified form of contains( x++y, "a" ) given
+   * sigma = { x -> "" } is contains(y,"a").
+   */
+  class ExtfInfoTmp
+  {
+   public:
+    ExtfInfoTmp() : d_model_active(true) {}
+    /**
+     * If s is in d_ctn[true] (resp. d_ctn[false]), then contains( t, s )
+     * (resp. ~contains( t, s )) holds in the current context. The vector
+     * d_ctn_from is the explanation for why this holds. For example,
+     * if d_ctn[false][i] is "A", then d_ctn_from[false][i] might be
+     * t = x ++ y AND x = "" AND y = "B".
+     */
+    std::map<bool, std::vector<Node> > d_ctn;
+    std::map<bool, std::vector<Node> > d_ctn_from;
+    /**
+     * The constant that t is entailed to be equal to, or null if none exist.
+     */
+    Node d_const;
+    /**
+     * The explanation for why t is equal to its context-dependent simplified
+     * form.
+     */
+    std::vector<Node> d_exp;
+    /** This flag is false if t is reduced in the model. */
+    bool d_model_active;
+  };
+  /** map extended functions to the above information */
+  std::map<Node, ExtfInfoTmp> d_extf_info_tmp;
+  /** check extended function inferences
+   *
+   * This function makes additional inferences for n that do not contribute
+   * to its reduction, but may help show a refutation.
+   *
+   * This function is called when the context-depdendent simplified form of
+   * n is nr. The argument "in" is the information object for n. The argument
+   * "effort" has the same meaning as the effort argument of checkExtfEval.
+   */
+  void checkExtfInference(Node n, Node nr, ExtfInfoTmp& in, int effort);
+  //--------------------------end for checkExtfEval
+
   //--------------------------for checkFlatForm
   /**
    * This checks whether there are flat form inferences between eqc[start] and