1 files changed, 29 insertions, 7 deletions
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index a6644b8bb..6b8144d6e 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -36,6 +36,7 @@ namespace strings {
 class TheoryStrings : public Theory {
   typedef context::CDChunkList<Node> NodeList;
   typedef context::CDHashMap<Node, NodeList*, NodeHashFunction> NodeListMap;
+  typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
   public:
 
   TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe);
@@ -45,7 +46,11 @@ class TheoryStrings : public Theory {
 
   std::string identify() const { return std::string("TheoryStrings"); }
 
-
+  Node getRepresentative( Node t );
+  bool hasTerm( Node a );
+  bool areEqual( Node a, Node b );
+  bool areDisequal( Node a, Node b );
+  Node getLength( Node t );
   public:
 
   void propagate(Effort e);
@@ -113,7 +118,7 @@ class TheoryStrings : public Theory {
     eq::EqualityEngine d_equalityEngine;
     /** Are we in conflict */
     context::CDO<bool> d_conflict;
-
+	std::vector< Node > d_length_intro_vars;
     Node d_emptyString;
     Node d_true;
     Node d_false;
@@ -122,8 +127,7 @@ class TheoryStrings : public Theory {
       std::map< Node, Node > d_pending_exp;
       std::vector< Node > d_pending;
       std::vector< Node > d_lemma_cache;
-  bool hasTerm( Node a );
-  bool areEqual( Node a, Node b );
+	  std::map< Node, bool > d_pending_req_phase;
   /** inferences */
   NodeList d_infer;
   NodeList d_infer_exp;
@@ -137,7 +141,11 @@ class TheoryStrings : public Theory {
   NodeListMap d_ind_map2;
   NodeListMap d_ind_map_exp;
   NodeListMap d_ind_map_lemma;
-  void addInductiveEquation( Node x, Node y, Node z, Node exp );
+  bool addInductiveEquation( Node x, Node y, Node z, Node exp, const char * c );
+
+  //for unrolling inductive equations
+  NodeBoolMap d_lit_to_unroll;
+
 
   /////////////////////////////////////////////////////////////////////////////
   // MODEL GENERATION
@@ -158,8 +166,8 @@ class TheoryStrings : public Theory {
   // MAIN SOLVER
   /////////////////////////////////////////////////////////////////////////////
   private:
-  void dealPositiveWordEquation(TNode n);
   void addSharedTerm(TNode n);
+  EqualityStatus getEqualityStatus(TNode a, TNode b);
 
   private:
   class EqcInfo
@@ -183,11 +191,12 @@ class TheoryStrings : public Theory {
     void getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf,
     std::vector< std::vector< Node > > &normal_forms,  std::vector< std::vector< Node > > &normal_forms_exp, std::vector< Node > &normal_form_src);
     void normalizeEquivalenceClass( Node n, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp );
-    bool areLengthsEqual( Node n1, Node n2 ); //TODO
+    bool normalizeDisequality( Node n1, Node n2 );
 
     bool checkNormalForms();
     bool checkCardinality();
     bool checkInductiveEquations();
+	int gcd(int a, int b);
   public:
   void preRegisterTerm(TNode n);
   void check(Effort e);
@@ -208,11 +217,24 @@ protected:
 
   //do pending merges
   void doPendingFacts();
+  void doPendingLemmas();
 
+  void sendLemma( Node ant, Node conc, const char * c );
+  void sendSplit( Node a, Node b, const char * c );
   /** mkConcat **/
   Node mkConcat( std::vector< Node >& c );
   /** mkExplain **/
   Node mkExplain( std::vector< Node >& a, std::vector< Node >& an );
+
+  //get equivalence classes
+  void getEquivalenceClasses( std::vector< Node >& eqcs );
+  //get final normal form
+  void getFinalNormalForm( Node n, std::vector< Node >& nf, std::vector< Node >& exp );
+
+  //seperate into collections with equal length
+  void seperateByLength( std::vector< Node >& n, std::vector< std::vector< Node > >& col, std::vector< Node >& lts );
+private:
+  void printConcat( std::vector< Node >& n, const char * c );
 };/* class TheoryStrings */
 
 }/* CVC4::theory::strings namespace */