add strings-opt2 for regular splitting
authorTianyi Liang <tianyi-liang@uiowa.edu>
Mon, 28 Apr 2014 21:29:27 +0000 (16:29 -0500)
committerTianyi Liang <tianyi-liang@uiowa.edu>
Mon, 28 Apr 2014 22:37:00 +0000 (17:37 -0500)
12 files changed:
src/theory/strings/options
src/theory/strings/regexp_operation.cpp
src/theory/strings/regexp_operation.h
src/theory/strings/theory_strings.cpp
src/theory/strings/theory_strings.h
src/theory/strings/theory_strings_preprocess.cpp
src/theory/strings/theory_strings_preprocess.h
src/theory/strings/theory_strings_rewriter.cpp
src/theory/strings/theory_strings_type_rules.h
src/theory/strings/type_enumerator.h
src/util/regexp.cpp
src/util/regexp.h

index f6d765fc4837e29f96aaf95725d4fc21fbde71bb..10f22b05a8a7a6c8d7c6bb361f5738eaaedb5457 100644 (file)
@@ -17,6 +17,12 @@ option stringFMF strings-fmf --strings-fmf bool :default false :read-write
 option stringEIT strings-eit --strings-eit bool :default false
  the eager intersection used by the theory of strings
 
+option stringOpt1 strings-opt1 --strings-opt1 bool :default true
+ internal option1 for strings: normal form
+
+option stringOpt2 strings-opt2 --strings-opt2 bool :default false
+ internal option2 for strings: constant regexp splitting
+
 expert-option stringCharCardinality strings-alphabet-card --strings-alphabet-card=N int16_t :default 256 :predicate CVC4::smt::beforeSearch :predicate-include "smt/smt_engine.h"
  the cardinality of the characters used by the theory of strings, default 256
 
index 16bb7e6942d762f8379f3072c28891264ec0043e..5c664ba3473482dfabe399d69a26461aec96e1d2 100644 (file)
@@ -33,14 +33,14 @@ namespace theory {
 namespace strings {\r
 \r
 RegExpOpr::RegExpOpr() {\r
-    d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") );\r
-    d_true = NodeManager::currentNM()->mkConst( true );\r
-    d_false = NodeManager::currentNM()->mkConst( false );\r
+  d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") );\r
+  d_true = NodeManager::currentNM()->mkConst( true );\r
+  d_false = NodeManager::currentNM()->mkConst( false );\r
        d_zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );\r
        d_one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );\r
        d_emptySingleton = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, d_emptyString );\r
        std::vector< Node > nvec;\r
-    d_emptyRegexp = NodeManager::currentNM()->mkNode( kind::REGEXP_EMPTY, nvec );\r
+  d_emptyRegexp = NodeManager::currentNM()->mkNode( kind::REGEXP_EMPTY, nvec );\r
        d_sigma = NodeManager::currentNM()->mkNode( kind::REGEXP_SIGMA, nvec );\r
        d_sigma_star = NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, d_sigma );\r
        d_card = 256;\r
@@ -1315,6 +1315,119 @@ Node RegExpOpr::complement(Node r, int &ret) {
        Trace("regexp-compl") << "COMPL( " << mkString(r) << " ) = " << mkString(rNode) << ", ret=" << ret << std::endl;\r
        return rNode;\r
 }\r
+\r
+void RegExpOpr::splitRegExp(Node r, std::vector< PairNodes > &pset) {\r
+       Assert(checkConstRegExp(r));\r
+       if(d_split_cache.find(r) != d_split_cache.end()) {\r
+               pset = d_split_cache[r];\r
+       } else {\r
+               switch( r.getKind() ) {\r
+                       case kind::REGEXP_EMPTY: {\r
+                               break;\r
+                       }\r
+                       case kind::REGEXP_OPT: {\r
+                               PairNodes tmp(d_emptySingleton, d_emptySingleton);\r
+                               pset.push_back(tmp);\r
+                       }\r
+                       case kind::REGEXP_RANGE:\r
+                       case kind::REGEXP_SIGMA: {\r
+                               PairNodes tmp1(d_emptySingleton, r);\r
+                               PairNodes tmp2(r, d_emptySingleton);\r
+                               pset.push_back(tmp1);\r
+                               pset.push_back(tmp2);\r
+                               break;\r
+                       }\r
+                       case kind::STRING_TO_REGEXP: {\r
+                               Assert(r[0].isConst());\r
+                               CVC4::String s = r[0].getConst< CVC4::String >();\r
+                               PairNodes tmp1(d_emptySingleton, r);\r
+                               pset.push_back(tmp1);\r
+                               for(unsigned i=1; i<s.size(); i++) {\r
+                                       CVC4::String s1 = s.substr(0, i);\r
+                                       CVC4::String s2 = s.substr(i);\r
+                                       Node n1 = NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst(s1));\r
+                                       Node n2 = NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst(s2));\r
+                                       PairNodes tmp3(n1, n2);\r
+                                       pset.push_back(tmp3);\r
+                               }\r
+                               PairNodes tmp2(r, d_emptySingleton);\r
+                               pset.push_back(tmp2);\r
+                               break;\r
+                       }\r
+                       case kind::REGEXP_CONCAT: {\r
+                               for(unsigned i=0; i<r.getNumChildren(); i++) {\r
+                                       std::vector< PairNodes > tset;\r
+                                       splitRegExp(r[i], tset);\r
+                                       std::vector< Node > hvec;\r
+                                       std::vector< Node > tvec;\r
+                                       for(unsigned j=0; j<=i; j++) {\r
+                                               hvec.push_back(r[j]);\r
+                                       }\r
+                                       for(unsigned j=i; j<r.getNumChildren(); j++) {\r
+                                               tvec.push_back(r[j]);\r
+                                       }\r
+                                       for(unsigned j=0; j<tset.size(); j++) {\r
+                                               hvec[i] = tset[j].first;\r
+                                               tvec[0] = tset[j].second;\r
+                                               Node r1 = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, hvec) );\r
+                                               Node r2 = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, tvec) );\r
+                                               PairNodes tmp2(r1, r2);\r
+                                               pset.push_back(tmp2);\r
+                                       }\r
+                               }\r
+                               break;\r
+                       }\r
+                       case kind::REGEXP_UNION: {\r
+                               for(unsigned i=0; i<r.getNumChildren(); ++i) {\r
+                                       std::vector< PairNodes > tset;\r
+                                       splitRegExp(r[i], tset);\r
+                                       pset.insert(pset.end(), tset.begin(), tset.end());\r
+                               }\r
+                               break;\r
+                       }\r
+                       case kind::REGEXP_INTER: {\r
+                               bool spflag = false;\r
+                               Node tmp = r[0];\r
+                               for(unsigned i=1; i<r.getNumChildren(); i++) {\r
+                                       tmp = intersect(tmp, r[i], spflag);\r
+                               }\r
+                               splitRegExp(tmp, pset);\r
+                               break;\r
+                       }\r
+                       case kind::REGEXP_STAR: {\r
+                               std::vector< PairNodes > tset;\r
+                               splitRegExp(r[0], tset);\r
+                               PairNodes tmp1(d_emptySingleton, d_emptySingleton);\r
+                               pset.push_back(tmp1);\r
+                               for(unsigned i=0; i<tset.size(); i++) {\r
+                                       Node r1 = tset[i].first==d_emptySingleton ? r : NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, r, tset[i].first);\r
+                                       Node r2 = tset[i].second==d_emptySingleton ? r : NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, tset[i].second, r);\r
+                                       PairNodes tmp2(r1, r2);\r
+                                       pset.push_back(tmp2);\r
+                               }\r
+                               break;\r
+                       }\r
+                       case kind::REGEXP_PLUS: {\r
+                               std::vector< PairNodes > tset;\r
+                               splitRegExp(r[0], tset);\r
+                               for(unsigned i=0; i<tset.size(); i++) {\r
+                                       Node r1 = NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, r, tset[i].first);\r
+                                       Node r2 = NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, tset[i].second, r);\r
+                                       PairNodes tmp2(r1, r2);\r
+                                       pset.push_back(tmp2);\r
+                               }\r
+                               break;\r
+                       }\r
+                       default: {\r
+                               Trace("strings-error") << "Unsupported term: " << r << " in splitRegExp." << std::endl;\r
+                               Assert( false );\r
+                               //return Node::null();\r
+                       }\r
+               }\r
+               d_split_cache[r] = pset;\r
+       }\r
+}\r
+\r
 //printing\r
 std::string RegExpOpr::niceChar( Node r ) {\r
        if(r.isConst()) {\r
index 11686882048f0f25a2f0fb7bf76b220c6f6174c1..0513eeef4af7a6845290a5d0d9f5a85fbbd8197d 100644 (file)
@@ -39,9 +39,9 @@ class RegExpOpr {
 \r
 private:\r
        unsigned d_card;\r
-    Node d_emptyString;\r
-    Node d_true;\r
-    Node d_false;\r
+  Node d_emptyString;\r
+  Node d_true;\r
+  Node d_false;\r
        Node d_emptySingleton;\r
        Node d_emptyRegexp;\r
        Node d_zero;\r
@@ -62,6 +62,7 @@ private:
        std::map< Node, std::pair< std::set<unsigned>, std::set<Node> > > d_cset_cache;\r
        std::map< Node, std::pair< std::set<unsigned>, std::set<Node> > > d_fset_cache;\r
        std::map< PairNodes, Node > d_inter_cache;\r
+       std::map< Node, std::vector< PairNodes > > d_split_cache;\r
        //bool checkStarPlus( Node t );\r
        void simplifyPRegExp( Node s, Node r, std::vector< Node > &new_nodes );\r
        void simplifyNRegExp( Node s, Node r, std::vector< Node > &new_nodes );\r
@@ -80,13 +81,14 @@ public:
        RegExpOpr();\r
 \r
        bool checkConstRegExp( Node r );\r
-    void simplify(Node t, std::vector< Node > &new_nodes, bool polarity);\r
+  void simplify(Node t, std::vector< Node > &new_nodes, bool polarity);\r
        int delta( Node r, Node &exp );\r
        int derivativeS( Node r, CVC4::String c, Node &retNode );\r
        Node derivativeSingle( Node r, CVC4::String c );\r
        bool guessLength( Node r, int &co );\r
        Node intersect(Node r1, Node r2, bool &spflag);\r
        Node complement(Node r, int &ret);\r
+       void splitRegExp(Node r, std::vector< PairNodes > &pset);\r
 \r
        std::string mkString( Node r );\r
 };\r
index d44f38bc3f9eaeca6ab37ec1d68f04d6e9f922d3..61d60d4cd9617e991ea170bb3e39013f0c3c2613 100644 (file)
@@ -34,13 +34,13 @@ namespace theory {
 namespace strings {
 
 TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo)
-    : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo),
-    d_notify( *this ),
-    d_equalityEngine(d_notify, c, "theory::strings::TheoryStrings"),
-    d_conflict(c, false),
-    d_infer(c),
-    d_infer_exp(c),
-    d_nf_pairs(c),
+  : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo),
+  d_notify( *this ),
+  d_equalityEngine(d_notify, c, "theory::strings::TheoryStrings"),
+  d_conflict(c, false),
+  d_infer(c),
+  d_infer_exp(c),
+  d_nf_pairs(c),
        d_loop_antec(u),
        d_length_intro_vars(u),
        d_prereg_cached(u),
@@ -64,28 +64,28 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
        d_cardinality_lits(u),
        d_curr_cardinality(c, 0)
 {
-    // The kinds we are treating as function application in congruence
-    d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP);
-    d_equalityEngine.addFunctionKind(kind::STRING_LENGTH);
-    d_equalityEngine.addFunctionKind(kind::STRING_CONCAT);
-    d_equalityEngine.addFunctionKind(kind::STRING_STRCTN);
-    d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR_TOTAL);
-    d_equalityEngine.addFunctionKind(kind::STRING_ITOS);
-    d_equalityEngine.addFunctionKind(kind::STRING_STOI);
-    //d_equalityEngine.addFunctionKind(kind::STRING_U16TOS);
-    //d_equalityEngine.addFunctionKind(kind::STRING_STOU16);
-    //d_equalityEngine.addFunctionKind(kind::STRING_U32TOS);
-    //d_equalityEngine.addFunctionKind(kind::STRING_STOU32);
-
-    d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
-    d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
-    d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
-       std::vector< Node > nvec;
-       d_emptyRegexp = NodeManager::currentNM()->mkNode( kind::REGEXP_EMPTY, nvec );
-       d_true = NodeManager::currentNM()->mkConst( true );
-    d_false = NodeManager::currentNM()->mkConst( false );
-
-       //d_opt_regexp_gcd = true;
+  // The kinds we are treating as function application in congruence
+  d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP);
+  d_equalityEngine.addFunctionKind(kind::STRING_LENGTH);
+  d_equalityEngine.addFunctionKind(kind::STRING_CONCAT);
+  d_equalityEngine.addFunctionKind(kind::STRING_STRCTN);
+  d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR_TOTAL);
+  d_equalityEngine.addFunctionKind(kind::STRING_ITOS);
+  d_equalityEngine.addFunctionKind(kind::STRING_STOI);
+  //d_equalityEngine.addFunctionKind(kind::STRING_U16TOS);
+  //d_equalityEngine.addFunctionKind(kind::STRING_STOU16);
+  //d_equalityEngine.addFunctionKind(kind::STRING_U32TOS);
+  //d_equalityEngine.addFunctionKind(kind::STRING_STOU32);
+
+  d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
+  d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
+  d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
+  std::vector< Node > nvec;
+  d_emptyRegexp = NodeManager::currentNM()->mkNode( kind::REGEXP_EMPTY, nvec );
+  d_true = NodeManager::currentNM()->mkConst( true );
+  d_false = NodeManager::currentNM()->mkConst( false );
+
+  //d_opt_regexp_gcd = true;
 }
 
 TheoryStrings::~TheoryStrings() {
@@ -221,13 +221,13 @@ void TheoryStrings::explain(TNode literal, std::vector<TNode>& assumptions){
     d_equalityEngine.explainPredicate(atom, polarity, tassumptions);
   }
   for( unsigned i=0; i<tassumptions.size(); i++ ){
-       if( std::find( assumptions.begin(), assumptions.end(), tassumptions[i] )==assumptions.end() ){
-               assumptions.push_back( tassumptions[i] );
-       }
+    if( std::find( assumptions.begin(), assumptions.end(), tassumptions[i] )==assumptions.end() ){
+      assumptions.push_back( tassumptions[i] );
+    }
   }
   Debug("strings-explain-debug") << "Explanation for " << literal << " was " << std::endl;
   for( unsigned i=ps; i<assumptions.size(); i++ ){
-       Debug("strings-explain-debug") << "   " << assumptions[i] << std::endl;
+         Debug("strings-explain-debug") << "   " << assumptions[i] << std::endl;
   }
 }
 
@@ -263,7 +263,7 @@ void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) {
        Trace("strings-model") << "TheoryStrings : Collect model info, fullModel = " << fullModel << std::endl;
        Trace("strings-model") << "TheoryStrings : assertEqualityEngine." << std::endl;
        m->assertEqualityEngine( &d_equalityEngine );
-    // Generate model
+  // Generate model
        std::vector< Node > nodes;
        getEquivalenceClasses( nodes );
        std::map< Node, Node > processed;
@@ -410,120 +410,119 @@ void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) {
 
 void TheoryStrings::preRegisterTerm(TNode n) {
   if(d_prereg_cached.find(n) == d_prereg_cached.end()) {
-       Debug("strings-prereg") << "TheoryStrings::preRegisterTerm() " << n << endl;
-       //collectTerms( n );
-       switch (n.getKind()) {
-       case kind::EQUAL:
-               d_equalityEngine.addTriggerEquality(n);
-               break;
-       case kind::STRING_IN_REGEXP:
-               //do not add trigger here
-               d_equalityEngine.addTriggerPredicate(n);
-               break;
-       case kind::STRING_SUBSTR_TOTAL: {
-               Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ, 
-                                                       NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[0] ),
-                                                       NodeManager::currentNM()->mkNode( kind::PLUS, n[1], n[2] ) );
-               Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, n[1], d_zero);
-               Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, n[2], d_zero);
-               Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 ));
-               Node sk1 = NodeManager::currentNM()->mkSkolem( "ss1", NodeManager::currentNM()->stringType(), "created for charat/substr" );
-               Node sk3 = NodeManager::currentNM()->mkSkolem( "ss3", NodeManager::currentNM()->stringType(), "created for charat/substr" );
-               d_statistics.d_new_skolems += 2;
-               Node x_eq_123 = n[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, n, sk3 ) );
-               Node len_sk1_eq_i = n[1].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
-               Node lenc = n[2].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n ) );
-               Node lemma = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::ITE, cond, 
-                       NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i, lenc ),
-                       n.eqNode(d_emptyString)));
-               Trace("strings-lemma") << "Strings::Lemma SUBSTR : " << lemma << std::endl;
-               d_out->lemma(lemma);
-               //d_equalityEngine.addTerm(n);
-       }
-       default: {
-               if(n.getType().isString() && n.getKind()!=kind::STRING_CONCAT && n.getKind()!=kind::CONST_STRING ) {
-                 if( d_length_intro_vars.find(n)==d_length_intro_vars.end() ) {
-                         Node n_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n);
-                         Node n_len_eq_z = n_len.eqNode( d_zero );
-                         n_len_eq_z = Rewriter::rewrite( n_len_eq_z );
-                         Node n_len_geq_zero = NodeManager::currentNM()->mkNode( kind::OR, n_len_eq_z,
-                                                                               NodeManager::currentNM()->mkNode( kind::GT, n_len, d_zero) );
-                         Trace("strings-lemma") << "Strings::Lemma LENGTH >= 0 : " << n_len_geq_zero << std::endl;
-                         d_out->lemma(n_len_geq_zero);
-                         d_out->requirePhase( n_len_eq_z, true );
-                 }
-                 // FMF
-                 if( n.getKind() == kind::VARIABLE && options::stringFMF() ) {
-                         d_input_vars.insert(n);
-                 }
-               }
-               if (n.getType().isBoolean()) {
-                 // Get triggered for both equal and dis-equal
-                 d_equalityEngine.addTriggerPredicate(n);
-               } else {
-                 // Function applications/predicates
-                 d_equalityEngine.addTerm(n);
-               }
-       }
-       }
-       d_prereg_cached.insert(n);
+    Debug("strings-prereg") << "TheoryStrings::preRegisterTerm() " << n << endl;
+    //collectTerms( n );
+    switch (n.getKind()) {
+      case kind::EQUAL:
+        d_equalityEngine.addTriggerEquality(n);
+        break;
+      case kind::STRING_IN_REGEXP:
+        //do not add trigger here
+        d_equalityEngine.addTriggerPredicate(n);
+        break;
+      case kind::STRING_SUBSTR_TOTAL: {
+        Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ, 
+                  NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[0] ),
+                  NodeManager::currentNM()->mkNode( kind::PLUS, n[1], n[2] ) );
+        Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, n[1], d_zero);
+        Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, n[2], d_zero);
+        Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 ));
+        Node sk1 = NodeManager::currentNM()->mkSkolem( "ss1", NodeManager::currentNM()->stringType(), "created for charat/substr" );
+        Node sk3 = NodeManager::currentNM()->mkSkolem( "ss3", NodeManager::currentNM()->stringType(), "created for charat/substr" );
+        d_statistics.d_new_skolems += 2;
+        Node x_eq_123 = n[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, n, sk3 ) );
+        Node len_sk1_eq_i = n[1].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
+        Node lenc = n[2].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n ) );
+        Node lemma = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::ITE, cond, 
+          NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i, lenc ),
+          n.eqNode(d_emptyString)));
+        Trace("strings-lemma") << "Strings::Lemma SUBSTR : " << lemma << std::endl;
+        d_out->lemma(lemma);
+        //d_equalityEngine.addTerm(n);
+      }
+      default: {
+        if(n.getType().isString() && n.getKind()!=kind::STRING_CONCAT && n.getKind()!=kind::CONST_STRING ) {
+          if( d_length_intro_vars.find(n)==d_length_intro_vars.end() ) {
+            Node n_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n);
+            Node n_len_eq_z = n_len.eqNode( d_zero );
+            n_len_eq_z = Rewriter::rewrite( n_len_eq_z );
+            Node n_len_geq_zero = NodeManager::currentNM()->mkNode( kind::OR, n_len_eq_z,
+                        NodeManager::currentNM()->mkNode( kind::GT, n_len, d_zero) );
+            Trace("strings-lemma") << "Strings::Lemma LENGTH >= 0 : " << n_len_geq_zero << std::endl;
+            d_out->lemma(n_len_geq_zero);
+            d_out->requirePhase( n_len_eq_z, true );
+          }
+          // FMF
+          if( n.getKind() == kind::VARIABLE && options::stringFMF() ) {
+            d_input_vars.insert(n);
+          }
+        }
+        if (n.getType().isBoolean()) {
+          // Get triggered for both equal and dis-equal
+          d_equalityEngine.addTriggerPredicate(n);
+        } else {
+          // Function applications/predicates
+          d_equalityEngine.addTerm(n);
+        }
+      }
+    }
+    d_prereg_cached.insert(n);
   }
 }
 
 Node TheoryStrings::expandDefinition(LogicRequest &logicRequest, Node node) {
   switch (node.getKind()) {
-  case kind::STRING_CHARAT: {
-    if(d_ufSubstr.isNull()) {
-      std::vector< TypeNode > argTypes;
-      argTypes.push_back(NodeManager::currentNM()->stringType());
-      argTypes.push_back(NodeManager::currentNM()->integerType());
-      argTypes.push_back(NodeManager::currentNM()->integerType());
-      d_ufSubstr = NodeManager::currentNM()->mkSkolem("__ufSS",
-                                                     NodeManager::currentNM()->mkFunctionType(
-                                                                                              argTypes, NodeManager::currentNM()->stringType()),
-                                                     "uf substr",
-                                                     NodeManager::SKOLEM_EXACT_NAME);
+    case kind::STRING_CHARAT: {
+      if(d_ufSubstr.isNull()) {
+        std::vector< TypeNode > argTypes;
+        argTypes.push_back(NodeManager::currentNM()->stringType());
+        argTypes.push_back(NodeManager::currentNM()->integerType());
+        argTypes.push_back(NodeManager::currentNM()->integerType());
+        d_ufSubstr = NodeManager::currentNM()->mkSkolem("__ufSS",
+                    NodeManager::currentNM()->mkFunctionType(
+                               argTypes, NodeManager::currentNM()->stringType()),
+                    "uf substr",
+                    NodeManager::SKOLEM_EXACT_NAME);
+      }
+      Node lenxgti = NodeManager::currentNM()->mkNode( kind::GT,
+                   NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, node[0] ), node[1] );
+      Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
+      Node t1greq0 = NodeManager::currentNM()->mkNode( kind::GEQ, node[1], zero);
+      Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1greq0 ));
+      Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
+      Node totalf = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, node[0], node[1], one);
+      Node uf = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, node[0], node[1], one);
+      return NodeManager::currentNM()->mkNode( kind::ITE, cond, totalf, uf );
+      break;
     }
-    Node lenxgti = NodeManager::currentNM()->mkNode( kind::GT,
-                                                    NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, node[0] ), node[1] );
-    Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
-    Node t1greq0 = NodeManager::currentNM()->mkNode( kind::GEQ, node[1], zero);
-    Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1greq0 ));
-    Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
-    Node totalf = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, node[0], node[1], one);
-    Node uf = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, node[0], node[1], one);
-    return NodeManager::currentNM()->mkNode( kind::ITE, cond, totalf, uf );
-  }
-  break;
-
-  case kind::STRING_SUBSTR: {
-    if(d_ufSubstr.isNull()) {
-      std::vector< TypeNode > argTypes;
-      argTypes.push_back(NodeManager::currentNM()->stringType());
-      argTypes.push_back(NodeManager::currentNM()->integerType());
-      argTypes.push_back(NodeManager::currentNM()->integerType());
-      d_ufSubstr = NodeManager::currentNM()->mkSkolem("__ufSS",
-                                                     NodeManager::currentNM()->mkFunctionType(
-                                                                                              argTypes, NodeManager::currentNM()->stringType()),
-                                                     "uf substr",
-                                                     NodeManager::SKOLEM_EXACT_NAME);
+
+    case kind::STRING_SUBSTR: {
+      if(d_ufSubstr.isNull()) {
+        std::vector< TypeNode > argTypes;
+        argTypes.push_back(NodeManager::currentNM()->stringType());
+        argTypes.push_back(NodeManager::currentNM()->integerType());
+        argTypes.push_back(NodeManager::currentNM()->integerType());
+        d_ufSubstr = NodeManager::currentNM()->mkSkolem("__ufSS",
+                    NodeManager::currentNM()->mkFunctionType(
+                               argTypes, NodeManager::currentNM()->stringType()),
+                    "uf substr",
+                    NodeManager::SKOLEM_EXACT_NAME);
+      }
+      Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ,
+                   NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, node[0] ),
+                   NodeManager::currentNM()->mkNode( kind::PLUS, node[1], node[2] ) );
+      Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
+      Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, node[1], zero);
+      Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, node[2], zero);
+      Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 ));
+      Node totalf = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, node[0], node[1], node[2]);
+      Node uf = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, node[0], node[1], node[2]);
+      return NodeManager::currentNM()->mkNode( kind::ITE, cond, totalf, uf );
+      break;
     }
-    Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ,
-                                                    NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, node[0] ),
-                                                    NodeManager::currentNM()->mkNode( kind::PLUS, node[1], node[2] ) );
-    Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
-    Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, node[1], zero);
-    Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, node[2], zero);
-    Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 ));
-    Node totalf = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, node[0], node[1], node[2]);
-    Node uf = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, node[0], node[1], node[2]);
-    return NodeManager::currentNM()->mkNode( kind::ITE, cond, totalf, uf );
-  }
-  break;
 
-  default :
-    return node;
-    break;
+    default :
+      return node;
   }
 
   Unreachable();
@@ -543,7 +542,7 @@ void TheoryStrings::check(Effort e) {
   }*/
 
   if( !done() && !hasTerm( d_emptyString ) ) {
-        preRegisterTerm( d_emptyString );
+         preRegisterTerm( d_emptyString );
   }
 
  // Trace("strings-process") << "Theory of strings, check : " << e << std::endl;
@@ -635,9 +634,9 @@ void TheoryStrings::conflict(TNode a, TNode b){
          d_conflict = true;
          Node conflictNode;
          if (a.getKind() == kind::CONST_BOOLEAN) {
-               conflictNode = explain( a.iffNode(b) );
+                 conflictNode = explain( a.iffNode(b) );
          } else {
-               conflictNode = explain( a.eqNode(b) );
+                 conflictNode = explain( a.eqNode(b) );
          }
          Trace("strings-conflict") << "CONFLICT: Eq engine conflict : " << conflictNode << std::endl;
          d_out->conflict( conflictNode );
@@ -662,48 +661,48 @@ void TheoryStrings::eqNotifyNewClass(TNode t){
 void TheoryStrings::eqNotifyPreMerge(TNode t1, TNode t2){
     EqcInfo * e2 = getOrMakeEqcInfo(t2, false);
     if( e2 ){
-        EqcInfo * e1 = getOrMakeEqcInfo( t1 );
-        //add information from e2 to e1
-        if( !e2->d_const_term.get().isNull() ){
-            e1->d_const_term.set( e2->d_const_term );
-        }
-        if( !e2->d_length_term.get().isNull() ){
-            e1->d_length_term.set( e2->d_length_term );
-        }
-        if( e2->d_cardinality_lem_k.get()>e1->d_cardinality_lem_k.get() ) {
-            e1->d_cardinality_lem_k.set( e2->d_cardinality_lem_k );
-        }
-               if( !e2->d_normalized_length.get().isNull() ){
-                       e1->d_normalized_length.set( e2->d_normalized_length );
-               }
+      EqcInfo * e1 = getOrMakeEqcInfo( t1 );
+      //add information from e2 to e1
+      if( !e2->d_const_term.get().isNull() ){
+        e1->d_const_term.set( e2->d_const_term );
+      }
+      if( !e2->d_length_term.get().isNull() ){
+        e1->d_length_term.set( e2->d_length_term );
+      }
+      if( e2->d_cardinality_lem_k.get()>e1->d_cardinality_lem_k.get() ) {
+        e1->d_cardinality_lem_k.set( e2->d_cardinality_lem_k );
+      }
+      if( !e2->d_normalized_length.get().isNull() ){
+        e1->d_normalized_length.set( e2->d_normalized_length );
+      }
     }
     if( hasTerm( d_zero ) ){
-        Node leqc;
-        if( areEqual(d_zero, t1) ){
-            leqc = t2;
-        }else if( areEqual(d_zero, t2) ){
-            leqc = t1;
-        }
-        if( !leqc.isNull() ){
-            //scan equivalence class to see if we apply
-            eq::EqClassIterator eqc_i = eq::EqClassIterator( leqc, &d_equalityEngine );
-            while( !eqc_i.isFinished() ){
-              Node n = (*eqc_i);
-              if( n.getKind()==kind::STRING_LENGTH ){
-                if( !hasTerm( d_emptyString ) || !areEqual(n[0], d_emptyString ) ){
-                    //apply the rule length(n[0])==0 => n[0] == ""
-                    Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, n[0], d_emptyString );
-                    d_pending.push_back( eq );
-                    Node eq_exp = NodeManager::currentNM()->mkNode( kind::EQUAL, n, d_zero );
-                    d_pending_exp[eq] = eq_exp;
-                    Trace("strings-infer") << "Strings : Infer Empty : " << eq << " from " << eq_exp << std::endl;
-                    d_infer.push_back(eq);
-                    d_infer_exp.push_back(eq_exp);
-                }
-              }
-              ++eqc_i;
+      Node leqc;
+      if( areEqual(d_zero, t1) ){
+        leqc = t2;
+      }else if( areEqual(d_zero, t2) ){
+        leqc = t1;
+      }
+      if( !leqc.isNull() ){
+        //scan equivalence class to see if we apply
+        eq::EqClassIterator eqc_i = eq::EqClassIterator( leqc, &d_equalityEngine );
+        while( !eqc_i.isFinished() ){
+          Node n = (*eqc_i);
+          if( n.getKind()==kind::STRING_LENGTH ){
+            if( !hasTerm( d_emptyString ) || !areEqual(n[0], d_emptyString ) ){
+              //apply the rule length(n[0])==0 => n[0] == ""
+              Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, n[0], d_emptyString );
+              d_pending.push_back( eq );
+              Node eq_exp = NodeManager::currentNM()->mkNode( kind::EQUAL, n, d_zero );
+              d_pending_exp[eq] = eq_exp;
+              Trace("strings-infer") << "Strings : Infer Empty : " << eq << " from " << eq_exp << std::endl;
+              d_infer.push_back(eq);
+              d_infer_exp.push_back(eq_exp);
             }
+          }
+          ++eqc_i;
         }
+      }
     }
 }
 
@@ -726,21 +725,21 @@ void TheoryStrings::doPendingFacts() {
   while( !d_conflict && i<(int)d_pending.size() ){
     Node fact = d_pending[i];
     Node exp = d_pending_exp[ fact ];
-      Trace("strings-pending") << "Process pending fact : " << fact << " from " << exp << std::endl;
-      bool polarity = fact.getKind() != kind::NOT;
-      TNode atom = polarity ? fact : fact[0];
-      if (atom.getKind() == kind::EQUAL) {
-               //Assert( d_equalityEngine.hasTerm( atom[0] ) );
-               //Assert( d_equalityEngine.hasTerm( atom[1] ) );
-               for( unsigned j=0; j<2; j++ ){
-                       if( !d_equalityEngine.hasTerm( atom[j] ) ){
-                               d_equalityEngine.addTerm( atom[j] );
-                       }
-               }
-               d_equalityEngine.assertEquality( atom, polarity, exp );
-      }else{
-        d_equalityEngine.assertPredicate( atom, polarity, exp );
+    Trace("strings-pending") << "Process pending fact : " << fact << " from " << exp << std::endl;
+    bool polarity = fact.getKind() != kind::NOT;
+    TNode atom = polarity ? fact : fact[0];
+    if (atom.getKind() == kind::EQUAL) {
+      //Assert( d_equalityEngine.hasTerm( atom[0] ) );
+      //Assert( d_equalityEngine.hasTerm( atom[1] ) );
+      for( unsigned j=0; j<2; j++ ){
+        if( !d_equalityEngine.hasTerm( atom[j] ) ){
+          d_equalityEngine.addTerm( atom[j] );
+        }
       }
+      d_equalityEngine.assertEquality( atom, polarity, exp );
+    }else{
+      d_equalityEngine.assertPredicate( atom, polarity, exp );
+    }
     i++;
   }
   d_pending.clear();
@@ -753,8 +752,8 @@ void TheoryStrings::doPendingLemmas() {
                  d_out->lemma( d_lemma_cache[i] );
          }
          for( std::map< Node, bool >::iterator it = d_pending_req_phase.begin(); it != d_pending_req_phase.end(); ++it ){
-               Trace("strings-pending") << "Require phase : " << it->first << ", polarity = " << it->second << std::endl;
-               d_out->requirePhase( it->first, it->second );
+      Trace("strings-pending") << "Require phase : " << it->first << ", polarity = " << it->second << std::endl;
+      d_out->requirePhase( it->first, it->second );
          }
   }
   d_lemma_cache.clear();
@@ -762,7 +761,7 @@ void TheoryStrings::doPendingLemmas() {
 }
 
 bool TheoryStrings::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) {
+  std::vector< std::vector< Node > > &normal_forms,  std::vector< std::vector< Node > > &normal_forms_exp, std::vector< Node > &normal_form_src) {
        Trace("strings-process-debug") << "Get normal forms " << eqc << std::endl;
        // EqcItr
        eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
@@ -883,37 +882,37 @@ bool TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std
                ++eqc_i;
        }
 
-    // Test the result
-    if( !normal_forms.empty() ) {
-        Trace("strings-solve") << "--- Normal forms for equivlance class " << eqc << " : " << std::endl;
-        for( unsigned i=0; i<normal_forms.size(); i++ ) {
-            Trace("strings-solve") << "#" << i << " (from " << normal_form_src[i] << ") : ";
-                       //mergeCstVec(normal_forms[i]);
-            for( unsigned j=0; j<normal_forms[i].size(); j++ ) {
-                if(j>0) Trace("strings-solve") << ", ";
-                Trace("strings-solve") << normal_forms[i][j];
-            }
-            Trace("strings-solve") << std::endl;
-            Trace("strings-solve") << "   Explanation is : ";
-            if(normal_forms_exp[i].size() == 0) {
-                Trace("strings-solve") << "NONE";
-            } else {
-                for( unsigned j=0; j<normal_forms_exp[i].size(); j++ ) {
-                    if(j>0) Trace("strings-solve") << " AND ";
-                    Trace("strings-solve") << normal_forms_exp[i][j];
-                }
-            }
-            Trace("strings-solve") << std::endl;
+  // Test the result
+  if( !normal_forms.empty() ) {
+    Trace("strings-solve") << "--- Normal forms for equivlance class " << eqc << " : " << std::endl;
+    for( unsigned i=0; i<normal_forms.size(); i++ ) {
+      Trace("strings-solve") << "#" << i << " (from " << normal_form_src[i] << ") : ";
+      //mergeCstVec(normal_forms[i]);
+      for( unsigned j=0; j<normal_forms[i].size(); j++ ) {
+        if(j>0) Trace("strings-solve") << ", ";
+        Trace("strings-solve") << normal_forms[i][j];
+      }
+      Trace("strings-solve") << std::endl;
+      Trace("strings-solve") << "   Explanation is : ";
+      if(normal_forms_exp[i].size() == 0) {
+        Trace("strings-solve") << "NONE";
+      } else {
+        for( unsigned j=0; j<normal_forms_exp[i].size(); j++ ) {
+          if(j>0) Trace("strings-solve") << " AND ";
+          Trace("strings-solve") << normal_forms_exp[i][j];
         }
-    }else{
-      //std::vector< Node > nf;
-      //nf.push_back( eqc );
-      //normal_forms.push_back(nf);
-      //std::vector< Node > nf_exp_def;
-      //normal_forms_exp.push_back(nf_exp_def);
-      //normal_form_src.push_back(eqc);
-      Trace("strings-solve") << "--- Single normal form for equivalence class " << eqc << std::endl;
+      }
+      Trace("strings-solve") << std::endl;
     }
+  } else {
+    //std::vector< Node > nf;
+    //nf.push_back( eqc );
+    //normal_forms.push_back(nf);
+    //std::vector< Node > nf_exp_def;
+    //normal_forms_exp.push_back(nf_exp_def);
+    //normal_form_src.push_back(eqc);
+    Trace("strings-solve") << "--- Single normal form for equivalence class " << eqc << std::endl;
+  }
        return true;
 }
 
@@ -939,8 +938,8 @@ void TheoryStrings::mergeCstVec(std::vector< Node > &vec_strings) {
 }
 
 bool TheoryStrings::detectLoop( std::vector< std::vector< Node > > &normal_forms,
-                                                               int i, int j, int index_i, int index_j,
-                                                               int &loop_in_i, int &loop_in_j) {
+  int i, int j, int index_i, int index_j,
+  int &loop_in_i, int &loop_in_j) {
        int has_loop[2] = { -1, -1 };
        if( options::stringLB() != 2 ) {
                for( unsigned r=0; r<2; r++ ) {
@@ -968,10 +967,10 @@ bool TheoryStrings::detectLoop( std::vector< std::vector< Node > > &normal_forms
 }
 //xs(zy)=t(yz)xr
 bool TheoryStrings::processLoop(std::vector< Node > &antec,
-                                                               std::vector< std::vector< Node > > &normal_forms,
-                                                               std::vector< Node > &normal_form_src,
-                                                               int i, int j, int loop_n_index, int other_n_index,
-                                                               int loop_index, int index, int other_index) {
+  std::vector< std::vector< Node > > &normal_forms,
+  std::vector< Node > &normal_form_src,
+  int i, int j, int loop_n_index, int other_n_index,
+  int loop_index, int index, int other_index) {
        Node conc;
        Trace("strings-loop") << "Detected possible loop for " << normal_forms[loop_n_index][loop_index] << std::endl;
        Trace("strings-loop") << " ... (X)= " << normal_forms[other_n_index][other_index] << std::endl;
@@ -1135,8 +1134,8 @@ bool TheoryStrings::processLoop(std::vector< Node > &antec,
        return true;
 }
 bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms,
-                                                               std::vector< std::vector< Node > > &normal_forms_exp,
-                                                               std::vector< Node > &normal_form_src) {
+  std::vector< std::vector< Node > > &normal_forms_exp,
+  std::vector< Node > &normal_form_src) {
        bool flag_lb = false;
        std::vector< Node > c_lb_exp;
        int c_i, c_j, c_loop_n_index, c_other_n_index, c_loop_index, c_index, c_other_index;
@@ -1316,7 +1315,7 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms
 }
 
 bool TheoryStrings::processReverseNEq( std::vector< std::vector< Node > > &normal_forms,
-                                                                          std::vector< Node > &normal_form_src, std::vector< Node > &curr_exp, unsigned i, unsigned j ) {
+  std::vector< Node > &normal_form_src, std::vector< Node > &curr_exp, unsigned i, unsigned j ) {
        //reverse normal form of i, j
        std::reverse( normal_forms[i].begin(), normal_forms[i].end() );
        std::reverse( normal_forms[j].begin(), normal_forms[j].end() );
@@ -1335,8 +1334,8 @@ bool TheoryStrings::processReverseNEq( std::vector< std::vector< Node > > &norma
 }
 
 bool TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal_forms,
-                                                                         std::vector< Node > &normal_form_src, std::vector< Node > &curr_exp,
-                                                                         unsigned i, unsigned j, unsigned& index_i, unsigned& index_j, bool isRev ) {
+  std::vector< Node > &normal_form_src, std::vector< Node > &curr_exp,
+  unsigned i, unsigned j, unsigned& index_i, unsigned& index_j, bool isRev ) {
        bool success;
        do {
                success = false;
@@ -1463,79 +1462,79 @@ bool TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal
 
 //nf_exp is conjunction
 bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp ) {
-    Trace("strings-process") << "Process equivalence class " << eqc << std::endl;
-    if( std::find( visited.begin(), visited.end(), eqc )!=visited.end() ){
-               getConcatVec( eqc, nf );
-        Trace("strings-process") << "Return process equivalence class " << eqc << " : already visited." << std::endl;
-               return false;
-    } else if( areEqual( eqc, d_emptyString ) ) {
-               eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
-               while( !eqc_i.isFinished() ) {
-                       Node n = (*eqc_i);
-                       if( n.getKind()==kind::STRING_CONCAT ){
-                               for( unsigned i=0; i<n.getNumChildren(); i++ ){
-                                       if( !areEqual( n[i], d_emptyString ) ){
-                                               sendLemma( n.eqNode( d_emptyString ), n[i].eqNode( d_emptyString ), "CYCLE" );
-                                       }
-                               }
-                       }
-                       ++eqc_i;
-               }
-        //do nothing
-        Trace("strings-process") << "Return process equivalence class " << eqc << " : empty." << std::endl;
-               d_normal_forms_base[eqc] = d_emptyString;
-               d_normal_forms[eqc].clear();
-               d_normal_forms_exp[eqc].clear();
-               return true;
-    } else {
-        visited.push_back( eqc );
-               bool result;
-        if(d_normal_forms.find(eqc)==d_normal_forms.end() ) {
-            //phi => t = s1 * ... * sn
-            // normal form for each non-variable term in this eqc (s1...sn)
-            std::vector< std::vector< Node > > normal_forms;
-            // explanation for each normal form (phi)
-            std::vector< std::vector< Node > > normal_forms_exp;
-            // record terms for each normal form (t)
-            std::vector< Node > normal_form_src;
-            //Get Normal Forms
-            result = getNormalForms(eqc, visited, nf, normal_forms, normal_forms_exp, normal_form_src);
-            if( d_conflict || !d_pending.empty() || !d_lemma_cache.empty() ) {
-                return true;
-            } else if( result ) {
-                               if(processNEqc(normal_forms, normal_forms_exp, normal_form_src)) {
-                                       return true;
-                               }
-                       }
-
-            //construct the normal form
-            if( normal_forms.empty() ){
-                Trace("strings-solve-debug2") << "construct the normal form" << std::endl;
-                               getConcatVec( eqc, nf );
-            } else {
-                Trace("strings-solve-debug2") << "just take the first normal form" << std::endl;
-                //just take the first normal form
-                nf.insert( nf.end(), normal_forms[0].begin(), normal_forms[0].end() );
-                nf_exp.insert( nf_exp.end(), normal_forms_exp[0].begin(), normal_forms_exp[0].end() );
-                if( eqc!=normal_form_src[0] ){
-                    nf_exp.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, eqc, normal_form_src[0] ) );
-                }
-                Trace("strings-solve-debug2") << "just take the first normal form ... done" << std::endl;
-            }
+  Trace("strings-process") << "Process equivalence class " << eqc << std::endl;
+  if( std::find( visited.begin(), visited.end(), eqc )!=visited.end() ){
+    getConcatVec( eqc, nf );
+    Trace("strings-process") << "Return process equivalence class " << eqc << " : already visited." << std::endl;
+    return false;
+  } else if( areEqual( eqc, d_emptyString ) ) {
+    eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
+    while( !eqc_i.isFinished() ) {
+      Node n = (*eqc_i);
+      if( n.getKind()==kind::STRING_CONCAT ){
+        for( unsigned i=0; i<n.getNumChildren(); i++ ){
+          if( !areEqual( n[i], d_emptyString ) ){
+            sendLemma( n.eqNode( d_emptyString ), n[i].eqNode( d_emptyString ), "CYCLE" );
+          }
+        }
+      }
+      ++eqc_i;
+    }
+    //do nothing
+    Trace("strings-process") << "Return process equivalence class " << eqc << " : empty." << std::endl;
+    d_normal_forms_base[eqc] = d_emptyString;
+    d_normal_forms[eqc].clear();
+    d_normal_forms_exp[eqc].clear();
+    return true;
+  } else {
+    visited.push_back( eqc );
+    bool result;
+    if(d_normal_forms.find(eqc)==d_normal_forms.end() ) {
+      //phi => t = s1 * ... * sn
+      // normal form for each non-variable term in this eqc (s1...sn)
+      std::vector< std::vector< Node > > normal_forms;
+      // explanation for each normal form (phi)
+      std::vector< std::vector< Node > > normal_forms_exp;
+      // record terms for each normal form (t)
+      std::vector< Node > normal_form_src;
+      //Get Normal Forms
+      result = getNormalForms(eqc, visited, nf, normal_forms, normal_forms_exp, normal_form_src);
+      if( d_conflict || !d_pending.empty() || !d_lemma_cache.empty() ) {
+          return true;
+      } else if( result ) {
+        if(processNEqc(normal_forms, normal_forms_exp, normal_form_src)) {
+          return true;
+        }
+      }
 
-           d_normal_forms_base[eqc] = normal_form_src.empty() ? eqc : normal_form_src[0];
-            d_normal_forms[eqc].insert( d_normal_forms[eqc].end(), nf.begin(), nf.end() );
-            d_normal_forms_exp[eqc].insert( d_normal_forms_exp[eqc].end(), nf_exp.begin(), nf_exp.end() );
-            Trace("strings-process") << "Return process equivalence class " << eqc << " : returned, size = " << nf.size() << std::endl;
-        }else{
-            Trace("strings-process") << "Return process equivalence class " << eqc << " : already computed, size = " << d_normal_forms[eqc].size() << std::endl;
-            nf.insert( nf.end(), d_normal_forms[eqc].begin(), d_normal_forms[eqc].end() );
-            nf_exp.insert( nf_exp.end(), d_normal_forms_exp[eqc].begin(), d_normal_forms_exp[eqc].end() );
-                       result = true;
+      //construct the normal form
+      if( normal_forms.empty() ){
+        Trace("strings-solve-debug2") << "construct the normal form" << std::endl;
+        getConcatVec( eqc, nf );
+      } else {
+        Trace("strings-solve-debug2") << "just take the first normal form" << std::endl;
+        //just take the first normal form
+        nf.insert( nf.end(), normal_forms[0].begin(), normal_forms[0].end() );
+        nf_exp.insert( nf_exp.end(), normal_forms_exp[0].begin(), normal_forms_exp[0].end() );
+        if( eqc!=normal_form_src[0] ){
+          nf_exp.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, eqc, normal_form_src[0] ) );
         }
-        visited.pop_back();
-               return result;
+        Trace("strings-solve-debug2") << "just take the first normal form ... done" << std::endl;
+      }
+
+      d_normal_forms_base[eqc] = normal_form_src.empty() ? eqc : normal_form_src[0];
+      d_normal_forms[eqc].insert( d_normal_forms[eqc].end(), nf.begin(), nf.end() );
+      d_normal_forms_exp[eqc].insert( d_normal_forms_exp[eqc].end(), nf_exp.begin(), nf_exp.end() );
+      Trace("strings-process") << "Return process equivalence class " << eqc << " : returned, size = " << nf.size() << std::endl;
+    } else {
+      Trace("strings-process") << "Return process equivalence class " << eqc << " : already computed, size = " << d_normal_forms[eqc].size() << std::endl;
+      nf.insert( nf.end(), d_normal_forms[eqc].begin(), d_normal_forms[eqc].end() );
+      nf_exp.insert( nf_exp.end(), d_normal_forms_exp[eqc].begin(), d_normal_forms_exp[eqc].end() );
+      result = true;
     }
+    visited.pop_back();
+    return result;
+  }
 }
 
 //return true for lemma, false if we succeed
@@ -1560,9 +1559,9 @@ bool TheoryStrings::processDeq( Node ni, Node nj ) {
                unsigned index = 0;
                while( index<nfi.size() || index<nfj.size() ){
                        int ret = processSimpleDeq( nfi, nfj, ni, nj, index, false );
-                       if( ret!=0 ){
+                       if( ret!=0 ) {
                                return ret==-1;
-                       }else{
+                       } else {
                                Assert( index<nfi.size() && index<nfj.size() );
                                Node i = nfi[index];
                                Node j = nfj[index];
@@ -1649,8 +1648,8 @@ int TheoryStrings::processReverseDeq( std::vector< Node >& nfi, std::vector< Nod
 }
 
 int TheoryStrings::processSimpleDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj, unsigned& index, bool isRev ) {
-       while( index<nfi.size() || index<nfj.size() ){
-               if( index>=nfi.size() || index>=nfj.size() ){
+       while( index<nfi.size() || index<nfj.size() ) {
+               if( index>=nfi.size() || index>=nfj.size() ) {
                        std::vector< Node > ant;
                        //we have a conflict : because the lengths are equal, the remainder needs to be empty, which will lead to a conflict
                        Node lni = getLength( ni );
@@ -1708,7 +1707,7 @@ int TheoryStrings::processSimpleDeq( std::vector< Node >& nfi, std::vector< Node
                                                Trace("strings-solve") << "Simple Case 2 : found equal length disequal sub strings " << i << " " << j << std::endl;
                                                //we are done: D-Remove
                                                return 1;
-                                       }else{
+                                       } else {
                                                return 0;
                                        }
                                }
@@ -1722,54 +1721,53 @@ int TheoryStrings::processSimpleDeq( std::vector< Node >& nfi, std::vector< Node
 void TheoryStrings::addNormalFormPair( Node n1, Node n2 ) {
   if( !isNormalFormPair( n1, n2 ) ){
                //Assert( !isNormalFormPair( n1, n2 ) );
-        NodeList* lst;
-        NodeListMap::iterator nf_i = d_nf_pairs.find( n1 );
-        if( nf_i == d_nf_pairs.end() ){
-          if( d_nf_pairs.find( n2 )!=d_nf_pairs.end() ){
-            addNormalFormPair( n2, n1 );
-            return;
-          }
-          lst = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false,
-                                                                ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) );
-          d_nf_pairs.insertDataFromContextMemory( n1, lst );
-                 Trace("strings-nf") << "Create cache for " << n1 << std::endl;
-        }else{
-          lst = (*nf_i).second;
-        }
+    NodeList* lst;
+    NodeListMap::iterator nf_i = d_nf_pairs.find( n1 );
+    if( nf_i == d_nf_pairs.end() ){
+      if( d_nf_pairs.find( n2 )!=d_nf_pairs.end() ){
+        addNormalFormPair( n2, n1 );
+        return;
+      }
+      lst = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false,
+                                                           ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) );
+      d_nf_pairs.insertDataFromContextMemory( n1, lst );
+      Trace("strings-nf") << "Create cache for " << n1 << std::endl;
+    } else {
+      lst = (*nf_i).second;
+    }
                Trace("strings-nf") << "Add normal form pair : " << n1 << " " << n2 << std::endl;
-        lst->push_back( n2 );
+    lst->push_back( n2 );
                Assert( isNormalFormPair( n1, n2 ) );
-    }else{
+  } else {
                Trace("strings-nf-debug") << "Already a normal form pair " << n1 << " " << n2 << std::endl;
        }
-
 }
 bool TheoryStrings::isNormalFormPair( Node n1, Node n2 ) {
-    //TODO: modulo equality?
-    return isNormalFormPair2( n1, n2 ) || isNormalFormPair2( n2, n1 );
+  //TODO: modulo equality?
+  return isNormalFormPair2( n1, n2 ) || isNormalFormPair2( n2, n1 );
 }
 bool TheoryStrings::isNormalFormPair2( Node n1, Node n2 ) {
     //Trace("strings-debug") << "is normal form pair. " << n1 << " " << n2 << std::endl;
   NodeList* lst;
   NodeListMap::iterator nf_i = d_nf_pairs.find( n1 );
-  if( nf_i != d_nf_pairs.end() ){
+  if( nf_i != d_nf_pairs.end() ) {
     lst = (*nf_i).second;
     for( NodeList::const_iterator i = lst->begin(); i != lst->end(); ++i ) {
-        Node n = *i;
-        if( n==n2 ){
-            return true;
-        }
+      Node n = *i;
+      if( n==n2 ) {
+          return true;
+      }
     }
   }
   return false;
 }
 
 void TheoryStrings::sendLemma( Node ant, Node conc, const char * c ) {
-       if( conc.isNull() || conc == d_false ){
+       if( conc.isNull() || conc == d_false ) {
                d_out->conflict(ant);
                Trace("strings-conflict") << "Strings::Conflict : " << ant << std::endl;
                d_conflict = true;
-       }else{
+       } else {
                Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, ant, conc );
                if( ant == d_true ) {
                        lem = conc;
@@ -1781,9 +1779,9 @@ void TheoryStrings::sendLemma( Node ant, Node conc, const char * c ) {
 
 void TheoryStrings::sendInfer( Node eq_exp, Node eq, const char * c ) {
        eq = Rewriter::rewrite( eq );
-       if( eq==d_false ){
+       if( eq==d_false ) {
                sendLemma( eq_exp, eq, c );
-       }else{
+       } else {
                Trace("strings-lemma") << "Strings::Infer " << eq << " from " << eq_exp << " by " << c << std::endl;
                d_pending.push_back( eq );
                d_pending_exp[eq] = eq_exp;
@@ -1804,11 +1802,11 @@ void TheoryStrings::sendSplit( Node a, Node b, const char * c, bool preq ) {
 }
 
 Node TheoryStrings::mkConcat( Node n1, Node n2 ) {
-       return NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, n1, n2 );
+       return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, n1, n2 ) );
 }
 
 Node TheoryStrings::mkConcat( std::vector< Node >& c ) {
-    Node cc = c.size()>1 ? NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, c ) : ( c.size()==1 ? c[0] : d_emptyString );
+  Node cc = c.size()>1 ? NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, c ) : ( c.size()==1 ? c[0] : d_emptyString );
        return Rewriter::rewrite( cc );
 }
 
@@ -1818,51 +1816,51 @@ Node TheoryStrings::mkExplain( std::vector< Node >& a ) {
 }
 
 Node TheoryStrings::mkExplain( std::vector< Node >& a, std::vector< Node >& an ) {
-    std::vector< TNode > antec_exp;
-    for( unsigned i=0; i<a.size(); i++ ){
-               if( std::find( a.begin(), a.begin() + i, a[i] )==a.begin() + i ){
-                       bool exp = true;
-                       Trace("strings-solve-debug") << "Ask for explanation of " << a[i] << std::endl;
-                       //assert
-                       if(a[i].getKind() == kind::EQUAL) {
-                               //assert( hasTerm(a[i][0]) );
-                               //assert( hasTerm(a[i][1]) );
-                               Assert( areEqual(a[i][0], a[i][1]) );
-                               if( a[i][0]==a[i][1] ){
-                                       exp = false;
-                               }
-                       } else if( a[i].getKind()==kind::NOT && a[i][0].getKind()==kind::EQUAL ){
-                               Assert( hasTerm(a[i][0][0]) );
-                               Assert( hasTerm(a[i][0][1]) );
-                               AlwaysAssert( d_equalityEngine.areDisequal(a[i][0][0], a[i][0][1], true) );
-                       }
-                       if( exp ){
-                               unsigned ps = antec_exp.size();
-                               explain(a[i], antec_exp);
-                               Trace("strings-solve-debug") << "Done, explanation was : " << std::endl;
-                               for( unsigned j=ps; j<antec_exp.size(); j++ ){
-                                       Trace("strings-solve-debug") << "  " << antec_exp[j] << std::endl;
-                               }
-                               Trace("strings-solve-debug") << std::endl;
-                       }
-               }
-    }
-    for( unsigned i=0; i<an.size(); i++ ){
-               if( std::find( an.begin(), an.begin() + i, an[i] )==an.begin() + i ){
-                       Trace("strings-solve-debug") << "Add to explanation (new literal) " << an[i] << std::endl;
-                       antec_exp.push_back(an[i]);
-               }
+  std::vector< TNode > antec_exp;
+  for( unsigned i=0; i<a.size(); i++ ) {
+    if( std::find( a.begin(), a.begin() + i, a[i] )==a.begin() + i ) {
+      bool exp = true;
+      Trace("strings-solve-debug") << "Ask for explanation of " << a[i] << std::endl;
+      //assert
+      if(a[i].getKind() == kind::EQUAL) {
+        //assert( hasTerm(a[i][0]) );
+        //assert( hasTerm(a[i][1]) );
+        Assert( areEqual(a[i][0], a[i][1]) );
+        if( a[i][0]==a[i][1] ){
+          exp = false;
+        }
+      } else if( a[i].getKind()==kind::NOT && a[i][0].getKind()==kind::EQUAL ) {
+        Assert( hasTerm(a[i][0][0]) );
+        Assert( hasTerm(a[i][0][1]) );
+        AlwaysAssert( d_equalityEngine.areDisequal(a[i][0][0], a[i][0][1], true) );
+      }
+      if( exp ) {
+        unsigned ps = antec_exp.size();
+        explain(a[i], antec_exp);
+        Trace("strings-solve-debug") << "Done, explanation was : " << std::endl;
+        for( unsigned j=ps; j<antec_exp.size(); j++ ) {
+          Trace("strings-solve-debug") << "  " << antec_exp[j] << std::endl;
+        }
+        Trace("strings-solve-debug") << std::endl;
+      }
     }
-    Node ant;
-    if( antec_exp.empty() ) {
-        ant = d_true;
-    } else if( antec_exp.size()==1 ) {
-        ant = antec_exp[0];
-    } else {
-        ant = NodeManager::currentNM()->mkNode( kind::AND, antec_exp );
+  }
+  for( unsigned i=0; i<an.size(); i++ ) {
+    if( std::find( an.begin(), an.begin() + i, an[i] )==an.begin() + i ){
+      Trace("strings-solve-debug") << "Add to explanation (new literal) " << an[i] << std::endl;
+      antec_exp.push_back(an[i]);
     }
+  }
+  Node ant;
+  if( antec_exp.empty() ) {
+    ant = d_true;
+  } else if( antec_exp.size()==1 ) {
+    ant = antec_exp[0];
+  } else {
+    ant = NodeManager::currentNM()->mkNode( kind::AND, antec_exp );
+  }
        ant = Rewriter::rewrite( ant );
-    return ant;
+  return ant;
 }
 
 Node TheoryStrings::mkAnd( std::vector< Node >& a ) {
@@ -1876,13 +1874,13 @@ Node TheoryStrings::mkAnd( std::vector< Node >& a ) {
 }
 
 void TheoryStrings::getConcatVec( Node n, std::vector< Node >& c ) {
-       if( n.getKind()==kind::STRING_CONCAT ){
-               for( unsigned i=0; i<n.getNumChildren(); i++ ){
-                       if( !areEqual( n[i], d_emptyString ) ){
+       if( n.getKind()==kind::STRING_CONCAT ) {
+               for( unsigned i=0; i<n.getNumChildren(); i++ ) {
+                       if( !areEqual( n[i], d_emptyString ) ) {
                                c.push_back( n[i] );
                        }
                }
-       }else{
+       } else {
                c.push_back( n );
        }
 }
@@ -1892,91 +1890,91 @@ bool TheoryStrings::checkSimple() {
 
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
   while( !eqcs_i.isFinished() ) {
-       Node eqc = (*eqcs_i);
-       //if eqc.getType is string
-       if (eqc.getType().isString()) {
-               //EqcInfo* ei = getOrMakeEqcInfo( eqc, true );
-               //get the constant for the equivalence class
-               //int c_len = ...;
-               eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
-               while( !eqc_i.isFinished() ){
-                       Node n = (*eqc_i);
-                       //if n is concat, and
-                       //if n has not instantiatied the concat..length axiom
-                       //then, add lemma
-                       if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT ) {
-                               if( d_length_nodes.find(n)==d_length_nodes.end() ) {
-                                       Trace("strings-debug") << "get n: " << n << endl;
-                                       Node sk;
-                                       //if( d_length_inst.find(n)==d_length_inst.end() ) {
-                                               //Node nr = d_equalityEngine.getRepresentative( n );
-                                               sk = NodeManager::currentNM()->mkSkolem( "lsym", n.getType(), "created for length" );
-                                               d_statistics.d_new_skolems += 1;
-                                               d_length_intro_vars.insert( sk );
-                                               Node eq = sk.eqNode(n);
-                                               eq = Rewriter::rewrite(eq);
-                                               Trace("strings-lemma") << "Strings::Lemma LENGTH Term : " << eq << std::endl;
-                                               d_out->lemma(eq);
-                                       //} else {
-                                       //      sk = d_length_inst[n];
-                                       //}
-                                       Node skl = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk );
-                                       Node lsum;
-                                       if( n.getKind() == kind::STRING_CONCAT ) {
-                                               //add lemma
-                                               std::vector<Node> node_vec;
-                                               for( unsigned i=0; i<n.getNumChildren(); i++ ) {
-                                                       Node lni = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[i] );
-                                                       node_vec.push_back(lni);
-                                               }
-                                               lsum = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::PLUS, node_vec ) );
-                                       } else if( n.getKind() == kind::CONST_STRING ) {
-                                               //add lemma
-                                               lsum = NodeManager::currentNM()->mkConst( ::CVC4::Rational( n.getConst<String>().size() ) );
-                                       }
-                                       Node ceq = NodeManager::currentNM()->mkNode( kind::EQUAL, skl, lsum );
-                                       ceq = Rewriter::rewrite(ceq);
-                                       Trace("strings-lemma") << "Strings::Lemma LENGTH : " << ceq << std::endl;
-                                       d_out->lemma(ceq);
-                                       addedLemma = true;
+    Node eqc = (*eqcs_i);
+    //if eqc.getType is string
+    if (eqc.getType().isString()) {
+      //EqcInfo* ei = getOrMakeEqcInfo( eqc, true );
+      //get the constant for the equivalence class
+      //int c_len = ...;
+      eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
+      while( !eqc_i.isFinished() ) {
+        Node n = (*eqc_i);
+        //if n is concat, and
+        //if n has not instantiatied the concat..length axiom
+        //then, add lemma
+        if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT ) {
+          if( d_length_nodes.find(n)==d_length_nodes.end() ) {
+            Trace("strings-debug") << "get n: " << n << endl;
+            Node sk;
+            //if( d_length_inst.find(n)==d_length_inst.end() ) {
+              //Node nr = d_equalityEngine.getRepresentative( n );
+              sk = NodeManager::currentNM()->mkSkolem( "lsym", n.getType(), "created for length" );
+              d_statistics.d_new_skolems += 1;
+              d_length_intro_vars.insert( sk );
+              Node eq = sk.eqNode(n);
+              eq = Rewriter::rewrite(eq);
+              Trace("strings-lemma") << "Strings::Lemma LENGTH Term : " << eq << std::endl;
+              d_out->lemma(eq);
+            //} else {
+            // sk = d_length_inst[n];
+            //}
+            Node skl = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk );
+            Node lsum;
+            if( n.getKind() == kind::STRING_CONCAT ) {
+              //add lemma
+              std::vector<Node> node_vec;
+              for( unsigned i=0; i<n.getNumChildren(); i++ ) {
+                Node lni = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[i] );
+                node_vec.push_back(lni);
+              }
+              lsum = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::PLUS, node_vec ) );
+            } else if( n.getKind() == kind::CONST_STRING ) {
+              //add lemma
+              lsum = NodeManager::currentNM()->mkConst( ::CVC4::Rational( n.getConst<String>().size() ) );
+            }
+            Node ceq = NodeManager::currentNM()->mkNode( kind::EQUAL, skl, lsum );
+            ceq = Rewriter::rewrite(ceq);
+            Trace("strings-lemma") << "Strings::Lemma LENGTH : " << ceq << std::endl;
+            d_out->lemma(ceq);
+            addedLemma = true;
 
-                                       d_length_nodes.insert(n);
-                               }
-                       }
-                       ++eqc_i;
-               }
-       }
-       ++eqcs_i;
+            d_length_nodes.insert(n);
+          }
+        }
+        ++eqc_i;
+      }
+    }
+    ++eqcs_i;
   }
   return addedLemma;
 }
 
 bool TheoryStrings::checkNormalForms() {
-    Trace("strings-process") << "Normalize equivalence classes...." << std::endl;
+  Trace("strings-process") << "Normalize equivalence classes...." << std::endl;
        eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator( &d_equalityEngine );
-       for( unsigned t=0; t<2; t++ ){
+       for( unsigned t=0; t<2; t++ ) {
                Trace("strings-eqc") << (t==0 ? "STRINGS:" : "OTHER:") << std::endl;
                while( !eqcs2_i.isFinished() ){
-               Node eqc = (*eqcs2_i);
-               bool print = (t==0 && eqc.getType().isString() ) || (t==1 && !eqc.getType().isString() );
-               if (print) {
-                       eq::EqClassIterator eqc2_i = eq::EqClassIterator( eqc, &d_equalityEngine );
-                       Trace("strings-eqc") << "Eqc( " << eqc << " ) : { ";
-                       while( !eqc2_i.isFinished() ) {
-                               if( (*eqc2_i)!=eqc ){
-                                       Trace("strings-eqc") << (*eqc2_i) << " ";
-                               }
-                               ++eqc2_i;
-                       }
-                       Trace("strings-eqc") << " } " << std::endl;
-                       EqcInfo * ei = getOrMakeEqcInfo( eqc, false );
-                       if( ei ){
-                               Trace("strings-eqc-debug") << "* Length term : " << ei->d_length_term.get() << std::endl;
-                               Trace("strings-eqc-debug") << "* Cardinality lemma k : " << ei->d_cardinality_lem_k.get() << std::endl;
-                               Trace("strings-eqc-debug") << "* Normalization length lemma : " << ei->d_normalized_length.get() << std::endl;
-                       }
-               }
-               ++eqcs2_i;
+      Node eqc = (*eqcs2_i);
+      bool print = (t==0 && eqc.getType().isString() ) || (t==1 && !eqc.getType().isString() );
+      if (print) {
+        eq::EqClassIterator eqc2_i = eq::EqClassIterator( eqc, &d_equalityEngine );
+        Trace("strings-eqc") << "Eqc( " << eqc << " ) : { ";
+        while( !eqc2_i.isFinished() ) {
+          if( (*eqc2_i)!=eqc ){
+            Trace("strings-eqc") << (*eqc2_i) << " ";
+          }
+          ++eqc2_i;
+        }
+        Trace("strings-eqc") << " } " << std::endl;
+        EqcInfo * ei = getOrMakeEqcInfo( eqc, false );
+        if( ei ){
+          Trace("strings-eqc-debug") << "* Length term : " << ei->d_length_term.get() << std::endl;
+          Trace("strings-eqc-debug") << "* Cardinality lemma k : " << ei->d_cardinality_lem_k.get() << std::endl;
+          Trace("strings-eqc-debug") << "* Normalization length lemma : " << ei->d_normalized_length.get() << std::endl;
+        }
+      }
+      ++eqcs2_i;
                }
                Trace("strings-eqc") << std::endl;
        }
@@ -2012,56 +2010,56 @@ bool TheoryStrings::checkNormalForms() {
 
   bool addedFact;
   do {
-       Trace("strings-process") << "Check Normal Forms........next round" << std::endl;
+    Trace("strings-process") << "Check Normal Forms........next round" << std::endl;
     //calculate normal forms for each equivalence class, possibly adding splitting lemmas
     d_normal_forms.clear();
     d_normal_forms_exp.clear();
     std::map< Node, Node > nf_to_eqc;
     std::map< Node, Node > eqc_to_exp;
     d_lemma_cache.clear();
-       d_pending_req_phase.clear();
-       //get equivalence classes
-       std::vector< Node > eqcs;
-       getEquivalenceClasses( eqcs );
-       for( unsigned i=0; i<eqcs.size(); i++ ){
-               Node eqc = eqcs[i];
-               Trace("strings-process") << "- Verify normal forms are the same for " << eqc << std::endl;
-               std::vector< Node > visited;
-               std::vector< Node > nf;
-               std::vector< Node > nf_exp;
-               normalizeEquivalenceClass(eqc, visited, nf, nf_exp);
-               Trace("strings-debug") << "Finished normalizing eqc..." << std::endl;
-               if( d_conflict ){
-                       doPendingFacts();
-                       doPendingLemmas();
-                       return true;
-               }else if ( d_pending.empty() && d_lemma_cache.empty() ){
-                       Node nf_term;
-                       if( nf.size()==0 ){
-                               nf_term = d_emptyString;
-                       }else if( nf.size()==1 ) {
-                               nf_term = nf[0];
-                       } else {
-                               nf_term = NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, nf );
-                       }
-                       nf_term = Rewriter::rewrite( nf_term );
-                       Trace("strings-debug") << "Make nf_term_exp..." << std::endl;
-                       Node nf_term_exp = nf_exp.empty() ? d_true :
-                                                               nf_exp.size()==1 ? nf_exp[0] : NodeManager::currentNM()->mkNode( kind::AND, nf_exp );
-                       if( nf_to_eqc.find(nf_term)!=nf_to_eqc.end() ){
-                               //Trace("strings-debug") << "Merge because of normal form : " << eqc << " and " << nf_to_eqc[nf_term] << " both have normal form " << nf_term << std::endl;
-                               //two equivalence classes have same normal form, merge
-                               Node eq_exp = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, nf_term_exp, eqc_to_exp[nf_to_eqc[nf_term]] ) );
-                               Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, eqc, nf_to_eqc[nf_term] );
-                               sendInfer( eq_exp, eq, "Normal_Form" );
-                               //d_equalityEngine.assertEquality( eq, true, eq_exp );
-                       }else{
-                               nf_to_eqc[nf_term] = eqc;
-                               eqc_to_exp[eqc] = nf_term_exp;
-                       }
-               }
-               Trace("strings-process") << "Done verifying normal forms are the same for " << eqc << std::endl;
-       }
+    d_pending_req_phase.clear();
+    //get equivalence classes
+    std::vector< Node > eqcs;
+    getEquivalenceClasses( eqcs );
+    for( unsigned i=0; i<eqcs.size(); i++ ){
+      Node eqc = eqcs[i];
+      Trace("strings-process") << "- Verify normal forms are the same for " << eqc << std::endl;
+      std::vector< Node > visited;
+      std::vector< Node > nf;
+      std::vector< Node > nf_exp;
+      normalizeEquivalenceClass(eqc, visited, nf, nf_exp);
+      Trace("strings-debug") << "Finished normalizing eqc..." << std::endl;
+      if( d_conflict ) {
+        doPendingFacts();
+        doPendingLemmas();
+        return true;
+      } else if ( d_pending.empty() && d_lemma_cache.empty() ) {
+        Node nf_term;
+        if( nf.size()==0 ){
+          nf_term = d_emptyString;
+        }else if( nf.size()==1 ) {
+          nf_term = nf[0];
+        } else {
+          nf_term = NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, nf );
+        }
+        nf_term = Rewriter::rewrite( nf_term );
+        Trace("strings-debug") << "Make nf_term_exp..." << std::endl;
+        Node nf_term_exp = nf_exp.empty() ? d_true :
+                  nf_exp.size()==1 ? nf_exp[0] : NodeManager::currentNM()->mkNode( kind::AND, nf_exp );
+        if( nf_to_eqc.find(nf_term)!=nf_to_eqc.end() ) {
+          //Trace("strings-debug") << "Merge because of normal form : " << eqc << " and " << nf_to_eqc[nf_term] << " both have normal form " << nf_term << std::endl;
+          //two equivalence classes have same normal form, merge
+          Node eq_exp = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, nf_term_exp, eqc_to_exp[nf_to_eqc[nf_term]] ) );
+          Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, eqc, nf_to_eqc[nf_term] );
+          sendInfer( eq_exp, eq, "Normal_Form" );
+          //d_equalityEngine.assertEquality( eq, true, eq_exp );
+        } else {
+          nf_to_eqc[nf_term] = eqc;
+          eqc_to_exp[eqc] = nf_term_exp;
+        }
+      }
+      Trace("strings-process") << "Done verifying normal forms are the same for " << eqc << std::endl;
+    }
 
          Trace("strings-nf-debug") << "**** Normal forms are : " << std::endl;
          for( std::map< Node, Node >::iterator it = nf_to_eqc.begin(); it != nf_to_eqc.end(); ++it ){
@@ -2078,10 +2076,10 @@ bool TheoryStrings::checkNormalForms() {
   Trace("strings-solve") << "Finished check normal forms, #lemmas = " << d_lemma_cache.size() << ", conflict = " << d_conflict << std::endl;
   //flush pending lemmas
   if( !d_lemma_cache.empty() ){
-       doPendingLemmas();
-       return true;
+    doPendingLemmas();
+    return true;
   }else{
-       return false;
+    return false;
   }
 }
 
@@ -2148,7 +2146,7 @@ bool TheoryStrings::checkLengthsEqc() {
                                        addedLemma = true;
                                }
                        }
-               }else{
+               } else {
                        Trace("strings-process-debug") << "Do not process length constraints for " << nodes[i] << " " << d_normal_forms[nodes[i]].size() << std::endl;
                }
        }
@@ -2169,111 +2167,111 @@ bool TheoryStrings::checkCardinality() {
   std::vector< Node > lts;
   separateByLength( eqcs, cols, lts );
 
-  for( unsigned i = 0; i<cols.size(); ++i ){
+  for( unsigned i = 0; i<cols.size(); ++i ) {
     Node lr = lts[i];
     Trace("strings-card") << "Number of strings with length equal to " << lr << " is " << cols[i].size() << std::endl;
     if( cols[i].size() > 1 ) {
-               // size > c^k
-               double k = 1.0 + std::log((double) cols[i].size() - 1) / log((double) cardinality);
-               unsigned int int_k = (unsigned int) k;
-               //double c_k = pow ( (double)cardinality, (double)lr );
-
-        bool allDisequal = true;
-        for( std::vector< Node >::iterator itr1 = cols[i].begin();
-              itr1 != cols[i].end(); ++itr1) {
-            for( std::vector< Node >::iterator itr2 = itr1 + 1;
-                  itr2 != cols[i].end(); ++itr2) {
-                               if(!areDisequal( *itr1, *itr2 )) {
-                    allDisequal = false;
-                    // add split lemma
-                                       sendSplit( *itr1, *itr2, "CARD-SP" );
-                                       doPendingLemmas();
-                                       return true;
-                }
-            }
+      // size > c^k
+      double k = 1.0 + std::log((double) cols[i].size() - 1) / log((double) cardinality);
+      unsigned int int_k = (unsigned int) k;
+      //double c_k = pow ( (double)cardinality, (double)lr );
+
+      bool allDisequal = true;
+      for( std::vector< Node >::iterator itr1 = cols[i].begin();
+           itr1 != cols[i].end(); ++itr1) {
+        for( std::vector< Node >::iterator itr2 = itr1 + 1;
+          itr2 != cols[i].end(); ++itr2) {
+          if(!areDisequal( *itr1, *itr2 )) {
+            allDisequal = false;
+            // add split lemma
+            sendSplit( *itr1, *itr2, "CARD-SP" );
+            doPendingLemmas();
+            return true;
+          }
         }
-        if(allDisequal) {
-            EqcInfo* ei = getOrMakeEqcInfo( lr, true );
-            Trace("strings-card") << "Previous cardinality used for " << lr << " is " << ((int)ei->d_cardinality_lem_k.get()-1) << std::endl;
-            if( int_k+1 > ei->d_cardinality_lem_k.get() ){
-                               Node k_node = NodeManager::currentNM()->mkConst( ::CVC4::Rational( int_k ) );
-                               //add cardinality lemma
-                Node dist = NodeManager::currentNM()->mkNode( kind::DISTINCT, cols[i] );
-                std::vector< Node > vec_node;
-                vec_node.push_back( dist );
-                for( std::vector< Node >::iterator itr1 = cols[i].begin();
-                      itr1 != cols[i].end(); ++itr1) {
-                    Node len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, *itr1 );
-                    if( len!=lr ){
-                      Node len_eq_lr = len.eqNode(lr);
-                      vec_node.push_back( len_eq_lr );
-                    }
-                }
-                Node antc = NodeManager::currentNM()->mkNode( kind::AND, vec_node );
-                Node len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, cols[i][0] );
-                Node cons = NodeManager::currentNM()->mkNode( kind::GEQ, len, k_node );
-                               /*
-                               sendLemma( antc, cons, "Cardinality" );
-                               ei->d_cardinality_lem_k.set( int_k+1 );
-                               if( !d_lemma_cache.empty() ){
-                                       doPendingLemmas();
-                                       return true;
-                               }
-                               */
-                Node lemma = NodeManager::currentNM()->mkNode( kind::IMPLIES, antc, cons );
-                               lemma = Rewriter::rewrite( lemma );
-                               ei->d_cardinality_lem_k.set( int_k+1 );
-                               if( lemma!=d_true ){
-                                       Trace("strings-lemma") << "Strings::Lemma CARDINALITY : " << lemma << std::endl;
-                                       d_out->lemma(lemma);
-                                       return true;
-                               }
+      }
+      if(allDisequal) {
+        EqcInfo* ei = getOrMakeEqcInfo( lr, true );
+        Trace("strings-card") << "Previous cardinality used for " << lr << " is " << ((int)ei->d_cardinality_lem_k.get()-1) << std::endl;
+        if( int_k+1 > ei->d_cardinality_lem_k.get() ){
+          Node k_node = NodeManager::currentNM()->mkConst( ::CVC4::Rational( int_k ) );
+          //add cardinality lemma
+          Node dist = NodeManager::currentNM()->mkNode( kind::DISTINCT, cols[i] );
+          std::vector< Node > vec_node;
+          vec_node.push_back( dist );
+          for( std::vector< Node >::iterator itr1 = cols[i].begin();
+               itr1 != cols[i].end(); ++itr1) {
+            Node len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, *itr1 );
+            if( len!=lr ) {
+              Node len_eq_lr = len.eqNode(lr);
+              vec_node.push_back( len_eq_lr );
             }
+          }
+          Node antc = NodeManager::currentNM()->mkNode( kind::AND, vec_node );
+          Node len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, cols[i][0] );
+          Node cons = NodeManager::currentNM()->mkNode( kind::GEQ, len, k_node );
+          /*
+          sendLemma( antc, cons, "Cardinality" );
+          ei->d_cardinality_lem_k.set( int_k+1 );
+          if( !d_lemma_cache.empty() ){
+            doPendingLemmas();
+            return true;
+          }
+          */
+          Node lemma = NodeManager::currentNM()->mkNode( kind::IMPLIES, antc, cons );
+          lemma = Rewriter::rewrite( lemma );
+          ei->d_cardinality_lem_k.set( int_k+1 );
+          if( lemma!=d_true ){
+            Trace("strings-lemma") << "Strings::Lemma CARDINALITY : " << lemma << std::endl;
+            d_out->lemma(lemma);
+            return true;
+          }
         }
+      }
     }
   }
   return false;
 }
 
 void TheoryStrings::getEquivalenceClasses( std::vector< Node >& eqcs ) {
-    eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
-    while( !eqcs_i.isFinished() ) {
-        Node eqc = (*eqcs_i);
-        //if eqc.getType is string
-        if (eqc.getType().isString()) {
-                       eqcs.push_back( eqc );
-        }
-        ++eqcs_i;
+  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
+  while( !eqcs_i.isFinished() ) {
+    Node eqc = (*eqcs_i);
+    //if eqc.getType is string
+    if (eqc.getType().isString()) {
+      eqcs.push_back( eqc );
     }
+    ++eqcs_i;
+  }
 }
 
 void TheoryStrings::getFinalNormalForm( Node n, std::vector< Node >& nf, std::vector< Node >& exp ) {
-       if( n!=d_emptyString ){
-               if( n.getKind()==kind::STRING_CONCAT ){
-                       for( unsigned i=0; i<n.getNumChildren(); i++ ){
+       if( n!=d_emptyString ) {
+               if( n.getKind()==kind::STRING_CONCAT ) {
+                       for( unsigned i=0; i<n.getNumChildren(); i++ ) {
                                getFinalNormalForm( n[i], nf, exp );
                        }
-               }else{
+               } else {
                        Trace("strings-debug") << "Get final normal form " << n << std::endl;
                        Assert( d_equalityEngine.hasTerm( n ) );
                        Node nr = d_equalityEngine.getRepresentative( n );
                        EqcInfo *eqc_n = getOrMakeEqcInfo( nr, false );
                        Node nc = eqc_n ? eqc_n->d_const_term.get() : Node::null();
-                       if( !nc.isNull() ){
+                       if( !nc.isNull() ) {
                                nf.push_back( nc );
-                               if( n!=nc ){
+                               if( n!=nc ) {
                                        exp.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, n, nc ) );
                                }
-                       }else{
+                       } else {
                                Assert( d_normal_forms.find( nr )!=d_normal_forms.end() );
-                               if( d_normal_forms[nr][0]==nr ){
+                               if( d_normal_forms[nr][0]==nr ) {
                                        Assert( d_normal_forms[nr].size()==1 );
                                        nf.push_back( nr );
-                                       if( n!=nr ){
+                                       if( n!=nr ) {
                                                exp.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, n, nr ) );
                                        }
-                               }else{
-                                       for( unsigned i=0; i<d_normal_forms[nr].size(); i++ ){
+                               } else {
+                                       for( unsigned i=0; i<d_normal_forms[nr].size(); i++ ) {
                                                Assert( d_normal_forms[nr][i]!=nr );
                                                getFinalNormalForm( d_normal_forms[nr][i], nf, exp );
                                        }
@@ -2285,36 +2283,37 @@ void TheoryStrings::getFinalNormalForm( Node n, std::vector< Node >& nf, std::ve
        }
 }
 
-void TheoryStrings::separateByLength( std::vector< Node >& n, std::vector< std::vector< Node > >& cols,
-                                                                                        std::vector< Node >& lts ) {
+void TheoryStrings::separateByLength(std::vector< Node >& n,
+  std::vector< std::vector< Node > >& cols,
+       std::vector< Node >& lts ) {
   unsigned leqc_counter = 0;
   std::map< Node, unsigned > eqc_to_leqc;
   std::map< unsigned, Node > leqc_to_eqc;
   std::map< unsigned, std::vector< Node > > eqc_to_strings;
-  for( unsigned i=0; i<n.size(); i++ ){
-       Node eqc = n[i];
-       Assert( d_equalityEngine.getRepresentative(eqc)==eqc );
-       EqcInfo* ei = getOrMakeEqcInfo( eqc, false );
-       Node lt = ei ? ei->d_length_term : Node::null();
-       if( !lt.isNull() ){
-         lt = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt );
-         Node r = d_equalityEngine.getRepresentative( lt );
-         if( eqc_to_leqc.find( r )==eqc_to_leqc.end() ){
-               eqc_to_leqc[r] = leqc_counter;
-               leqc_to_eqc[leqc_counter] = r;
-               leqc_counter++;
-         }
-         eqc_to_strings[ eqc_to_leqc[r] ].push_back( eqc );
-       }else{
-         eqc_to_strings[leqc_counter].push_back( eqc );
-         leqc_counter++;
-       }
+  for( unsigned i=0; i<n.size(); i++ ) {
+    Node eqc = n[i];
+    Assert( d_equalityEngine.getRepresentative(eqc)==eqc );
+    EqcInfo* ei = getOrMakeEqcInfo( eqc, false );
+    Node lt = ei ? ei->d_length_term : Node::null();
+    if( !lt.isNull() ){
+      lt = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt );
+      Node r = d_equalityEngine.getRepresentative( lt );
+      if( eqc_to_leqc.find( r )==eqc_to_leqc.end() ){
+      eqc_to_leqc[r] = leqc_counter;
+      leqc_to_eqc[leqc_counter] = r;
+      leqc_counter++;
+      }
+      eqc_to_strings[ eqc_to_leqc[r] ].push_back( eqc );
+    }else{
+      eqc_to_strings[leqc_counter].push_back( eqc );
+      leqc_counter++;
+    }
   }
   for( std::map< unsigned, std::vector< Node > >::iterator it = eqc_to_strings.begin(); it != eqc_to_strings.end(); ++it ){
-       std::vector< Node > vec;
-       vec.insert( vec.end(), it->second.begin(), it->second.end() );
-       lts.push_back( leqc_to_eqc[it->first] );
-       cols.push_back( vec );
+    std::vector< Node > vec;
+    vec.insert( vec.end(), it->second.begin(), it->second.end() );
+    lts.push_back( leqc_to_eqc[it->first] );
+    cols.push_back( vec );
   }
 }
 
@@ -2350,10 +2349,12 @@ Node TheoryStrings::mkRegExpAntec(Node atom, Node ant) {
 
 bool TheoryStrings::checkMemberships() {
        bool addedLemma = false;
+       bool changed = false;
        std::vector< Node > processed;
        std::vector< Node > cprocessed;
 
        //if(options::stringEIT()) {
+               //TODO: Opt for normal forms
                for(NodeListMap::const_iterator itr_xr = d_str_re_map.begin();
                        itr_xr != d_str_re_map.end(); ++itr_xr ) {
                        bool spflag = false;
@@ -2415,175 +2416,248 @@ bool TheoryStrings::checkMemberships() {
 
        if(!addedLemma) {
          for( unsigned i=0; i<d_regexp_memberships.size(); i++ ) {
-               //check regular expression membership
-               Node assertion = d_regexp_memberships[i];
-               if( d_regexp_ucached.find(assertion) == d_regexp_ucached.end() 
-                       && d_regexp_ccached.find(assertion) == d_regexp_ccached.end() ) {
-                       Trace("strings-regexp") << "We have regular expression assertion : " << assertion << std::endl;
-                       Node atom = assertion.getKind()==kind::NOT ? assertion[0] : assertion;
-                       bool polarity = assertion.getKind()!=kind::NOT;
-                       bool flag = true;
-                       Node x = atom[0];
-                       Node r = atom[1];
-                       if( polarity ) {
-                               flag = checkPDerivative(x, r, atom, addedLemma, processed, cprocessed);
-                       } else {
-                               if(! options::stringExp()) {
-                                       throw LogicException("Strings Incomplete (due to Negative Membership) by default, try --strings-exp option.");
-                               }
-                       }
-                       if(flag) {
-                               //check if the term is atomic
-                               Node xr = getRepresentative( x );
-                               Trace("strings-regexp") << xr << " is rep of " << x << std::endl;
-                               Assert( d_normal_forms.find( xr )!=d_normal_forms.end() );
-                               //TODO
-                               if( true || r.getKind()!=kind::REGEXP_STAR || ( d_normal_forms[xr].size()==1 && x.getKind()!=kind::STRING_CONCAT ) ){
-                                       Trace("strings-regexp") << "Unroll/simplify membership of atomic term " << xr << std::endl;
-                                       //if so, do simple unrolling
-                                       std::vector< Node > nvec;
-                                       d_regexp_opr.simplify(atom, nvec, polarity);
-                                       Node antec = assertion;
-                                       if(d_regexp_ant.find(assertion) != d_regexp_ant.end()) {
-                                               antec = d_regexp_ant[assertion];
-                                               for(std::vector< Node >::const_iterator itr=nvec.begin(); itr<nvec.end(); itr++) {
-                                                       if(itr->getKind() == kind::STRING_IN_REGEXP) {
-                                                               if(d_regexp_ant.find( *itr ) == d_regexp_ant.end()) {
-                                                                       d_regexp_ant[ *itr ] = antec;
-                                                               }
-                                                       }
-                                               }
-                                       }
-                                       Node conc = nvec.size()==1 ? nvec[0] :
-                                                       NodeManager::currentNM()->mkNode(kind::AND, nvec);
-                                       conc = Rewriter::rewrite(conc);
-                                       sendLemma( antec, conc, "REGEXP" );
-                                       addedLemma = true;
-                                       processed.push_back( assertion );
-                                       //d_regexp_ucached[assertion] = true;
-                               } else {
-                                       Trace("strings-regexp") << "Unroll/simplify membership of non-atomic term " << xr << " = ";
-                                       for( unsigned j=0; j<d_normal_forms[xr].size(); j++ ){
-                                               Trace("strings-regexp") << d_normal_forms[xr][j] << " ";
-                                       }
-                                       Trace("strings-regexp") << ", polarity = " << polarity << std::endl;
-                                       //otherwise, distribute unrolling over parts
-                                       Node p1;
-                                       Node p2;
-                                       if( d_normal_forms[xr].size()>1 ){
-                                               p1 = d_normal_forms[xr][0];
-                                               std::vector< Node > cc;
-                                               cc.insert( cc.begin(), d_normal_forms[xr].begin() + 1, d_normal_forms[xr].end() );
-                                               p2 = mkConcat( cc );
-                                       }
+      //check regular expression membership
+      Node assertion = d_regexp_memberships[i];
+      if( d_regexp_ucached.find(assertion) == d_regexp_ucached.end() 
+        && d_regexp_ccached.find(assertion) == d_regexp_ccached.end() ) {
+        Trace("strings-regexp") << "We have regular expression assertion : " << assertion << std::endl;
+        Node atom = assertion.getKind()==kind::NOT ? assertion[0] : assertion;
+        bool polarity = assertion.getKind()!=kind::NOT;
+        bool flag = true;
+        Node x = atom[0];
+        Node r = atom[1];
+        std::vector< Node > rnfexp;
+
+        if(options::stringOpt1()) {
+          if(!x.isConst()) {
+            x = getNormalString(x, rnfexp);
+            changed = true;
+          }
+          if(!d_regexp_opr.checkConstRegExp(r)) {
+            r = getNormalSymRegExp(r, rnfexp);
+            changed = true;
+          }
+          Trace("strings-regexp-nf") << "Term " << atom << " is normalized to " << x << " IN " << r << std::endl;
+          if(changed) {
+            Node tmp = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x, r) );
+            if(!polarity) {
+              tmp = tmp.negate();
+            }
+            if(tmp == d_true) {
+              d_regexp_ccached.insert(assertion);
+              continue;
+            } else if(tmp == d_false) {
+              Node antec = mkRegExpAntec(assertion, mkExplain(rnfexp));
+              Node conc = Node::null();
+              sendLemma(antec, conc, "REGEXP NF Conflict");
+              addedLemma = true;
+              break;
+            }
+          }
+        }
 
-                                       Trace("strings-regexp-debug") << "Construct antecedant..." << std::endl;
-                                       std::vector< Node > antec;
-                                       std::vector< Node > antecn;
-                                       antec.insert( antec.begin(), d_normal_forms_exp[xr].begin(), d_normal_forms_exp[xr].end() );
-                                       if( x!=xr ){
-                                               antec.push_back( x.eqNode( xr ) );
-                                       }
-                                       antecn.push_back( assertion );
-                                       Node ant = mkExplain( antec, antecn );
-                                       Trace("strings-regexp-debug") << "Construct conclusion..." << std::endl;
-                                       Node conc;
-                                       if( polarity ){
-                                               if( d_normal_forms[xr].size()==0 ){
-                                                       conc = d_true;
-                                               }else if( d_normal_forms[xr].size()==1 ){
-                                                       Trace("strings-regexp-debug") << "Case 1\n";
-                                                       conc = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, d_normal_forms[xr][0], r);
-                                               }else{
-                                                       Trace("strings-regexp-debug") << "Case 2\n";
-                                                       std::vector< Node > conc_c;
-                                                       Node s11 = NodeManager::currentNM()->mkSkolem( "s11", NodeManager::currentNM()->stringType(), "created for re" );
-                                                       Node s12 = NodeManager::currentNM()->mkSkolem( "s12", NodeManager::currentNM()->stringType(), "created for re" );
-                                                       Node s21 = NodeManager::currentNM()->mkSkolem( "s21", NodeManager::currentNM()->stringType(), "created for re" );
-                                                       Node s22 = NodeManager::currentNM()->mkSkolem( "s22", NodeManager::currentNM()->stringType(), "created for re" );
-                                                       conc = p1.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s11, s12));
-                                                       conc_c.push_back(conc);
-                                                       conc = p2.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s21, s22));
-                                                       conc_c.push_back(conc);
-                                                       conc = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s11, r);
-                                                       conc_c.push_back(conc);
-                                                       conc = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s12, s21), r[0]);
-                                                       conc_c.push_back(conc);
-                                                       conc = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s22, r);
-                                                       conc_c.push_back(conc);
-                                                       conc = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND, conc_c));
-                                                       Node eqz = Rewriter::rewrite(x.eqNode(d_emptyString));
-                                                       conc = NodeManager::currentNM()->mkNode(kind::OR, eqz, conc);
-                                                       d_pending_req_phase[eqz] = true;
-                                               }
-                                       }else{
-                                               if( d_normal_forms[xr].size()==0 ){
-                                                       conc = d_false;
-                                               }else if( d_normal_forms[xr].size()==1 ){
-                                                       Trace("strings-regexp-debug") << "Case 3\n";
-                                                       conc = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, d_normal_forms[xr][0], r).negate();
-                                               }else{
-                                                       Trace("strings-regexp-debug") << "Case 4\n";
-                                                       Node len1 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, p1);
-                                                       Node len2 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, p2);
-                                                       Node bi = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
-                                                       Node bj = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
-                                                       Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, bi, bj);
-                                                       Node g1 = NodeManager::currentNM()->mkNode(kind::AND, 
-                                                                               NodeManager::currentNM()->mkNode(kind::GEQ, bi, d_zero),
-                                                                               NodeManager::currentNM()->mkNode(kind::GEQ, len1, bi),
-                                                                               NodeManager::currentNM()->mkNode(kind::GEQ, bj, d_zero),
-                                                                               NodeManager::currentNM()->mkNode(kind::GEQ, len2, bj));
-                                                       Node s11 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, p1, d_zero, bi);
-                                                       Node s12 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, p1, bi, NodeManager::currentNM()->mkNode(kind::MINUS, len1, bi));
-                                                       Node s21 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, p2, d_zero, bj);
-                                                       Node s22 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, p2, bj, NodeManager::currentNM()->mkNode(kind::MINUS, len2, bj));
-                                                       Node cc1 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s11, r).negate();
-                                                       Node cc2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s12, s21), r[0]).negate();
-                                                       Node cc3 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s22, r).negate();
-                                                       conc = NodeManager::currentNM()->mkNode(kind::OR, cc1, cc2, cc3);
-                                                       conc = NodeManager::currentNM()->mkNode(kind::IMPLIES, g1, conc);
-                                                       conc = NodeManager::currentNM()->mkNode(kind::FORALL, b1v, conc);
-                                                       conc = NodeManager::currentNM()->mkNode(kind::AND, x.eqNode(d_emptyString).negate(), conc);
-                                               }
-                                       }
-                                       if( conc!=d_true ){
-                                               ant = mkRegExpAntec(assertion, ant);
-                                               sendLemma(ant, conc, "REGEXP CSTAR");
-                                               addedLemma = true;
-                                               if( conc==d_false ){
-                                                       d_regexp_ccached.insert( assertion );
-                                               }else{
-                                                       cprocessed.push_back( assertion );
-                                               }
-                                       }else{
-                                               d_regexp_ccached.insert(assertion);
-                                       }
-                               }
-                       }
-               }
-               if(d_conflict) {
-                       break;
-               }
+        if( polarity ) {
+          flag = checkPDerivative(x, r, atom, addedLemma, processed, cprocessed, rnfexp);
+          if(options::stringOpt2() && flag) {
+            if(d_regexp_opr.checkConstRegExp(r) && x.getKind()==kind::STRING_CONCAT) {
+              std::vector< std::pair< Node, Node > > vec_can;
+              d_regexp_opr.splitRegExp(r, vec_can);
+              //TODO: lazy cache or eager?
+              std::vector< Node > vec_or;
+              std::vector< Node > vec_s2;
+              for(unsigned int s2i=1; s2i<x.getNumChildren(); s2i++) {
+                vec_s2.push_back(x[s2i]);
+              }
+              Node s1 = x[0];
+              Node s2 = vec_s2.size()==1? vec_s2[0]: NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, vec_s2);
+              for(unsigned int i=0; i<vec_can.size(); i++) {
+                Node m1 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s1, vec_can[i].first);
+                Node m2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s2, vec_can[i].second);
+                Node c = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND, m1, m2) );
+                vec_or.push_back( c );
+              }
+              Node conc = vec_or.size()==1 ? vec_or[0] : Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::OR, vec_or) );
+              //Trace("regexp-split") << "R " << r << " to " << conc << std::endl;
+              Node antec = mkRegExpAntec(atom, mkExplain(rnfexp));
+              if(conc == d_true) {
+                if(changed) {
+                  cprocessed.push_back( assertion );
+                } else {
+                  processed.push_back( assertion );
+                }
+              } else if(conc == d_false) {
+                conc = Node::null();
+                sendLemma(antec, conc, "RegExp CST-SP Conflict");
+              } else {
+                sendLemma(antec, conc, "RegExp-CST-SP");
+              }
+              addedLemma = true;
+              flag = false;
+            }
+          }
+        } else {
+          if(! options::stringExp()) {
+            throw LogicException("Strings Incomplete (due to Negative Membership) by default, try --strings-exp option.");
+          }
+        }
+        if(flag) {
+          //check if the term is atomic
+          Node xr = getRepresentative( x );
+          //Trace("strings-regexp") << xr << " is rep of " << x << std::endl;
+          //Assert( d_normal_forms.find( xr )!=d_normal_forms.end() );
+          //TODO
+          if( true || r.getKind()!=kind::REGEXP_STAR || ( d_normal_forms[xr].size()==1 && x.getKind()!=kind::STRING_CONCAT ) ){
+            Trace("strings-regexp") << "Unroll/simplify membership of atomic term " << xr << std::endl;
+            //if so, do simple unrolling
+            std::vector< Node > nvec;
+            d_regexp_opr.simplify(atom, nvec, polarity);
+            Node antec = assertion;
+            if(d_regexp_ant.find(assertion) != d_regexp_ant.end()) {
+              antec = d_regexp_ant[assertion];
+              for(std::vector< Node >::const_iterator itr=nvec.begin(); itr<nvec.end(); itr++) {
+                if(itr->getKind() == kind::STRING_IN_REGEXP) {
+                  if(d_regexp_ant.find( *itr ) == d_regexp_ant.end()) {
+                    d_regexp_ant[ *itr ] = antec;
+                  }
+                }
+              }
+            }
+            antec = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND, antec, mkExplain(rnfexp)) );
+            Node conc = nvec.size()==1 ? nvec[0] :
+                NodeManager::currentNM()->mkNode(kind::AND, nvec);
+            conc = Rewriter::rewrite(conc);
+            sendLemma( antec, conc, "REGEXP" );
+            addedLemma = true;
+            if(changed) {
+              cprocessed.push_back( assertion );
+            } else {
+              processed.push_back( assertion );
+            }
+            //d_regexp_ucached[assertion] = true;
+          } else {
+            Trace("strings-regexp") << "Unroll/simplify membership of non-atomic term " << xr << " = ";
+            for( unsigned j=0; j<d_normal_forms[xr].size(); j++ ){
+              Trace("strings-regexp") << d_normal_forms[xr][j] << " ";
+            }
+            Trace("strings-regexp") << ", polarity = " << polarity << std::endl;
+            //otherwise, distribute unrolling over parts
+            Node p1;
+            Node p2;
+            if( d_normal_forms[xr].size()>1 ){
+              p1 = d_normal_forms[xr][0];
+              std::vector< Node > cc;
+              cc.insert( cc.begin(), d_normal_forms[xr].begin() + 1, d_normal_forms[xr].end() );
+              p2 = mkConcat( cc );
+            }
+
+            Trace("strings-regexp-debug") << "Construct antecedant..." << std::endl;
+            std::vector< Node > antec;
+            std::vector< Node > antecn;
+            antec.insert( antec.begin(), d_normal_forms_exp[xr].begin(), d_normal_forms_exp[xr].end() );
+            if( x!=xr ){
+              antec.push_back( x.eqNode( xr ) );
+            }
+            antecn.push_back( assertion );
+            Node ant = mkExplain( antec, antecn );
+            Trace("strings-regexp-debug") << "Construct conclusion..." << std::endl;
+            Node conc;
+            if( polarity ){
+              if( d_normal_forms[xr].size()==0 ){
+                conc = d_true;
+              }else if( d_normal_forms[xr].size()==1 ){
+                Trace("strings-regexp-debug") << "Case 1\n";
+                conc = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, d_normal_forms[xr][0], r);
+              }else{
+                Trace("strings-regexp-debug") << "Case 2\n";
+                std::vector< Node > conc_c;
+                Node s11 = NodeManager::currentNM()->mkSkolem( "s11", NodeManager::currentNM()->stringType(), "created for re" );
+                Node s12 = NodeManager::currentNM()->mkSkolem( "s12", NodeManager::currentNM()->stringType(), "created for re" );
+                Node s21 = NodeManager::currentNM()->mkSkolem( "s21", NodeManager::currentNM()->stringType(), "created for re" );
+                Node s22 = NodeManager::currentNM()->mkSkolem( "s22", NodeManager::currentNM()->stringType(), "created for re" );
+                conc = p1.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s11, s12));
+                conc_c.push_back(conc);
+                conc = p2.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s21, s22));
+                conc_c.push_back(conc);
+                conc = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s11, r);
+                conc_c.push_back(conc);
+                conc = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s12, s21), r[0]);
+                conc_c.push_back(conc);
+                conc = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s22, r);
+                conc_c.push_back(conc);
+                conc = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND, conc_c));
+                Node eqz = Rewriter::rewrite(x.eqNode(d_emptyString));
+                conc = NodeManager::currentNM()->mkNode(kind::OR, eqz, conc);
+                d_pending_req_phase[eqz] = true;
+              }
+            }else{
+              if( d_normal_forms[xr].size()==0 ){
+                conc = d_false;
+              }else if( d_normal_forms[xr].size()==1 ){
+                Trace("strings-regexp-debug") << "Case 3\n";
+                conc = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, d_normal_forms[xr][0], r).negate();
+              }else{
+                Trace("strings-regexp-debug") << "Case 4\n";
+                Node len1 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, p1);
+                Node len2 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, p2);
+                Node bi = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
+                Node bj = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
+                Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, bi, bj);
+                Node g1 = NodeManager::currentNM()->mkNode(kind::AND, 
+                      NodeManager::currentNM()->mkNode(kind::GEQ, bi, d_zero),
+                      NodeManager::currentNM()->mkNode(kind::GEQ, len1, bi),
+                      NodeManager::currentNM()->mkNode(kind::GEQ, bj, d_zero),
+                      NodeManager::currentNM()->mkNode(kind::GEQ, len2, bj));
+                Node s11 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, p1, d_zero, bi);
+                Node s12 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, p1, bi, NodeManager::currentNM()->mkNode(kind::MINUS, len1, bi));
+                Node s21 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, p2, d_zero, bj);
+                Node s22 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, p2, bj, NodeManager::currentNM()->mkNode(kind::MINUS, len2, bj));
+                Node cc1 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s11, r).negate();
+                Node cc2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s12, s21), r[0]).negate();
+                Node cc3 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s22, r).negate();
+                conc = NodeManager::currentNM()->mkNode(kind::OR, cc1, cc2, cc3);
+                conc = NodeManager::currentNM()->mkNode(kind::IMPLIES, g1, conc);
+                conc = NodeManager::currentNM()->mkNode(kind::FORALL, b1v, conc);
+                conc = NodeManager::currentNM()->mkNode(kind::AND, x.eqNode(d_emptyString).negate(), conc);
+              }
+            }
+            if( conc!=d_true ){
+              ant = mkRegExpAntec(assertion, ant);
+              sendLemma(ant, conc, "REGEXP CSTAR");
+              addedLemma = true;
+              if( conc==d_false ){
+                d_regexp_ccached.insert( assertion );
+              }else{
+                cprocessed.push_back( assertion );
+              }
+            }else{
+              d_regexp_ccached.insert(assertion);
+            }
+          }
+        }
+      }
+      if(d_conflict) {
+        break;
+      }
          }
        }
-       if( addedLemma ){
+       if( addedLemma ) {
                if( !d_conflict ){
-                       for( unsigned i=0; i<processed.size(); i++ ){
+                       for( unsigned i=0; i<processed.size(); i++ ) {
                                d_regexp_ucached.insert(processed[i]);
                        }
-                       for( unsigned i=0; i<cprocessed.size(); i++ ){
+                       for( unsigned i=0; i<cprocessed.size(); i++ ) {
                                d_regexp_ccached.insert(cprocessed[i]);
                        }
                }
                doPendingLemmas();
                return true;
-       }else{
+       } else {
                return false;
        }
 }
 
-bool TheoryStrings::checkPDerivative(Node x, Node r, Node atom, bool &addedLemma, std::vector< Node > &processed, std::vector< Node > &cprocessed) {
+bool TheoryStrings::checkPDerivative(Node x, Node r, Node atom, bool &addedLemma,
+       std::vector< Node > &processed, std::vector< Node > &cprocessed, std::vector< Node > &nf_exp) {
        /*if(d_opt_regexp_gcd) {
                if(d_membership_length.find(atom) == d_membership_length.end()) {
                        addedLemma = addMembershipLength(atom);
@@ -2592,11 +2666,14 @@ bool TheoryStrings::checkPDerivative(Node x, Node r, Node atom, bool &addedLemma
                        Trace("strings-regexp") << "Membership length is already added." << std::endl;
                }
        }*/
+       Node antnf = mkExplain(nf_exp);
+
        if(areEqual(x, d_emptyString)) {
                Node exp;
                switch(d_regexp_opr.delta(r, exp)) {
                        case 0: {
                                Node antec = mkRegExpAntec(atom, x.eqNode(d_emptyString));
+                               antec = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND, antec, antnf));
                                sendLemma(antec, exp, "RegExp Delta");
                                addedLemma = true;
                                d_regexp_ccached.insert(atom);
@@ -2608,6 +2685,7 @@ bool TheoryStrings::checkPDerivative(Node x, Node r, Node atom, bool &addedLemma
                        }
                        case 2: {
                                Node antec = mkRegExpAntec(atom, x.eqNode(d_emptyString));
+                               antec = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND, antec, antnf));
                                Node conc = Node::null();
                                sendLemma(antec, conc, "RegExp Delta CONFLICT");
                                addedLemma = true;
@@ -2619,7 +2697,7 @@ bool TheoryStrings::checkPDerivative(Node x, Node r, Node atom, bool &addedLemma
                                break;
                }
        } else {
-               Node xr = getRepresentative( x );
+               /*Node xr = getRepresentative( x );
                if(x != xr) {
                        Node n = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, xr, r);
                        Node nn = Rewriter::rewrite( n );
@@ -2634,9 +2712,10 @@ bool TheoryStrings::checkPDerivative(Node x, Node r, Node atom, bool &addedLemma
                                d_regexp_ccached.insert(atom);
                                return false;
                        }
-               }
+               }*/
                Node sREant = mkRegExpAntec(atom, d_true);
-               if(splitRegExp( x, r, sREant )) {
+               sREant = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND, sREant, antnf));
+               if(deriveRegExp( x, r, sREant )) {
                        addedLemma = true;
                        processed.push_back( atom );
                        return false;
@@ -2809,10 +2888,10 @@ bool TheoryStrings::addMembershipLength(Node atom) {
        return false;
 }
 
-bool TheoryStrings::splitRegExp( Node x, Node r, Node ant ) {
+bool TheoryStrings::deriveRegExp( Node x, Node r, Node ant ) {
        // TODO cstr in vre
        Assert(x != d_emptyString);
-       Trace("regexp-split") << "TheoryStrings::splitRegExp: x=" << x << ", r= " << r << std::endl;
+       Trace("regexp-derive") << "TheoryStrings::deriveRegExp: x=" << x << ", r= " << r << std::endl;
        //if(x.isConst()) {
        //      Node n = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, x, r );
        //      Node r = Rewriter::rewrite( n );
@@ -2841,7 +2920,7 @@ bool TheoryStrings::splitRegExp( Node x, Node r, Node ant ) {
                // send lemma
                if(flag) {
                        if(x.isConst()) {
-                               Assert(false, "Impossible: TheoryStrings::splitRegExp: const string in const regular expression.");
+                               Assert(false, "Impossible: TheoryStrings::deriveRegExp: const string in const regular expression.");
                                return false;
                        } else {
                                Assert( x.getKind() == kind::STRING_CONCAT );
@@ -2862,7 +2941,7 @@ bool TheoryStrings::splitRegExp( Node x, Node r, Node ant ) {
                                }
                        }
                }
-               sendLemma(ant, conc, "RegExp-CST-SP");
+               sendLemma(ant, conc, "RegExp-Derive");
                return true;
        } else {
                return false;
@@ -2904,9 +2983,93 @@ void TheoryStrings::addMembership(Node assertion) {
        d_regexp_memberships.push_back( assertion );
 }
 
-Node TheoryStrings::instantiateSymRegExp(Node r) {
-       //TODO:
-       return r;
+Node TheoryStrings::getNormalString(Node x, std::vector<Node> &nf_exp) {
+       Node ret = x;
+       if(x.getKind() == kind::STRING_CONCAT) {
+               std::vector< Node > vec_nodes;
+               for(unsigned i=0; i<x.getNumChildren(); i++) {
+                       if(x[i].isConst()) {
+                               vec_nodes.push_back(x[i]);
+                       } else {
+                               Node tmp = x[i];
+                               if(d_normal_forms.find( tmp ) != d_normal_forms.end()) {
+                                       Trace("regexp-debug") << "Term: " << tmp << " has a normal form." << std::endl;
+                                       vec_nodes.insert(vec_nodes.end(), d_normal_forms[tmp].begin(), d_normal_forms[tmp].end());
+                                       nf_exp.insert(nf_exp.end(), d_normal_forms_exp[tmp].begin(), d_normal_forms_exp[tmp].end());
+                               } else {
+                                       Trace("regexp-debug") << "Term: " << tmp << " has NO normal form." << std::endl;
+                                       vec_nodes.push_back(tmp);
+                               }
+                       }
+               }
+               ret = mkConcat(vec_nodes);
+       } else {
+               if(d_normal_forms.find( x ) != d_normal_forms.end()) {
+                       ret = mkConcat( d_normal_forms[x] );
+                       nf_exp.insert(nf_exp.end(), d_normal_forms_exp[x].begin(), d_normal_forms_exp[x].end());
+                       Trace("regexp-debug") << "Term: " << x << " has a normal form " << ret << std::endl;
+               } else {
+                       Trace("regexp-debug") << "Term: " << x << " has NO normal form." << std::endl;
+               }
+       }
+       return ret;
+}
+
+Node TheoryStrings::getNormalSymRegExp(Node r, std::vector<Node> &nf_exp) {
+       Node ret = r;
+       switch( r.getKind() ) {
+               case kind::REGEXP_EMPTY:
+               case kind::REGEXP_SIGMA:
+                       break;
+               case kind::STRING_TO_REGEXP: {
+                       if(!r[0].isConst()) {
+                               Node tmp = getNormalString( r[0], nf_exp );
+                               if(tmp != r[0]) {
+                                       ret = NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, tmp);
+                               }
+                       }
+                       break;
+               }
+               case kind::REGEXP_CONCAT: {
+                       std::vector< Node > vec_nodes;
+                       for(unsigned i=0; i<r.getNumChildren(); ++i) {
+                               vec_nodes.push_back( getNormalSymRegExp(r[i], nf_exp) );
+                       }
+                       ret = mkConcat(vec_nodes);
+                       break;
+               }
+               case kind::REGEXP_UNION: {
+                       std::vector< Node > vec_nodes;
+                       for(unsigned i=0; i<r.getNumChildren(); ++i) {
+                               vec_nodes.push_back( getNormalSymRegExp(r[i], nf_exp) );
+                       }
+                       ret = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vec_nodes) );
+                       break;
+               }
+               case kind::REGEXP_INTER: {
+                       std::vector< Node > vec_nodes;
+                       for(unsigned i=0; i<r.getNumChildren(); ++i) {
+                               vec_nodes.push_back( getNormalSymRegExp(r[i], nf_exp) );
+                       }
+                       ret = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_INTER, vec_nodes) );
+                       break;
+               }
+               case kind::REGEXP_STAR: {
+                       ret = getNormalSymRegExp( r[0], nf_exp );
+                       ret = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, ret) );
+                       break;
+               }
+               //case kind::REGEXP_PLUS:
+               //case kind::REGEXP_OPT:
+               //case kind::REGEXP_RANGE:
+               default: {
+                       Trace("strings-error") << "Unsupported term: " << r << " in normalization SymRegExp." << std::endl;
+                       Assert( false );
+                       //return Node::null();
+               }
+       }
+
+       return ret;
 }
 
 //// Finite Model Finding
index 33283d1cfb4e9e4b6a377fe37759ae948b21fea9..f4a17fa46518e42b646faa30c8d96ea5e974a634 100644 (file)
@@ -67,18 +67,18 @@ public:
                bool eqNotifyTriggerEquality(TNode equality, bool value) {
                  Debug("strings") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl;
                  if (value) {
-                       return d_str.propagate(equality);
+                         return d_str.propagate(equality);
                  } else {
-                       // We use only literal triggers so taking not is safe
-                       return d_str.propagate(equality.notNode());
+        // We use only literal triggers so taking not is safe
+        return d_str.propagate(equality.notNode());
                  }
                }
                bool eqNotifyTriggerPredicate(TNode predicate, bool value) {
                  Debug("strings") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl;
                  if (value) {
-                       return d_str.propagate(predicate);
+        return d_str.propagate(predicate);
                  } else {
-                  return d_str.propagate(predicate.notNode());
+         return d_str.propagate(predicate.notNode());
                  }
                }
                bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
@@ -119,11 +119,11 @@ private:
        Node d_ufSubstr;
 
        // Constants
-    Node d_emptyString;
+  Node d_emptyString;
        Node d_emptyRegexp;
-    Node d_true;
-    Node d_false;
-    Node d_zero;
+  Node d_true;
+  Node d_false;
+  Node d_zero;
        Node d_one;
        // Options
        bool d_opt_fmf;
@@ -137,12 +137,12 @@ private:
        Node getLength( Node t );
 
 private:
-    /** The notify class */
-    NotifyClass d_notify;
-    /** Equaltity engine */
-    eq::EqualityEngine d_equalityEngine;
-    /** Are we in conflict */
-    context::CDO<bool> d_conflict;
+  /** The notify class */
+  NotifyClass d_notify;
+  /** Equaltity engine */
+  eq::EqualityEngine d_equalityEngine;
+  /** 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;
@@ -206,41 +206,43 @@ private:
        NodeNodeMap d_length_inst;
 private:
        void mergeCstVec(std::vector< Node > &vec_strings);
-    bool 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);
+  bool 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);
        bool detectLoop(std::vector< std::vector< Node > > &normal_forms,
-                                       int i, int j, int index_i, int index_j, 
-                                       int &loop_in_i, int &loop_in_j);
+        int i, int j, int index_i, int index_j, 
+        int &loop_in_i, int &loop_in_j);
        bool processLoop(std::vector< Node > &antec,
-                                        std::vector< std::vector< Node > > &normal_forms,
-                                        std::vector< Node > &normal_form_src,
-                                        int i, int j, int loop_n_index, int other_n_index,
-                                        int loop_index, int index, int other_index);
+        std::vector< std::vector< Node > > &normal_forms,
+        std::vector< Node > &normal_form_src,
+        int i, int j, int loop_n_index, int other_n_index,
+        int loop_index, int index, int other_index);
        bool processNEqc(std::vector< std::vector< Node > > &normal_forms,
-                                        std::vector< std::vector< Node > > &normal_forms_exp,
-                                        std::vector< Node > &normal_form_src);
+        std::vector< std::vector< Node > > &normal_forms_exp,
+        std::vector< Node > &normal_form_src);
        bool processReverseNEq(std::vector< std::vector< Node > > &normal_forms,
-                                                  std::vector< Node > &normal_form_src, std::vector< Node > &curr_exp, unsigned i, unsigned j );
+        std::vector< Node > &normal_form_src, std::vector< Node > &curr_exp, unsigned i, unsigned j );
        bool processSimpleNEq( std::vector< std::vector< Node > > &normal_forms,
-                                                  std::vector< Node > &normal_form_src, std::vector< Node > &curr_exp, unsigned i, unsigned j,
-                                                  unsigned& index_i, unsigned& index_j, bool isRev );
-    bool normalizeEquivalenceClass( Node n, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp );
-    bool processDeq( Node n1, Node n2 );
+        std::vector< Node > &normal_form_src, std::vector< Node > &curr_exp, unsigned i, unsigned j,
+        unsigned& index_i, unsigned& index_j, bool isRev );
+  bool normalizeEquivalenceClass( Node n, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp );
+  bool processDeq( Node n1, Node n2 );
        int processReverseDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj );
        int processSimpleDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj, unsigned& index, bool isRev );
        //bool unrollStar( Node atom );
        Node mkRegExpAntec(Node atom, Node ant);
 
        bool checkSimple();
-    bool checkNormalForms();
+  bool checkNormalForms();
        void checkDeqNF();
        bool checkLengthsEqc();
-    bool checkCardinality();
-    bool checkInductiveEquations();
+  bool checkCardinality();
+  bool checkInductiveEquations();
        bool checkMemberships();
-       bool checkPDerivative(Node x, Node r, Node atom, bool &addedLemma, std::vector< Node > &processed, std::vector< Node > &cprocessed);
+       bool checkPDerivative(Node x, Node r, Node atom, bool &addedLemma,
+               std::vector< Node > &processed, std::vector< Node > &cprocessed,
+               std::vector< Node > &nf_exp);
        bool checkContains();
        bool checkPosContains();
        bool checkNegContains();
@@ -320,10 +322,11 @@ private:
        RegExpOpr d_regexp_opr;
 
        CVC4::String getHeadConst( Node x );
-       bool splitRegExp( Node x, Node r, Node ant );
+       bool deriveRegExp( Node x, Node r, Node ant );
        bool addMembershipLength(Node atom);
        void addMembership(Node assertion);
-       Node instantiateSymRegExp(Node r);
+       Node getNormalString(Node x, std::vector<Node> &nf_exp);
+       Node getNormalSymRegExp(Node r, std::vector<Node> &nf_exp);
 
 
        // Finite Model Finding
@@ -334,7 +337,7 @@ private:
        context::CDO< int > d_curr_cardinality;
 public:
        //for finite model finding
-    Node getNextDecisionRequest();
+  Node getNextDecisionRequest();
        void assertNode( Node lit );
 
 public:
index 85ab73691bda24ab0f9f1aff1937eb2c0fa73312..ef5da000fa6a3e7460bb84dffee292c4e8007861 100644 (file)
@@ -137,10 +137,10 @@ int StringsPreprocess::checkFixLenVar( Node t ) {
        return ret;
 }
 Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
-    std::hash_map<TNode, Node, TNodeHashFunction>::const_iterator i = d_cache.find(t);
-    if(i != d_cache.end()) {
-      return (*i).second.isNull() ? t : (*i).second;
-    }
+  std::hash_map<TNode, Node, TNodeHashFunction>::const_iterator i = d_cache.find(t);
+  if(i != d_cache.end()) {
+    return (*i).second.isNull() ? t : (*i).second;
+  }
 
        Trace("strings-preprocess") << "StringsPreprocess::simplify: " << t << std::endl;
        Node retNode = t;
@@ -179,8 +179,8 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                retNode = n;
        } else if( t.getKind() == kind::STRING_SUBSTR_TOTAL ) {
                Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ, 
-                                                       NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ),
-                                                       NodeManager::currentNM()->mkNode( kind::PLUS, t[1], t[2] ) );
+          NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ),
+          NodeManager::currentNM()->mkNode( kind::PLUS, t[1], t[2] ) );
                Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, t[1], d_zero);
                Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, t[2], d_zero);
                Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 ));
@@ -554,10 +554,10 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
 }
 
 Node StringsPreprocess::decompose(Node t, std::vector< Node > & new_nodes) {
-    std::hash_map<TNode, Node, TNodeHashFunction>::const_iterator i = d_cache.find(t);
-    if(i != d_cache.end()) {
-      return (*i).second.isNull() ? t : (*i).second;
-    }
+  std::hash_map<TNode, Node, TNodeHashFunction>::const_iterator i = d_cache.find(t);
+  if(i != d_cache.end()) {
+    return (*i).second.isNull() ? t : (*i).second;
+  }
 
        unsigned num = t.getNumChildren();
        if(num == 0) {
index 69454db847c956b85dd7353b063c41fdf1a07270..6d0af4d1bafeb18077dc719bc67e5e8e8edeec3d 100644 (file)
@@ -40,8 +40,8 @@ private:
        Node simplify( Node t, std::vector< Node > &new_nodes );
        Node decompose( Node t, std::vector< Node > &new_nodes );
 public:
-    void simplify(std::vector< Node > &vec_node, std::vector< Node > &new_nodes);
-    void simplify(std::vector< Node > &vec_node);
+  void simplify(std::vector< Node > &vec_node, std::vector< Node > &new_nodes);
+  void simplify(std::vector< Node > &vec_node);
        StringsPreprocess();
 };
 
index f6de1b129b2a772866cd10b3f201fb680a5c2f55..a47b4fbca549cc8c5a67006ca0e7618fa899e495 100644 (file)
@@ -25,52 +25,52 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::strings;
 
 Node TheoryStringsRewriter::rewriteConcatString( TNode node ) {
-    Trace("strings-prerewrite") << "Strings::rewriteConcatString start " << node << std::endl;
-    Node retNode = node;
-    std::vector<Node> node_vec;
-    Node preNode = Node::null();
-    for(unsigned int i=0; i<node.getNumChildren(); ++i) {
-        Node tmpNode = node[i];
+  Trace("strings-prerewrite") << "Strings::rewriteConcatString start " << node << std::endl;
+  Node retNode = node;
+  std::vector<Node> node_vec;
+  Node preNode = Node::null();
+  for(unsigned int i=0; i<node.getNumChildren(); ++i) {
+    Node tmpNode = node[i];
                if(node[i].getKind() == kind::STRING_CONCAT) {
-            tmpNode = rewriteConcatString(node[i]);
-            if(tmpNode.getKind() == kind::STRING_CONCAT) {
+      tmpNode = rewriteConcatString(node[i]);
+      if(tmpNode.getKind() == kind::STRING_CONCAT) {
                                unsigned j=0;
-                if(!preNode.isNull()) {
-                    if(tmpNode[0].isConst()) {
-                        preNode = NodeManager::currentNM()->mkConst( preNode.getConst<String>().concat( tmpNode[0].getConst<String>() ) );
-                        node_vec.push_back( preNode );
-                        preNode = Node::null();
-                    } else {
-                        node_vec.push_back( preNode );
-                        preNode = Node::null();
-                        node_vec.push_back( tmpNode[0] );
-                    }
-                                       ++j;
-                }
-                for(; j<tmpNode.getNumChildren() - 1; ++j) {
-                    node_vec.push_back( tmpNode[j] );
-                }
-                tmpNode = tmpNode[j];
-            }
+        if(!preNode.isNull()) {
+          if(tmpNode[0].isConst()) {
+            preNode = NodeManager::currentNM()->mkConst( preNode.getConst<String>().concat( tmpNode[0].getConst<String>() ) );
+            node_vec.push_back( preNode );
+            preNode = Node::null();
+          } else {
+            node_vec.push_back( preNode );
+            preNode = Node::null();
+            node_vec.push_back( tmpNode[0] );
+          }
+          ++j;
         }
-        if(!tmpNode.isConst()) {
-            if(!preNode.isNull()) {
-                if(preNode.getKind() == kind::CONST_STRING && preNode.getConst<String>().isEmptyString() ) {
-                    preNode = Node::null();
-                } else {
-                    node_vec.push_back( preNode );
-                    preNode = Node::null();
-                }
-            }
-            node_vec.push_back( tmpNode );
+        for(; j<tmpNode.getNumChildren() - 1; ++j) {
+          node_vec.push_back( tmpNode[j] );
+        }
+        tmpNode = tmpNode[j];
+      }
+    }
+    if(!tmpNode.isConst()) {
+      if(!preNode.isNull()) {
+        if(preNode.getKind() == kind::CONST_STRING && preNode.getConst<String>().isEmptyString() ) {
+          preNode = Node::null();
         } else {
-            if(preNode.isNull()) {
-                preNode = tmpNode;
-            } else {
-                preNode = NodeManager::currentNM()->mkConst( preNode.getConst<String>().concat( tmpNode.getConst<String>() ) );
-            }
+          node_vec.push_back( preNode );
+          preNode = Node::null();
         }
+      }
+      node_vec.push_back( tmpNode );
+    } else {
+      if(preNode.isNull()) {
+        preNode = tmpNode;
+      } else {
+        preNode = NodeManager::currentNM()->mkConst( preNode.getConst<String>().concat( tmpNode.getConst<String>() ) );
+      }
     }
+  }
        if(preNode != Node::null()) {
                node_vec.push_back( preNode );
        }
@@ -79,65 +79,65 @@ Node TheoryStringsRewriter::rewriteConcatString( TNode node ) {
        } else {
                retNode = node_vec[0];
        }
-    Trace("strings-prerewrite") << "Strings::rewriteConcatString end " << retNode << std::endl;
-    return retNode;
+  Trace("strings-prerewrite") << "Strings::rewriteConcatString end " << retNode << std::endl;
+  return retNode;
 }
 
 Node TheoryStringsRewriter::prerewriteConcatRegExp( TNode node ) {
-       Assert( node.getKind() == kind::REGEXP_CONCAT );
-    Trace("strings-prerewrite") << "Strings::prerewriteConcatRegExp start " << node << std::endl;
-    Node retNode = node;
-    std::vector<Node> node_vec;
-    Node preNode = Node::null();
-       bool emptyflag = false;
-    for(unsigned int i=0; i<node.getNumChildren(); ++i) {
+  Assert( node.getKind() == kind::REGEXP_CONCAT );
+  Trace("strings-prerewrite") << "Strings::prerewriteConcatRegExp start " << node << std::endl;
+  Node retNode = node;
+  std::vector<Node> node_vec;
+  Node preNode = Node::null();
+  bool emptyflag = false;
+  for(unsigned int i=0; i<node.getNumChildren(); ++i) {
                Trace("strings-prerewrite") << "Strings::prerewriteConcatRegExp preNode: " << preNode << std::endl;
-        Node tmpNode = node[i];
-        if(tmpNode.getKind() == kind::REGEXP_CONCAT) {
-            tmpNode = prerewriteConcatRegExp(node[i]);
-            if(tmpNode.getKind() == kind::REGEXP_CONCAT) {
-                               unsigned j=0;
-                if(!preNode.isNull()) {
-                    if(tmpNode[0].getKind() == kind::STRING_TO_REGEXP) {
-                        preNode = rewriteConcatString(
-                                                       NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, preNode, tmpNode[0][0] ) );
-                        node_vec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, preNode ) );
-                        preNode = Node::null();
-                    } else {
-                        node_vec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, preNode ) );
-                        preNode = Node::null();
-                        node_vec.push_back( tmpNode[0] );
-                    }
-                                       ++j;
-                }
-                for(; j<tmpNode.getNumChildren() - 1; ++j) {
-                    node_vec.push_back( tmpNode[j] );
-                }
-                tmpNode = tmpNode[j];
-            }
+    Node tmpNode = node[i];
+    if(tmpNode.getKind() == kind::REGEXP_CONCAT) {
+      tmpNode = prerewriteConcatRegExp(node[i]);
+      if(tmpNode.getKind() == kind::REGEXP_CONCAT) {
+        unsigned j=0;
+        if(!preNode.isNull()) {
+          if(tmpNode[0].getKind() == kind::STRING_TO_REGEXP) {
+            preNode = rewriteConcatString(
+            NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, preNode, tmpNode[0][0] ) );
+            node_vec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, preNode ) );
+            preNode = Node::null();
+          } else {
+            node_vec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, preNode ) );
+            preNode = Node::null();
+            node_vec.push_back( tmpNode[0] );
+          }
+          ++j;
+        }
+        for(; j<tmpNode.getNumChildren() - 1; ++j) {
+          node_vec.push_back( tmpNode[j] );
         }
-        if( tmpNode.getKind() == kind::STRING_TO_REGEXP ) {
-            if(preNode.isNull()) {
-                preNode = tmpNode[0];
-            } else {
-                               preNode = rewriteConcatString(
-                                                       NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, preNode, tmpNode[0] ) );
-            }
-        } else if( tmpNode.getKind() == kind::REGEXP_EMPTY ) {
-                       emptyflag = true;
-                       break;
+        tmpNode = tmpNode[j];
+      }
+    }
+    if( tmpNode.getKind() == kind::STRING_TO_REGEXP ) {
+      if(preNode.isNull()) {
+        preNode = tmpNode[0];
+      } else {
+        preNode = rewriteConcatString(
+        NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, preNode, tmpNode[0] ) );
+      }
+    } else if( tmpNode.getKind() == kind::REGEXP_EMPTY ) {
+      emptyflag = true;
+      break;
                } else {
-            if(!preNode.isNull()) {
-                if(preNode.getKind() == kind::CONST_STRING && preNode.getConst<String>().isEmptyString() ) {
-                    preNode = Node::null();
-                } else {
-                    node_vec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, preNode ) );
-                    preNode = Node::null();
-                }
-            }
-            node_vec.push_back( tmpNode );
+      if(!preNode.isNull()) {
+        if(preNode.getKind() == kind::CONST_STRING && preNode.getConst<String>().isEmptyString() ) {
+          preNode = Node::null();
+        } else {
+          node_vec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, preNode ) );
+          preNode = Node::null();
         }
+      }
+      node_vec.push_back( tmpNode );
     }
+  }
        if(emptyflag) {
                std::vector< Node > nvec;
                retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_EMPTY, nvec );
@@ -151,17 +151,17 @@ Node TheoryStringsRewriter::prerewriteConcatRegExp( TNode node ) {
                        retNode = node_vec[0];
                }
        }
-    Trace("strings-prerewrite") << "Strings::prerewriteConcatRegExp end " << retNode << std::endl;
-    return retNode;
+  Trace("strings-prerewrite") << "Strings::prerewriteConcatRegExp end " << retNode << std::endl;
+  return retNode;
 }
 
 Node TheoryStringsRewriter::prerewriteOrRegExp(TNode node) {
        Assert( node.getKind() == kind::REGEXP_UNION );
-    Trace("strings-prerewrite") << "Strings::prerewriteOrRegExp start " << node << std::endl;
-    Node retNode = node;
-    std::vector<Node> node_vec;
+  Trace("strings-prerewrite") << "Strings::prerewriteOrRegExp start " << node << std::endl;
+  Node retNode = node;
+  std::vector<Node> node_vec;
        bool flag = false;
-    for(unsigned i=0; i<node.getNumChildren(); ++i) {
+  for(unsigned i=0; i<node.getNumChildren(); ++i) {
                if(node[i].getKind() == kind::REGEXP_UNION) {
                        Node tmpNode = prerewriteOrRegExp( node[i] );
                        for(unsigned int j=0; j<tmpNode.getNumChildren(); ++j) {
@@ -180,7 +180,7 @@ Node TheoryStringsRewriter::prerewriteOrRegExp(TNode node) {
                                        node_vec.size() == 1 ? node_vec[0] : NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, node_vec);
        }
        Trace("strings-prerewrite") << "Strings::prerewriteOrRegExp end " << retNode << std::endl;
-    return retNode;
+  return retNode;
 }
 
 bool TheoryStringsRewriter::checkConstRegExp( TNode t ) {
@@ -322,54 +322,54 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
        Node retNode = node;
        Node orig = retNode;
 
-    if(node.getKind() == kind::STRING_CONCAT) {
-        retNode = rewriteConcatString(node);
-    } else if(node.getKind() == kind::EQUAL) {
-        Node leftNode  = node[0];
-        if(node[0].getKind() == kind::STRING_CONCAT) {
-            leftNode = rewriteConcatString(node[0]);
-        }
-        Node rightNode = node[1];
-        if(node[1].getKind() == kind::STRING_CONCAT) {
-            rightNode = rewriteConcatString(node[1]);
-        }
+  if(node.getKind() == kind::STRING_CONCAT) {
+    retNode = rewriteConcatString(node);
+  } else if(node.getKind() == kind::EQUAL) {
+    Node leftNode  = node[0];
+    if(node[0].getKind() == kind::STRING_CONCAT) {
+      leftNode = rewriteConcatString(node[0]);
+    }
+    Node rightNode = node[1];
+    if(node[1].getKind() == kind::STRING_CONCAT) {
+      rightNode = rewriteConcatString(node[1]);
+    }
 
-        if(leftNode == rightNode) {
-            retNode = NodeManager::currentNM()->mkConst(true);
-        } else if(leftNode.isConst() && rightNode.isConst()) {
-            retNode = NodeManager::currentNM()->mkConst(false);
-        } else if(leftNode > rightNode) {
-            retNode = NodeManager::currentNM()->mkNode(kind::EQUAL, rightNode, leftNode);
-        } else if( leftNode != node[0] || rightNode != node[1]) {
-            retNode = NodeManager::currentNM()->mkNode(kind::EQUAL, leftNode, rightNode);
-        }
-    } else if(node.getKind() == kind::STRING_LENGTH) {
-        if(node[0].isConst()) {
-            retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( node[0].getConst<String>().size() ) );
-        } /*else if(node[0].getKind() == kind::STRING_SUBSTR_TOTAL) {
-            retNode = node[0][2];
-        }*/ else if(node[0].getKind() == kind::STRING_CONCAT) {
-            Node tmpNode = rewriteConcatString(node[0]);
-            if(tmpNode.isConst()) {
-                retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( tmpNode.getConst<String>().size() ) );
-            } /*else if(tmpNode.getKind() == kind::STRING_SUBSTR_TOTAL) {
-                               retNode = tmpNode[2];
-            }*/ else {
-                // it has to be string concat
-                std::vector<Node> node_vec;
-                for(unsigned int i=0; i<tmpNode.getNumChildren(); ++i) {
-                    if(tmpNode[i].isConst()) {
-                        node_vec.push_back( NodeManager::currentNM()->mkConst( ::CVC4::Rational( tmpNode[i].getConst<String>().size() ) ) );
-                                       } else if(tmpNode[i].getKind() == kind::STRING_SUBSTR_TOTAL) {
-                        node_vec.push_back( tmpNode[i][2] );
-                    } else {
-                        node_vec.push_back( NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, tmpNode[i]) );
-                    }
-                }
-                retNode = NodeManager::currentNM()->mkNode(kind::PLUS, node_vec);
-            }
+    if(leftNode == rightNode) {
+      retNode = NodeManager::currentNM()->mkConst(true);
+    } else if(leftNode.isConst() && rightNode.isConst()) {
+      retNode = NodeManager::currentNM()->mkConst(false);
+    } else if(leftNode > rightNode) {
+      retNode = NodeManager::currentNM()->mkNode(kind::EQUAL, rightNode, leftNode);
+    } else if( leftNode != node[0] || rightNode != node[1]) {
+      retNode = NodeManager::currentNM()->mkNode(kind::EQUAL, leftNode, rightNode);
+    }
+  } else if(node.getKind() == kind::STRING_LENGTH) {
+    if(node[0].isConst()) {
+      retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( node[0].getConst<String>().size() ) );
+    } /*else if(node[0].getKind() == kind::STRING_SUBSTR_TOTAL) {
+        retNode = node[0][2];
+    }*/ else if(node[0].getKind() == kind::STRING_CONCAT) {
+      Node tmpNode = rewriteConcatString(node[0]);
+      if(tmpNode.isConst()) {
+        retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( tmpNode.getConst<String>().size() ) );
+      } /*else if(tmpNode.getKind() == kind::STRING_SUBSTR_TOTAL) {
+      retNode = tmpNode[2];
+      }*/ else {
+        // it has to be string concat
+        std::vector<Node> node_vec;
+        for(unsigned int i=0; i<tmpNode.getNumChildren(); ++i) {
+          if(tmpNode[i].isConst()) {
+            node_vec.push_back( NodeManager::currentNM()->mkConst( ::CVC4::Rational( tmpNode[i].getConst<String>().size() ) ) );
+          } else if(tmpNode[i].getKind() == kind::STRING_SUBSTR_TOTAL) {
+            node_vec.push_back( tmpNode[i][2] );
+          } else {
+            node_vec.push_back( NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, tmpNode[i]) );
+          }
         }
-    } else if(node.getKind() == kind::STRING_SUBSTR_TOTAL) {
+        retNode = NodeManager::currentNM()->mkNode(kind::PLUS, node_vec);
+      }
+    }
+  } else if(node.getKind() == kind::STRING_SUBSTR_TOTAL) {
                Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
                if(node[2] == zero) {
                        retNode = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
@@ -552,15 +552,15 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
 }
 
 RewriteResponse TheoryStringsRewriter::preRewrite(TNode node) {
-    Node retNode = node;
+  Node retNode = node;
        Node orig = retNode;
-    Trace("strings-prerewrite") << "Strings::preRewrite start " << node << std::endl;
+  Trace("strings-prerewrite") << "Strings::preRewrite start " << node << std::endl;
 
-    if(node.getKind() == kind::STRING_CONCAT) {
-        retNode = rewriteConcatString(node);
-    } else if(node.getKind() == kind::REGEXP_CONCAT) {
-               retNode = prerewriteConcatRegExp(node);
-    } else if(node.getKind() == kind::REGEXP_UNION) {
+  if(node.getKind() == kind::STRING_CONCAT) {
+    retNode = rewriteConcatString(node);
+  } else if(node.getKind() == kind::REGEXP_CONCAT) {
+    retNode = prerewriteConcatRegExp(node);
+  } else if(node.getKind() == kind::REGEXP_UNION) {
                retNode = prerewriteOrRegExp(node);
        } else if(node.getKind() == kind::REGEXP_STAR) {
                if(node[0].getKind() == kind::REGEXP_STAR) {
@@ -568,7 +568,7 @@ RewriteResponse TheoryStringsRewriter::preRewrite(TNode node) {
                }
        } else if(node.getKind() == kind::REGEXP_PLUS) {
                retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, node[0],
-                                       NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, node[0]));
+      NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, node[0]));
        } else if(node.getKind() == kind::REGEXP_OPT) {
                retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_UNION,
                                        NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst( ::CVC4::String("") ) ),
@@ -623,6 +623,6 @@ RewriteResponse TheoryStringsRewriter::preRewrite(TNode node) {
                Trace("strings-lp") << "Strings::lp " << node << " => " << retNode << std::endl;
        }
 
-    Trace("strings-prerewrite") << "Strings::preRewrite returning " << retNode << std::endl;
-    return RewriteResponse(orig==retNode ? REWRITE_DONE : REWRITE_AGAIN_FULL, retNode);
+  Trace("strings-prerewrite") << "Strings::preRewrite returning " << retNode << std::endl;
+  return RewriteResponse(orig==retNode ? REWRITE_DONE : REWRITE_AGAIN_FULL, retNode);
 }
index e4778e86ce8c6792fcbbb68f94c66d48a4fecc26..9ffe9150dce9739678af6ff761561bbd8507cb57 100644 (file)
@@ -26,7 +26,7 @@ namespace strings {
 class StringConstantTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate, AssertionException) {
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
     return nodeManager->stringType();
   }
 };
@@ -34,22 +34,22 @@ public:
 class StringConcatTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate, AssertionException) {
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ){
-               TNode::iterator it = n.begin();
-               TNode::iterator it_end = n.end();
-               int size = 0;
-               for (; it != it_end; ++ it) {
-                  TypeNode t = (*it).getType(check);
-                  if (!t.isString()) {
-                        throw TypeCheckingExceptionPrivate(n, "expecting string terms in string concat");
-                  }
-                  ++size;
-               }
-               if(size < 2) {
-                  throw TypeCheckingExceptionPrivate(n, "expecting at least 2 terms in string concat");
-               }
-       }
+      TNode::iterator it = n.begin();
+      TNode::iterator it_end = n.end();
+      int size = 0;
+      for (; it != it_end; ++ it) {
+       TypeNode t = (*it).getType(check);
+       if (!t.isString()) {
+         throw TypeCheckingExceptionPrivate(n, "expecting string terms in string concat");
+       }
+       ++size;
+      }
+      if(size < 2) {
+        throw TypeCheckingExceptionPrivate(n, "expecting at least 2 terms in string concat");
+      }
+    }
     return nodeManager->stringType();
   }
 };
@@ -57,12 +57,12 @@ public:
 class StringLengthTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate, AssertionException) {
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
-        TypeNode t = n[0].getType(check);
-        if (!t.isString()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting string terms in string length");
-        }
+      TypeNode t = n[0].getType(check);
+      if (!t.isString()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting string terms in string length");
+      }
     }
     return nodeManager->integerType();
   }
@@ -71,20 +71,20 @@ public:
 class StringSubstrTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate, AssertionException) {
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
-        TypeNode t = n[0].getType(check);
-        if (!t.isString()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting a string term in substr");
-        }
-               t = n[1].getType(check);
-        if (!t.isInteger()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting a start int term in substr");
-        }
-               t = n[2].getType(check);
-        if (!t.isInteger()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting a length int term in substr");
-        }
+      TypeNode t = n[0].getType(check);
+      if (!t.isString()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting a string term in substr");
+      }
+      t = n[1].getType(check);
+      if (!t.isInteger()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting a start int term in substr");
+      }
+      t = n[2].getType(check);
+      if (!t.isInteger()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting a length int term in substr");
+      }
     }
     return nodeManager->stringType();
   }
@@ -95,14 +95,14 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
-        TypeNode t = n[0].getType(check);
-        if (!t.isString()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting an orginal string term in string contain");
-        }
-               t = n[1].getType(check);
-        if (!t.isString()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting a target string term in string contain");
-        }
+      TypeNode t = n[0].getType(check);
+      if (!t.isString()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting an orginal string term in string contain");
+      }
+      t = n[1].getType(check);
+      if (!t.isString()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting a target string term in string contain");
+      }
     }
     return nodeManager->booleanType();
   }
@@ -113,14 +113,14 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
-        TypeNode t = n[0].getType(check);
-        if (!t.isString()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting a string term in string char at 0");
-        }
-               t = n[1].getType(check);
-        if (!t.isInteger()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting an integer term in string char at 1");
-        }
+      TypeNode t = n[0].getType(check);
+      if (!t.isString()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting a string term in string char at 0");
+      }
+      t = n[1].getType(check);
+      if (!t.isInteger()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting an integer term in string char at 1");
+      }
     }
     return nodeManager->stringType();
   }
@@ -131,18 +131,18 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
-        TypeNode t = n[0].getType(check);
-        if (!t.isString()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting a string term in string indexof 0");
-        }
-               t = n[1].getType(check);
-        if (!t.isString()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting a string term in string indexof 1");
-        }
-               t = n[2].getType(check);
-        if (!t.isInteger()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting an integer term in string indexof 2");
-        }
+      TypeNode t = n[0].getType(check);
+      if (!t.isString()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting a string term in string indexof 0");
+      }
+      t = n[1].getType(check);
+      if (!t.isString()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting a string term in string indexof 1");
+      }
+      t = n[2].getType(check);
+      if (!t.isInteger()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting an integer term in string indexof 2");
+      }
     }
     return nodeManager->integerType();
   }
@@ -153,18 +153,18 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
-        TypeNode t = n[0].getType(check);
-        if (!t.isString()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting a string term in string replace 0");
-        }
-               t = n[1].getType(check);
-        if (!t.isString()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting a string term in string replace 1");
-        }
-               t = n[2].getType(check);
-        if (!t.isString()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting a string term in string replace 2");
-        }
+      TypeNode t = n[0].getType(check);
+      if (!t.isString()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting a string term in string replace 0");
+      }
+      t = n[1].getType(check);
+      if (!t.isString()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting a string term in string replace 1");
+      }
+      t = n[2].getType(check);
+      if (!t.isString()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting a string term in string replace 2");
+      }
     }
     return nodeManager->stringType();
   }
@@ -175,14 +175,14 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
-        TypeNode t = n[0].getType(check);
-        if (!t.isString()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting a string term in string prefixof 0");
-        }
-               t = n[1].getType(check);
-        if (!t.isString()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting a string term in string prefixof 1");
-        }
+      TypeNode t = n[0].getType(check);
+      if (!t.isString()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting a string term in string prefixof 0");
+      }
+      t = n[1].getType(check);
+      if (!t.isString()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting a string term in string prefixof 1");
+      }
     }
     return nodeManager->booleanType();
   }
@@ -193,14 +193,14 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
-        TypeNode t = n[0].getType(check);
-        if (!t.isString()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting a string term in string suffixof 0");
-        }
-               t = n[1].getType(check);
-        if (!t.isString()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting a string term in string suffixof 1");
-        }
+      TypeNode t = n[0].getType(check);
+      if (!t.isString()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting a string term in string suffixof 0");
+      }
+      t = n[1].getType(check);
+      if (!t.isString()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting a string term in string suffixof 1");
+      }
     }
     return nodeManager->booleanType();
   }
@@ -211,10 +211,10 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
-        TypeNode t = n[0].getType(check);
-        if (!t.isInteger()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting an integer term in int to string 0");
-        }
+      TypeNode t = n[0].getType(check);
+      if (!t.isInteger()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting an integer term in int to string 0");
+      }
     }
     return nodeManager->stringType();
   }
@@ -225,10 +225,10 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
-        TypeNode t = n[0].getType(check);
-        if (!t.isString()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting a string term in string to int 0");
-        }
+      TypeNode t = n[0].getType(check);
+      if (!t.isString()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting a string term in string to int 0");
+      }
     }
     return nodeManager->integerType();
   }
@@ -247,20 +247,20 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
-               TNode::iterator it = n.begin();
-               TNode::iterator it_end = n.end();
-               int size = 0;
-               for (; it != it_end; ++ it) {
-                  TypeNode t = (*it).getType(check);
-                  if (!t.isRegExp()) {
-                        throw TypeCheckingExceptionPrivate(n, "expecting regexp terms in regexp concat");
-                  }
-                  ++size;
-               }
-               if(size < 2) {
-                  throw TypeCheckingExceptionPrivate(n, "expecting at least 2 terms in regexp concat");
-               }
-       }
+      TNode::iterator it = n.begin();
+      TNode::iterator it_end = n.end();
+      int size = 0;
+      for (; it != it_end; ++ it) {
+         TypeNode t = (*it).getType(check);
+         if (!t.isRegExp()) {
+           throw TypeCheckingExceptionPrivate(n, "expecting regexp terms in regexp concat");
+         }
+         ++size;
+      }
+      if(size < 2) {
+         throw TypeCheckingExceptionPrivate(n, "expecting at least 2 terms in regexp concat");
+      }
+    }
     return nodeManager->regexpType();
   }
 };
@@ -270,15 +270,15 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
-               TNode::iterator it = n.begin();
-               TNode::iterator it_end = n.end();
-               for (; it != it_end; ++ it) {
-                  TypeNode t = (*it).getType(check);
-                  if (!t.isRegExp()) {
-                        throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
-                  }
-               }
-       }
+      TNode::iterator it = n.begin();
+      TNode::iterator it_end = n.end();
+      for (; it != it_end; ++ it) {
+         TypeNode t = (*it).getType(check);
+         if (!t.isRegExp()) {
+           throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
+         }
+      }
+    }
     return nodeManager->regexpType();
   }
 };
@@ -288,15 +288,15 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
-               TNode::iterator it = n.begin();
-               TNode::iterator it_end = n.end();
-               for (; it != it_end; ++ it) {
-                  TypeNode t = (*it).getType(check);
-                  if (!t.isRegExp()) {
-                        throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
-                  }
-               }
-       }
+      TNode::iterator it = n.begin();
+      TNode::iterator it_end = n.end();
+      for (; it != it_end; ++ it) {
+       TypeNode t = (*it).getType(check);
+       if (!t.isRegExp()) {
+         throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
+       }
+      }
+    }
     return nodeManager->regexpType();
   }
 };
@@ -306,12 +306,13 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
-               TNode::iterator it = n.begin();
-               TypeNode t = (*it).getType(check);
-               if (!t.isRegExp()) {
-                 throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
-               }
-       }
+      TNode::iterator it = n.begin();
+      TNode::iterator it_end = n.end();
+      TypeNode t = (*it).getType(check);
+      if (!t.isRegExp()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
+      }
+    }
     return nodeManager->regexpType();
   }
 };
@@ -321,12 +322,13 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
-               TNode::iterator it = n.begin();
-               TypeNode t = (*it).getType(check);
-               if (!t.isRegExp()) {
-                 throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
-               }
-       }
+      TNode::iterator it = n.begin();
+      TNode::iterator it_end = n.end();
+      TypeNode t = (*it).getType(check);
+      if (!t.isRegExp()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
+      }
+    }
     return nodeManager->regexpType();
   }
 };
@@ -336,12 +338,13 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
-               TNode::iterator it = n.begin();
-               TypeNode t = (*it).getType(check);
-               if (!t.isRegExp()) {
-                 throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
-               }
-       }
+      TNode::iterator it = n.begin();
+      TNode::iterator it_end = n.end();
+      TypeNode t = (*it).getType(check);
+      if (!t.isRegExp()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
+      }
+    }
     return nodeManager->regexpType();
   }
 };
@@ -351,27 +354,28 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
-               TNode::iterator it = n.begin();
-               char ch[2];
-
-               for(int i=0; i<2; ++i) {
-                       TypeNode t = (*it).getType(check);
-                       if (!t.isString()) {
-                         throw TypeCheckingExceptionPrivate(n, "expecting a string term in regexp range");
-                       }
-                       if( (*it).getKind() != kind::CONST_STRING ) {
-                         throw TypeCheckingExceptionPrivate(n, "expecting a constant string term in regexp range");
-                       }
-                       if( (*it).getConst<String>().size() != 1 ) {
-                         throw TypeCheckingExceptionPrivate(n, "expecting a single constant string term in regexp range");
-                       }
-                       ch[i] = (*it).getConst<String>().getFirstChar();
-                       ++it;
-               }
-               if(ch[0] > ch[1]) {
-                       throw TypeCheckingExceptionPrivate(n, "expecting the first constant is less or equal to the second one in regexp range");
-               }
-       }
+      TNode::iterator it = n.begin();
+      TNode::iterator it_end = n.end();
+      char ch[2];
+
+      for(int i=0; i<2; ++i) {
+        TypeNode t = (*it).getType(check);
+        if (!t.isString()) {
+          throw TypeCheckingExceptionPrivate(n, "expecting a string term in regexp range");
+        }
+        if( (*it).getKind() != kind::CONST_STRING ) {
+          throw TypeCheckingExceptionPrivate(n, "expecting a constant string term in regexp range");
+        }
+        if( (*it).getConst<String>().size() != 1 ) {
+          throw TypeCheckingExceptionPrivate(n, "expecting a single constant string term in regexp range");
+        }
+        ch[i] = (*it).getConst<String>().getFirstChar();
+        ++it;
+      }
+      if(ch[0] > ch[1]) {
+        throw TypeCheckingExceptionPrivate(n, "expecting the first constant is less or equal to the second one in regexp range");
+      }
+    }
     return nodeManager->regexpType();
   }
 };
@@ -381,33 +385,33 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
-               TNode::iterator it = n.begin();
-               TNode::iterator it_end = n.end();
-               TypeNode t = (*it).getType(check);
-               if (!t.isRegExp()) {
-                 throw TypeCheckingExceptionPrivate(n, "expecting a regexp term in regexp loop 1");
-               }
-               ++it; t = (*it).getType(check);
-               if (!t.isInteger()) {
-                 throw TypeCheckingExceptionPrivate(n, "expecting an integer term in regexp loop 2");
-               }
-               if(!(*it).isConst()) {
-                 throw TypeCheckingExceptionPrivate(n, "expecting an const integer term in regexp loop 2");
-               }
-               ++it;
-               if(it != it_end) {
-                       t = (*it).getType(check);
-                       if (!t.isInteger()) {
-                         throw TypeCheckingExceptionPrivate(n, "expecting an integer term in regexp loop 3");
-                       }
-                       if(!(*it).isConst()) {
-                         throw TypeCheckingExceptionPrivate(n, "expecting an const integer term in regexp loop 3");
-                       }
-                       //if(++it != it_end) {
-                       //  throw TypeCheckingExceptionPrivate(n, "too many regexp");
-                       //}
-               }
-       }
+      TNode::iterator it = n.begin();
+      TNode::iterator it_end = n.end();
+      TypeNode t = (*it).getType(check);
+      if (!t.isRegExp()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting a regexp term in regexp loop 1");
+      }
+      ++it; t = (*it).getType(check);
+      if (!t.isInteger()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting an integer term in regexp loop 2");
+      }
+      if(!(*it).isConst()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting an const integer term in regexp loop 2");
+      }
+      ++it;
+      if(it != it_end) {
+        t = (*it).getType(check);
+        if (!t.isInteger()) {
+          throw TypeCheckingExceptionPrivate(n, "expecting an integer term in regexp loop 3");
+        }
+        if(!(*it).isConst()) {
+          throw TypeCheckingExceptionPrivate(n, "expecting an const integer term in regexp loop 3");
+        }
+        //if(++it != it_end) {
+        //  throw TypeCheckingExceptionPrivate(n, "too many regexp");
+        //}
+      }
+    }
     return nodeManager->regexpType();
   }
 };
@@ -417,15 +421,16 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
-               TNode::iterator it = n.begin();
-               TypeNode t = (*it).getType(check);
-               if (!t.isString()) {
-                 throw TypeCheckingExceptionPrivate(n, "expecting string terms");
-               }
-               //if( (*it).getKind() != kind::CONST_STRING ) {
-               //  throw TypeCheckingExceptionPrivate(n, "expecting constant string terms");
-               //}
-       }
+      TNode::iterator it = n.begin();
+      TNode::iterator it_end = n.end();
+      TypeNode t = (*it).getType(check);
+      if (!t.isString()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting string terms");
+      }
+      //if( (*it).getKind() != kind::CONST_STRING ) {
+      //  throw TypeCheckingExceptionPrivate(n, "expecting constant string terms");
+      //}
+    }
     return nodeManager->regexpType();
   }
 };
@@ -435,17 +440,18 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
-               TNode::iterator it = n.begin();
-               TypeNode t = (*it).getType(check);
-               if (!t.isString()) {
-                 throw TypeCheckingExceptionPrivate(n, "expecting string terms");
-               }
-               ++it;
-               t = (*it).getType(check);
-               if (!t.isRegExp()) {
-                 throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
-               }
-       }
+      TNode::iterator it = n.begin();
+      TNode::iterator it_end = n.end();
+      TypeNode t = (*it).getType(check);
+      if (!t.isString()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting string terms");
+      }
+      ++it;
+      t = (*it).getType(check);
+      if (!t.isRegExp()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
+      }
+    }
     return nodeManager->booleanType();
   }
 };
index 3dc12009be5cf3d4bea5ad6c680e1b5b4018b1ac..1a101fa70f529fd72a6326f05c868805fe0e8733 100644 (file)
@@ -44,8 +44,8 @@ public:
     TypeEnumeratorBase<StringEnumerator>(type) {
     Assert(type.getKind() == kind::TYPE_CONSTANT &&
            type.getConst<TypeConstant>() == STRING_TYPE);
-       d_cardinality = 256;
-       mkCurr();
+    d_cardinality = 256;
+    mkCurr();
   }
   Node operator*() throw() {
     return d_curr;
@@ -89,10 +89,10 @@ private:
        }
 public:
   StringEnumeratorLength(unsigned length, unsigned card = 256) : d_cardinality(card) {
-     for( unsigned i=0; i<length; i++ ){
-               d_data.push_back( 0 );
-        }
-        mkCurr();
+    for( unsigned i=0; i<length; i++ ){
+      d_data.push_back( 0 );
+         }
+         mkCurr();
   }
 
   Node operator*() throw() {
@@ -100,21 +100,21 @@ public:
   }
 
   StringEnumeratorLength& operator++() throw() {
-       bool changed = false;
-       for(unsigned i=0; i<d_data.size(); ++i) {
-               if( d_data[i] + 1 < d_cardinality ) {
-                       ++d_data[i]; changed = true;
-                       break;
-               } else {
-                       d_data[i] = 0;
-               }
-       }
-       
-       if(!changed) {
-               d_curr = Node::null();
-       }else{
-               mkCurr();
-       }
+    bool changed = false;
+    for(unsigned i=0; i<d_data.size(); ++i) {
+      if( d_data[i] + 1 < d_cardinality ) {
+        ++d_data[i]; changed = true;
+        break;
+      } else {
+        d_data[i] = 0;
+      }
+    }
+    
+    if(!changed) {
+      d_curr = Node::null();
+    }else{
+      mkCurr();
+    }
     return *this;
   }
 
index 3bc17b050ee17df32595b252455c946a1f89025b..3e2fa948cfc67ff242b6c8949687099ad55c67fc 100644 (file)
@@ -96,10 +96,7 @@ void String::getCharSet(std::set<unsigned int> &cset) const {
 }\r
 \r
 bool String::overlap(String &y) const {\r
-       unsigned n = y.size();\r
-       if(d_str.size() < y.size()) {\r
-               n = d_str.size();\r
-       }\r
+       unsigned n = d_str.size() < y.size() ? d_str.size() : y.size();\r
        for(unsigned i=1; i<n; i++) {\r
                String s = suffix(i);\r
                String p = y.prefix(i);\r
index 2bb2b5c4cb720cbcf9b00c58900614b602f71ab6..1ae01343d0cba9b844a97b1251e8870f487cf986 100644 (file)
@@ -34,29 +34,29 @@ namespace CVC4 {
 class CVC4_PUBLIC String {
 public:
   static unsigned int convertCharToUnsignedInt( char c ) {
-       int i = (int)c;
-       i = i-65;
-       return (unsigned int)(i<0 ? i+256 : i);
+    int i = (int)c;
+    i = i-65;
+    return (unsigned int)(i<0 ? i+256 : i);
   }
   static char convertUnsignedIntToChar( unsigned int i ){
-       int ii = i+65;
-       return (char)(ii>=256 ? ii-256 : ii);
+    int ii = i+65;
+    return (char)(ii>=256 ? ii-256 : ii);
   }
   static bool isPrintable( unsigned int i ){
-       char c = convertUnsignedIntToChar( i );
-       return isprint( (int)c );
+    char c = convertUnsignedIntToChar( i );
+    return isprint( (int)c );
   }
 
 private:
   std::vector<unsigned int> d_str;
 
   bool isVecSame(const std::vector<unsigned int> &a, const std::vector<unsigned int> &b) const {
-      if(a.size() != b.size()) return false;
-      else {
-          for(unsigned int i=0; i<a.size(); ++i)
-              if(a[i] != b[i]) return false;
-          return true;
-      }
+    if(a.size() != b.size()) return false;
+    else {
+      for(unsigned int i=0; i<a.size(); ++i)
+        if(a[i] != b[i]) return false;
+      return true;
+    }
   }
 
   //guarded
@@ -76,12 +76,12 @@ public:
   String() {}
 
   String(const std::string &s) {
-       toInternal(s);
+    toInternal(s);
   }
 
   String(const char* s) {
-       std::string stmp(s);
-       toInternal(stmp);
+    std::string stmp(s);
+    toInternal(stmp);
   }
 
   String(const char c) {
@@ -114,53 +114,53 @@ public:
   bool operator <(const String& y) const {
     if(d_str.size() != y.d_str.size()) return d_str.size() < y.d_str.size();
     else {
-        for(unsigned int i=0; i<d_str.size(); ++i)
-            if(d_str[i] != y.d_str[i]) return d_str[i] < y.d_str[i];
+      for(unsigned int i=0; i<d_str.size(); ++i)
+        if(d_str[i] != y.d_str[i]) return d_str[i] < y.d_str[i];
 
-        return false;
+      return false;
     }
   }
 
   bool operator >(const String& y) const {
     if(d_str.size() != y.d_str.size()) return d_str.size() > y.d_str.size();
     else {
-        for(unsigned int i=0; i<d_str.size(); ++i)
-            if(d_str[i] != y.d_str[i]) return d_str[i] > y.d_str[i];
+      for(unsigned int i=0; i<d_str.size(); ++i)
+        if(d_str[i] != y.d_str[i]) return d_str[i] > y.d_str[i];
 
-        return false;
+      return false;
     }
   }
 
   bool operator <=(const String& y) const {
     if(d_str.size() != y.d_str.size()) return d_str.size() < y.d_str.size();
     else {
-        for(unsigned int i=0; i<d_str.size(); ++i)
-            if(d_str[i] != y.d_str[i]) return d_str[i] < y.d_str[i];
+      for(unsigned int i=0; i<d_str.size(); ++i)
+        if(d_str[i] != y.d_str[i]) return d_str[i] < y.d_str[i];
 
-        return true;
+      return true;
     }
   }
 
   bool operator >=(const String& y) const {
     if(d_str.size() != y.d_str.size()) return d_str.size() > y.d_str.size();
     else {
-        for(unsigned int i=0; i<d_str.size(); ++i)
-            if(d_str[i] != y.d_str[i]) return d_str[i] > y.d_str[i];
+      for(unsigned int i=0; i<d_str.size(); ++i)
+        if(d_str[i] != y.d_str[i]) return d_str[i] > y.d_str[i];
 
-        return true;
+      return true;
     }
   }
 
   bool strncmp(const String &y, unsigned int n) const {
-      for(unsigned int i=0; i<n; ++i)
-          if(d_str[i] != y.d_str[i]) return false;
-      return true;
+    for(unsigned int i=0; i<n; ++i)
+      if(d_str[i] != y.d_str[i]) return false;
+    return true;
   }
 
   bool rstrncmp(const String &y, unsigned int n) const {
-      for(unsigned int i=0; i<n; ++i)
-          if(d_str[d_str.size() - i - 1] != y.d_str[y.d_str.size() - i - 1]) return false;
-      return true;
+    for(unsigned int i=0; i<n; ++i)
+      if(d_str[d_str.size() - i - 1] != y.d_str[y.d_str.size() - i - 1]) return false;
+    return true;
   }
 
   bool isEmptyString() const {
@@ -229,16 +229,16 @@ public:
   }
 
   String replace(const String &s, const String &t) const {
-       std::size_t ret = find(s);
-       if( ret != std::string::npos ) {
-               std::vector<unsigned int> vec;
-               vec.insert(vec.begin(), d_str.begin(), d_str.begin() + ret); 
-               vec.insert(vec.end(), t.d_str.begin(), t.d_str.end());
-               vec.insert(vec.end(), d_str.begin() + ret + s.d_str.size(), d_str.end());
-               return String(vec);
-       } else {
-               return *this;
-       }
+    std::size_t ret = find(s);
+    if( ret != std::string::npos ) {
+      std::vector<unsigned int> vec;
+      vec.insert(vec.begin(), d_str.begin(), d_str.begin() + ret); 
+      vec.insert(vec.end(), t.d_str.begin(), t.d_str.end());
+      vec.insert(vec.end(), d_str.begin() + ret + s.d_str.size(), d_str.end());
+      return String(vec);
+    } else {
+      return *this;
+    }
   }
 
   String substr(unsigned i) const {