adds regular expression range

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 885a7c4875e4605585e27a4fc88b6073e3f4570b..c7e088124557cb00d3e1098abb365fe04ae02eaf 100644 (file)
--- 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 f4fbd7194be9bd91d4a44e84a6df4a63003c3ce8..e325708c2cc34d7a522fdf2bf420ade5b2027321 100644 (file)
--- 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 5ba67c25f434c29db5f95b4e7184b313c75bb2af..95e19c5aa933025da7720c9b77c4c4d131683159 100644 (file)
--- 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 8af06328468ee6b09a3b39b9eaa6342fbf51b14b..080d6abf565021089ffb7c8882523a16b3e5dd5e 100644 (file)
--- 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 31a39e6f9f4e25616322398250d6dfaa03d6f988..024bfd32ec6ad0bd5aec730b7a8a915c3e86e137 100644 (file)
--- 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 ffbfb077d472f4100e282ac5461c57b42746ed28..cd3116eacd1237b1ff92d3047d44153f07ed4a89 100644 (file)
--- 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 (file)
index 0000000..14f50c7
--- /dev/null
+++ b/test/regress/regress0/strings/fmf002.smt2
@@ -0,0 +1,16 @@
+(set-logic QF_S)\r
+(set-option :fmf-strings true)\r
+(set-info :status sat)\r
+\r
+(declare-fun x () String)\r
+(declare-fun y () String)\r
+(declare-fun z () String)\r
+\r
+(assert (str.in.re x\r
+                (re.+ (re.range "a" "c"))\r
+                                               ))\r
+\r
+(assert (= x (str.++ y "c" z "b")))\r
+(assert (> (str.len z) 1))\r
+\r
+(check-sat)\r