summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/printer/smt2/smt2_printer.cpp1
-rw-r--r--src/smt/smt_engine.cpp22
-rw-r--r--src/theory/strings/theory_strings.cpp325
-rw-r--r--src/theory/strings/theory_strings.h1
-rw-r--r--src/theory/strings/theory_strings_preprocess.cpp44
-rw-r--r--src/theory/strings/theory_strings_rewriter.cpp2
-rw-r--r--src/theory/theory_engine.cpp2
-rw-r--r--test/regress/regress0/strings/at001.smt24
8 files changed, 272 insertions, 129 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 0ca7f323b..cf3fac971 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -124,6 +124,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
case BOOLEAN_TYPE: out << "Bool"; break;
case REAL_TYPE: out << "Real"; break;
case INTEGER_TYPE: out << "Int"; break;
+ case STRING_TYPE: out << "String"; break;
default:
// fall back on whatever operator<< does on underlying type; we
// might luck out and be SMT-LIB v2 compliant
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 761348890..406db286f 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -309,6 +309,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;
@@ -440,6 +441,7 @@ public:
d_fakeContext(),
d_abstractValueMap(&d_fakeContext),
d_abstractValues(),
+ d_charAtUF(),
d_charAtUndef(),
d_substrUndef(),
d_divByZero(),
@@ -1534,11 +1536,17 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
node = expandBVDivByZero(node);
break;
- case kind::STRING_CHARAT: {
- if(d_charAtUndef.isNull()) {
+ /*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,
@@ -1551,14 +1559,17 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
d_smt.d_logic.lock();
}
}
- TNode str = n[0], num = n[1];
+ 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;
+ break;*/
case kind::STRING_SUBSTR: {
if(d_substrUndef.isNull()) {
std::vector< TypeNode > argTypes;
@@ -1577,7 +1588,8 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
d_smt.d_logic.lock();
}
}
- TNode str = n[0];
+ 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);
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 4b479e348..ac50ed21d 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -41,6 +41,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
d_infer(c),
d_infer_exp(c),
d_nf_pairs(c),
+ d_length_nodes(c),
//d_var_lmin( c ),
//d_var_lmax( c ),
d_str_pos_ctn( c ),
@@ -53,6 +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_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
@@ -104,11 +107,18 @@ Node TheoryStrings::getLengthTerm( Node t ) {
//typically shouldnt be necessary
length_term = t;
}
+ Debug("strings") << "TheoryStrings::getLengthTerm" << t << std::endl;
return length_term;
}
Node TheoryStrings::getLength( Node t ) {
- return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, getLengthTerm( t ) ) );
+ Node retNode;
+ if(t.isConst()) {
+ retNode = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t );
+ } else {
+ retNode = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, getLengthTerm( t ) );
+ }
+ return Rewriter::rewrite( retNode );
}
void TheoryStrings::setMasterEqualityEngine(eq::EqualityEngine* eq) {
@@ -370,8 +380,8 @@ void TheoryStrings::preRegisterTerm(TNode n) {
//d_equalityEngine.addTriggerPredicate(n);
break;
default:
- if(n.getKind() == kind::VARIABLE || n.getKind()==kind::SKOLEM) {
- if( std::find( d_length_intro_vars.begin(), d_length_intro_vars.end(), n )==d_length_intro_vars.end() ){
+ if(n.getType().isString() && (n.getKind() == kind::VARIABLE || n.getKind()==kind::SKOLEM)) {
+ if( std::find( d_length_intro_vars.begin(), d_length_intro_vars.end(), n )==d_length_intro_vars.end() ) {
Node n_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n);
Node n_len_eq_z = n_len.eqNode( d_zero );
Node n_len_geq_zero = NodeManager::currentNM()->mkNode( kind::OR, n_len_eq_z,
@@ -1343,6 +1353,12 @@ bool TheoryStrings::normalizeDisequality( Node ni, Node nj ) {
Node sk1 = NodeManager::currentNM()->mkSkolem( "x_dsplit_$$", ni.getType(), "created for disequality normalization" );
Node sk2 = NodeManager::currentNM()->mkSkolem( "y_dsplit_$$", ni.getType(), "created for disequality normalization" );
Node sk3 = NodeManager::currentNM()->mkSkolem( "z_dsplit_$$", ni.getType(), "created for disequality normalization" );
+ Node nemp = sk1.eqNode(d_emptyString).negate();
+ conc.push_back(nemp);
+ nemp = sk2.eqNode(d_emptyString).negate();
+ conc.push_back(nemp);
+ nemp = sk3.eqNode(d_emptyString).negate();
+ conc.push_back(nemp);
Node lsk1 = getLength( sk1 );
conc.push_back( lsk1.eqNode( li ) );
Node lsk2 = getLength( sk2 );
@@ -1350,17 +1366,17 @@ bool TheoryStrings::normalizeDisequality( Node ni, Node nj ) {
conc.push_back( NodeManager::currentNM()->mkNode( kind::OR,
j.eqNode( mkConcat( sk1, sk3 ) ), i.eqNode( mkConcat( sk2, sk3 ) ) ) );
- sendLemma( mkExplain( antec, antec_new_lits ), NodeManager::currentNM()->mkNode( kind::AND, conc ), "Disequality Normalize" );
+ sendLemma( mkExplain( antec, antec_new_lits ), NodeManager::currentNM()->mkNode( kind::AND, conc ), "D-DISL-Split" );
return true;
}else if( areEqual( li, lj ) ){
if( areDisequal( i, j ) ){
Trace("strings-solve") << "Case 1 : found equal length disequal sub strings " << i << " " << j << std::endl;
- //we are done
+ //we are done: D-Remove
return false;
} else {
//splitting on demand : try to make them disequal
Node eq = i.eqNode( j );
- sendSplit( i, j, "Disequality : disequal terms" );
+ sendSplit( i, j, "D-EQL-Split" );
eq = Rewriter::rewrite( eq );
d_pending_req_phase[ eq ] = false;
return true;
@@ -1368,7 +1384,7 @@ bool TheoryStrings::normalizeDisequality( Node ni, Node nj ) {
}else{
//splitting on demand : try to make lengths equal
Node eq = li.eqNode( lj );
- sendSplit( li, lj, "Disequality : equal length" );
+ sendSplit( li, lj, "D-UNK-Split" );
eq = Rewriter::rewrite( eq );
d_pending_req_phase[ eq ] = true;
return true;
@@ -1429,7 +1445,7 @@ bool TheoryStrings::isNormalFormPair2( Node n1, Node n2 ) {
}
void TheoryStrings::sendLemma( Node ant, Node conc, const char * c ) {
- if( conc.isNull() ){
+ if( conc.isNull() || conc == d_false ){
d_out->conflict(ant);
Trace("strings-conflict") << "Strings::Conflict : " << ant << std::endl;
d_conflict = true;
@@ -1547,34 +1563,40 @@ bool TheoryStrings::checkLengths() {
//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( d_length_inst.find(n)==d_length_inst.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" );
- d_length_intro_vars.push_back( sk );
- Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, n );
- eq = Rewriter::rewrite(eq);
- Trace("strings-lemma") << "Strings::Lemma LENGTH term : " << eq << std::endl;
- d_out->lemma(eq);
- Node skl = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk );
- Node lsum;
- if( n.getKind() == kind::STRING_CONCAT ) {
- //add lemma
- std::vector<Node> node_vec;
- for( unsigned i=0; i<n.getNumChildren(); i++ ) {
- Node lni = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[i] );
- node_vec.push_back(lni);
+ 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 );
+ 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" );
+ d_length_intro_vars.push_back( sk );
+ Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, n );
+ eq = Rewriter::rewrite(eq);
+ Trace("strings-lemma") << "Strings::Lemma LENGTH term : " << eq << std::endl;
+ d_out->lemma(eq);
+ Node skl = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk );
+ Node lsum;
+ if( n.getKind() == kind::STRING_CONCAT ) {
+ //add lemma
+ std::vector<Node> node_vec;
+ for( unsigned i=0; i<n.getNumChildren(); i++ ) {
+ Node lni = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[i] );
+ node_vec.push_back(lni);
+ }
+ lsum = NodeManager::currentNM()->mkNode( kind::PLUS, node_vec );
+ } else {
+ //add lemma
+ lsum = NodeManager::currentNM()->mkConst( ::CVC4::Rational( n.getConst<String>().size() ) );
+ }
+ Node ceq = NodeManager::currentNM()->mkNode( kind::EQUAL, skl, lsum );
+ ceq = Rewriter::rewrite(ceq);
+ Trace("strings-lemma") << "Strings::Lemma LENGTH : " << ceq << std::endl;
+ d_out->lemma(ceq);
+ addedLemma = true;
}
- lsum = NodeManager::currentNM()->mkNode( kind::PLUS, node_vec );
- } else {
- //add lemma
- lsum = NodeManager::currentNM()->mkConst( ::CVC4::Rational( n.getConst<String>().size() ) );
}
- Node ceq = NodeManager::currentNM()->mkNode( kind::EQUAL, skl, lsum );
- ceq = Rewriter::rewrite(ceq);
- Trace("strings-lemma") << "Strings::Lemma LENGTH : " << ceq << std::endl;
- d_out->lemma(ceq);
- addedLemma = true;
+ d_length_nodes[n] = true;
}
}
++eqc_i;
@@ -2114,7 +2136,7 @@ bool TheoryStrings::checkMemberships() {
bool TheoryStrings::checkContains() {
bool addedLemma = checkPosContains();
Trace("strings-process") << "Done check positive contain constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
- if(!addedLemma) {
+ if(!d_conflict && !addedLemma) {
addedLemma = checkNegContains();
Trace("strings-process") << "Done check positive contain constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
}
@@ -2124,24 +2146,26 @@ bool TheoryStrings::checkContains() {
bool TheoryStrings::checkPosContains() {
bool addedLemma = false;
for( unsigned i=0; i<d_str_pos_ctn.size(); i++ ) {
- Node atom = d_str_pos_ctn[i];
- Trace("strings-ctn") << "We have positive contain assertion : " << atom << std::endl;
- Assert( atom.getKind()==kind::STRING_STRCTN );
- Node x = atom[0];
- Node s = atom[1];
- if( !areEqual( s, d_emptyString ) && !areEqual( s, x ) ) {
- if(d_str_pos_ctn_rewritten.find(atom) == d_str_pos_ctn_rewritten.end()) {
- Node sk1 = NodeManager::currentNM()->mkSkolem( "sc1_$$", s.getType(), "created for contain" );
- Node sk2 = NodeManager::currentNM()->mkSkolem( "sc2_$$", s.getType(), "created for contain" );
- Node eq = Rewriter::rewrite( x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, s, sk2 ) ) );
- sendLemma( atom, eq, "POS-INC" );
- addedLemma = true;
- d_str_pos_ctn_rewritten[ atom ] = true;
+ if( !d_conflict ){
+ Node atom = d_str_pos_ctn[i];
+ Trace("strings-ctn") << "We have positive contain assertion : " << atom << std::endl;
+ Assert( atom.getKind()==kind::STRING_STRCTN );
+ Node x = atom[0];
+ Node s = atom[1];
+ if( !areEqual( s, d_emptyString ) && !areEqual( s, x ) ) {
+ if(d_str_pos_ctn_rewritten.find(atom) == d_str_pos_ctn_rewritten.end()) {
+ Node sk1 = NodeManager::currentNM()->mkSkolem( "sc1_$$", s.getType(), "created for contain" );
+ Node sk2 = NodeManager::currentNM()->mkSkolem( "sc2_$$", s.getType(), "created for contain" );
+ Node eq = Rewriter::rewrite( x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, s, sk2 ) ) );
+ sendLemma( atom, eq, "POS-INC" );
+ addedLemma = true;
+ d_str_pos_ctn_rewritten[ atom ] = true;
+ } else {
+ Trace("strings-ctn") << "... is already rewritten." << std::endl;
+ }
} else {
- Trace("strings-ctn") << "... is already rewritten." << std::endl;
+ Trace("strings-ctn") << "... is satisfied." << std::endl;
}
- } else {
- Trace("strings-ctn") << "... is satisfied." << std::endl;
}
}
if( addedLemma ){
@@ -2156,70 +2180,147 @@ bool TheoryStrings::checkNegContains() {
bool is_unk = false;
bool addedLemma = false;
for( unsigned i=0; i<d_str_neg_ctn.size(); i++ ){
- Node atom = d_str_neg_ctn[i];
- Trace("strings-ctn") << "We have nagetive contain assertion : (not " << atom << " )" << std::endl;
- if( areEqual( atom[1], d_emptyString ) ) {
- Node ant = NodeManager::currentNM()->mkNode( kind::AND, atom.negate(), atom[1].eqNode( d_emptyString ) );
- Node conc = Node::null();
- sendLemma( ant, conc, "NEG-CTN Conflict 1" );
- addedLemma = true;
- } else if( areEqual( atom[1], atom[0] ) ) {
- Node ant = NodeManager::currentNM()->mkNode( kind::AND, atom.negate(), atom[1].eqNode( atom[0] ) );
- Node conc = Node::null();
- sendLemma( ant, conc, "NEG-CTN Conflict 2" );
- addedLemma = true;
- } else {
- if(options::stringExp()) {
- Node x = atom[0];
- Node s = atom[1];
- Node lenx = getLength(x);
- Node lens = getLength(s);
- if(areEqual(lenx, lens)) {
- if(d_str_ctn_eqlen.find(atom) == d_str_ctn_eqlen.end()) {
- Node eq = lenx.eqNode(lens);
- Node antc = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, atom.negate(), eq ) );
- Node xneqs = x.eqNode(s).negate();
- d_str_ctn_eqlen[ atom ] = true;
- sendLemma( antc, xneqs, "NEG-CTN-EQL" );
+ if( !d_conflict ){
+ Node atom = d_str_neg_ctn[i];
+ Trace("strings-ctn") << "We have nagetive contain assertion : (not " << atom << " )" << std::endl;
+ if( areEqual( atom[1], d_emptyString ) ) {
+ Node ant = NodeManager::currentNM()->mkNode( kind::AND, atom.negate(), atom[1].eqNode( d_emptyString ) );
+ Node conc = Node::null();
+ sendLemma( ant, conc, "NEG-CTN Conflict 1" );
+ addedLemma = true;
+ } else if( areEqual( atom[1], atom[0] ) ) {
+ Node ant = NodeManager::currentNM()->mkNode( kind::AND, atom.negate(), atom[1].eqNode( atom[0] ) );
+ Node conc = Node::null();
+ sendLemma( ant, conc, "NEG-CTN Conflict 2" );
+ addedLemma = true;
+ } else {
+ if(options::stringExp()) {
+ Node x = atom[0];
+ Node s = atom[1];
+ Node lenx = getLength(x);
+ Node lens = getLength(s);
+ if(areEqual(lenx, lens)) {
+ if(d_str_ctn_eqlen.find(atom) == d_str_ctn_eqlen.end()) {
+ Node eq = lenx.eqNode(lens);
+ Node antc = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, atom.negate(), eq ) );
+ Node xneqs = x.eqNode(s).negate();
+ d_str_ctn_eqlen[ atom ] = true;
+ sendLemma( antc, xneqs, "NEG-CTN-EQL" );
+ addedLemma = true;
+ }
+ } else if(!areDisequal(lenx, lens)) {
+ sendSplit(lenx, lens, "NEG-CTN-SP");
addedLemma = true;
+ } else {
+ if(d_str_neg_ctn_rewritten.find(atom) == d_str_neg_ctn_rewritten.end()) {
+ /*std::vector< TypeNode > argTypes;
+ argTypes.push_back(NodeManager::currentNM()->stringType());
+ argTypes.push_back(NodeManager::currentNM()->integerType());
+ Node d_charAtUF = NodeManager::currentNM()->mkSkolem("charAt",
+ NodeManager::currentNM()->mkFunctionType(
+ argTypes,
+ NodeManager::currentNM()->stringType()),
+ "total charat",
+ NodeManager::SKOLEM_EXACT_NAME);*/
+ /*
+ Node e1 = NodeManager::currentNM()->mkSkolem( "nc1_$$", s.getType(), "created for contain" );
+ Node e2 = NodeManager::currentNM()->mkSkolem( "nc2_$$", s.getType(), "created for contain" );
+ Node z = NodeManager::currentNM()->mkSkolem( "ncz_$$", s.getType(), "created for contain" );
+ Node w = NodeManager::currentNM()->mkSkolem( "ncw_$$", s.getType(), "created for contain" );
+ std::vector< Node > vec_conc;
+ Node cc = Rewriter::rewrite( x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, e1, z ) ) );
+ vec_conc.push_back(cc);
+ cc = Rewriter::rewrite( x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, w, e2 ) ) );
+ vec_conc.push_back(cc);
+ cc = Rewriter::rewrite( z.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, s, e2 ) ).negate() );
+ vec_conc.push_back(cc);
+ cc = Rewriter::rewrite( w.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, e1, s ) ).negate() );
+ vec_conc.push_back(cc);
+ cc = Rewriter::rewrite( lenx.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH,
+ NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, e1, s, e2 ) ) ) );
+ vec_conc.push_back(cc);
+ //Incomplete
+ //cc = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, e1, s ).negate();
+ //vec_conc.push_back(cc);
+ //cc = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, e2, s ).negate();
+ //vec_conc.push_back(cc);
+ Node conc = NodeManager::currentNM()->mkNode( kind::AND, vec_conc );
+ */
+ //x[i+j] != y[j]
+ /*Node conc = NodeManager::currentNM()->mkNode( kind::STRING_CHARAT, x , NodeManager::currentNM()->mkNode( kind::PLUS, b1, b2 ) ).eqNode(
+ NodeManager::currentNM()->mkNode( kind::STRING_CHARAT, s , b2) ).negate();
+ Node conc = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_charAtUF, x, NodeManager::currentNM()->mkNode(kind::PLUS, b1, b2)).eqNode(
+ NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_charAtUF, s , b2)).negate();
+ conc = NodeManager::currentNM()->mkNode( kind::AND, g2, conc );
+ conc = NodeManager::currentNM()->mkNode( kind::EXISTS, b2v, conc );
+ conc = NodeManager::currentNM()->mkNode( kind::IMPLIES, g1, conc );
+ conc = NodeManager::currentNM()->mkNode( kind::FORALL, b1v, conc );
+ Node xlss = NodeManager::currentNM()->mkNode( kind::GT, lens, lenx );
+ conc = NodeManager::currentNM()->mkNode( kind::OR, xlss, conc );
+ */
+ Node b1 = NodeManager::currentNM()->mkBoundVar("bi", NodeManager::currentNM()->integerType());
+ Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1);
+ 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 d_charAtUF;
+ 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);
+ Node s2 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_charAtUF, x, NodeManager::currentNM()->mkNode( kind::PLUS, b1, b2 ));
+ Node s5 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_charAtUF, s, b2);
+
+ Node s1 = NodeManager::currentNM()->mkBoundVar("s1", NodeManager::currentNM()->stringType());
+ Node s3 = NodeManager::currentNM()->mkBoundVar("s3", NodeManager::currentNM()->stringType());
+ Node s4 = NodeManager::currentNM()->mkBoundVar("s4", NodeManager::currentNM()->stringType());
+ Node s6 = NodeManager::currentNM()->mkBoundVar("s6", NodeManager::currentNM()->stringType());
+ Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b2, s1, s3, s4, s6);
+
+ std::vector< Node > vec_nodes;
+ Node cc = NodeManager::currentNM()->mkNode( kind::GEQ, b2, d_zero );
+ vec_nodes.push_back(cc);
+ cc = NodeManager::currentNM()->mkNode( kind::GEQ, lens, b2 );
+ vec_nodes.push_back(cc);
+
+ cc = x.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s1, s2, s3));
+ vec_nodes.push_back(cc);
+ cc = s.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s4, s5, s6));
+ vec_nodes.push_back(cc);
+ cc = s2.eqNode(s5).negate();
+ vec_nodes.push_back(cc);
+ cc = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s2).eqNode(NodeManager::currentNM()->mkConst( Rational(1)));
+ vec_nodes.push_back(cc);
+ cc = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s5).eqNode(NodeManager::currentNM()->mkConst( Rational(1)));
+ vec_nodes.push_back(cc);
+ cc = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s1).eqNode(NodeManager::currentNM()->mkNode( kind::PLUS, b1, b2 ));
+ vec_nodes.push_back(cc);
+ cc = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s4).eqNode(b2);
+ vec_nodes.push_back(cc);
+
+ Node conc = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND, vec_nodes) );
+ Node xlss = NodeManager::currentNM()->mkNode( kind::GT, lens, lenx );
+ conc = NodeManager::currentNM()->mkNode( kind::OR, xlss, conc );
+ //conc = NodeManager::currentNM()->mkNode( kind::AND, g2, conc );
+ conc = NodeManager::currentNM()->mkNode( kind::EXISTS, b2v, conc );
+ conc = NodeManager::currentNM()->mkNode( kind::IMPLIES, g1, conc );
+ conc = NodeManager::currentNM()->mkNode( kind::FORALL, b1v, conc );
+
+ d_str_neg_ctn_rewritten[ atom ] = true;
+ sendLemma( atom.negate(), conc, "NEG-CTN-BRK" );
+ //d_pending_req_phase[xlss] = true;
+ addedLemma = true;
+ }
}
- } else if(!areDisequal(lenx, lens)) {
- sendSplit(lenx, lens, "NEG-CTN-SP");
- addedLemma = true;
} else {
- if(d_str_neg_ctn_rewritten.find(atom) == d_str_neg_ctn_rewritten.end()) {
- Node e1 = NodeManager::currentNM()->mkSkolem( "nc1_$$", s.getType(), "created for contain" );
- Node e2 = NodeManager::currentNM()->mkSkolem( "nc2_$$", s.getType(), "created for contain" );
- Node z = NodeManager::currentNM()->mkSkolem( "ncz_$$", s.getType(), "created for contain" );
- Node w = NodeManager::currentNM()->mkSkolem( "ncw_$$", s.getType(), "created for contain" );
- std::vector< Node > vec_conc;
- Node cc = Rewriter::rewrite( x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, e1, z ) ) );
- vec_conc.push_back(cc);
- cc = Rewriter::rewrite( x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, w, e2 ) ) );
- vec_conc.push_back(cc);
- cc = Rewriter::rewrite( z.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, s, e2 ) ).negate() );
- vec_conc.push_back(cc);
- cc = Rewriter::rewrite( w.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, e1, s ) ).negate() );
- vec_conc.push_back(cc);
- cc = Rewriter::rewrite( lenx.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH,
- NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, e1, s, e2 ) ) ) );
- vec_conc.push_back(cc);
- //Incomplete
- //cc = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, e1, s ).negate();
- //vec_conc.push_back(cc);
- //cc = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, e2, s ).negate();
- //vec_conc.push_back(cc);
- Node conc = NodeManager::currentNM()->mkNode( kind::AND, vec_conc );
- Node xlss = NodeManager::currentNM()->mkNode( kind::GT, lens, lenx );
- conc = NodeManager::currentNM()->mkNode( kind::OR, xlss, conc );
- d_str_neg_ctn_rewritten[ atom ] = true;
- sendLemma( atom.negate(), conc, "NEG-INC-BRK" );
- addedLemma = true;
- }
+ Trace("strings-ctn") << "Strings Incomplete (due to Negative Contain) by default." << std::endl;
+ is_unk = true;
}
- } else {
- Trace("strings-ctn") << "Strings Incomplete (due to Negative Contain) by default." << std::endl;
- is_unk = true;
}
}
}
@@ -2228,7 +2329,7 @@ bool TheoryStrings::checkNegContains() {
return true;
} else {
if( is_unk ){
- Trace("strings-ctn") << "Strings::inc: possibly incomplete." << std::endl;
+ Trace("strings-ctn") << "Strings::CTN: possibly incomplete." << std::endl;
d_out->setIncomplete();
}
return false;
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 1d92abbd2..6b4899c80 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -190,6 +190,7 @@ private:
EqcInfo * getOrMakeEqcInfo( Node eqc, bool doMake = true );
//maintain which concat terms have the length lemma instantiated
std::map< Node, bool > d_length_inst;
+ NodeBoolMap d_length_nodes;
private:
void mergeCstVec(std::vector< Node > &vec_strings);
bool getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf,
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 11e206eeb..7edddbe76 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -119,9 +119,9 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
// 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_$$", t.getType(), "created for substr" );
- Node sk2 = NodeManager::currentNM()->mkSkolem( "st2_$$", t.getType(), "created for substr" );
- Node sk3 = NodeManager::currentNM()->mkSkolem( "st3_$$", t.getType(), "created for substr" );
+ 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 ),
@@ -140,9 +140,9 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
d_cache[t] = sk2;
retNode = sk2;
} else if( t.getKind() == kind::STRING_CHARAT_TOTAL ){
- Node sk1 = NodeManager::currentNM()->mkSkolem( "ca1_$$", t.getType(), "created for charat" );
- Node sk2 = NodeManager::currentNM()->mkSkolem( "ca2_$$", t.getType(), "created for charat" );
- Node sk3 = NodeManager::currentNM()->mkSkolem( "ca3_$$", t.getType(), "created for charat" );
+ Node sk1 = NodeManager::currentNM()->mkSkolem( "ca1_$$", NodeManager::currentNM()->stringType(), "created for charat" );
+ Node sk2 = NodeManager::currentNM()->mkSkolem( "ca2_$$", 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] );
@@ -226,7 +226,37 @@ 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 || t.getKind() == kind::STRING_SUBSTR) {
+ } else if(t.getKind() == kind::STRING_CHARAT) {
+ Node d_charAtUF;
+ 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);
+ Node sk2 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_charAtUF, 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 = 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_1 = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkConst( Rational( 1 ) ),
+ NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2 ) );
+
+ Node tp = NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i, len_sk2_eq_1 );
+ 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("CharAt and Substr should not be reached here.");
} else if( t.getNumChildren()>0 ) {
std::vector< Node > cc;
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 9f278aac2..a4c12dfdc 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -360,7 +360,7 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
retNode = NodeManager::currentNM()->mkConst( false );
}
}
- } else if(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/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index e55d6a9c9..ff84e63b7 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -419,11 +419,9 @@ void TheoryEngine::check(Theory::Effort effort) {
if(!d_inConflict && Theory::fullEffort(effort) && d_masterEqualityEngine != NULL && !d_lemmasAdded) {
AlwaysAssert(d_masterEqualityEngine->consistent());
}
-
} catch(const theory::Interrupted&) {
Trace("theory") << "TheoryEngine::check() => interrupted" << endl;
}
-
// If fulleffort, check all theories
if(Dump.isOn("theory::fullcheck") && Theory::fullEffort(effort)) {
if (!d_inConflict && !needCheck()) {
diff --git a/test/regress/regress0/strings/at001.smt2 b/test/regress/regress0/strings/at001.smt2
index 855957430..616189d96 100644
--- a/test/regress/regress0/strings/at001.smt2
+++ b/test/regress/regress0/strings/at001.smt2
@@ -5,8 +5,8 @@
(declare-fun i () Int)
(assert (= (str.at x i) "b"))
-(assert (> i 5))
-(assert (< (str.len x) 4))
+(assert (and (>= i 4) (< i (str.len x))))
+(assert (< (str.len x) 7))
(assert (> (str.len x) 2))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback