Refactor strings to use an inference manager object (#3076)

1 files changed, 44 insertions, 107 deletions

diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 8371a27ea..a83a6ad12 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/inference_manager.h"
 #include "theory/strings/normal_form.h"
 #include "theory/strings/regexp_elim.h"
 #include "theory/strings/regexp_operation.h"
@@ -135,6 +136,7 @@ struct StringsProxyVarAttributeId {};
 typedef expr::Attribute< StringsProxyVarAttributeId, bool > StringsProxyVarAttribute;
 
 class TheoryStrings : public Theory {
+  friend class InferenceManager;
   typedef context::CDList<Node> NodeList;
   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
   typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
@@ -298,16 +300,10 @@ class TheoryStrings : public Theory {
   NotifyClass d_notify;
   /** Equaltity engine */
   eq::EqualityEngine d_equalityEngine;
+  /** The (custom) output channel of the theory of strings */
+  InferenceManager d_im;
   /** Are we in conflict */
   context::CDO<bool> d_conflict;
-  //list of pairs of nodes to merge
-  std::map< Node, Node > d_pending_exp;
-  std::vector< Node > d_pending;
-  std::vector< Node > d_lemma_cache;
-  std::map< Node, bool > d_pending_req_phase;
-  /** inferences: maintained to ensure ref count for internally introduced nodes */
-  NodeList d_infer;
-  NodeList d_infer_exp;
   /** map from terms to their normal forms */
   std::map<Node, NormalForm> d_normal_form;
   /** get normal form */
@@ -421,8 +417,21 @@ private:
    * should currently be a representative of the equality engine of this class.
    */
   EqcInfo * getOrMakeEqcInfo( Node eqc, bool doMake = true );
-  //maintain which concat terms have the length lemma instantiated
+  /**
+   * Map string terms to their "proxy variables". Proxy variables are used are
+   * intermediate variables so that length information can be communicated for
+   * constants. For example, to communicate that "ABC" has length 3, we
+   * introduce a proxy variable v_{"ABC"} for "ABC", and assert:
+   *   v_{"ABC"} = "ABC" ^ len( v_{"ABC"} ) = 3
+   * Notice this is required since we cannot directly write len( "ABC" ) = 3,
+   * which rewrites to 3 = 3.
+   * In the above example, we store "ABC" -> v_{"ABC"} in this map.
+   */
   NodeNodeMap d_proxy_var;
+  /**
+   * Map from proxy variables to their normalized length. In the above example,
+   * we store "ABC" -> 3.
+   */
   NodeNodeMap d_proxy_var_to_length;
   /** All the function terms that the theory has seen */
   context::CDList<TNode> d_functionsTerms;
@@ -492,7 +501,23 @@ private:
   SkolemCache d_sk_cache;
 
   void checkConstantEquivalenceClasses( TermIndex* ti, std::vector< Node >& vecc );
-  Node getSymbolicDefinition( Node n, std::vector< Node >& exp );
+  /** Get proxy variable
+   *
+   * If this method returns the proxy variable for (string) term n if one
+   * exists, otherwise it returns null.
+   */
+  Node getProxyVariableFor(Node n) const;
+  /** Get symbolic definition
+   *
+   * This method returns the "symbolic definition" of n, call it n', and
+   * populates the vector exp with an explanation such that exp => n = n'.
+   *
+   * The symbolic definition of n is the term where (maximal) subterms of n
+   * are replaced by their proxy variables. For example, if we introduced
+   * proxy variable v for x ++ y, then given input x ++ y = w, this method
+   * returns v = w and adds v = x ++ y to exp.
+   */
+  Node getSymbolicDefinition(Node n, std::vector<Node>& exp) const;
 
   //--------------------------for checkExtfEval
   /**
@@ -704,11 +729,15 @@ private:
    */
   bool areCareDisequal(TNode x, TNode y);
 
-  // do pending merges
+  /** assert pending fact
+   *
+   * This asserts atom with polarity to the equality engine of this class,
+   * where exp is the explanation of why (~) atom holds.
+   *
+   * This call may trigger further initialization steps involving the terms
+   * of atom, including calls to registerTerm.
+   */
   void assertPendingFact(Node atom, bool polarity, Node exp);
-  void doPendingFacts();
-  void doPendingLemmas();
-  bool hasProcessed();
   /**
    * 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.
@@ -736,98 +765,13 @@ private:
    * effort, the call to this method does nothing.
    */
   void registerTerm(Node n, int effort);
-  //-------------------------------------send inferences
- public:
-  /** send internal inferences
-   *
-   * This is called when we have inferred exp => conc, where exp is a set
-   * of equalities and disequalities that hold in the current equality engine.
-   * This method adds equalities and disequalities ~( s = t ) via
-   * sendInference such that both s and t are either constants or terms
-   * that already occur in the equality engine, and ~( s = t ) is a consequence
-   * of conc. This function can be seen as a "conservative" version of
-   * sendInference below in that it does not introduce any new non-constant
-   * terms to the state.
-   *
-   * The argument c is a string identifying the reason for the inference.
-   * This string is used for debugging purposes.
-   *
-   * Return true if the inference is complete, in the sense that we infer
-   * inferences that are equivalent to conc. This returns false e.g. if conc
-   * (or one of its conjuncts if it is a conjunction) was not inferred due
-   * to the criteria mentioned above.
-   */
-  bool sendInternalInference(std::vector<Node>& exp, Node conc, const char* c);
-  /** send inference
-   *
-   * This function should be called when ( exp ^ exp_n ) => eq. The set exp
-   * contains literals that are explainable by this class, i.e. those that
-   * hold in the equality engine of this class. On the other hand, the set
-   * exp_n ("explanations new") contain nodes that are not explainable by this
-   * class. This method may call sendInfer or sendLemma. Overall, the result
-   * of this method is one of the following:
-   *
-   * [1] (No-op) Do nothing if eq is true,
-   *
-   * [2] (Infer) Indicate that eq should be added to the equality engine of this
-   * class with explanation EXPLAIN(exp), where EXPLAIN returns the
-   * explanation of the node in exp in terms of the literals asserted to this
-   * class,
-   *
-   * [3] (Lemma) Indicate that the lemma ( EXPLAIN(exp) ^ exp_n ) => eq should
-   * be sent on the output channel of this class, or
-   *
-   * [4] (Conflict) Immediately report a conflict EXPLAIN(exp) on the output
-   * channel of this class.
-   *
-   * Determining which case to apply depends on the form of eq and whether
-   * exp_n is empty. In particular, lemmas must be used whenever exp_n is
-   * non-empty, conflicts are used when exp_n is empty and eq is false.
-   *
-   * The argument c is a string identifying the reason for inference, used for
-   * debugging.
-   *
-   * If the flag asLemma is true, then this method will send a lemma instead
-   * of an inference whenever applicable.
-   */
-  void sendInference(std::vector<Node>& exp,
-                     std::vector<Node>& exp_n,
-                     Node eq,
-                     const char* c,
-                     bool asLemma = false);
-  /** same as above, but where exp_n is empty */
-  void sendInference(std::vector<Node>& exp,
-                     Node eq,
-                     const char* c,
-                     bool asLemma = false);
+
   /**
    * Are we in conflict? This returns true if this theory has called its output
    * channel's conflict method in the current SAT context.
    */
   bool inConflict() const { return d_conflict; }
 
- protected:
-  /**
-   * Indicates that ant => conc should be sent on the output channel of this
-   * class. This will either trigger an immediate call to the conflict
-   * method of the output channel of this class of conc is false, or adds the
-   * above lemma to the lemma cache d_lemma_cache, which may be flushed
-   * later within the current call to TheoryStrings::check.
-   *
-   * The argument c is a string identifying the reason for inference, used for
-   * debugging.
-   */
-  void sendLemma(Node ant, Node conc, const char* c);
-  /**
-   * Indicates that conc should be added to the equality engine of this class
-   * with explanation eq_exp. It must be the case that eq_exp is a (conjunction
-   * of) literals that each are explainable, i.e. they already hold in the
-   * equality engine of this class.
-   */
-  void sendInfer(Node eq_exp, Node eq, const char* c);
-  bool sendSplit(Node a, Node b, const char* c, bool preq = true);
-  //-------------------------------------end send inferences
-
   /** mkConcat **/
   inline Node mkConcat(Node n1, Node n2);
   inline Node mkConcat(Node n1, Node n2, Node n3);
@@ -839,8 +783,6 @@ private:
   Node mkExplain(std::vector<Node>& a, std::vector<Node>& an);
 
  protected:
-  /** mkAnd **/
-  Node mkAnd(std::vector<Node>& a);
 
   /** get equivalence classes
    *
@@ -861,11 +803,6 @@ private:
                         std::vector<Node>& lts);
   void printConcat(std::vector<Node>& n, const char* c);
 
-  void inferSubstitutionProxyVars(Node n,
-                                  std::vector<Node>& vars,
-                                  std::vector<Node>& subs,
-                                  std::vector<Node>& unproc);
-
   // Symbolic Regular Expression
  private:
   /** regular expression solver module */