From: Tianyi Liang Date: Thu, 9 Jan 2014 22:23:59 +0000 (-0600) Subject: add constant replace, indexof X-Git-Tag: cvc5-1.0.0~7158 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=12dae128053342fef8af2f560fd98e1ab6a71cca;p=cvc5.git add constant replace, indexof --- diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 39329e424..497705cb6 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1254,6 +1254,8 @@ builtinOp[CVC4::Kind& kind] | STRSUB_TOK { $kind = CVC4::kind::STRING_SUBSTR; } | STRCTN_TOK { $kind = CVC4::kind::STRING_STRCTN; } | STRCAT_TOK { $kind = CVC4::kind::STRING_CHARAT; } + | STRIDOF_TOK { $kind = CVC4::kind::STRING_STRIDOF; } + | STRREPL_TOK { $kind = CVC4::kind::STRING_STRREPL; } | STRINRE_TOK { $kind = CVC4::kind::STRING_IN_REGEXP; } | STRTORE_TOK { $kind = CVC4::kind::STRING_TO_REGEXP; } | RECON_TOK { $kind = CVC4::kind::REGEXP_CONCAT; } @@ -1630,8 +1632,8 @@ STRLEN_TOK : 'str.len'; STRSUB_TOK : 'str.substr' ; STRCTN_TOK : 'str.contain' ; STRCAT_TOK : 'str.at' ; -//STRIDOF_TOK : 'str.indexof' ; -//STRREPL_TOK : 'str.repalce' ; +STRIDOF_TOK : 'str.indexof' ; +STRREPL_TOK : 'str.replace' ; STRINRE_TOK : 'str.in.re'; STRTORE_TOK : 'str.to.re'; RECON_TOK : 're.++'; diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index a421d6fa8..9e0897c00 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -15,7 +15,9 @@ operator STRING_IN_REGEXP 2 "membership" operator STRING_LENGTH 1 "string length" operator STRING_SUBSTR 3 "string substr" operator STRING_STRCTN 2 "string contains" -operator STRING_CHARAT 2 "string char at" +operator STRING_CHARAT 2 "string charat" +operator STRING_STRIDOF 3 "string indexof" +operator STRING_STRREPL 3 "string replace" #sort CHAR_TYPE \ # Cardinality::INTEGERS \ @@ -105,6 +107,8 @@ typerule STRING_LENGTH ::CVC4::theory::strings::StringLengthTypeRule typerule STRING_SUBSTR ::CVC4::theory::strings::StringSubstrTypeRule typerule STRING_STRCTN ::CVC4::theory::strings::StringContainTypeRule typerule STRING_CHARAT ::CVC4::theory::strings::StringCharAtTypeRule +typerule STRING_STRIDOF ::CVC4::theory::strings::StringIndexOfTypeRule +typerule STRING_STRREPL ::CVC4::theory::strings::StringReplaceTypeRule typerule STRING_IN_REGEXP ::CVC4::theory::strings::StringInRegExpTypeRule diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index ddc729e1e..c667aedf0 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -2036,33 +2036,18 @@ bool TheoryStrings::checkMemberships() { } } else { //TODO: negative membership - //Node r = Rewriter::rewrite( atom[1] ); - //r = d_regexp_opr.complement( r ); - //Trace("strings-regexp-test") << "Compl( " << d_regexp_opr.mkString( atom[1] ) << " ) is " << d_regexp_opr.mkString( r ) << std::endl; - //Trace("strings-regexp-test") << "Delta( " << d_regexp_opr.mkString( atom[1] ) << " ) is " << d_regexp_opr.delta( atom[1] ) << std::endl; - //Trace("strings-regexp-test") << "Delta( " << d_regexp_opr.mkString( r ) << " ) is " << d_regexp_opr.delta( r ) << std::endl; - //Trace("strings-regexp-test") << "Deriv( " << d_regexp_opr.mkString( r ) << ", c='b' ) is " << d_regexp_opr.mkString( d_regexp_opr.derivativeSingle( r, ::CVC4::String("b") ) ) << std::endl; - //Trace("strings-regexp-test") << "FHC( " << d_regexp_opr.mkString( r ) <<" ) is " << std::endl; - //d_regexp_opr.firstChar( r ); - //r = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, atom[0], r ); - /* - std::vector< Node > vec_r; - vec_r.push_back( r ); - - StringsPreprocess spp; - spp.simplify( vec_r ); - for( unsigned i=1; imkNode( kind::AND, assertion, x.eqNode( d_emptyString ) ); + Node conc = Node::null(); + sendLemma( ant, conc, "RegExp Empty Conflict" ); + addedLemma = true; + } else { + Trace("strings-regexp") << "RegEx is incomplete due to " << assertion << "." << std::endl; + is_unk = true; } - */ - Trace("strings-regexp") << "RegEx is incomplete due to " << assertion << "." << std::endl; - is_unk = true; } } if( addedLemma ){ diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 4d1643fbd..ca48d2fef 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -157,6 +157,20 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { } else { throw LogicException("string char at not supported in this release"); } + } else if( t.getKind() == kind::STRING_STRIDOF ){ + //if(options::stringExp()) { + //// d_cache[t] = t; + // retNode = t; + //} else { + throw LogicException("string indexof not supported in this release"); + //} + } else if( t.getKind() == kind::STRING_STRREPL ){ + //if(options::stringExp()) { + // d_cache[t] = t; + // retNode = t; + //} else { + throw LogicException("string replace not supported in this release"); + //} } else if( t.getNumChildren()>0 ){ std::vector< Node > cc; if (t.getMetaKind() == kind::metakind::PARAMETERIZED) { diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index af19095a0..f68deda54 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -371,6 +371,41 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { retNode = NodeManager::currentNM()->mkConst( false ); } } + } else if(node.getKind() == kind::STRING_STRIDOF) { + if( node[0].isConst() && node[1].isConst() && node[2].isConst() ) { + CVC4::String s = node[0].getConst(); + CVC4::String t = node[1].getConst(); + int i = node[2].getConst().getNumerator().toUnsignedInt(); + std::size_t ret = s.find(t, i); + if( ret != std::string::npos ) { + retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational((int) ret) ); + } else { + retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) ); + } + } + } else if(node.getKind() == kind::STRING_STRREPL) { + if(node[1] != node[2]) { + if(node[0].isConst() && node[1].isConst()) { + CVC4::String s = node[0].getConst(); + CVC4::String t = node[1].getConst(); + std::size_t p = s.find(t); + if( p != std::string::npos ) { + if(node[2].isConst()) { + CVC4::String r = node[2].getConst(); + CVC4::String ret = s.replace(t, r); + retNode = NodeManager::currentNM()->mkConst( ::CVC4::String(ret) ); + } else { + CVC4::String s1 = s.substr(0, (int)p); + CVC4::String s3 = s.substr((int)p + (int)t.size()); + Node ns1 = NodeManager::currentNM()->mkConst( ::CVC4::String(s1) ); + Node ns3 = NodeManager::currentNM()->mkConst( ::CVC4::String(s3) ); + retNode = NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, ns1, node[2], ns3 ); + } + } else { + retNode = node[0]; + } + } + } } else if(node.getKind() == kind::STRING_IN_REGEXP) { retNode = rewriteMembership(node); } diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h index 9d3197517..29fdf27a6 100644 --- a/src/theory/strings/theory_strings_type_rules.h +++ b/src/theory/strings/theory_strings_type_rules.h @@ -113,11 +113,55 @@ public: if( check ){ TypeNode t = n[0].getType(check); if (!t.isString()) { - throw TypeCheckingExceptionPrivate(n, "expecting a string term in string char at"); + throw TypeCheckingExceptionPrivate(n, "expecting a string term in string char at 0"); } t = n[1].getType(check); if (!t.isInteger()) { - throw TypeCheckingExceptionPrivate(n, "expecting an integer string term in string char at"); + throw TypeCheckingExceptionPrivate(n, "expecting an integer term in string char at 1"); + } + } + return nodeManager->stringType(); + } +}; + +class StringIndexOfTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + if( check ){ + TypeNode t = n[0].getType(check); + if (!t.isString()) { + throw TypeCheckingExceptionPrivate(n, "expecting a string term in string indexof 0"); + } + t = n[1].getType(check); + if (!t.isString()) { + throw TypeCheckingExceptionPrivate(n, "expecting a string term in string indexof 1"); + } + t = n[2].getType(check); + if (!t.isInteger()) { + throw TypeCheckingExceptionPrivate(n, "expecting an integer term in string indexof 2"); + } + } + return nodeManager->integerType(); + } +}; + +class StringReplaceTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + if( check ){ + TypeNode t = n[0].getType(check); + if (!t.isString()) { + throw TypeCheckingExceptionPrivate(n, "expecting a string term in string replace 0"); + } + t = n[1].getType(check); + if (!t.isString()) { + throw TypeCheckingExceptionPrivate(n, "expecting a string term in string replace 1"); + } + t = n[2].getType(check); + if (!t.isString()) { + throw TypeCheckingExceptionPrivate(n, "expecting a string term in string replace 2"); } } return nodeManager->stringType(); diff --git a/src/util/regexp.h b/src/util/regexp.h index 3f9df6aaf..f6c5b2b0f 100644 --- a/src/util/regexp.h +++ b/src/util/regexp.h @@ -183,11 +183,12 @@ public: return true; } - std::size_t find(const String &y) const { - if(y.d_str.size() == 0) return 0; + std::size_t find(const String &y, const int start = 0) const { + if(d_str.size() < y.d_str.size() + (std::size_t) start) return std::string::npos; + if(y.d_str.size() == 0) return (std::size_t) start; if(d_str.size() == 0) return std::string::npos; std::size_t ret = std::string::npos; - for(int i = 0; i <= (int) d_str.size() - (int) y.d_str.size(); i++) { + for(int i = start; i <= (int) d_str.size() - (int) y.d_str.size(); i++) { if(d_str[i] == y.d_str[0]) { std::size_t j=0; for(; j vec; + vec.insert(vec.begin(), d_str.begin(), d_str.begin() + ret); + vec.insert(vec.end(), t.d_str.begin(), t.d_str.end()); + vec.insert(vec.end(), d_str.begin() + ret + s.d_str.size(), d_str.end()); + return String(vec); + } else { + return *this; + } + } + String substr(unsigned i) const { std::vector ret_vec; std::vector::const_iterator itr = d_str.begin() + i;