From: Tianyi Liang Date: Wed, 26 Feb 2014 17:29:38 +0000 (-0600) Subject: for merging X-Git-Tag: cvc5-1.0.0~7060^2 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ce0f9b3e72394ef726d3e4270241f007b6f7381a;p=cvc5.git for merging --- 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; imkSkolem( "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; imkNode( 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_vec; Node preNode = Node::null(); + bool emptyflag = false; for(unsigned int i=0; i 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_vec; Node preNode = Node::null(); + bool emptyflag = false; for(unsigned int i=0; imkNode( 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().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(); 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 46417cdb6..94447fd86 100644 --- a/src/util/regexp.h +++ b/src/util/regexp.h @@ -236,42 +236,7 @@ public: /* * Convenience functions */ - std::string toString() const { - std::string str; - for(unsigned int i=0; i( &(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(); @@ -388,75 +353,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) { - return os << "\"" << s.toString() << "\""; -} +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 */ /** @@ -464,14 +397,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 */