1 files changed, 19 insertions, 4 deletions

diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index b9da524de..2deb09654 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -33,6 +33,11 @@
 
 namespace CVC4 {
 namespace theory {
+
+namespace quantifiers{
+  class TermArgTrie;
+}
+
 namespace strings {
 
 /**
@@ -45,7 +50,6 @@ typedef expr::Attribute< StringsProxyVarAttributeId, bool > StringsProxyVarAttri
 
 class TheoryStrings : public Theory {
   typedef context::CDChunkList<Node> NodeList;
-  typedef context::CDHashMap<Node, NodeList*, NodeHashFunction> NodeListMap;
   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
   typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
@@ -160,7 +164,8 @@ private:
   std::map< Node, std::vector< Node > > d_normal_forms_exp;
   std::map< Node, std::map< Node, std::map< bool, int > > > d_normal_forms_exp_depend;
   //map of pairs of terms that have the same normal form
-  NodeListMap d_nf_pairs;
+  NodeIntMap d_nf_pairs;
+  std::map< Node, std::vector< Node > > d_nf_pairs_data;
   void addNormalFormPair( Node n1, Node n2 );
   bool isNormalFormPair( Node n1, Node n2 );
   bool isNormalFormPair2( Node n1, Node n2 );
@@ -176,6 +181,8 @@ private:
   // extended functions inferences cache
   NodeSet d_extf_infer_cache;
   std::vector< Node > d_empty_vec;
+  //
+  NodeList d_ee_disequalities;
 private:
   NodeSet d_congruent;
   std::map< Node, Node > d_eqc_to_const;
@@ -236,6 +243,8 @@ private:
   //maintain which concat terms have the length lemma instantiated
   NodeNodeMap d_proxy_var;
   NodeNodeMap d_proxy_var_to_length;
+  /** All the function terms that the theory has seen */
+  context::CDList<TNode> d_functionsTerms;
 private:
   //initial check
   void checkInit();
@@ -304,6 +313,8 @@ private:
   //cardinality check
   void checkCardinality();
 
+private:
+  void addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth );
 public:
   /** preregister term */
   void preRegisterTerm(TNode n);
@@ -410,8 +421,12 @@ private:
   NodeSet d_regexp_ucached;
   NodeSet d_regexp_ccached;
   // stored assertions
-  NodeListMap d_pos_memberships;
-  NodeListMap d_neg_memberships;
+  NodeIntMap d_pos_memberships;
+  std::map< Node, std::vector< Node > > d_pos_memberships_data;
+  NodeIntMap d_neg_memberships;
+  std::map< Node, std::vector< Node > > d_neg_memberships_data;
+  unsigned getNumMemberships( Node n, bool isPos );
+  Node getMembership( Node n, bool isPos, unsigned i );
   // semi normal forms for symbolic expression
   std::map< Node, Node > d_nf_regexps;
   std::map< Node, std::vector< Node > > d_nf_regexps_exp;