summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/printer/smt2/smt2_printer.cpp8
-rw-r--r--src/smt/smt_engine.cpp71
-rw-r--r--src/theory/strings/kinds4
-rw-r--r--src/theory/strings/theory_strings.cpp75
-rw-r--r--src/theory/strings/theory_strings.h2
-rw-r--r--src/theory/strings/theory_strings_preprocess.cpp44
-rw-r--r--src/theory/strings/theory_strings_preprocess.h1
-rw-r--r--src/theory/strings/theory_strings_rewriter.cpp16
-rw-r--r--test/regress/regress0/strings/substr001.smt22
9 files changed, 84 insertions, 139 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index cf3fac971..aae9938b7 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -278,12 +278,8 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
case kind::STRING_CONCAT: out << "str.++ "; break;
case kind::STRING_IN_REGEXP: out << "str.in.re "; break;
case kind::STRING_LENGTH: out << "str.len "; break;
- case kind::STRING_SUBSTR:
- case kind::STRING_SUBSTR_TOTAL:
- out << "str.substr "; break;
- case kind::STRING_CHARAT:
- case kind::STRING_CHARAT_TOTAL:
- out << "str.at "; break;
+ case kind::STRING_SUBSTR: out << "str.substr "; break;
+ case kind::STRING_CHARAT: out << "str.at "; break;
case kind::STRING_STRCTN: out << "str.contain "; break;
case kind::STRING_STRIDOF: out << "str.indexof "; break;
case kind::STRING_STRREPL: out << "str.replace "; break;
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index c77c05423..8754dc084 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -310,9 +310,7 @@ class SmtEnginePrivate : public NodeManagerListener {
* Function symbol used to implement uninterpreted undefined string
* semantics. Needed to deal with partial charat/substr function.
*/
- Node d_charAtUF;
- Node d_charAtUndef;
- Node d_substrUndef;
+ //Node d_substrUndef;
/**
* Function symbol used to implement uninterpreted division-by-zero
@@ -442,9 +440,6 @@ public:
d_fakeContext(),
d_abstractValueMap(&d_fakeContext),
d_abstractValues(),
- d_charAtUF(),
- d_charAtUndef(),
- d_substrUndef(),
d_divByZero(),
d_intDivByZero(),
d_modZero(),
@@ -1560,68 +1555,8 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
node = expandBVDivByZero(node);
break;
- /*case kind::STRING_CHARAT: {
- if(d_charAtUF.isNull()) {
- std::vector< TypeNode > argTypes;
- argTypes.push_back(NodeManager::currentNM()->stringType());
- argTypes.push_back(NodeManager::currentNM()->integerType());
- d_charAtUF = NodeManager::currentNM()->mkSkolem("charAt",
- NodeManager::currentNM()->mkFunctionType(
- argTypes,
- NodeManager::currentNM()->stringType()),
- "total charat",
- NodeManager::SKOLEM_EXACT_NAME);
- d_charAtUndef = NodeManager::currentNM()->mkSkolem("charAt_undef",
- NodeManager::currentNM()->mkFunctionType(
- argTypes,
- NodeManager::currentNM()->stringType()),
- "partial charat undef",
- NodeManager::SKOLEM_EXACT_NAME);
- if(!d_smt.d_logic.isTheoryEnabled(THEORY_UF)) {
- d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
- d_smt.d_logic.enableTheory(THEORY_UF);
- d_smt.d_logic.lock();
- }
- }
- Node str = n[0];
- Node num = n[1];
- //Assert(str.getType() == NodeManager::currentNM()->stringType(), "String Type Check 1");
- Node lenx = nm->mkNode(kind::STRING_LENGTH, str);
- Node cond = nm->mkNode(kind::GT, lenx, num);
- Node total = nm->mkNode(kind::STRING_CHARAT_TOTAL, str, num);
- Node undef = nm->mkNode(kind::APPLY_UF, d_charAtUndef, str, num);
- node = nm->mkNode(kind::ITE, cond, total, undef);
- node = nm->mkNode(kind::APPLY_UF, d_charAtUF, n[0], n[1]);
- }
- break;*/
- case kind::STRING_SUBSTR: {
- if(d_substrUndef.isNull()) {
- std::vector< TypeNode > argTypes;
- argTypes.push_back(NodeManager::currentNM()->stringType());
- argTypes.push_back(NodeManager::currentNM()->integerType());
- argTypes.push_back(NodeManager::currentNM()->integerType());
- d_substrUndef = NodeManager::currentNM()->mkSkolem("substr_undef",
- NodeManager::currentNM()->mkFunctionType(
- argTypes,
- NodeManager::currentNM()->stringType()),
- "partial substring undef",
- NodeManager::SKOLEM_EXACT_NAME);
- if(!d_smt.d_logic.isTheoryEnabled(THEORY_UF)) {
- d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
- d_smt.d_logic.enableTheory(THEORY_UF);
- d_smt.d_logic.lock();
- }
- }
- Node str = n[0];
- //Assert(str.getType() == NodeManager::currentNM()->stringType(), "String Type Check 2");
- Node lenx = nm->mkNode(kind::STRING_LENGTH, str);
- Node num = nm->mkNode(kind::PLUS, n[1], n[2]);
- Node cond = nm->mkNode(kind::GEQ, lenx, num);
- Node total = nm->mkNode(kind::STRING_SUBSTR_TOTAL, str, n[1], n[2]);
- Node undef = nm->mkNode(kind::APPLY_UF, d_substrUndef, str, n[1], n[2]);
- node = nm->mkNode(kind::ITE, cond, total, undef);
- }
- break;
+ //case kind::STRING_CHARAT:
+ //case kind::STRING_SUBSTR:
case kind::DIVISION: {
// partial function: division
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index b30bf8f36..e55891ec2 100644
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -14,9 +14,7 @@ operator STRING_CONCAT 2: "string concat"
operator STRING_IN_REGEXP 2 "membership"
operator STRING_LENGTH 1 "string length"
operator STRING_SUBSTR 3 "string substr (user symbol)"
-operator STRING_SUBSTR_TOTAL 3 "string substr (internal symbol)"
operator STRING_CHARAT 2 "string charat (user symbol)"
-operator STRING_CHARAT_TOTAL 2 "string charat (internal symbol)"
operator STRING_STRCTN 2 "string contains"
operator STRING_STRIDOF 3 "string indexof"
operator STRING_STRREPL 3 "string replace"
@@ -107,9 +105,7 @@ typerule STRING_TO_REGEXP ::CVC4::theory::strings::StringToRegExpTypeRule
typerule STRING_CONCAT ::CVC4::theory::strings::StringConcatTypeRule
typerule STRING_LENGTH ::CVC4::theory::strings::StringLengthTypeRule
typerule STRING_SUBSTR ::CVC4::theory::strings::StringSubstrTypeRule
-typerule STRING_SUBSTR_TOTAL ::CVC4::theory::strings::StringSubstrTypeRule
typerule STRING_CHARAT ::CVC4::theory::strings::StringCharAtTypeRule
-typerule STRING_CHARAT_TOTAL ::CVC4::theory::strings::StringCharAtTypeRule
typerule STRING_STRCTN ::CVC4::theory::strings::StringContainTypeRule
typerule STRING_STRIDOF ::CVC4::theory::strings::StringIndexOfTypeRule
typerule STRING_STRREPL ::CVC4::theory::strings::StringReplaceTypeRule
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 4deb0a9d9..0a8781abb 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -54,8 +54,8 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
d_equalityEngine.addFunctionKind(kind::STRING_LENGTH);
d_equalityEngine.addFunctionKind(kind::STRING_CONCAT);
d_equalityEngine.addFunctionKind(kind::STRING_STRCTN);
- d_equalityEngine.addFunctionKind(kind::STRING_CHARAT_TOTAL);
- //d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR_TOTAL);
+ d_equalityEngine.addFunctionKind(kind::STRING_CHARAT);
+ d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR);
d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
@@ -381,22 +381,36 @@ void TheoryStrings::preRegisterTerm(TNode n) {
case kind::STRING_IN_REGEXP:
//d_equalityEngine.addTriggerPredicate(n);
break;
+ case kind::CONST_STRING:
+ case kind::STRING_CONCAT:
+ case kind::STRING_CHARAT:
+ case kind::STRING_SUBSTR:
+ //do nothing
+ break;
default:
- if(n.getType().isString() && n.getKind() != kind::CONST_STRING && n.getKind()!=kind::STRING_CONCAT ) {
+ if(n.getType().isString() ) {
if( std::find( d_length_intro_vars.begin(), d_length_intro_vars.end(), n )==d_length_intro_vars.end() ) {
- if(n.getKind() == kind::STRING_CHARAT_TOTAL) {
+ /*
+ if(n.getKind() == kind::STRING_CHARAT) {
Node lenc_eq_one = d_one.eqNode(NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n));
Trace("strings-lemma") << "Strings::Lemma LEN(CHAR) = 1 : " << lenc_eq_one << std::endl;
d_out->lemma(lenc_eq_one);
+ } else if(n.getKind() == kind::STRING_SUBSTR) {
+ Node n_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n);
+ Node lenc_eq_n2 = n_len.eqNode(n[2]);
+ Trace("strings-lemma") << "Strings::Lemma LEN(SUBSTR) : " << lenc_eq_n2 << std::endl;
+ d_out->lemma(lenc_eq_n2);
} else {
+ */
Node n_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n);
Node n_len_eq_z = n_len.eqNode( d_zero );
+ n_len_eq_z = Rewriter::rewrite( n_len_eq_z );
Node n_len_geq_zero = NodeManager::currentNM()->mkNode( kind::OR, n_len_eq_z,
NodeManager::currentNM()->mkNode( kind::GT, n_len, d_zero) );
Trace("strings-lemma") << "Strings::Lemma LENGTH >= 0 : " << n_len_geq_zero << std::endl;
d_out->lemma(n_len_geq_zero);
d_out->requirePhase( n_len_eq_z, true );
- }
+ //}
}
// FMF
if( n.getKind() == kind::VARIABLE ) {//options::stringFMF() &&
@@ -466,8 +480,8 @@ void TheoryStrings::check(Effort e) {
bool addedLemma = false;
if( e == EFFORT_FULL && !d_conflict ) {
- addedLemma = checkLengths();
- Trace("strings-process") << "Done check (constant) lengths, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
+ addedLemma = checkSimple();
+ Trace("strings-process") << "Done simple checking, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
if( !addedLemma ) {
addedLemma = checkNormalForms();
Trace("strings-process") << "Done check normal forms, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
@@ -1693,7 +1707,7 @@ void TheoryStrings::getConcatVec( Node n, std::vector< Node >& c ) {
}
}
-bool TheoryStrings::checkLengths() {
+bool TheoryStrings::checkSimple() {
bool addedLemma = false;
eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
while( !eqcs_i.isFinished() ) {
@@ -1709,14 +1723,14 @@ bool TheoryStrings::checkLengths() {
//if n is concat, and
//if n has not instantiatied the concat..length axiom
//then, add lemma
- if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT ) { // || n.getKind() == kind::STRING_CONCAT ){
+ if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT || n.getKind()==kind::STRING_CHARAT || n.getKind()==kind::STRING_SUBSTR ) {
if( d_length_nodes.find(n)==d_length_nodes.end() ) {
if( d_length_inst.find(n)==d_length_inst.end() ) {
- Node nr = d_equalityEngine.getRepresentative( n );
+ //Node nr = d_equalityEngine.getRepresentative( n );
//if( d_length_nodes.find(nr)==d_length_nodes.end() ) {
d_length_inst[n] = true;
Trace("strings-debug") << "get n: " << n << endl;
- Node sk = NodeManager::currentNM()->mkSkolem( "lsym_$$", n.getType(), "created for concat lemma" );
+ Node sk = NodeManager::currentNM()->mkSkolem( "lsym_$$", n.getType(), "created for length" );
d_length_intro_vars.push_back( sk );
Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, n );
eq = Rewriter::rewrite(eq);
@@ -1731,10 +1745,41 @@ bool TheoryStrings::checkLengths() {
Node lni = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[i] );
node_vec.push_back(lni);
}
- lsum = NodeManager::currentNM()->mkNode( kind::PLUS, node_vec );
- } else {
+ lsum = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::PLUS, node_vec ) );
+ } else if( n.getKind() == kind::CONST_STRING ) {
//add lemma
lsum = NodeManager::currentNM()->mkConst( ::CVC4::Rational( n.getConst<String>().size() ) );
+ } else if( n.getKind() == kind::STRING_CHARAT ) {
+ lsum = d_one;
+ Node sk1 = NodeManager::currentNM()->mkSkolem( "ca1_$$", NodeManager::currentNM()->stringType(), "created for charat" );
+ Node sk3 = NodeManager::currentNM()->mkSkolem( "ca3_$$", NodeManager::currentNM()->stringType(), "created for charat" );
+ Node lenxgti = NodeManager::currentNM()->mkNode( kind::GT,
+ NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[0] ), n[1] );
+ Node t1greq0 = NodeManager::currentNM()->mkNode( kind::GEQ, n[1], d_zero);
+ Node x_eq_123 = n[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk, sk3 ) );
+ Node len_sk1_eq_i = n[1].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
+ Node lemma = NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i );
+ lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::IMPLIES, lenxgti, lemma ) );
+ Trace("strings-lemma") << "Strings::Lemma CHARAT : " << lemma << std::endl;
+ d_out->lemma(lemma);
+ } else if( n.getKind() == kind::STRING_SUBSTR ) {
+ lsum = n[2];
+ Node sk1 = NodeManager::currentNM()->mkSkolem( "st1_$$", NodeManager::currentNM()->stringType(), "created for substr" );
+ Node sk3 = NodeManager::currentNM()->mkSkolem( "st3_$$", NodeManager::currentNM()->stringType(), "created for substr" );
+ Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ,
+ NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[0] ),
+ NodeManager::currentNM()->mkNode( kind::PLUS, n[1], n[2] ) );
+ Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, n[1], d_zero);
+ Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, n[2], d_zero);
+ Node x_eq_123 = n[0].eqNode(NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk, sk3 ));
+ Node len_sk1_eq_i = NodeManager::currentNM()->mkNode( kind::EQUAL, n[1],
+ NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
+
+ Node lemma = NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i );
+ Node cond = NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 );
+ lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::IMPLIES, cond, lemma ) );
+ Trace("strings-lemma") << "Strings::Lemma SUBSTR : " << lemma << std::endl;
+ d_out->lemma(lemma);
}
Node ceq = NodeManager::currentNM()->mkNode( kind::EQUAL, skl, lsum );
ceq = Rewriter::rewrite(ceq);
@@ -2366,8 +2411,8 @@ bool TheoryStrings::checkNegContains() {
Node g1 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode( kind::GEQ, b1, d_zero ),
NodeManager::currentNM()->mkNode( kind::GEQ, NodeManager::currentNM()->mkNode( kind::MINUS, lenx, lens ), b1 ) ) );
Node b2 = NodeManager::currentNM()->mkBoundVar("bj", NodeManager::currentNM()->integerType());
- Node s2 = NodeManager::currentNM()->mkNode(kind::STRING_CHARAT_TOTAL, x, NodeManager::currentNM()->mkNode( kind::PLUS, b1, b2 ));
- Node s5 = NodeManager::currentNM()->mkNode(kind::STRING_CHARAT_TOTAL, s, b2);
+ Node s2 = NodeManager::currentNM()->mkNode(kind::STRING_CHARAT, x, NodeManager::currentNM()->mkNode( kind::PLUS, b1, b2 ));
+ Node s5 = NodeManager::currentNM()->mkNode(kind::STRING_CHARAT, s, b2);
Node s1 = NodeManager::currentNM()->mkBoundVar("s1", NodeManager::currentNM()->stringType());
Node s3 = NodeManager::currentNM()->mkBoundVar("s3", NodeManager::currentNM()->stringType());
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 1dae73360..d15a76aad 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -221,7 +221,7 @@ private:
int processSimpleDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj, unsigned& index, bool isRev );
bool unrollStar( Node atom );
- bool checkLengths();
+ bool checkSimple();
bool checkNormalForms();
bool checkLengthsEqc();
bool checkCardinality();
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 00d02e015..ae5303d9d 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -27,6 +27,9 @@ StringsPreprocess::StringsPreprocess() {
std::vector< TypeNode > argTypes;
argTypes.push_back(NodeManager::currentNM()->stringType());
argTypes.push_back(NodeManager::currentNM()->integerType());
+
+ //Constants
+ d_zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
}
void StringsPreprocess::simplifyRegExp( Node s, Node r, std::vector< Node > &ret, std::vector< Node > &nn ) {
@@ -134,7 +137,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
std::vector< Node > vec;
for(int i=0; i<len; i++) {
Node num = NodeManager::currentNM()->mkConst( ::CVC4::Rational(i) );
- Node sk = NodeManager::currentNM()->mkNode(kind::STRING_CHARAT_TOTAL, t[v_id][0], num);
+ Node sk = NodeManager::currentNM()->mkNode(kind::STRING_CHARAT, t[v_id][0], num);
vec.push_back(sk);
}
Node lem = t[v_id][0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, vec ) );
@@ -161,27 +164,6 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
// TODO
// return (t0 == t[0]) ? t : NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, t0, t[1] );
//}
- } else if( t.getKind() == kind::STRING_SUBSTR_TOTAL ){
- Node sk1 = NodeManager::currentNM()->mkSkolem( "st1_$$", NodeManager::currentNM()->stringType(), "created for substr" );
- Node sk2 = NodeManager::currentNM()->mkSkolem( "st2_$$", NodeManager::currentNM()->stringType(), "created for substr" );
- Node sk3 = NodeManager::currentNM()->mkSkolem( "st3_$$", NodeManager::currentNM()->stringType(), "created for substr" );
- Node x = simplify( t[0], new_nodes );
- Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ,
- NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, x ),
- NodeManager::currentNM()->mkNode( kind::PLUS, t[1], t[2] ) );
- Node x_eq_123 = NodeManager::currentNM()->mkNode( kind::EQUAL,
- NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2, sk3 ), x );
- Node len_sk1_eq_i = NodeManager::currentNM()->mkNode( kind::EQUAL, t[1],
- NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
- Node len_sk2_eq_j = NodeManager::currentNM()->mkNode( kind::EQUAL, t[2],
- NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2 ) );
-
- Node tp = NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i, len_sk2_eq_j );
- tp = NodeManager::currentNM()->mkNode( kind::IMPLIES, lenxgti, tp );
- new_nodes.push_back( tp );
-
- d_cache[t] = sk2;
- retNode = sk2;
} else if( t.getKind() == kind::STRING_STRIDOF ){
if(options::stringExp()) {
Node sk1 = NodeManager::currentNM()->mkSkolem( "io1_$$", t[0].getType(), "created for indexof" );
@@ -228,7 +210,6 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
}
} else if( t.getKind() == kind::STRING_STRREPL ){
if(options::stringExp()) {
- Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
Node x = t[0];
Node y = t[1];
Node z = t[2];
@@ -248,23 +229,6 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
} else {
throw LogicException("string replace not supported in this release");
}
- } else if(t.getKind() == kind::STRING_CHARAT) {
- Node sk2 = NodeManager::currentNM()->mkNode(kind::STRING_CHARAT_TOTAL, t[0], t[1]);
- Node sk1 = NodeManager::currentNM()->mkSkolem( "ca1_$$", NodeManager::currentNM()->stringType(), "created for charat" );
- Node sk3 = NodeManager::currentNM()->mkSkolem( "ca3_$$", NodeManager::currentNM()->stringType(), "created for charat" );
- Node x = simplify( t[0], new_nodes );
- Node lenxgti = NodeManager::currentNM()->mkNode( kind::GT,
- NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, x ), t[1] );
- Node x_eq_123 = x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2, sk3 ) );
- Node len_sk1_eq_i = t[1].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
- Node tp = NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i );
- tp = NodeManager::currentNM()->mkNode( kind::IMPLIES, lenxgti, tp );
- new_nodes.push_back( tp );
-
- d_cache[t] = sk2;
- retNode = sk2;
- } else if(t.getKind() == kind::STRING_SUBSTR) {
- InternalError("Substr should not be reached here.");
} else if( t.getNumChildren()>0 ) {
std::vector< Node > cc;
if (t.getMetaKind() == kind::metakind::PARAMETERIZED) {
diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h
index 99312ddc0..630c7595c 100644
--- a/src/theory/strings/theory_strings_preprocess.h
+++ b/src/theory/strings/theory_strings_preprocess.h
@@ -31,6 +31,7 @@ namespace strings {
class StringsPreprocess {
// NOTE: this class is NOT context-dependent
std::hash_map<TNode, Node, TNodeHashFunction> d_cache;
+ Node d_zero;
private:
bool checkStarPlus( Node t );
int checkFixLenVar( Node t );
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 86af2ffa8..ddfe1a39c 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -323,22 +323,28 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
} else if(node.getKind() == kind::STRING_LENGTH) {
if(node[0].isConst()) {
retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( node[0].getConst<String>().size() ) );
- } else if(node[0].getKind() == kind::STRING_CHARAT_TOTAL) {
+ } else if(node[0].getKind() == kind::STRING_CHARAT) {
retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( 1 ) );
+ } else if(node[0].getKind() == kind::STRING_SUBSTR) {
+ retNode = node[0][2];
} else if(node[0].getKind() == kind::STRING_CONCAT) {
Node tmpNode = rewriteConcatString(node[0]);
if(tmpNode.isConst()) {
retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( tmpNode.getConst<String>().size() ) );
- } else if(tmpNode.getKind() == kind::STRING_CHARAT_TOTAL) {
+ } else if(tmpNode.getKind() == kind::STRING_CHARAT) {
retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( 1 ) );
+ } else if(tmpNode.getKind() == kind::STRING_SUBSTR) {
+ retNode = tmpNode[2];
} else {
// it has to be string concat
std::vector<Node> node_vec;
for(unsigned int i=0; i<tmpNode.getNumChildren(); ++i) {
if(tmpNode[i].isConst()) {
node_vec.push_back( NodeManager::currentNM()->mkConst( ::CVC4::Rational( tmpNode[i].getConst<String>().size() ) ) );
- } else if(tmpNode[i].getKind() == kind::STRING_CHARAT_TOTAL) {
+ } else if(tmpNode[i].getKind() == kind::STRING_CHARAT) {
node_vec.push_back( NodeManager::currentNM()->mkConst( ::CVC4::Rational( 1 ) ) );
+ } else if(tmpNode[i].getKind() == kind::STRING_SUBSTR) {
+ node_vec.push_back( tmpNode[i][2] );
} else {
node_vec.push_back( NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, tmpNode[i]) );
}
@@ -346,7 +352,7 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
retNode = NodeManager::currentNM()->mkNode(kind::PLUS, node_vec);
}
}
- } else if(node.getKind() == kind::STRING_SUBSTR_TOTAL) {
+ } else if(node.getKind() == kind::STRING_SUBSTR) {
if( node[0].isConst() && node[1].isConst() && node[2].isConst() ) {
int i = node[1].getConst<Rational>().getNumerator().toUnsignedInt();
int j = node[2].getConst<Rational>().getNumerator().toUnsignedInt();
@@ -366,7 +372,7 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
retNode = NodeManager::currentNM()->mkConst( false );
}
}
- } else if(node.getKind() == kind::STRING_CHARAT || node.getKind() == kind::STRING_CHARAT_TOTAL) {
+ } else if(node.getKind() == kind::STRING_CHARAT) {
if( node[0].isConst() && node[1].isConst() ) {
int i = node[1].getConst<Rational>().getNumerator().toUnsignedInt();
if( node[0].getConst<String>().size() > (unsigned) i ) {
diff --git a/test/regress/regress0/strings/substr001.smt2 b/test/regress/regress0/strings/substr001.smt2
index 476b82699..bdfa33afb 100644
--- a/test/regress/regress0/strings/substr001.smt2
+++ b/test/regress/regress0/strings/substr001.smt2
@@ -7,6 +7,8 @@
(declare-fun i3 () Int)
(declare-fun i4 () Int)
+(assert (and (>= i1 0) (>= i2 0) (< (+ i1 i2) (str.len x))))
+(assert (and (>= i3 0) (>= i4 0) (< (+ i3 i4) (str.len x))))
(assert (= "efg" (str.substr x i1 i2) ) )
(assert (= "bef" (str.substr x i3 i4) ) )
(assert (> (str.len x) 5))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback