Solver state for theory of strings (#3181)

This refactors the theory of strings to use a solver state object, which manages state information regarding assertions.

It also deletes some unused/undefined functions in theory_strings.h.

There are no major changes to the behavior of the code or its documentation in this PR.

This is work towards #1881.

1 files changed, 8 insertions, 151 deletions

diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 94811636c..9db40f8fe 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -31,6 +31,7 @@
 #include "theory/strings/regexp_operation.h"
 #include "theory/strings/regexp_solver.h"
 #include "theory/strings/skolem_cache.h"
+#include "theory/strings/solver_state.h"
 #include "theory/strings/theory_strings_preprocess.h"
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
@@ -191,42 +192,7 @@ class TheoryStrings : public Theory {
     }
   };/* class TheoryStrings::NotifyClass */
 
-  //--------------------------- equality engine
-  /**
-   * Get the representative of t in the equality engine of this class, or t
-   * itself if it is not registered as a term.
-   */
-  Node getRepresentative(Node t);
-  /** Is t registered as a term in the equality engine of this class? */
-  bool hasTerm(Node a);
-  /**
-   * Are a and b equal according to the equality engine of this class? Also
-   * returns true if a and b are identical.
-   */
-  bool areEqual(Node a, Node b);
-  /**
-   * Are a and b disequal according to the equality engine of this class? Also
-   * returns true if the representative of a and b are distinct constants.
-   */
-  bool areDisequal(Node a, Node b);
-  //--------------------------- end equality engine
-
   //--------------------------- helper functions
-  /** get length with explanation
-   *
-   * If possible, this returns an arithmetic term that exists in the current
-   * context that is equal to the length of te, or otherwise returns the
-   * length of t. It adds to exp literals that hold in the current context that
-   * explain why that term is equal to the length of t. For example, if
-   * we have assertions:
-   *   len( x ) = 5 ^ z = x ^ x = y,
-   * then getLengthExp( z, exp, y ) returns len( x ) and adds { z = x } to
-   * exp. On the other hand, getLengthExp( z, exp, x ) returns len( x ) and
-   * adds nothing to exp.
-   */
-  Node getLengthExp(Node t, std::vector<Node>& exp, Node te);
-  /** shorthand for getLengthExp(t, exp, t) */
-  Node getLength(Node t, std::vector<Node>& exp);
   /** get normal string
    *
    * This method returns the node that is equivalent to the normal form of x,
@@ -252,12 +218,12 @@ class TheoryStrings : public Theory {
   NotifyClass d_notify;
   /** Equaltity engine */
   eq::EqualityEngine d_equalityEngine;
+  /** The solver state object */
+  SolverState d_state;
   /** The (custom) output channel of the theory of strings */
   InferenceManager d_im;
   /** Are we in conflict */
   context::CDO<bool> d_conflict;
-  /** Pending conflict */
-  context::CDO<Node> d_pendingConflict;
   /** map from terms to their normal forms */
   std::map<Node, NormalForm> d_normal_form;
   /** get normal form */
@@ -276,7 +242,6 @@ class TheoryStrings : public Theory {
   StringsPreprocess d_preproc;
   // extended functions inferences cache
   NodeSet d_extf_infer_cache;
-  NodeSet d_extf_infer_cache_u;
   std::vector< Node > d_empty_vec;
   //
   NodeList d_ee_disequalities;
@@ -327,7 +292,11 @@ private:
   public:
     Node d_data;
     std::map< TNode, TermIndex > d_children;
-    Node add( TNode n, unsigned index, TheoryStrings* t, Node er, std::vector< Node >& c );
+    Node add(TNode n,
+             unsigned index,
+             const SolverState& s,
+             Node er,
+             std::vector<Node>& c);
     void clear(){ d_children.clear(); }
   };
   std::map< Kind, TermIndex > d_term_index;
@@ -337,7 +306,6 @@ private:
   std::map< Node, std::vector< int > > d_flat_form_index;
 
   void debugPrintFlatForms( const char * tc );
-  void debugPrintNormalForms( const char * tc );
   /////////////////////////////////////////////////////////////////////////////
   // MODEL GENERATION
   /////////////////////////////////////////////////////////////////////////////
@@ -359,55 +327,6 @@ private:
   EqualityStatus getEqualityStatus(TNode a, TNode b) override;
 
  private:
-  /** SAT-context-dependent information about an equivalence class */
-  class EqcInfo {
-  public:
-    EqcInfo( context::Context* c );
-    ~EqcInfo(){}
-    /**
-     * If non-null, this is a term x from this eq class such that str.len( x )
-     * occurs as a term in this SAT context.
-     */
-    context::CDO< Node > d_length_term;
-    /**
-     * If non-null, this is a term x from this eq class such that str.code( x )
-     * occurs as a term in this SAT context.
-     */
-    context::CDO<Node> d_code_term;
-    context::CDO< unsigned > d_cardinality_lem_k;
-    context::CDO< Node > d_normalized_length;
-    /**
-     * A node that explains the longest constant prefix known of this
-     * equivalence class. This can either be:
-     * (1) A term from this equivalence class, including a constant "ABC" or
-     * concatenation term (str.++ "ABC" ...), or
-     * (2) A membership of the form (str.in.re x R) where x is in this
-     * equivalence class and R is a regular expression of the form
-     * (str.to.re "ABC") or (re.++ (str.to.re "ABC") ...).
-     */
-    context::CDO<Node> d_prefixC;
-    /** same as above, for suffix. */
-    context::CDO<Node> d_suffixC;
-    /** add prefix constant
-     *
-     * This informs this equivalence class info that a term t in its
-     * equivalence class has a constant prefix (if isSuf=true) or suffix
-     * (if isSuf=false). The constant c (if non-null) is the value of that
-     * constant, if it has been computed already.
-     *
-     * If this method returns a non-null node ret, then ret is a conjunction
-     * corresponding to a conflict that holds in the current context.
-     */
-    Node addEndpointConst(Node t, Node c, bool isSuf);
-  };
-  /** map from representatives to information necessary for equivalence classes */
-  std::map< Node, EqcInfo* > d_eqc_info;
-  /**
-   * Get the above information for equivalence class eqc. If doMake is true,
-   * we construct a new information class if one does not exist. The term eqc
-   * should currently be a representative of the equality engine of this class.
-   */
-  EqcInfo * getOrMakeEqcInfo( Node eqc, bool doMake = true );
   /**
    * Map string terms to their "proxy variables". Proxy variables are used are
    * intermediate variables so that length information can be communicated for
@@ -643,15 +562,6 @@ private:
   int processSimpleDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj, unsigned& index, bool isRev );
   //--------------------------end for checkNormalFormsDeq
 
-  //--------------------------------for checkMemberships
-  // check membership constraints
-  Node mkRegExpAntec(Node atom, Node ant);
-  bool checkPDerivative( Node x, Node r, Node atom, bool &addedLemma, std::vector< Node > &nf_exp);
-  //check contains
-  void checkPosContains( std::vector< Node >& posContains );
-  void checkNegContains( std::vector< Node >& negContains );
-  //--------------------------------end for checkMemberships
-
  private:
   void addCarePairs(TNodeTrie* t1,
                     TNodeTrie* t2,
@@ -698,41 +608,12 @@ private:
    * of atom, including calls to registerTerm.
    */
   void assertPendingFact(Node atom, bool polarity, Node exp);
-  /** add endpoints to eqc info
-   *
-   * This method is called when term t is the explanation for why equivalence
-   * class eqc may have a constant endpoint due to a concatentation term concat.
-   * For example, we may call this method on:
-   *   t := (str.++ x y), concat := (str.++ x y), eqc
-   * for some eqc that is currently equal to t. Another example is:
-   *   t := (str.in.re z (re.++ r s)), concat := (re.++ r s), eqc
-   * for some eqc that is currently equal to z.
-   */
-  void addEndpointsToEqcInfo(Node t, Node concat, Node eqc);
-  /** set pending conflict
-   *
-   * If conf is non-null, this is called when conf is a conjunction of literals
-   * that hold in the current context that are unsatisfiable. It is set as the
-   * "pending conflict" to be processed as a conflict lemma on the output
-   * channel of this class. It is not sent out immediately since it may require
-   * explanation from the equality engine, and may be called at any time, e.g.
-   * during a merge operation, when the equality engine is not in a state to
-   * provide explanations.
-   */
-  void setPendingConflictWhen(Node conf);
   /**
    * 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.
-   */
-  void addToExplanation(Node a, Node b, std::vector<Node>& exp);
-  /** Adds lit to the vector exp if it is non-null */
-  void addToExplanation(Node lit, std::vector<Node>& exp);
 
   /** Register term
    *
@@ -754,18 +635,6 @@ private:
    */
   void registerTerm(Node n, int effort);
 
-  /**
-   * 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; }
-
-  /** mkConcat **/
-  inline Node mkConcat(Node n1, Node n2);
-  inline Node mkConcat(Node n1, Node n2, Node n3);
-  inline Node mkConcat(const std::vector<Node>& c);
-  inline Node mkLength(Node n);
-
   /** make explanation
    *
    * This returns a node corresponding to the explanation of formulas in a,
@@ -778,18 +647,6 @@ private:
 
  protected:
 
-  /** get equivalence classes
-   *
-   * This adds the representative of all equivalence classes to eqcs
-   */
-  void getEquivalenceClasses(std::vector<Node>& eqcs);
-  /** get relevant equivalence classes
-   *
-   * This adds the representative of all equivalence classes that contain at
-   * least one term in termSet.
-   */
-  void getRelevantEquivalenceClasses(std::vector<Node>& eqcs,
-                                     std::set<Node>& termSet);
 
   // separate into collections with equal length
   void separateByLength(std::vector<Node>& n,