Remove some dead code from theory strings (#2125)

6 files changed, 33 insertions, 809 deletions

diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml
index a6e7aa412..66b312737 100644
--- a/src/options/strings_options.toml
+++ b/src/options/strings_options.toml
@@ -57,24 +57,6 @@ header = "options/strings_options.h"
   help       = "the eager intersection used by the theory of strings"
 
 [[option]]
-  name       = "stringOpt1"
-  category   = "regular"
-  long       = "strings-opt1"
-  type       = "bool"
-  default    = "true"
-  read_only  = true
-  help       = "internal option1 for strings: normal form"
-
-[[option]]
-  name       = "stringOpt2"
-  category   = "regular"
-  long       = "strings-opt2"
-  type       = "bool"
-  default    = "false"
-  read_only  = true
-  help       = "internal option2 for strings: constant regexp splitting"
-
-[[option]]
   name       = "stringIgnNegMembership"
   category   = "regular"
   long       = "strings-inm"
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 0eccc72c7..e130d5e4b 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -634,76 +634,6 @@ Node RegExpOpr::derivativeSingle( Node r, CVC4::String c ) {
   return retNode;
 }
 
-//TODO:
-bool RegExpOpr::guessLength( Node r, int &co ) {
-  int k = r.getKind();
-  switch( k ) {
-    case kind::STRING_TO_REGEXP:
-    {
-      if(r[0].isConst()) {
-        co += r[0].getConst< CVC4::String >().size();
-        return true;
-      } else {
-        return false;
-      }
-    }
-      break;
-    case kind::REGEXP_CONCAT:
-    {
-      for(unsigned i=0; i<r.getNumChildren(); ++i) {
-        if(!guessLength( r[i], co)) {
-          return false;
-        }
-      }
-      return true;
-    }
-      break;
-    case kind::REGEXP_UNION:
-    {
-      int g_co;
-      for(unsigned i=0; i<r.getNumChildren(); ++i) {
-        int cop = 0;
-        if(!guessLength( r[i], cop)) {
-          return false;
-        }
-        if(i == 0) {
-          g_co = cop;
-        } else {
-          g_co = gcd(g_co, cop);
-        }
-      }
-      return true;
-    }
-      break;
-    case kind::REGEXP_INTER:
-    {
-      int g_co;
-      for(unsigned i=0; i<r.getNumChildren(); ++i) {
-        int cop = 0;
-        if(!guessLength( r[i], cop)) {
-          return false;
-        }
-        if(i == 0) {
-          g_co = cop;
-        } else {
-          g_co = gcd(g_co, cop);
-        }
-      }
-      return true;
-    }
-      break;
-    case kind::REGEXP_STAR:
-    {
-      co = 0;
-      return true;
-    }
-      break;
-    default:
-      Trace("strings-error") << "Unsupported term: " << mkString( r ) << " in membership of RegExp." << std::endl;
-      return false;
-  }
-}
-
 void RegExpOpr::firstChars( Node r, std::set<unsigned char> &pcset, SetNodes &pvset ) {
   Trace("regexp-fset") << "Start FSET(" << mkString(r) << ")" << std::endl;
   std::map< Node, std::pair< std::set<unsigned char>, SetNodes > >::const_iterator itr = d_fset_cache.find(r);
@@ -809,124 +739,6 @@ void RegExpOpr::firstChars( Node r, std::set<unsigned char> &pcset, SetNodes &pv
   }
 }
 
-bool RegExpOpr::follow( Node r, CVC4::String c, std::vector< unsigned char > &vec_chars ) {
-  int k = r.getKind();
-  switch( k ) {
-    case kind::STRING_TO_REGEXP:
-    {
-      if(r[0].isConst()) {
-        if(r[0] != d_emptyString) {
-          unsigned char t1 = r[0].getConst< CVC4::String >().getFirstChar();
-          if(c.isEmptyString()) {
-            vec_chars.push_back( t1 );
-            return true;
-          } else {
-            unsigned char t2 = c.getFirstChar();
-            if(t1 != t2) {
-              return false;
-            } else {
-              if(c.size() >= 2) {
-                vec_chars.push_back( c.substr(1,1).getFirstChar() );
-              } else {
-                vec_chars.push_back( '\0' );
-              }
-              return true;
-            }
-          }
-        } else {
-          return false;
-        }
-      } else {
-        return false;
-      }
-    }
-      break;
-    case kind::REGEXP_CONCAT:
-    {
-      for(unsigned i=0; i<r.getNumChildren(); ++i) {
-        if( follow(r[i], c, vec_chars) ) {
-          if(vec_chars[vec_chars.size() - 1] == '\0') {
-            vec_chars.pop_back();
-            c = d_emptyString.getConst< CVC4::String >();
-          }
-        } else {
-          return false;
-        }
-      }
-      vec_chars.push_back( '\0' );
-      return true;
-    }
-      break;
-    case kind::REGEXP_UNION:
-    {
-      bool flag = false;
-      for(unsigned i=0; i<r.getNumChildren(); ++i) {
-        if( follow(r[i], c, vec_chars) ) {
-          flag=true;
-        }
-      }
-      return flag;
-    }
-      break;
-    case kind::REGEXP_INTER:
-    {
-      std::vector< unsigned char > vt2;
-      for(unsigned i=0; i<r.getNumChildren(); ++i) {
-        std::vector< unsigned char > v_tmp;
-        if( !follow(r[i], c, v_tmp) ) {
-          return false;
-        }
-        std::vector< unsigned char > vt3(vt2);
-        vt2.clear();
-        std::set_intersection( vt3.begin(), vt3.end(), v_tmp.begin(), v_tmp.end(), vt2.begin() );
-        if(vt2.size() == 0) {
-          return false;
-        }
-      }
-      vec_chars.insert( vec_chars.end(), vt2.begin(), vt2.end() );
-      return true;
-    }
-      break;
-    case kind::REGEXP_STAR:
-    {
-      if(follow(r[0], c, vec_chars)) {
-        if(vec_chars[vec_chars.size() - 1] == '\0') {
-          if(c.isEmptyString()) {
-            return true;
-          } else {
-            vec_chars.pop_back();
-            c = d_emptyString.getConst< CVC4::String >();
-            return follow(r[0], c, vec_chars);
-          }
-        } else {
-          return true;
-        }
-      } else {
-        vec_chars.push_back( '\0' );
-        return true;
-      }
-    }
-      break;
-    default: {
-      Trace("strings-error") << "Unsupported term: " << mkString( r ) << " in follow of RegExp." << std::endl;
-      //AlwaysAssert( false );
-      //return Node::null();
-      return false;
-    }
-  }
-}
-
-Node RegExpOpr::mkAllExceptOne( unsigned char exp_c ) {
-  std::vector< Node > vec_nodes;
-  for(unsigned char c=d_char_start; c<=d_char_end; ++c) {
-    if(c != exp_c ) {
-      Node n = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst( ::CVC4::String( c ) ) );
-      vec_nodes.push_back( n );
-    }
-  }
-  return NodeManager::currentNM()->mkNode( kind::REGEXP_UNION, vec_nodes );
-}
-
 //simplify
 void RegExpOpr::simplify(Node t, std::vector< Node > &new_nodes, bool polarity) {
   Trace("strings-regexp-simpl") << "RegExp-Simpl starts with " << t << ", polarity=" << polarity << std::endl;
@@ -1297,99 +1109,6 @@ void RegExpOpr::simplifyPRegExp( Node s, Node r, std::vector< Node > &new_nodes
   }
 }
 
-void RegExpOpr::getCharSet( Node r, std::set<unsigned char> &pcset, SetNodes &pvset ) {
-  std::map< Node, std::pair< std::set<unsigned char>, SetNodes > >::const_iterator itr = d_cset_cache.find(r);
-  if(itr != d_cset_cache.end()) {
-    pcset.insert((itr->second).first.begin(), (itr->second).first.end());
-    pvset.insert((itr->second).second.begin(), (itr->second).second.end());
-  } else {
-    std::set<unsigned char> cset;
-    SetNodes vset;
-    int k = r.getKind();
-    switch( k ) {
-      case kind::REGEXP_EMPTY: {
-        break;
-      }
-      case kind::REGEXP_SIGMA: {
-        for(unsigned char i='\0'; i<=d_lastchar; i++) {
-          cset.insert(i);
-        }
-        break;
-      }
-      case kind::REGEXP_RANGE: {
-        unsigned char a = r[0].getConst<String>().getFirstChar();
-        unsigned char b = r[1].getConst<String>().getFirstChar();
-        for(unsigned char i=a; i<=b; i++) {
-          cset.insert(i);
-        }
-        break;
-      }
-      case kind::STRING_TO_REGEXP: {
-        Node st = Rewriter::rewrite(r[0]);
-        if(st.isConst()) {
-          CVC4::String s = st.getConst< CVC4::String >();
-          cset.insert(s.getVec().begin(), s.getVec().end());
-        } else if(st.getKind() == kind::VARIABLE) {
-          vset.insert( st );
-        } else {
-          for(unsigned i=0; i<st.getNumChildren(); i++) {
-            if(st[i].isConst()) {
-              CVC4::String s = st[i].getConst< CVC4::String >();
-              cset.insert(s.getVec().begin(), s.getVec().end());
-            } else {
-              vset.insert( st[i] );
-            }
-          }
-        }
-        break;
-      }
-      case kind::REGEXP_CONCAT: {
-        for(unsigned i=0; i<r.getNumChildren(); i++) {
-          getCharSet(r[i], cset, vset);
-        }
-        break;
-      }
-      case kind::REGEXP_UNION: {
-        for(unsigned i=0; i<r.getNumChildren(); i++) {
-          getCharSet(r[i], cset, vset);
-        }
-        break;
-      }
-      case kind::REGEXP_INTER: {
-        //TODO: Overapproximation for now
-        //for(unsigned i=0; i<r.getNumChildren(); i++) {
-          //getCharSet(r[i], cset, vset);
-        //}
-        getCharSet(r[0], cset, vset);
-        break;
-      }
-      case kind::REGEXP_STAR: {
-        getCharSet(r[0], cset, vset);
-        break;
-      }
-      case kind::REGEXP_LOOP: {
-        getCharSet(r[0], cset, vset);
-        break;
-      }
-      default: {
-        //Trace("strings-error") << "Unsupported term: " << r << " in getCharSet." << std::endl;
-        Unreachable();
-      }
-    }
-    pcset.insert(cset.begin(), cset.end());
-    pvset.insert(vset.begin(), vset.end());
-    std::pair< std::set<unsigned char>, SetNodes > p(cset, vset);
-    d_cset_cache[r] = p;
-
-    Trace("regexp-cset") << "CSET( " << mkString(r) << " ) = { ";
-    for(std::set<unsigned char>::const_iterator itr = cset.begin();
-      itr != cset.end(); itr++) {
-        Trace("regexp-cset") << (*itr) << ",";
-      }
-    Trace("regexp-cset") << " }" << std::endl;
-  }
-}
-
 bool RegExpOpr::isPairNodesInSet(std::set< PairNodes > &s, Node n1, Node n2) {
   for(std::set< PairNodes >::const_iterator itr = s.begin();
       itr != s.end(); ++itr) {
@@ -1734,337 +1453,6 @@ Node RegExpOpr::intersect(Node r1, Node r2, bool &spflag) {
   }
 }
 
-Node RegExpOpr::complement(Node r, int &ret) {
-  Node rNode;
-  ret = 1;
-  if(d_compl_cache.find(r) != d_compl_cache.end()) {
-    rNode = d_compl_cache[r].first;
-    ret = d_compl_cache[r].second;
-  } else {
-    if(r == d_emptyRegexp) {
-      rNode = d_sigma_star;
-    } else if(r == d_emptySingleton) {
-      rNode = NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, d_sigma, d_sigma_star);
-    } else if(!checkConstRegExp(r)) {
-      //TODO: var to be extended
-      ret = 0;
-    } else {
-      std::set<unsigned char> cset;
-      SetNodes vset;
-      firstChars(r, cset, vset);
-      std::vector< Node > vec_nodes;
-      for(unsigned char i=0; i<=d_lastchar; i++) {
-        CVC4::String c(i);
-        Node n = NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst(c));
-        Node r2;
-        if(cset.find(i) == cset.end()) {
-          r2 = d_sigma_star;
-        } else {
-          int rt;
-          derivativeS(r, c, r2);
-          if(r2 == r) {
-            r2 = d_emptyRegexp;
-          } else {
-            r2 = complement(r2, rt);
-          }
-        }
-        n = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, n, r2));
-        vec_nodes.push_back(n);
-      }
-      rNode = vec_nodes.size()==0? d_emptyRegexp : vec_nodes.size()==1? vec_nodes[0] :
-            NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vec_nodes);
-    }
-    rNode = Rewriter::rewrite(rNode);
-    std::pair< Node, int > p(rNode, ret);
-    d_compl_cache[r] = p;
-  }
-  Trace("regexp-compl") << "COMPL( " << mkString(r) << " ) = " << mkString(rNode) << ", ret=" << ret << std::endl;
-  return rNode;
-}
-
-void RegExpOpr::splitRegExp(Node r, std::vector< PairNodes > &pset) {
-  Assert(checkConstRegExp(r));
-  if(d_split_cache.find(r) != d_split_cache.end()) {
-    pset = d_split_cache[r];
-  } else {
-    switch( r.getKind() ) {
-      case kind::REGEXP_EMPTY: {
-        break;
-      }
-      case kind::REGEXP_OPT: {
-        PairNodes tmp(d_emptySingleton, d_emptySingleton);
-        pset.push_back(tmp);
-      }
-      case kind::REGEXP_RANGE:
-      case kind::REGEXP_SIGMA: {
-        PairNodes tmp1(d_emptySingleton, r);
-        PairNodes tmp2(r, d_emptySingleton);
-        pset.push_back(tmp1);
-        pset.push_back(tmp2);
-        break;
-      }
-      case kind::STRING_TO_REGEXP: {
-        Assert(r[0].isConst());
-        CVC4::String s = r[0].getConst< CVC4::String >();
-        PairNodes tmp1(d_emptySingleton, r);
-        pset.push_back(tmp1);
-        for(unsigned i=1; i<s.size(); i++) {
-          CVC4::String s1 = s.substr(0, i);
-          CVC4::String s2 = s.substr(i);
-          Node n1 = NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst(s1));
-          Node n2 = NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst(s2));
-          PairNodes tmp3(n1, n2);
-          pset.push_back(tmp3);
-        }
-        PairNodes tmp2(r, d_emptySingleton);
-        pset.push_back(tmp2);
-        break;
-      }
-      case kind::REGEXP_CONCAT: {
-        for(unsigned i=0; i<r.getNumChildren(); i++) {
-          std::vector< PairNodes > tset;
-          splitRegExp(r[i], tset);
-          std::vector< Node > hvec;
-          std::vector< Node > tvec;
-          for(unsigned j=0; j<=i; j++) {
-            hvec.push_back(r[j]);
-          }
-          for(unsigned j=i; j<r.getNumChildren(); j++) {
-            tvec.push_back(r[j]);
-          }
-          for(unsigned j=0; j<tset.size(); j++) {
-            hvec[i] = tset[j].first;
-            tvec[0] = tset[j].second;
-            Node r1 = Rewriter::rewrite( hvec.size()==1?hvec[0]:NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, hvec) );
-            Node r2 = Rewriter::rewrite( tvec.size()==1?tvec[0]:NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, tvec) );
-            PairNodes tmp2(r1, r2);
-            pset.push_back(tmp2);
-          }
-        }
-        break;
-      }
-      case kind::REGEXP_UNION: {
-        for(unsigned i=0; i<r.getNumChildren(); ++i) {
-          std::vector< PairNodes > tset;
-          splitRegExp(r[i], tset);
-          pset.insert(pset.end(), tset.begin(), tset.end());
-        }
-        break;
-      }
-      case kind::REGEXP_INTER: {
-        bool spflag = false;
-        Node tmp = r[0];
-        for(unsigned i=1; i<r.getNumChildren(); i++) {
-          tmp = intersect(tmp, r[i], spflag);
-        }
-        splitRegExp(tmp, pset);
-        break;
-      }
-      case kind::REGEXP_STAR: {
-        std::vector< PairNodes > tset;
-        splitRegExp(r[0], tset);
-        PairNodes tmp1(d_emptySingleton, d_emptySingleton);
-        pset.push_back(tmp1);
-        for(unsigned i=0; i<tset.size(); i++) {
-          Node r1 = tset[i].first==d_emptySingleton ? r : NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, r, tset[i].first);
-          Node r2 = tset[i].second==d_emptySingleton ? r : NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, tset[i].second, r);
-          PairNodes tmp2(r1, r2);
-          pset.push_back(tmp2);
-        }
-        break;
-      }
-      case kind::REGEXP_LOOP: {
-        unsigned l = r[1].getConst<Rational>().getNumerator().toUnsignedInt();
-        unsigned u = r[2].getConst<Rational>().getNumerator().toUnsignedInt();
-        if(l == u) {
-          //R^n
-          if(l == 0) {
-            PairNodes tmp1(d_emptySingleton, d_emptySingleton);
-            pset.push_back(tmp1);
-          } else if(l == 1) {
-            splitRegExp(r[0], pset);
-          } else {
-            std::vector< PairNodes > tset;
-            splitRegExp(r[0], tset);
-            for(unsigned j=0; j<l; j++) {
-              Node num1 = NodeManager::currentNM()->mkConst(CVC4::Rational(j));
-              Node r1 = j==0? d_emptySingleton : j==1? r[0] : NodeManager::currentNM()->mkNode(kind::REGEXP_LOOP, r[0], num1, num1);
-              unsigned j2 = l - j - 1;
-              Node num2 = NodeManager::currentNM()->mkConst(CVC4::Rational(j2));
-              Node r2 = j2==0? d_emptySingleton : j2==1? r[0] : NodeManager::currentNM()->mkNode(kind::REGEXP_LOOP, r[0], num2, num2);
-              for(unsigned i=0; i<tset.size(); i++) {
-                r1 = tset[i].first==d_emptySingleton? r1 : NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, r1, tset[i].first);
-                r2 = tset[i].second==d_emptySingleton? r2 : NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, tset[i].second, r2);
-                PairNodes tmp2(r1, r2);
-                pset.push_back(tmp2);
-              }
-            }
-          }
-        } else {
-          //R{0,n}
-          PairNodes tmp1(d_emptySingleton, d_emptySingleton);
-          pset.push_back(tmp1);
-          std::vector< PairNodes > tset;
-          splitRegExp(r[0], tset);
-          pset.insert(pset.end(), tset.begin(), tset.end());
-          for(unsigned k=2; k<=u; k++) {
-            for(unsigned j=0; j<k; j++) {
-              Node num1 = NodeManager::currentNM()->mkConst(CVC4::Rational(j));
-              Node r1 = j==0? d_emptySingleton : j==1? r[0] : NodeManager::currentNM()->mkNode(kind::REGEXP_LOOP, r[0], num1, num1);
-              unsigned j2 = k - j - 1;
-              Node num2 = NodeManager::currentNM()->mkConst(CVC4::Rational(j2));
-              Node r2 = j2==0? d_emptySingleton : j2==1? r[0] : NodeManager::currentNM()->mkNode(kind::REGEXP_LOOP, r[0], num2, num2);
-              for(unsigned i=0; i<tset.size(); i++) {
-                r1 = tset[i].first==d_emptySingleton? r1 : NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, r1, tset[i].first);
-                r2 = tset[i].second==d_emptySingleton? r2 : NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, tset[i].second, r2);
-                PairNodes tmp2(r1, r2);
-                pset.push_back(tmp2);
-              }
-            }
-          }
-        }
-        break;
-      }
-      case kind::REGEXP_PLUS: {
-        std::vector< PairNodes > tset;
-        splitRegExp(r[0], tset);
-        for(unsigned i=0; i<tset.size(); i++) {
-          Node r1 = NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, r, tset[i].first);
-          Node r2 = NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, tset[i].second, r);
-          PairNodes tmp2(r1, r2);
-          pset.push_back(tmp2);
-        }
-        break;
-      }
-      default: {
-        Trace("strings-error") << "Unsupported term: " << r << " in splitRegExp." << std::endl;
-        Assert( false );
-        //return Node::null();
-      }
-    }
-    d_split_cache[r] = pset;
-  }
-}
-
-void RegExpOpr::flattenRegExp(Node r, std::vector< std::pair< CVC4::String, unsigned > > &fvec) {
-  Assert(false);
-  Assert(checkConstRegExp(r));
-  switch( r.getKind() ) {
-      case kind::REGEXP_EMPTY: {
-        //TODO
-        break;
-      }
-      case kind::REGEXP_SIGMA: {
-        CVC4::String s("a");
-        std::pair< CVC4::String, unsigned > tmp(s, 0);
-        //TODO
-        break;
-      }
-      case kind::STRING_TO_REGEXP: {
-        Assert(r[0].isConst());
-        CVC4::String s = r[0].getConst< CVC4::String >();
-        std::pair< CVC4::String, unsigned > tmp(s, 0);
-        //TODO
-        break;
-      }
-      case kind::REGEXP_CONCAT: {
-        for(unsigned i=0; i<r.getNumChildren(); i++) {
-          //TODO
-        }
-        break;
-      }
-      case kind::REGEXP_UNION: {
-        for(unsigned i=0; i<r.getNumChildren(); ++i) {
-          //TODO
-        }
-        break;
-      }
-      case kind::REGEXP_INTER: {
-        //TODO
-        break;
-      }
-      case kind::REGEXP_STAR: {
-        //TODO
-        break;
-      }
-      case kind::REGEXP_LOOP: {
-        //TODO
-        break;
-      }
-      default: {
-        Unreachable();
-      }
-  }
-}
-
-void RegExpOpr::disjunctRegExp(Node r, std::vector<Node> &vec_or) {
-  switch(r.getKind()) {
-      case kind::REGEXP_EMPTY: {
-        vec_or.push_back(r);
-        break;
-      }
-      case kind::REGEXP_SIGMA: {
-        vec_or.push_back(r);
-        break;
-      }
-      case kind::REGEXP_RANGE: {
-        vec_or.push_back(r);
-        break;
-      }
-      case kind::STRING_TO_REGEXP: {
-        vec_or.push_back(r);
-        break;
-      }
-      case kind::REGEXP_CONCAT: {
-        disjunctRegExp(r[0], vec_or);
-        for(unsigned i=1; i<r.getNumChildren(); i++) {
-          std::vector<Node> vec_con;
-          disjunctRegExp(r[i], vec_con);
-          std::vector<Node> vec_or2;
-          for(unsigned k1=0; k1<vec_or.size(); k1++) {
-            for(unsigned k2=0; k2<vec_con.size(); k2++) {
-              Node tmp = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, vec_or[k1], vec_con[k2]) );
-              if(std::find(vec_or2.begin(), vec_or2.end(), tmp) == vec_or2.end()) {
-                vec_or2.push_back( tmp );
-              }
-            }
-          }
-          vec_or = vec_or2;
-        }
-        break;
-      }
-      case kind::REGEXP_UNION: {
-        for(unsigned i=0; i<r.getNumChildren(); ++i) {
-          std::vector<Node> vec_or2;
-          disjunctRegExp(r[i], vec_or2);
-          vec_or.insert(vec_or.end(), vec_or2.begin(), vec_or2.end());
-        }
-        break;
-      }
-      case kind::REGEXP_INTER: {
-        Assert(checkConstRegExp(r));
-        Node rtmp = r[0];
-        bool spflag = false;
-        for(unsigned i=1; i<r.getNumChildren(); ++i) {
-          rtmp = intersect(rtmp, r[i], spflag);
-        }
-        disjunctRegExp(rtmp, vec_or);
-        break;
-      }
-      case kind::REGEXP_STAR: {
-        vec_or.push_back(r);
-        break;
-      }
-      case kind::REGEXP_LOOP: {
-        vec_or.push_back(r);
-        break;
-      }
-      default: {
-        Unreachable();
-      }
-  }
-}
-
 //printing
 std::string RegExpOpr::niceChar(Node r) {
   if(r.isConst()) {
diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h
index 04ac11549..d33a2b70c 100644
--- a/src/theory/strings/regexp_operation.h
+++ b/src/theory/strings/regexp_operation.h
@@ -75,7 +75,6 @@ private:
   Node mkAllExceptOne( unsigned char c );
   bool isPairNodesInSet(std::set< PairNodes > &s, Node n1, Node n2);
 
-  void getCharSet( Node r, std::set<unsigned char> &pcset, SetNodes &pvset );
   bool containC2(unsigned cnt, Node n);
   Node convert1(unsigned cnt, Node n);
   void convert2(unsigned cnt, Node n, Node &r1, Node &r2);
@@ -83,20 +82,6 @@ private:
   Node intersectInternal( Node r1, Node r2, std::map< PairNodes, Node > cache, unsigned cnt );
   Node removeIntersection(Node r);
   void firstChars( Node r, std::set<unsigned char> &pcset, SetNodes &pvset );
-
-  //TODO: for intersection
-  bool follow( Node r, CVC4::String c, std::vector< unsigned char > &vec_chars );
-
-  /*class CState {
-  public:
-    Node r1;
-    Node r2;
-    unsigned cnt;
-    Node head;
-    CState(Node rr1, Node rr2, Node rcnt, Node rhead)
-      : r1(rr1), r2(rr2), cnt(rcnt), head(rhead) {}
-  };*/
-
 public:
   RegExpOpr();
   ~RegExpOpr();
@@ -106,12 +91,7 @@ public:
   int delta( Node r, Node &exp );
   int derivativeS( Node r, CVC4::String c, Node &retNode );
   Node derivativeSingle( Node r, CVC4::String c );
-  bool guessLength( Node r, int &co );
   Node intersect(Node r1, Node r2, bool &spflag);
-  Node complement(Node r, int &ret);
-  void splitRegExp(Node r, std::vector< PairNodes > &pset);
-  void flattenRegExp(Node r, std::vector< std::pair< CVC4::String, unsigned > > &fvec);
-  void disjunctRegExp(Node r, std::vector<Node> &vec_or);
 
   std::string mkString( Node r );
 };
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index e81968843..66788bf13 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -885,7 +885,8 @@ void TheoryStrings::checkExtfReductions( int effort ) {
     Assert( nr.isNull() );
     if( ret!=0 ){
       getExtTheory()->markReduced( extf[i] );
-      if( options::stringOpt1() && hasProcessed() ){
+      if (hasProcessed())
+      {
         return;
       }
     }
@@ -4338,57 +4339,6 @@ Node TheoryStrings::mkRegExpAntec(Node atom, Node ant) {
   }
 }
 
-bool TheoryStrings::applyRConsume( CVC4::String &s, Node &r) {
-  Trace("regexp-derivative") << "TheoryStrings::derivative: s=" << s << ", r= " << r << std::endl;
-  Assert( d_regexp_opr.checkConstRegExp(r) );
-
-  if( !s.isEmptyString() ) {
-    Node dc = r;
-
-    for(unsigned i=0; i<s.size(); ++i) {
-      CVC4::String c = s.substr(i, 1);
-      Node dc2;
-      int rt = d_regexp_opr.derivativeS(dc, c, dc2);
-      dc = dc2;
-      if(rt == 0) {
-        Unreachable();
-      } else if(rt == 2) {
-        return false;
-      }
-    }
-    r = dc;
-  }
-
-  return true;
-}
-
-Node TheoryStrings::applyRSplit(Node s1, Node s2, Node r) {
-  Assert(d_regexp_opr.checkConstRegExp(r));
-
-  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;
-
-  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()==0? Node::null() : vec_or.size()==1 ? vec_or[0] : Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::OR, vec_or) );
-  return conc;
-}
-
-bool TheoryStrings::applyRLen(std::map< Node, std::vector< Node > > &XinR_with_exps) {
-  if(XinR_with_exps.size() > 0) {
-    //TODO: get vector, var, store.
-    return true;
-  } else  {
-    return false;
-  }
-}
-
 void TheoryStrings::checkMemberships() {
   //add the memberships
   std::vector<Node> mems = getExtTheory()->getActive(kind::STRING_IN_REGEXP);
@@ -4472,6 +4422,7 @@ void TheoryStrings::checkMemberships() {
 
   Trace("regexp-debug") << "... No Intersect Conflict in Memberships, addedLemma: " << addedLemma << std::endl;
   if(!addedLemma) {
+    NodeManager* nm = NodeManager::currentNM();
     for( unsigned i=0; i<d_regexp_memberships.size(); i++ ) {
       //check regular expression membership
       Node assertion = d_regexp_memberships[i];
@@ -4486,71 +4437,43 @@ void TheoryStrings::checkMemberships() {
         Node r = atom[1];
         std::vector< Node > rnfexp;
 
-        //if(options::stringOpt1()) {
-        if(true){
-          if(!x.isConst()) {
-            x = getNormalString( x, rnfexp);
-            changed = true;
+        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(nm->mkNode(kind::STRING_IN_REGEXP, x, r));
+          if (!polarity)
+          {
+            tmp = tmp.negate();
           }
-          if(!d_regexp_opr.checkConstRegExp(r)) {
-            r = getNormalSymRegExp(r, rnfexp);
-            changed = true;
+          if (tmp == d_true)
+          {
+            d_regexp_ccached.insert(assertion);
+            continue;
           }
-          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;
-            }
+          else if (tmp == d_false)
+          {
+            Node antec = mkRegExpAntec(assertion, mkExplain(rnfexp));
+            Node conc = Node::null();
+            sendLemma(antec, conc, "REGEXP NF Conflict");
+            addedLemma = true;
+            break;
           }
         }
 
         if( polarity ) {
           flag = checkPDerivative(x, r, atom, addedLemma, 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 = mkConcat(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 {
-                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.");
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 6e638e445..0d4b1f282 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -457,9 +457,6 @@ private:
   //--------------------------------for checkMemberships
   // check membership constraints
   Node mkRegExpAntec(Node atom, Node ant);
-  bool applyRConsume( CVC4::String &s, Node &r );
-  Node applyRSplit( Node s1, Node s2, Node r );
-  bool applyRLen( std::map< Node, std::vector< Node > > &XinR_with_exps );
   bool checkPDerivative( Node x, Node r, Node atom, bool &addedLemma, std::vector< Node > &nf_exp);
   //check contains
   void checkPosContains( std::vector< Node >& posContains );
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 2f3f87657..b7cb22329 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -663,9 +663,6 @@ Node TheoryStringsRewriter::applyAX( TNode node ) {
       }
       break;
     }
-/*    case kind::REGEXP_UNION: {
-      break;
-    }*/
     case kind::REGEXP_SIGMA: {
       break;
     }
@@ -1326,49 +1323,6 @@ RewriteResponse TheoryStringsRewriter::preRewrite(TNode node) {
     if(r.getKind() == kind::REGEXP_STAR) {
       retNode = r;
     } else {
-      /* //lazy
-      Node n1 = Rewriter::rewrite( node[1] );
-      if(!n1.isConst()) {
-        throw LogicException("re.loop contains non-constant integer (1).");
-      }
-      CVC4::Rational rz(0);
-      CVC4::Rational RMAXINT(LONG_MAX);
-      AlwaysAssert(rz <= n1.getConst<Rational>(), "Negative integer in string REGEXP_LOOP (1)");
-      Assert(n1.getConst<Rational>() <= RMAXINT, "Exceeded LONG_MAX in string REGEXP_LOOP (1)");
-      unsigned l = n1.getConst<Rational>().getNumerator().toUnsignedInt();
-      if(node.getNumChildren() == 3) {
-        Node n2 = Rewriter::rewrite( node[2] );
-        if(!n2.isConst()) {
-          throw LogicException("re.loop contains non-constant integer (2).");
-        }
-        if(n1 == n2) {
-          if(l == 0) {
-            retNode = NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP,
-              NodeManager::currentNM()->mkConst(CVC4::String("")));
-          } else if(l == 1) {
-            retNode = node[0];
-          }
-        } else {
-          AlwaysAssert(rz <= n2.getConst<Rational>(), "Negative integer in string REGEXP_LOOP (2)");
-          Assert(n2.getConst<Rational>() <= RMAXINT, "Exceeded LONG_MAX in string REGEXP_LOOP (2)");
-          unsigned u = n2.getConst<Rational>().getNumerator().toUnsignedInt();
-          AlwaysAssert(l <= u, "REGEXP_LOOP (1) > REGEXP_LOOP (2)");
-          if(l != 0) {
-            Node zero = NodeManager::currentNM()->mkConst( CVC4::Rational(0) );
-            Node num = NodeManager::currentNM()->mkConst( CVC4::Rational(u - l) );
-            Node t1 = NodeManager::currentNM()->mkNode(kind::REGEXP_LOOP, node[0], n1, n1);
-            Node t2 = NodeManager::currentNM()->mkNode(kind::REGEXP_LOOP, node[0], zero, num);
-            retNode = NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, t1, t2);
-          }
-        }
-      } else {
-        retNode = l==0? NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, node[0]) :
-          NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT,
-            NodeManager::currentNM()->mkNode(kind::REGEXP_LOOP, node[0], n1, n1),
-            NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, node[0]));
-      }
-    }*/ //lazy
-    /*else {*/
       // eager
       TNode n1 = Rewriter::rewrite( node[1] );
       //