From 368e2945a871e16bdf2f3a26a401b9d157240a9d Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Fri, 17 Jan 2014 17:56:08 -0600 Subject: [PATCH] strings with new ideas --- src/printer/smt2/smt2_printer.cpp | 1 + src/smt/smt_engine.cpp | 22 +- src/theory/strings/theory_strings.cpp | 325 ++++++++++++------ src/theory/strings/theory_strings.h | 1 + .../strings/theory_strings_preprocess.cpp | 44 ++- .../strings/theory_strings_rewriter.cpp | 2 +- src/theory/theory_engine.cpp | 2 - test/regress/regress0/strings/at001.smt2 | 4 +- 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 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_mapstringType(), "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_mapstringType(), "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_vec; - for( unsigned i=0; imkNode( 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_vec; + for( unsigned i=0; imkNode( 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().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().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; imkSkolem( "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; imkNode( 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().getNumerator().toUnsignedInt(); if( node[0].getConst().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) -- 2.30.2