From: Tianyi Liang Date: Fri, 10 Jan 2014 23:42:01 +0000 (-0600) Subject: normal form breaking X-Git-Tag: cvc5-1.0.0~7152 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d141fef84073b7f948e750e473cc6876ba157b5d;p=cvc5.git normal form breaking --- diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index aa3ab12c5..a2b21aa40 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -436,8 +436,8 @@ void TheoryStrings::check(Effort e) { addedLemma = checkMemberships(); Trace("strings-process") << "Done check membership constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; if( !d_conflict && !addedLemma ) { - addedLemma = checkInclusions(); - Trace("strings-process") << "Done check inclusion constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; + addedLemma = checkContains(); + Trace("strings-process") << "Done check contain constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; } } } @@ -721,6 +721,7 @@ bool TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std Trace("strings-solve") << "--- Normal forms for equivlance class " << eqc << " : " << std::endl; for( unsigned i=0; i0) Trace("strings-solve") << ", "; Trace("strings-solve") << normal_forms[i][j]; @@ -741,6 +742,27 @@ bool TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std return true; } +void TheoryStrings::mergeCstVec(std::vector< Node > &vec_strings) { + std::vector< Node >::iterator itr = vec_strings.begin(); + while(itr != vec_strings.end()) { + if(itr->isConst()) { + std::vector< Node >::iterator itr2 = itr + 1; + if(itr2 == vec_strings.end()) { + break; + } else if(itr2->isConst()) { + CVC4::String s1 = itr->getConst(); + CVC4::String s2 = itr2->getConst(); + *itr = NodeManager::currentNM()->mkConst(s1.concat(s2)); + vec_strings.erase(itr2); + } else { + ++itr; + } + } else { + ++itr; + } + } +} + bool TheoryStrings::detectLoop( std::vector< std::vector< Node > > &normal_forms, int i, int j, int index_i, int index_j, int &loop_in_i, int &loop_in_j) { @@ -2070,12 +2092,12 @@ bool TheoryStrings::checkMemberships() { } } -bool TheoryStrings::checkInclusions() { +bool TheoryStrings::checkContains() { bool is_unk = false; bool addedLemma = false; for( unsigned i=0; imkSkolem( "sc1_$$", s.getType(), "created for inclusion" ); - Node sk2 = NodeManager::currentNM()->mkSkolem( "sc2_$$", s.getType(), "created for inclusion" ); + 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( assertion, eq, "inclusion" ); + sendLemma( assertion, eq, "POS-INC" ); addedLemma = true; d_str_ctn_rewritten[ atom ] = true; } else { - Trace("strings-inc") << "... is already rewritten." << std::endl; + Trace("strings-ctn") << "... is already rewritten." << std::endl; } } else { - Trace("strings-inc") << "... is satisfied." << std::endl; + Trace("strings-ctn") << "... is satisfied." << 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, "inclusion conflict 1" ); + 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, "inclusion conflict 2" ); + sendLemma( ant, conc, "NEG-CTN Conflict 2" ); addedLemma = true; } else { - if(d_str_ctn_rewritten.find(assertion) == d_str_ctn_rewritten.end()) { - if(options::stringExp()) { - Node x = atom[0]; - Node s = atom[1]; - Node sk1 = NodeManager::currentNM()->mkSkolem( "sc3_$$", s.getType(), "created for inclusion" ); - Node sk2 = NodeManager::currentNM()->mkSkolem( "sc4_$$", s.getType(), "created for inclusion" ); - Node eq = Rewriter::rewrite( x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, s, sk2 ) ) ); - Node antc = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, assertion, eq ) ); - d_str_ctn_rewritten[ assertion ] = true; - sendLemma( antc, d_false, "negative inclusion" ); + 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"); addedLemma = true; } else { - Trace("strings-inc") << "Strings Incomplete (due to Negative Contain) by default." << std::endl; - is_unk = true; + addedLemma = processNegContains(assertion); } + } else { + Trace("strings-ctn") << "Strings Incomplete (due to Negative Contain) by default." << std::endl; + is_unk = true; } } } @@ -2140,6 +2170,27 @@ bool TheoryStrings::checkInclusions() { } } +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 >(); @@ -2155,8 +2206,8 @@ CVC4::String TheoryStrings::getHeadConst( Node x ) { } bool TheoryStrings::addMembershipLength(Node atom) { - Node x = atom[0]; - Node r = atom[1]; + //Node x = atom[0]; + //Node r = atom[1]; /*std::vector< int > co; co.push_back(0); diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 62524ee14..77ea298bd 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -191,6 +191,7 @@ private: //maintain which concat terms have the length lemma instantiated std::map< Node, bool > d_length_inst; private: + void mergeCstVec(std::vector< Node > &vec_strings); bool getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< std::vector< Node > > &normal_forms, std::vector< std::vector< Node > > &normal_forms_exp, @@ -216,7 +217,8 @@ private: bool checkCardinality(); bool checkInductiveEquations(); bool checkMemberships(); - bool checkInclusions(); + bool checkContains(); + bool processNegContains(Node assertion); public: void preRegisterTerm(TNode n); @@ -272,6 +274,7 @@ private: // Special String Functions NodeList d_str_ctn; + std::map< Node, bool > d_str_ctn_eqlen; std::map< Node, bool > d_str_ctn_rewritten; // Regular Expression