| 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; }
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.++';
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 \
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
}
} 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; i<vec_r.size(); i++ ){
- if(vec_r[i].getKind() == kind::STRING_IN_REGEXP) {
- d_reg_exp_mem.push_back( vec_r[i] );
- } else if(vec_r[i].getKind() == kind::EQUAL) {
- d_equalityEngine.assertEquality(vec_r[i], true, vec_r[i]);
- } else {
- Assert(false);
- }
+ Node x = atom[0];
+ Node r = atom[1];
+ Assert( r.getKind()==kind::REGEXP_STAR );
+ if( areEqual( x, d_emptyString ) ) {
+ Node ant = NodeManager::currentNM()->mkNode( 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 ){
} 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) {
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<String>();
+ CVC4::String t = node[1].getConst<String>();
+ int i = node[2].getConst<Rational>().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<String>();
+ CVC4::String t = node[1].getConst<String>();
+ std::size_t p = s.find(t);
+ if( p != std::string::npos ) {
+ if(node[2].isConst()) {
+ CVC4::String r = node[2].getConst<String>();
+ 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);
}
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();
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<y.d_str.size(); j++) {
return ret;
}
+ String replace(const String &s, const String &t) const {
+ std::size_t ret = find(s);
+ if( ret != std::string::npos ) {
+ std::vector<unsigned int> 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<unsigned int> ret_vec;
std::vector<unsigned int>::const_iterator itr = d_str.begin() + i;
projects / cvc5.git / commitdiff