Added C++/Java api examples;

Converted cset to be vector of char, instead of vector of int, since we only accept ascii in input.

11 files changed, 314 insertions, 87 deletions

diff --git a/examples/api/Makefile.am b/examples/api/Makefile.am
index a1455d168..1b3e0b086 100644
--- a/examples/api/Makefile.am
+++ b/examples/api/Makefile.am
@@ -12,7 +12,8 @@ noinst_PROGRAMS = \
 	datatypes \
 	helloworld \
 	linear_arith \
-	sets
+	sets \
+	strings
 
 noinst_DATA =
 
@@ -53,6 +54,11 @@ sets_SOURCES = \
 sets_LDADD = \
 	@builddir@/../../src/libcvc4.la
 
+strings_SOURCES = \
+	strings.cpp
+strings_LDADD = \
+	@builddir@/../../src/libcvc4.la
+
 # for installation
 examplesdir = $(docdir)/$(subdir)
 examples_DATA = $(DIST_SOURCES) $(EXTRA_DIST)
diff --git a/examples/api/java/Makefile.am b/examples/api/java/Makefile.am
index 7216d758e..d12f2877e 100644
--- a/examples/api/java/Makefile.am
+++ b/examples/api/java/Makefile.am
@@ -9,7 +9,8 @@ noinst_DATA += \
 	HelloWorld.class \
 	LinearArith.class \
 	Datatypes.class \
-	PipedInput.class
+	PipedInput.class \
+	Strings.class
 endif
 
 %.class: %.java
@@ -23,7 +24,8 @@ EXTRA_DIST = \
 	HelloWorld.java \
 	LinearArith.java \
 	Datatypes.java \
-	PipedInput.java
+	PipedInput.java \
+	Strings.java
 
 # for installation
 examplesdir = $(docdir)/$(subdir)
diff --git a/examples/api/java/Strings.java b/examples/api/java/Strings.java
new file mode 100644
index 000000000..293118d62
--- /dev/null
+++ b/examples/api/java/Strings.java
@@ -0,0 +1,67 @@
+/*********************                                                        */

+/*! \file Strings.java

+ ** \verbatim

+ ** Original author: Tianyi Liang

+ ** Major contributors: none

+ ** Minor contributors (to current version): none

+ ** This file is part of the CVC4 project.

+ ** Copyright (c) 2009-2014  New York University and The University of Iowa

+ ** See the file COPYING in the top-level source directory for licensing

+ ** information.\endverbatim

+ **

+ ** \brief Reasoning about strings with CVC4 via Java API.

+ **

+ ** A simple demonstration of reasoning about strings with CVC4 via Jave API.

+ **/

+

+import edu.nyu.acsys.CVC4.*;

+

+public class Strings {

+  public static void main(String[] args) {

+    System.loadLibrary("cvc4jni");

+

+    ExprManager em = new ExprManager();

+    SmtEngine smt = new SmtEngine(em);

+

+    // Set the logic

+    smt.setLogic("S");

+

+    // Produce models

+    smt.setOption("produce-models", new SExpr(true));

+    // The option strings-exp is needed

+    smt.setOption("strings-exp", new SExpr(true));

+	// output-language

+    smt.setOption("output-language", new SExpr("smt2"));

+

+    // String type

+    Type string = em.stringType();

+

+    // Variables

+    Expr x = em.mkVar("x", string);

+    Expr y = em.mkVar("y", string);

+    Expr z = em.mkVar("z", string);

+

+    // String concatenation: x.y

+    Expr lhs = em.mkExpr(Kind.STRING_CONCAT, x, y);

+    // String concatenation: z.z

+    Expr rhs = em.mkExpr(Kind.STRING_CONCAT, z, z);;

+    // x.y = z.z

+    Expr formula1 = em.mkExpr(Kind.EQUAL, lhs, rhs);

+

+    // Length of y: |y|

+    Expr leny = em.mkExpr(Kind.STRING_LENGTH, y);

+    // |y| >= 1

+    Expr formula2 = em.mkExpr(Kind.GEQ, leny, em.mkConst(new Rational(1)));

+

+    // Make a query

+    Expr q = em.mkExpr(Kind.AND,

+      formula1,

+      formula2);

+

+     // check sat

+     Result result = smt.checkSat(q);

+     System.out.println("CVC4 reports: " + q + " is " + result + ".");

+

+     System.out.println("  x  = " + smt.getValue(x));

+  }

+}

diff --git a/examples/api/strings.cpp b/examples/api/strings.cpp
new file mode 100644
index 000000000..a424c654a
--- /dev/null
+++ b/examples/api/strings.cpp
@@ -0,0 +1,101 @@
+/*********************                                                        */

+/*! \file sets.cpp

+ ** \verbatim

+ ** Original author: Tianyi Liang

+ ** Major contributors: none

+ ** Minor contributors (to current version): none

+ ** This file is part of the CVC4 project.

+ ** Copyright (c) 2009-2014  New York University and The University of Iowa

+ ** See the file COPYING in the top-level source directory for licensing

+ ** information.\endverbatim

+ **

+ ** \brief Reasoning about strings with CVC4 via C++ API.

+ **

+ ** A simple demonstration of reasoning about strings with CVC4 via C++ API.

+ **/

+

+#include <iostream>

+

+//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed

+#include "smt/smt_engine.h"

+

+using namespace CVC4;

+

+int main() {

+  ExprManager em;

+  SmtEngine smt(&em);

+

+  // Set the logic

+  smt.setLogic("S");

+

+  // Produce models

+  smt.setOption("produce-models", true);

+

+  // The option strings-exp is needed

+  smt.setOption("strings-exp", true);

+

+  // Set output language to SMTLIB2

+  std::cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2);

+  

+  // String type

+  Type string = em.stringType();

+

+  // std::string

+  std::string std_str_ab("ab");

+  // CVC4::String

+  CVC4::String cvc4_str_ab(std_str_ab);

+  CVC4::String cvc4_str_abc("abc");

+  // String constants

+  Expr ab  = em.mkConst(cvc4_str_ab);

+  Expr abc = em.mkConst(CVC4::String("abc"));

+  // String variables

+  Expr x = em.mkVar("x", string);

+  Expr y = em.mkVar("y", string);

+  Expr z = em.mkVar("z", string);

+

+  // String concatenation: x.ab.y

+  Expr lhs = em.mkExpr(kind::STRING_CONCAT, x, ab, y);

+  // String concatenation: abc.z

+  Expr rhs = em.mkExpr(kind::STRING_CONCAT, abc, z);

+  // x.ab.y = abc.z

+  Expr formula1 = em.mkExpr(kind::EQUAL, lhs, rhs);

+

+  // Length of y: |y|

+  Expr leny = em.mkExpr(kind::STRING_LENGTH, y);

+  // |y| >= 0

+  Expr formula2 = em.mkExpr(kind::GEQ, leny, em.mkConst(Rational(0)));

+

+  // Regular expression: (ab[c-e]*f)|g|h

+  Expr r = em.mkExpr(kind::REGEXP_UNION,

+    em.mkExpr(kind::REGEXP_CONCAT,

+      em.mkExpr(kind::STRING_TO_REGEXP, em.mkConst(String("ab"))),

+      em.mkExpr(kind::REGEXP_STAR,

+        em.mkExpr(kind::REGEXP_RANGE, em.mkConst(String("c")), em.mkConst(String("e")))),

+      em.mkExpr(kind::STRING_TO_REGEXP, em.mkConst(String("f")))),

+    em.mkExpr(kind::STRING_TO_REGEXP, em.mkConst(String("g"))),

+    em.mkExpr(kind::STRING_TO_REGEXP, em.mkConst(String("h"))));

+

+  // String variables

+  Expr s1 = em.mkVar("s1", string);

+  Expr s2 = em.mkVar("s2", string);

+  // String concatenation: s1.s2

+  Expr s = em.mkExpr(kind::STRING_CONCAT, s1, s2);

+

+  // s1.s2 in (ab[c-e]*f)|g|h

+  Expr formula3 = em.mkExpr(kind::STRING_IN_REGEXP, s, r);

+

+  // Make a query

+  Expr q = em.mkExpr(kind::AND,

+    formula1,

+    formula2,

+    formula3);

+

+  // check sat

+  Result result = smt.checkSat(q);

+  std::cout << "CVC4 reports: " << q << " is " << result << "." << std::endl;

+

+  if(result == Result::SAT) {

+    std::cout << "  x  = " << smt.getValue(x) << std::endl;

+    std::cout << "  s1.s2 = " << smt.getValue(s) << std::endl;

+  }

+}

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index b3b548450..2197cd648 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -215,7 +215,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
     }
 
     case kind::CONST_STRING: {
-      const String& s = n.getConst<String>();
+      const std::vector<unsigned int>& s = n.getConst<String>().getVec();
       out << '"';
       for(size_t i = 0; i < s.size(); ++i) {
         char c = String::convertUnsignedIntToChar(s[i]);
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 2347af3e6..9d83b91a8 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -22,7 +22,7 @@ namespace theory {
 namespace strings {
 
 RegExpOpr::RegExpOpr()
-  : d_card( 256 ),
+  : d_lastchar( '\xff' ),
   RMAXINT( LONG_MAX )
 {
   d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
@@ -240,6 +240,12 @@ int RegExpOpr::derivativeS( Node r, CVC4::String c, Node &retNode ) {
         retNode = d_emptySingleton;
         break;
       }
+      case kind::REGEXP_RANGE: {
+        CVC4::String a = r[0].getConst<String>();
+        CVC4::String b = r[1].getConst<String>();
+        retNode = (a <= c && c <= b) ? d_emptySingleton : d_emptyRegexp;
+        break;
+      }
       case kind::STRING_TO_REGEXP: {
         Node tmp = Rewriter::rewrite(r[0]);
         if(tmp.isConst()) {
@@ -450,6 +456,12 @@ Node RegExpOpr::derivativeSingle( Node r, CVC4::String c ) {
         retNode = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, d_emptyString );
         break;
       }
+      case kind::REGEXP_RANGE: {
+        CVC4::String a = r[0].getConst<String>();
+        CVC4::String b = r[1].getConst<String>();
+        retNode = (a <= c && c <= b) ? d_emptySingleton : d_emptyRegexp;
+        break;
+      }
       case kind::STRING_TO_REGEXP: {
         if(r[0].isConst()) {
           if(r[0] == d_emptyString) {
@@ -556,7 +568,7 @@ Node RegExpOpr::derivativeSingle( Node r, CVC4::String c ) {
       default: {
         //TODO: special sym: sigma, none, all
         Trace("strings-error") << "Unsupported term: " << mkString( r ) << " in derivative of RegExp." << std::endl;
-        Assert( false, "Unsupported Term" );
+        Unreachable();
         //return Node::null();
       }
     }
@@ -639,13 +651,13 @@ bool RegExpOpr::guessLength( Node r, int &co ) {
   }
 }
 
-void RegExpOpr::firstChars( Node r, std::set<unsigned> &pcset, SetNodes &pvset ) {
-  std::map< Node, std::pair< std::set<unsigned>, SetNodes > >::const_iterator itr = d_fset_cache.find(r);
+void RegExpOpr::firstChars( Node r, std::set<char> &pcset, SetNodes &pvset ) {
+  std::map< Node, std::pair< std::set<char>, SetNodes > >::const_iterator itr = d_fset_cache.find(r);
   if(itr != d_fset_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> cset;
+    std::set<char> cset;
     SetNodes vset;
     int k = r.getKind();
     switch( k ) {
@@ -653,7 +665,7 @@ void RegExpOpr::firstChars( Node r, std::set<unsigned> &pcset, SetNodes &pvset )
         break;
       }
       case kind::REGEXP_SIGMA: {
-        for(unsigned i=0; i<d_card; i++) {
+        for(char i='\0'; i<=d_lastchar; i++) {
           cset.insert(i);
         }
         break;
@@ -663,14 +675,14 @@ void RegExpOpr::firstChars( Node r, std::set<unsigned> &pcset, SetNodes &pvset )
         if(st.isConst()) {
           CVC4::String s = st.getConst< CVC4::String >();
           if(s.size() != 0) {
-            cset.insert(s[0]);
+            cset.insert(s.getFirstChar());
           }
         } else if(st.getKind() == kind::VARIABLE) {
           vset.insert( st );
         } else {
           if(st[0].isConst()) {
             CVC4::String s = st[0].getConst< CVC4::String >();
-            cset.insert(s[0]);
+            cset.insert(s.getFirstChar());
           } else {
             vset.insert( st[0] );
           }
@@ -707,23 +719,23 @@ void RegExpOpr::firstChars( Node r, std::set<unsigned> &pcset, SetNodes &pvset )
         break;
       }
       default: {
-        Trace("strings-regexp") << "Unsupported term: " << r << " in getCharSet." << std::endl;
-        Assert( false, "Unsupported Term" );
+        //Trace("regexp-error") << "Unsupported term: " << r << " in firstChars." << std::endl;
+        Unreachable();
       }
     }
     pcset.insert(cset.begin(), cset.end());
     pvset.insert(vset.begin(), vset.end());
-    std::pair< std::set<unsigned>, SetNodes > p(cset, vset);
+    std::pair< std::set<char>, SetNodes > p(cset, vset);
     d_fset_cache[r] = p;
 
     if(Trace.isOn("regexp-fset")) {
       Trace("regexp-fset") << "FSET(" << mkString(r) << ") = {";
-      for(std::set<unsigned>::const_iterator itr = cset.begin();
+      for(std::set<char>::const_iterator itr = cset.begin();
         itr != cset.end(); itr++) {
           if(itr != cset.begin()) {
             Trace("regexp-fset") << ",";
           }
-          Trace("regexp-fset") << CVC4::String::convertUnsignedIntToChar(*itr);
+          Trace("regexp-fset") << (*itr);
         }
       Trace("regexp-fset") << "}" << std::endl;
     }
@@ -1109,13 +1121,13 @@ void RegExpOpr::simplifyPRegExp( Node s, Node r, std::vector< Node > &new_nodes
   }
 }
 
-void RegExpOpr::getCharSet( Node r, std::set<unsigned> &pcset, SetNodes &pvset ) {
-  std::map< Node, std::pair< std::set<unsigned>, SetNodes > >::const_iterator itr = d_cset_cache.find(r);
+void RegExpOpr::getCharSet( Node r, std::set<char> &pcset, SetNodes &pvset ) {
+  std::map< Node, std::pair< std::set<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> cset;
+    std::set<char> cset;
     SetNodes vset;
     int k = r.getKind();
     switch( k ) {
@@ -1123,7 +1135,15 @@ void RegExpOpr::getCharSet( Node r, std::set<unsigned> &pcset, SetNodes &pvset )
         break;
       }
       case kind::REGEXP_SIGMA: {
-        for(unsigned i=0; i<d_card; i++) {
+        for(char i='\0'; i<=d_lastchar; i++) {
+          cset.insert(i);
+        }
+        break;
+      }
+      case kind::REGEXP_RANGE: {
+        char a = r[0].getConst<String>().getFirstChar();
+        char b = r[1].getConst<String>().getFirstChar();
+        for(char i=a; i<=b; i++) {
           cset.insert(i);
         }
         break;
@@ -1172,19 +1192,19 @@ void RegExpOpr::getCharSet( Node r, std::set<unsigned> &pcset, SetNodes &pvset )
         break;
       }
       default: {
-        Trace("strings-regexp") << "Unsupported term: " << r << " in getCharSet." << std::endl;
-        Assert( false, "Unsupported Term" );
+        //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>, SetNodes > p(cset, vset);
+    std::pair< std::set<char>, SetNodes > p(cset, vset);
     d_cset_cache[r] = p;
 
     Trace("regexp-cset") << "CSET( " << mkString(r) << " ) = { ";
-    for(std::set<unsigned>::const_iterator itr = cset.begin();
+    for(std::set<char>::const_iterator itr = cset.begin();
       itr != cset.end(); itr++) {
-        Trace("regexp-cset") << CVC4::String::convertUnsignedIntToChar(*itr) << ",";
+        Trace("regexp-cset") << (*itr) << ",";
       }
     Trace("regexp-cset") << " }" << std::endl;
   }
@@ -1251,11 +1271,6 @@ void RegExpOpr::convert2(unsigned cnt, Node n, Node &r1, Node &r2) {
       r2 = n;
     }
   } else if(n.getKind() == kind::REGEXP_CONCAT) {
-    //TODO
-    //convert2 x (r@(Seq l r1))
-    //   | contains x r1 = let (r2,r3) = convert2 x r1
-    //                     in (Seq l r2, r3)
-    //   | otherwise = (Empty, r)
     bool flag = true;
     std::vector<Node> vr1, vr2;
     for( unsigned i=0; i<n.getNumChildren(); i++ ) {
@@ -1291,11 +1306,12 @@ void RegExpOpr::convert2(unsigned cnt, Node n, Node &r1, Node &r2) {
     }
     r1 = NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vr1);
     r2 = NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vr2);
-  } else if(n.getKind() == kind::STRING_TO_REGEXP) {
+  } else if(n.getKind() == kind::STRING_TO_REGEXP || n.getKind() == kind::REGEXP_SIGMA || n.getKind() == kind::REGEXP_RANGE) {
       r1 = d_emptySingleton;
       r2 = n;
   } else {
     //is it possible?
+    Unreachable();
   }
 }
 
@@ -1318,7 +1334,7 @@ bool RegExpOpr::testNoRV(Node r) {
 }
 
 Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< PairNodes, Node > cache, unsigned cnt ) {
-  //(checkConstRegExp(r1) && checkConstRegExp(r2))
+  //Assert(checkConstRegExp(r1) && checkConstRegExp(r2));
   if(r1 > r2) {
     TNode tmpNode = r1;
     r1 = r2;
@@ -1358,8 +1374,8 @@ Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< PairNodes, Node >
       if(itrcache != cache.end()) {
         rNode = itrcache->second;
       } else {
-        std::vector< unsigned > cset;
-        std::set< unsigned > cset1, cset2;
+        std::vector< char > cset;
+        std::set< char > cset1, cset2;
         std::set< Node > vset1, vset2;
         firstChars(r1, cset1, vset1);
         firstChars(r2, cset2, vset2);
@@ -1379,20 +1395,20 @@ Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< PairNodes, Node >
         }
         if(Trace.isOn("regexp-int-debug")) {
           Trace("regexp-int-debug") << "Try CSET(" << cset.size() << ") = {";
-          for(std::vector<unsigned>::const_iterator itr = cset.begin();
+          for(std::vector<char>::const_iterator itr = cset.begin();
             itr != cset.end(); itr++) {
-            CVC4::String c( CVC4::String::convertUnsignedIntToChar(*itr) );
+            //CVC4::String c( *itr );
             if(itr != cset.begin()) {
               Trace("regexp-int-debug") << ", ";
             }
-            Trace("regexp-int-debug") << c;
+            Trace("regexp-int-debug") << ( *itr );
           }
           Trace("regexp-int-debug") << std::endl;
         }
         std::map< PairNodes, Node > cacheX;
-        for(std::vector<unsigned>::const_iterator itr = cset.begin();
+        for(std::vector<char>::const_iterator itr = cset.begin();
           itr != cset.end(); itr++) {
-          CVC4::String c( CVC4::String::convertUnsignedIntToChar(*itr) );
+          CVC4::String c( *itr );
           Trace("regexp-int-debug") << "Try character " << c << " ... " << std::endl;
           Node r1l = derivativeSingle(r1, c);
           Node r2l = derivativeSingle(r2, c);
@@ -1502,8 +1518,10 @@ Node RegExpOpr::intersect(Node r1, Node r2, bool &spflag) {
     Node rr1 = removeIntersection(r1);
     Node rr2 = removeIntersection(r2);
     std::map< PairNodes, Node > cache;
-    //std::map< PairNodes, Node > inter_cache;
-    return intersectInternal(rr1, rr2, cache, 1);
+    Trace("regexp-intersect") << "Start INTERSECTION(\n\t" << mkString(r1) << ",\n\t"<< mkString(r2) << ")" << std::endl;
+    Node retNode = intersectInternal(rr1, rr2, cache, 1);
+    Trace("regexp-intersect") << "End INTERSECTION(\n\t" << mkString(r1) << ",\n\t"<< mkString(r2) << ") =\n\t" << mkString(retNode) << std::endl;
+    return retNode;
   } else {
     spflag = true;
     return Node::null();
@@ -1525,12 +1543,12 @@ Node RegExpOpr::complement(Node r, int &ret) {
       //TODO: var to be extended
       ret = 0;
     } else {
-      std::set<unsigned> cset;
+      std::set<char> cset;
       SetNodes vset;
       firstChars(r, cset, vset);
       std::vector< Node > vec_nodes;
-      for(unsigned i=0; i<d_card; i++) {
-        CVC4::String c = CVC4::String::convertUnsignedIntToChar(i);
+      for(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()) {
@@ -1781,7 +1799,7 @@ void RegExpOpr::disjunctRegExp(Node r, std::vector<Node> &vec_or) {
 std::string RegExpOpr::niceChar(Node r) {
   if(r.isConst()) {
     std::string s = r.getConst<CVC4::String>().toString() ;
-    return s == "" ? "{E}" : ( s == " " ? "{ }" : s.size()>1? "("+s+")" : s );
+    return s == "" ? "{E}" : ( s == " " ? "{ }" : s );
   } else {
     std::string ss = "$" + r.toString();
     return ss;
diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h
index a522161fb..d170bd17a 100644
--- a/src/theory/strings/regexp_operation.h
+++ b/src/theory/strings/regexp_operation.h
@@ -39,7 +39,7 @@ class RegExpOpr {
   typedef std::pair< Node, Node > PairNodes;
 
 private:
-  unsigned d_card;
+  const char d_lastchar;
   Node d_emptyString;
   Node d_true;
   Node d_false;
@@ -61,8 +61,8 @@ private:
   std::map< PairNodeStr, std::pair< Node, int > > d_deriv_cache;
   std::map< Node, std::pair< Node, int > > d_compl_cache;
   std::map< Node, bool > d_cstre_cache;
-  std::map< Node, std::pair< std::set<unsigned>, std::set<Node> > > d_cset_cache;
-  std::map< Node, std::pair< std::set<unsigned>, std::set<Node> > > d_fset_cache;
+  std::map< Node, std::pair< std::set<char>, std::set<Node> > > d_cset_cache;
+  std::map< Node, std::pair< std::set<char>, std::set<Node> > > d_fset_cache;
   std::map< PairNodes, Node > d_inter_cache;
   std::map< Node, Node > d_rm_inter_cache;
   std::map< Node, bool > d_norv_cache;
@@ -75,18 +75,28 @@ private:
   Node mkAllExceptOne( char c );
   bool isPairNodesInSet(std::set< PairNodes > &s, Node n1, Node n2);
 
-  void getCharSet( Node r, std::set<unsigned> &pcset, SetNodes &pvset );
+  void getCharSet( Node r, std::set<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);
   bool testNoRV(Node r);
   Node intersectInternal( Node r1, Node r2, std::map< PairNodes, Node > cache, unsigned cnt );
   Node removeIntersection(Node r);
-  void firstChars( Node r, std::set<unsigned> &pcset, SetNodes &pvset );
+  void firstChars( Node r, std::set<char> &pcset, SetNodes &pvset );
 
   //TODO: for intersection
   bool follow( Node r, CVC4::String c, std::vector< 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();
 
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 384d4567b..f394047fa 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -472,12 +472,15 @@ void TheoryStrings::preRegisterTerm(TNode n) {
 void TheoryStrings::preRegisterTerm(TNode n) {
   if( d_registed_terms_cache.find(n) == d_registed_terms_cache.end() ) {
     switch( n.getKind() ) {
-      case kind::EQUAL:
+      case kind::EQUAL: {
         d_equalityEngine.addTriggerEquality(n);
         break;
-      case kind::STRING_IN_REGEXP:
+      }
+      case kind::STRING_IN_REGEXP: {
+        d_out->requirePhase(n, true);
         d_equalityEngine.addTriggerPredicate(n);
         break;
+      }
       //case kind::STRING_SUBSTR_TOTAL:
       default: {
         if( n.getType().isString() ) {
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 6fcbdfff3..56f6a2ef0 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -358,6 +358,16 @@ bool TheoryStringsRewriter::testConstStringInRegExp( CVC4::String &s, unsigned i
         return false;
       }
     }
+    case kind::REGEXP_RANGE: {
+      if(s.size() == index_start + 1) {
+        char a = r[0].getConst<String>().getFirstChar();
+        char b = r[1].getConst<String>().getFirstChar();
+        char c = s.getLastChar();
+        return (a <= c && c <= b);
+      } else {
+        return false;
+      }
+    }
     default: {
       Trace("strings-error") << "Unsupported term: " << r << " in testConstStringInRegExp." << std::endl;
       Assert( false, "Unsupported Term" );
diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp
index b1b454cfa..1c672d4b9 100644
--- a/src/util/regexp.cpp
+++ b/src/util/regexp.cpp
@@ -91,10 +91,10 @@ void String::toInternal(const std::string &s) {
   }
 }
 
-void String::getCharSet(std::set<unsigned int> &cset) const {
+void String::getCharSet(std::set<char> &cset) const {
   for(std::vector<unsigned int>::const_iterator itr = d_str.begin();
     itr != d_str.end(); itr++) {
-      cset.insert( *itr );
+      cset.insert( convertUnsignedIntToChar(*itr) );
     }
 }
 
@@ -114,33 +114,33 @@ std::string String::toString() const {
   std::string str;
   for(unsigned int i=0; i<d_str.size(); ++i) {
     char c = convertUnsignedIntToChar( d_str[i] );
-    if(isprint( c )) {
-    if(c == '\\') {
-      str += "\\\\";
-    } else if(c == '\"') {
-      str += "\\\"";
-    } else {
-      str += c;
-    }
+      if(isprint( c )) {
+      if(c == '\\') {
+        str += "\\\\";
+      } else if(c == '\"') {
+        str += "\\\"";
+      } else {
+        str += c;
+      }
     } else {
       std::string s;
       switch(c) {
-      case '\a': s = "\\a"; break;
-      case '\b': s = "\\b"; break;
-      case '\t': s = "\\t"; break;
-      case '\r': s = "\\r"; break;
-      case '\v': s = "\\v"; break;
-      case '\f': s = "\\f"; break;
-      case '\n': s = "\\n"; break;
-      case '\e': s = "\\e"; break;
-      default  : {
-        std::stringstream ss;
-        ss << std::setfill ('0') << std::setw(2) << std::hex << ((int)c);
-        std::string t = ss.str();
-        t = t.substr(t.size()-2, 2);
-        s = "\\x" + t;
-        //std::string s2 = static_cast<std::ostringstream*>( &(std::ostringstream() << (int)c) )->str();
-      }
+        case '\a': s = "\\a"; break;
+        case '\b': s = "\\b"; break;
+        case '\t': s = "\\t"; break;
+        case '\r': s = "\\r"; break;
+        case '\v': s = "\\v"; break;
+        case '\f': s = "\\f"; break;
+        case '\n': s = "\\n"; break;
+        case '\e': s = "\\e"; break;
+        default  : {
+          std::stringstream ss;
+          ss << std::setfill ('0') << std::setw(2) << std::hex << ((int)c);
+          std::string t = ss.str();
+          t = t.substr(t.size()-2, 2);
+          s = "\\x" + t;
+          //std::string s2 = static_cast<std::ostringstream*>( &(std::ostringstream() << (int)c) )->str();
+        }
       }
       str += s;
     }
diff --git a/src/util/regexp.h b/src/util/regexp.h
index 2b7bfa303..26d468a30 100644
--- a/src/util/regexp.h
+++ b/src/util/regexp.h
@@ -116,7 +116,7 @@ public:
     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];
+        if(d_str[i] != y.d_str[i]) return convertUnsignedIntToChar(d_str[i]) < convertUnsignedIntToChar(y.d_str[i]);
 
       return false;
     }
@@ -126,7 +126,7 @@ public:
     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];
+        if(d_str[i] != y.d_str[i]) return convertUnsignedIntToChar(d_str[i]) > convertUnsignedIntToChar(y.d_str[i]);
 
       return false;
     }
@@ -136,7 +136,7 @@ public:
     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];
+        if(d_str[i] != y.d_str[i]) return convertUnsignedIntToChar(d_str[i]) < convertUnsignedIntToChar(y.d_str[i]);
 
       return true;
     }
@@ -146,7 +146,7 @@ public:
     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];
+        if(d_str[i] != y.d_str[i]) return convertUnsignedIntToChar(d_str[i]) > convertUnsignedIntToChar(y.d_str[i]);
 
       return true;
     }
@@ -188,10 +188,10 @@ public:
     return ( d_str.size() == 0 );
   }
 
-  unsigned int operator[] (const std::size_t i) const {
+  /*char operator[] (const std::size_t i) const {
     assert( i < d_str.size() );
-    return d_str[i];
-  }
+    return convertUnsignedIntToChar(d_str[i]);
+  }*/
   /*
    * Convenience functions
    */
@@ -205,6 +205,11 @@ public:
     return convertUnsignedIntToChar( d_str[0] );
   }
 
+  char getLastChar() const {
+    assert(d_str.size() != 0);
+    return convertUnsignedIntToChar( d_str[d_str.size() - 1] );
+  }
+
   bool isRepeated() const {
   if(d_str.size() > 1) {
     unsigned int f = d_str[0];
@@ -307,7 +312,12 @@ public:
      return -1;
    }
   }
-  void getCharSet(std::set<unsigned int> &cset) const;
+
+  void getCharSet(std::set<char> &cset) const;
+
+  std::vector<unsigned int> getVec() const {
+    return d_str;
+  }
 };/* class String */
 
 namespace strings {