From 6b96fdafc74d4de42fa875c59aec89fbf809ca8d Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Wed, 15 Jan 2014 17:20:27 -0600 Subject: [PATCH] adds smt2 print for strings --- src/printer/smt2/smt2_printer.cpp | 18 ++ src/theory/strings/theory_strings.cpp | 202 +++++++++++------- src/theory/strings/theory_strings.h | 9 +- .../strings/theory_strings_rewriter.cpp | 4 +- 4 files changed, 150 insertions(+), 83 deletions(-) diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index c56d87da6..409c9b4dd 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -273,6 +273,24 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::STORE: case kind::ARRAY_TYPE: out << smtKindString(k) << " "; break; + // string theory + 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: out << "str.substr "; break; + case kind::STRING_STRCTN: out << "str.contain "; break; + case kind::STRING_CHARAT: out << "str.at "; break; + case kind::STRING_STRIDOF: out << "str.indexof "; break; + case kind::STRING_STRREPL: out << "str.replace "; break; + case kind::STRING_TO_REGEXP: out << "str.to.re "; break; + case kind::REGEXP_CONCAT: out << "re.++ "; break; + case kind::REGEXP_OR: out << "re.or "; break; + case kind::REGEXP_INTER: out << "re.itr "; break; + case kind::REGEXP_STAR: out << "re.* "; break; + case kind::REGEXP_PLUS: out << "re.+ "; break; + case kind::REGEXP_OPT: out << "re.opt "; break; + case kind::REGEXP_RANGE: out << "re.range "; break; + // bv theory case kind::BITVECTOR_CONCAT: out << "concat "; break; case kind::BITVECTOR_AND: out << "bvand "; break; diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index a2b21aa40..4b479e348 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -43,7 +43,8 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu d_nf_pairs(c), //d_var_lmin( c ), //d_var_lmax( c ), - d_str_ctn( c ), + d_str_pos_ctn( c ), + d_str_neg_ctn( c ), d_reg_exp_mem( c ), d_curr_cardinality( c, 0 ) { @@ -310,7 +311,7 @@ void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) { } } } - Trace("strings-model") << "String Model : Finished." << std::endl; + Trace("strings-model") << "String Model : Pure Assigned." << std::endl; //step 4 : assign constants to all other equivalence classes for( unsigned i=0; iassertEquality( nodes[i], cc, true ); } } + Trace("strings-model") << "String Model : Assigned." << std::endl; + //check for negative contains + /* + Trace("strings-model") << "String Model : Check Neg Contains, size = " << d_str_neg_ctn.size() << std::endl; + for( unsigned i=0; igetValue(x); + //Node yv = m->getValue(y); + //Trace("strings-model") << "String Model : Check Neg contains Value: ~contains(" << xv << ", " << yv << ")." << std::endl; + } + */ + Trace("strings-model") << "String Model : Finished." << std::endl; } ///////////////////////////////////////////////////////////////////////////// @@ -408,7 +423,11 @@ void TheoryStrings::check(Effort e) { if ( atom.getKind() == kind::STRING_IN_REGEXP ) { d_reg_exp_mem.push_back( assertion ); } else if (atom.getKind() == kind::STRING_STRCTN) { - d_str_ctn.push_back( assertion ); + if(polarity) { + d_str_pos_ctn.push_back( atom ); + } else { + d_str_neg_ctn.push_back( atom ); + } d_equalityEngine.assertPredicate(atom, polarity, fact); } else if (atom.getKind() == kind::EQUAL) { d_equalityEngine.assertEquality(atom, polarity, fact); @@ -2093,68 +2112,114 @@ bool TheoryStrings::checkMemberships() { } bool TheoryStrings::checkContains() { - bool is_unk = false; + bool addedLemma = checkPosContains(); + Trace("strings-process") << "Done check positive contain constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; + if(!addedLemma) { + addedLemma = checkNegContains(); + Trace("strings-process") << "Done check positive contain constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; + } + return addedLemma; +} + +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( assertion, eq, "POS-INC" ); - addedLemma = true; - d_str_ctn_rewritten[ atom ] = true; - } else { - Trace("strings-ctn") << "... is already rewritten." << std::endl; - } + 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; } else { - Trace("strings-ctn") << "... is satisfied." << std::endl; + Trace("strings-ctn") << "... is already rewritten." << std::endl; } } else { - if( areEqual( atom[1], d_emptyString ) ) { - Node ant = NodeManager::currentNM()->mkNode( kind::AND, assertion, 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, assertion, 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 = getLengthTerm(x); - Node lens = getLengthTerm(s); - if(areEqual(lenx, lens)) { - if(d_str_ctn_eqlen.find(assertion) == d_str_ctn_eqlen.end()) { - Node eq = lenx.eqNode(lens); - Node antc = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, assertion, eq ) ); - Node xneqs = x.eqNode(s).negate(); - d_str_ctn_eqlen[ assertion ] = true; - sendLemma( antc, xneqs, "NEG-CTN-EQL" ); - addedLemma = true; - } - } else if(!areDisequal(lenx, lens)) { - sendSplit(lenx, lens, "NEG-CTN-SP"); + Trace("strings-ctn") << "... is satisfied." << std::endl; + } + } + if( addedLemma ){ + doPendingLemmas(); + return true; + } else { + return false; + } +} + +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" ); addedLemma = true; - } else { - addedLemma = processNegContains(assertion); } + } else if(!areDisequal(lenx, lens)) { + sendSplit(lenx, lens, "NEG-CTN-SP"); + addedLemma = true; } else { - Trace("strings-ctn") << "Strings Incomplete (due to Negative Contain) by default." << std::endl; - is_unk = true; + 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; + } } + } else { + Trace("strings-ctn") << "Strings Incomplete (due to Negative Contain) by default." << std::endl; + is_unk = true; } } } @@ -2163,34 +2228,13 @@ bool TheoryStrings::checkContains() { return true; } else { if( is_unk ){ - Trace("strings-inc") << "Strings::inc: possibly incomplete." << std::endl; + Trace("strings-ctn") << "Strings::inc: possibly incomplete." << std::endl; d_out->setIncomplete(); } return false; } } -bool TheoryStrings::processNegContains(Node assertion) { - Node atom = assertion[0]; - Node x = atom[0]; - Node s = atom[1]; - Node lenx = getLengthTerm(x); - Node lens = getLengthTerm(s); - - if(d_str_ctn_rewritten.find(assertion) == d_str_ctn_rewritten.end()) { - Node sk1 = NodeManager::currentNM()->mkSkolem( "sc3_$$", s.getType(), "created for contain" ); - Node sk2 = NodeManager::currentNM()->mkSkolem( "sc4_$$", s.getType(), "created for contain" ); - Node eq = Rewriter::rewrite( x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, s, sk2 ) ) ); - Node gt = NodeManager::currentNM()->mkNode( kind::GT, lenx, lens ); - Node antc = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, assertion, eq, gt ) ); - d_str_ctn_rewritten[ assertion ] = true; - sendLemma( antc, d_false, "NEG-INC-BRK" ); - return true; - } else { - return false; - } -} - CVC4::String TheoryStrings::getHeadConst( Node x ) { if( x.isConst() ) { return x.getConst< String >(); diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 77ea298bd..1d92abbd2 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -218,7 +218,8 @@ private: bool checkInductiveEquations(); bool checkMemberships(); bool checkContains(); - bool processNegContains(Node assertion); + bool checkPosContains(); + bool checkNegContains(); public: void preRegisterTerm(TNode n); @@ -273,9 +274,11 @@ private: int getMaxPossibleLength( Node x ); // Special String Functions - NodeList d_str_ctn; + NodeList d_str_pos_ctn; + NodeList d_str_neg_ctn; std::map< Node, bool > d_str_ctn_eqlen; - std::map< Node, bool > d_str_ctn_rewritten; + std::map< Node, bool > d_str_pos_ctn_rewritten; + std::map< Node, bool > d_str_neg_ctn_rewritten; // Regular Expression private: diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index f68deda54..d21754820 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -352,7 +352,9 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { } } } else if(node.getKind() == kind::STRING_STRCTN) { - if( node[0].isConst() && node[1].isConst() ) { + if( node[0] == node[1] ) { + retNode = NodeManager::currentNM()->mkConst( true ); + } else if( node[0].isConst() && node[1].isConst() ) { CVC4::String s = node[0].getConst(); CVC4::String t = node[1].getConst(); if( s.find(t) != std::string::npos ) { -- 2.30.2