adds regular expression range

7 files changed, 76 insertions, 0 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 885a7c487..c7e088124 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1255,6 +1255,7 @@ builtinOp[CVC4::Kind& kind]
   | RESTAR_TOK     { $kind = CVC4::kind::REGEXP_STAR; }
   | REPLUS_TOK     { $kind = CVC4::kind::REGEXP_PLUS; }
   | REOPT_TOK      { $kind = CVC4::kind::REGEXP_OPT; }
+  | RERANGE_TOK      { $kind = CVC4::kind::REGEXP_RANGE; }
 
   // NOTE: Theory operators go here
   ;
@@ -1628,6 +1629,7 @@ REINTER_TOK : 're.itr';
 RESTAR_TOK : 're.*';
 REPLUS_TOK : 're.+';
 REOPT_TOK : 're.opt';
+RERANGE_TOK : 're.range';
 
 /**
  * A sequence of printable ASCII characters (except backslash) that starts
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index f4fbd7194..e325708c2 100644
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -70,6 +70,7 @@ operator REGEXP_INTER 2: "regexp intersection"
 operator REGEXP_STAR 1 "regexp *"
 operator REGEXP_PLUS 1 "regexp +"
 operator REGEXP_OPT 1 "regexp ?"
+operator REGEXP_RANGE 2 "regexp range"
 
 #constant REGEXP_EMPTY \
 #	::CVC4::RegExp \
@@ -95,6 +96,7 @@ typerule REGEXP_INTER ::CVC4::theory::strings::RegExpInterTypeRule
 typerule REGEXP_STAR ::CVC4::theory::strings::RegExpStarTypeRule
 typerule REGEXP_PLUS ::CVC4::theory::strings::RegExpPlusTypeRule
 typerule REGEXP_OPT ::CVC4::theory::strings::RegExpOptTypeRule
+typerule REGEXP_RANGE ::CVC4::theory::strings::RegExpRangeTypeRule
 
 typerule STRING_TO_REGEXP ::CVC4::theory::strings::StringToRegExpTypeRule
 
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 5ba67c25f..95e19c5aa 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -351,6 +351,19 @@ RewriteResponse TheoryStringsRewriter::preRewrite(TNode node) {
 		retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_OR,
 					NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst( ::CVC4::String("") ) ),
 					node[0]);
+	} else if(node.getKind() == kind::REGEXP_RANGE) {
+		std::vector< Node > vec_nodes;
+		char c = node[0].getConst<String>().getFirstChar();
+		char end = node[1].getConst<String>().getFirstChar();
+		for(; c<=end; ++c) {
+			Node n = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst( ::CVC4::String( c ) ) );
+			vec_nodes.push_back( n );
+		}
+		if(vec_nodes.size() == 1) {
+			retNode = vec_nodes[0];
+		} else {
+			retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_OR, vec_nodes );
+		}
 	}
 
     Trace("strings-prerewrite") << "Strings::preRewrite returning " << retNode << std::endl;
diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h
index 8af063284..080d6abf5 100644
--- a/src/theory/strings/theory_strings_type_rules.h
+++ b/src/theory/strings/theory_strings_type_rules.h
@@ -203,6 +203,40 @@ public:
   }
 };
 
+class RegExpRangeTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
+    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");
+	}
+
+    if( it != it_end ) {
+      throw TypeCheckingExceptionPrivate(n, "too many terms in regexp range");
+    }
+
+    return nodeManager->regexpType();
+  }
+};
+
 class StringToRegExpTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
diff --git a/src/util/regexp.h b/src/util/regexp.h
index 31a39e6f9..024bfd32e 100644
--- a/src/util/regexp.h
+++ b/src/util/regexp.h
@@ -57,6 +57,10 @@ public:
     }
   }
 
+  String(const char c) {
+    d_str.push_back( convertCharToUnsignedInt(c) );
+  }
+
   String(const std::vector<unsigned int> &s) : d_str(s) { }
 
   ~String() {}
@@ -151,6 +155,10 @@ public:
     return d_str.size();
   }
 
+  char getFirstChar() const {
+    return convertUnsignedIntToChar( d_str[0] );
+  }
+
   String substr(unsigned i) const {
     std::vector<unsigned int> ret_vec;
     std::vector<unsigned int>::const_iterator itr = d_str.begin() + i;
diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index ffbfb077d..cd3116eac 100644
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -27,6 +27,7 @@ TESTS =	\
   str005.smt2 \
   str006.smt2 \
   fmf001.smt2 \
+  fmf002.smt2 \
   model001.smt2 \
   substr001.smt2 \
   regexp001.smt2 \
diff --git a/test/regress/regress0/strings/fmf002.smt2 b/test/regress/regress0/strings/fmf002.smt2
new file mode 100644
index 000000000..14f50c710
--- /dev/null
+++ b/test/regress/regress0/strings/fmf002.smt2
@@ -0,0 +1,16 @@
+(set-logic QF_S)

+(set-option :fmf-strings true)

+(set-info :status sat)

+

+(declare-fun x () String)

+(declare-fun y () String)

+(declare-fun z () String)

+

+(assert (str.in.re x

+                (re.+ (re.range "a" "c"))

+				                ))

+

+(assert (= x (str.++ y "c" z "b")))

+(assert (> (str.len z) 1))

+

+(check-sat)