summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/strings/kinds25
-rw-r--r--src/theory/strings/regexp_operation.cpp79
-rw-r--r--src/theory/strings/theory_strings_rewriter.cpp75
-rw-r--r--src/theory/strings/theory_strings_type_rules.h19
-rw-r--r--src/util/Makefile.am3
-rw-r--r--src/util/regexp.h121
6 files changed, 187 insertions, 135 deletions
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index 7fbefe251..f8f8b9555 100644
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -78,11 +78,17 @@ operator REGEXP_PLUS 1 "regexp +"
operator REGEXP_OPT 1 "regexp ?"
operator REGEXP_RANGE 2 "regexp range"
-#constant REGEXP_EMPTY \
-# ::CVC4::RegExp \
-# ::CVC4::RegExpHashFunction \
-# "util/string.h" \
-# "a regexp contains nothing"
+constant REGEXP_EMPTY \
+ ::CVC4::RegExpEmpty \
+ ::CVC4::RegExpHashFunction \
+ "util/regexp.h" \
+ "a regexp contains nothing"
+
+constant REGEXP_SIGMA \
+ ::CVC4::RegExpSigma \
+ ::CVC4::RegExpHashFunction \
+ "util/regexp.h" \
+ "a regexp contains an arbitrary charactor"
#constant REGEXP_ALL \
# ::CVC4::RegExp \
@@ -90,12 +96,6 @@ operator REGEXP_RANGE 2 "regexp range"
# "util/string.h" \
# "a regexp contains all strings"
-#constant REGEXP_SIGMA \
-# ::CVC4::RegExp \
-# ::CVC4::RegExpHashFunction \
-# "util/string.h" \
-# "a regexp contains an arbitrary charactor"
-
typerule REGEXP_CONCAT ::CVC4::theory::strings::RegExpConcatTypeRule
typerule REGEXP_OR ::CVC4::theory::strings::RegExpOrTypeRule
typerule REGEXP_INTER ::CVC4::theory::strings::RegExpInterTypeRule
@@ -122,4 +122,7 @@ typerule STRING_STOI ::CVC4::theory::strings::StringStrToIntTypeRule
typerule STRING_IN_REGEXP ::CVC4::theory::strings::StringInRegExpTypeRule
+typerule REGEXP_EMPTY ::CVC4::theory::strings::EmptyRegExpTypeRule
+typerule REGEXP_SIGMA ::CVC4::theory::strings::SigmaRegExpTypeRule
+
endtheory
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 3b81ae4a5..1f4e86846 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -1,14 +1,25 @@
-/********************* */
+/********************* */
+
/*! \file regexp_operation.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-2013 New York University and The University of Iowa
+
** See the file COPYING in the top-level source directory for licensing
+
** information.\endverbatim
+
**
+
** \brief Regular Expresion Operations
**
** Regular Expresion Operations
@@ -661,6 +672,21 @@ void RegExpOpr::simplifyRegExp( Node s, Node r, std::vector< Node > &new_nodes )
} else {
int k = r.getKind();
switch( k ) {
+ case kind::REGEXP_EMPTY:
+ {
+ Node eq = NodeManager::currentNM()->mkConst( false );
+ new_nodes.push_back( eq );
+ d_simpl_cache[p] = eq;
+ }
+ break;
+ case kind::REGEXP_SIGMA:
+ {
+ Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
+ Node eq = one.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s));
+ new_nodes.push_back( eq );
+ d_simpl_cache[p] = eq;
+ }
+ break;
case kind::STRING_TO_REGEXP:
{
Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, s, r[0] );
@@ -671,18 +697,34 @@ void RegExpOpr::simplifyRegExp( Node s, Node r, std::vector< Node > &new_nodes )
case kind::REGEXP_CONCAT:
{
std::vector< Node > cc;
+ bool emptyflag = false;
+ Node ff = NodeManager::currentNM()->mkConst( false );
for(unsigned i=0; i<r.getNumChildren(); ++i) {
if(r[i].getKind() == kind::STRING_TO_REGEXP) {
cc.push_back( r[i][0] );
+ } if(r[i].getKind() == kind::STRING_TO_REGEXP) {
+ emptyflag = true;
+ break;
} else {
Node sk = NodeManager::currentNM()->mkSkolem( "rcon_$$", s.getType(), "created for regular expression concat" );
simplifyRegExp( sk, r[i], new_nodes );
+ if(new_nodes.size() != 0) {
+ if(new_nodes[new_nodes.size() - 1] == ff) {
+ emptyflag = true;
+ break;
+ }
+ }
cc.push_back( sk );
}
}
- Node cc_eq = s.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, cc) );
- new_nodes.push_back( cc_eq );
- d_simpl_cache[p] = cc_eq;
+ if(emptyflag) {
+ new_nodes.push_back( ff );
+ d_simpl_cache[p] = ff;
+ } else {
+ Node cc_eq = s.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, cc) );
+ new_nodes.push_back( cc_eq );
+ d_simpl_cache[p] = cc_eq;
+ }
}
break;
case kind::REGEXP_OR:
@@ -697,13 +739,28 @@ void RegExpOpr::simplifyRegExp( Node s, Node r, std::vector< Node > &new_nodes )
}
break;
case kind::REGEXP_INTER:
+ {
+ Node nfalse = NodeManager::currentNM()->mkConst( false );
for(unsigned i=0; i<r.getNumChildren(); ++i) {
simplifyRegExp( s, r[i], new_nodes );
+ if(new_nodes.size() != 0) {
+ if(new_nodes[new_nodes.size() - 1] == nfalse) {
+ break;
+ }
+ }
}
+ }
break;
case kind::REGEXP_STAR:
{
- Node eq = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, s, r );
+ Node eq;
+ if(r[0].getKind() == kind::REGEXP_EMPTY) {
+ eq = NodeManager::currentNM()->mkConst( false );
+ } else if(r[0].getKind() == kind::REGEXP_SIGMA) {
+ eq = NodeManager::currentNM()->mkConst( true );
+ } else {
+ eq = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, s, r );
+ }
new_nodes.push_back( eq );
d_simpl_cache[p] = eq;
}
@@ -729,10 +786,20 @@ std::string RegExpOpr::niceChar( Node r ) {
std::string RegExpOpr::mkString( Node r ) {
std::string retStr;
if(r.isNull()) {
- retStr = "EmptySet";
+ retStr = "Empty";
} else {
int k = r.getKind();
switch( k ) {
+ case kind::REGEXP_EMPTY:
+ {
+ retStr += "Empty";
+ }
+ break;
+ case kind::REGEXP_SIGMA:
+ {
+ retStr += "{W}";
+ }
+ break;
case kind::STRING_TO_REGEXP:
{
retStr += niceChar( r[0] );
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index c459d7d7e..c0d66ab22 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -28,9 +28,13 @@ Node TheoryStringsRewriter::rewriteConcatString( TNode node ) {
Node retNode = node;
std::vector<Node> node_vec;
Node preNode = Node::null();
+ bool emptyflag = false;
for(unsigned int i=0; i<node.getNumChildren(); ++i) {
Node tmpNode = node[i];
- if(node[i].getKind() == kind::STRING_CONCAT) {
+ if( tmpNode.getKind() == kind::REGEXP_EMPTY ) {
+ emptyflag = true;
+ break;
+ } else if(node[i].getKind() == kind::STRING_CONCAT) {
tmpNode = rewriteConcatString(node[i]);
if(tmpNode.getKind() == kind::STRING_CONCAT) {
unsigned int j=0;
@@ -71,14 +75,18 @@ Node TheoryStringsRewriter::rewriteConcatString( TNode node ) {
}
}
}
- if(preNode != Node::null()) {
- node_vec.push_back( preNode );
- }
- if(node_vec.size() > 1) {
- retNode = NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, node_vec);
- } else {
- retNode = node_vec[0];
- }
+ if(emptyflag) {
+ retNode = NodeManager::currentNM()->mkConst( kind::REGEXP_EMPTY );
+ } else {
+ if(preNode != Node::null()) {
+ node_vec.push_back( preNode );
+ }
+ if(node_vec.size() > 1) {
+ retNode = NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, node_vec);
+ } else {
+ retNode = node_vec[0];
+ }
+ }
Trace("strings-prerewrite") << "Strings::rewriteConcatString end " << retNode << std::endl;
return retNode;
}
@@ -89,6 +97,7 @@ Node TheoryStringsRewriter::prerewriteConcatRegExp( TNode node ) {
Node retNode = node;
std::vector<Node> node_vec;
Node preNode = Node::null();
+ bool emptyflag = false;
for(unsigned int i=0; i<node.getNumChildren(); ++i) {
Trace("strings-prerewrite") << "Strings::prerewriteConcatRegExp preNode: " << preNode << std::endl;
Node tmpNode = node[i];
@@ -123,7 +132,10 @@ Node TheoryStringsRewriter::prerewriteConcatRegExp( TNode node ) {
preNode = rewriteConcatString(
NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, preNode, tmpNode[0] ) );
}
- } else {
+ } else if( tmpNode.getKind() == kind::REGEXP_EMPTY ) {
+ emptyflag = true;
+ break;
+ } else {
if(!preNode.isNull()) {
if(preNode.getKind() == kind::CONST_STRING && preNode.getConst<String>().isEmptyString() ) {
preNode = Node::null();
@@ -135,14 +147,18 @@ Node TheoryStringsRewriter::prerewriteConcatRegExp( TNode node ) {
node_vec.push_back( tmpNode );
}
}
- if(!preNode.isNull()) {
- node_vec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, preNode ) );
- }
- if(node_vec.size() > 1) {
- retNode = NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, node_vec);
- } else {
- retNode = node_vec[0];
- }
+ if(emptyflag) {
+ retNode = NodeManager::currentNM()->mkConst( kind::REGEXP_EMPTY );
+ } else {
+ if(!preNode.isNull()) {
+ node_vec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, preNode ) );
+ }
+ if(node_vec.size() > 1) {
+ retNode = NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, node_vec);
+ } else {
+ retNode = node_vec[0];
+ }
+ }
Trace("strings-prerewrite") << "Strings::prerewriteConcatRegExp end " << retNode << std::endl;
return retNode;
}
@@ -161,11 +177,14 @@ Node TheoryStringsRewriter::prerewriteOrRegExp(TNode node) {
}
flag = false;
} else {
- node_vec.push_back( node[i] );
+ if(node[i].getKind() != kind::REGEXP_EMPTY) {
+ node_vec.push_back( node[i] );
+ }
}
}
if(flag) {
- retNode = NodeManager::currentNM()->mkNode(kind::REGEXP_OR, node_vec);
+ retNode = node_vec.size() == 0 ? NodeManager::currentNM()->mkConst( kind::REGEXP_EMPTY ) :
+ node_vec.size() == 1 ? node_vec[0] : NodeManager::currentNM()->mkNode(kind::REGEXP_OR, node_vec);
}
Trace("strings-prerewrite") << "Strings::prerewriteOrRegExp end " << retNode << std::endl;
return retNode;
@@ -267,6 +286,18 @@ bool TheoryStringsRewriter::testConstStringInRegExp( CVC4::String &s, unsigned i
return true;
}
}
+ case kind::REGEXP_EMPTY:
+ {
+ return false;
+ }
+ case kind::REGEXP_SIGMA:
+ {
+ if(s.size() == 1) {
+ return true;
+ } else {
+ return false;
+ }
+ }
default:
//TODO: special sym: sigma, none, all
Trace("strings-postrewrite") << "Unsupported term: " << r << " in testConstStringInRegExp." << std::endl;
@@ -282,7 +313,9 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) {
x = rewriteConcatString(node[0]);
}
- if( x.getKind() == kind::CONST_STRING && checkConstRegExp(node[1]) ) {
+ if(node[1].getKind() == kind::REGEXP_EMPTY) {
+ retNode = NodeManager::currentNM()->mkConst( false );
+ } else if( x.getKind() == kind::CONST_STRING && checkConstRegExp(node[1]) ) {
//test whether x in node[1]
CVC4::String s = x.getConst<String>();
retNode = NodeManager::currentNM()->mkConst( testConstStringInRegExp( s, 0, node[1] ) );
diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h
index 0c365e993..4ac4c26b4 100644
--- a/src/theory/strings/theory_strings_type_rules.h
+++ b/src/theory/strings/theory_strings_type_rules.h
@@ -425,6 +425,25 @@ public:
}
};
+class EmptyRegExpTypeRule {
+public:
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+
+ Assert(n.getKind() == kind::REGEXP_EMPTY);
+ return nodeManager->regexpType();
+ }
+};
+
+class SigmaRegExpTypeRule {
+public:
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+
+ Assert(n.getKind() == kind::REGEXP_SIGMA);
+ return nodeManager->regexpType();
+ }
+};
}/* CVC4::theory::strings namespace */
}/* CVC4::theory namespace */
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 0717df907..5c16db2a7 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -93,7 +93,8 @@ libutil_la_SOURCES = \
model.cpp \
sort_inference.h \
sort_inference.cpp \
- regexp.h
+ regexp.h \
+ regexp.cpp
libstatistics_la_SOURCES = \
statistics_registry.h \
diff --git a/src/util/regexp.h b/src/util/regexp.h
index 0cd92810b..dadc5996c 100644
--- a/src/util/regexp.h
+++ b/src/util/regexp.h
@@ -237,42 +237,7 @@ public:
/*
* Convenience functions
*/
- std::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;
- }
- } 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::string s2 = static_cast<std::ostringstream*>( &(std::ostringstream() << (int)c) )->str();
- if(s2.size() == 1) {
- s2 = "0" + s2;
- }
- s = "\\x" + s2;
- }
- }
- str += s;
- }
- }
- return str;
- }
+ std::string toString() const;
unsigned size() const {
return d_str.size();
@@ -389,86 +354,43 @@ struct CVC4_PUBLIC StringHashFunction {
}/* CVC4::strings namespace */
-inline std::ostream& operator <<(std::ostream& os, const String& s) CVC4_PUBLIC;
-inline std::ostream& operator <<(std::ostream& os, const String& s) {
- os << '"';
- std::string str = s.toString();
- for(std::string::iterator i = str.begin(); i != str.end(); ++i) {
- if(*i == '\\' || *i == '"') {
- os << '\\';
- } else if(!isprint(*i)) {
- os << "\\x" << std::ios::hex << std::setw(2) << (unsigned(*i) % 0x100);
- continue;
- }
- os << *i;
- }
- return os << '"';
-}
+std::ostream& operator <<(std::ostream& os, const String& s) CVC4_PUBLIC;
class CVC4_PUBLIC RegExp {
-
-private:
- std::string d_str;
-
+protected:
+ int d_type;
public:
- RegExp() {}
+ RegExp() : d_type(1) {}
- RegExp(const std::string s)
- : d_str(s) {}
+ RegExp(const int t) : d_type(t) {}
~RegExp() {}
- RegExp& operator =(const RegExp& y) {
- if(this != &y) d_str = y.d_str;
- return *this;
- }
-
bool operator ==(const RegExp& y) const {
- return d_str == y.d_str ;
+ return d_type == y.d_type ;
}
bool operator !=(const RegExp& y) const {
- return d_str != y.d_str ;
- }
-
- String concat (const RegExp& other) const {
- return String(d_str + other.d_str);
+ return d_type != y.d_type ;
}
bool operator <(const RegExp& y) const {
- return d_str < y.d_str;
+ return d_type < y.d_type;
}
bool operator >(const RegExp& y) const {
- return d_str > y.d_str ;
+ return d_type > y.d_type ;
}
bool operator <=(const RegExp& y) const {
- return d_str <= y.d_str;
+ return d_type <= y.d_type;
}
bool operator >=(const RegExp& y) const {
- return d_str >= y.d_str ;
- }
-
- /*
- * Convenience functions
- */
-
- size_t hash() const {
- unsigned int h = 1;
-
- for (size_t i = 0; i < d_str.length(); ++i) {
- h = (h << 5) + d_str[i];
- }
-
- return h;
- }
-
- std::string toString() const {
- return d_str;
+ return d_type >= y.d_type ;
}
+ int getType() const { return d_type; }
};/* class RegExp */
/**
@@ -476,14 +398,21 @@ public:
*/
struct CVC4_PUBLIC RegExpHashFunction {
inline size_t operator()(const RegExp& s) const {
- return s.hash();
+ return (size_t)s.getType();
}
};/* struct RegExpHashFunction */
-inline std::ostream& operator <<(std::ostream& os, const RegExp& s) CVC4_PUBLIC;
-inline std::ostream& operator <<(std::ostream& os, const RegExp& s) {
- return os << s.toString();
-}
+std::ostream& operator <<(std::ostream& os, const RegExp& s) CVC4_PUBLIC;
+
+class CVC4_PUBLIC RegExpEmpty : public RegExp {
+public:
+ RegExpEmpty() : RegExp(0) {}
+};
+
+class CVC4_PUBLIC RegExpSigma : public RegExp {
+public:
+ RegExpSigma() : RegExp(2) {}
+};
}/* CVC4 namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback