From: Tianyi Liang Date: Mon, 21 Oct 2013 02:25:57 +0000 (-0500) Subject: adds regular expression range X-Git-Tag: cvc5-1.0.0~7275^2~10 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=60aab6e5b7dde21603eb039f37921614d4424d59;p=cvc5.git adds regular expression range --- 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().getFirstChar(); + char end = node[1].getConst().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().size() != 1 ) { + throw TypeCheckingExceptionPrivate(n, "expecting a single constant string term in regexp range"); + } + ch[i] = (*it).getConst().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 &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 ret_vec; std::vector::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)