From d79b6f0d64e6c205009b70b3c30577f38374231f Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Fri, 24 Jan 2014 11:58:07 -0600 Subject: [PATCH] optimize for the reverse direction --- src/theory/strings/theory_strings.cpp | 445 +++++++++++++++----------- src/theory/strings/theory_strings.h | 7 + 2 files changed, 257 insertions(+), 195 deletions(-) diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 96d880a8a..f283ab1e7 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -700,9 +700,9 @@ bool TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std } } } - if( nf_n.size()>1 || ( nf_n.size()==1 && nf_n[0].getKind()==kind::CONST_STRING ) ){ + if( nf_n.size()>1 || ( nf_n.size()==1 && nf_n[0].getKind()==kind::CONST_STRING ) ) { if( nf_n.size()>1 ){ - Trace("strings-process-debug") << "Check for component lemmas for normal form "; + Trace("strings-process-debug") << "Check for cycle lemma for normal form "; printConcat(nf_n,"strings-process-debug"); Trace("strings-process-debug") << "..." << std::endl; for( unsigned i=0; i & visited, std } std::vector< Node > empty_vec; Node conc = cc.size()==1 ? cc[0] : NodeManager::currentNM()->mkNode( kind::AND, cc ); - sendLemma( mkExplain( ant ), conc, "COMPONENT" ); + sendLemma( mkExplain( ant ), conc, "CYCLE" ); return true; } } } - if( !result ){ + if( !result ) { //we have a normal form that will cause a component lemma at a higher level normal_forms.clear(); normal_forms_exp.clear(); @@ -739,7 +739,7 @@ bool TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std if( !result ){ return false; } - }else{ + } else { Node nn = nf_n.size()==0 ? d_emptyString : nf_n[0]; //Assert( areEqual( nf_n[0], eqc ) ); if( !areEqual( nn, eqc ) ){ @@ -747,7 +747,7 @@ bool TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std ant.insert( ant.end(), nf_exp_n.begin(), nf_exp_n.end() ); ant.push_back( n.eqNode( eqc ) ); Node conc = nn.eqNode( eqc ); - sendLemma( mkExplain( ant ), conc, "Trivial Equal Normal Form" ); + sendLemma( mkExplain( ant ), conc, "CYCLE-T" ); return true; } } @@ -893,10 +893,10 @@ bool TheoryStrings::processLoop(std::vector< Node > &antec, //require that x is non-empty if( !areDisequal( normal_forms[loop_n_index][loop_index], d_emptyString ) ){ //try to make normal_forms[loop_n_index][loop_index] equal to empty to avoid loop - sendSplit( normal_forms[loop_n_index][loop_index], d_emptyString, "Loop Empty x" ); + sendSplit( normal_forms[loop_n_index][loop_index], d_emptyString, "Loop-X-E-Split" ); } else if( !areDisequal( t_yz, d_emptyString ) && t_yz.getKind()!=kind::CONST_STRING ) { //try to make normal_forms[loop_n_index][loop_index] equal to empty to avoid loop - sendSplit( t_yz, d_emptyString, "Loop Empty yz" ); + sendSplit( t_yz, d_emptyString, "Loop-YZ-E-SPlit" ); } else { //need to break antec.push_back( normal_forms[loop_n_index][loop_index].eqNode( d_emptyString ).negate() ); @@ -972,7 +972,7 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms int c_i, c_j, c_loop_n_index, c_other_n_index, c_loop_index, c_index, c_other_index; for(unsigned i=0; i > &normal_forms curr_exp.insert(curr_exp.end(), normal_forms_exp[i].begin(), normal_forms_exp[i].end() ); curr_exp.insert(curr_exp.end(), normal_forms_exp[j].begin(), normal_forms_exp[j].end() ); curr_exp.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, normal_form_src[i], normal_form_src[j] ) ); + + //process the reverse direction first (check for easy conflicts and inferences) + if( processReverseNEq( normal_forms, normal_form_src, curr_exp, i, j ) ){ + return true; + } + //ensure that normal_forms[i] and normal_forms[j] are the same modulo equality unsigned index_i = 0; unsigned index_j = 0; bool success; do { + //---------------------do simple stuff first + if( processSimpleNeq( normal_forms, normal_form_src, curr_exp, i, j, index_i, index_j ) ){ + //added a lemma, return + return true; + } + //---------------------- + success = false; //if we are at the end if(index_i==normal_forms[i].size() || index_j==normal_forms[j].size() ) { - if( index_i==normal_forms[i].size() && index_j==normal_forms[j].size() ) { - //we're done - //addNormalFormPair( normal_form_src[i], normal_form_src[j] ); - } else { - //the remainder must be empty - unsigned k = index_i==normal_forms[i].size() ? j : i; - unsigned index_k = index_i==normal_forms[i].size() ? index_j : index_i; - Node eq_exp; - if( curr_exp.empty() ) { - eq_exp = d_true; - } else if( curr_exp.size() == 1 ) { - eq_exp = curr_exp[0]; - } else { - eq_exp = NodeManager::currentNM()->mkNode( kind::AND, curr_exp ); - } - while(!d_conflict && index_kmkNode( kind::EQUAL, length_term_i, length_term_j ); + Trace("strings-solve-debug") << "Non-simple Case 1 : string lengths neither equal nor disequal" << std::endl; + //try to make the lengths equal via splitting on demand + sendSplit( length_term_i, length_term_j, "Length" ); + length_eq = Rewriter::rewrite( length_eq ); + d_pending_req_phase[ length_eq ] = true; + return true; } else { - Node length_term_i = getLength( normal_forms[i][index_i] ); - Node length_term_j = getLength( normal_forms[j][index_j] ); - //check length(normal_forms[i][index]) == length(normal_forms[j][index]) - if( !areDisequal(length_term_i, length_term_j) && - !areEqual(length_term_i, length_term_j) && - normal_forms[i][index_i].getKind()!=kind::CONST_STRING && - normal_forms[j][index_j].getKind()!=kind::CONST_STRING ) { - //length terms are equal, merge equivalence classes if not already done so - Node length_eq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j ); - Trace("strings-solve-debug") << "Case 2.1 : string lengths neither equal nor disequal" << std::endl; - //try to make the lengths equal via splitting on demand - sendSplit( length_term_i, length_term_j, "Length" ); - length_eq = Rewriter::rewrite( length_eq ); - d_pending_req_phase[ length_eq ] = true; - return true; - } else if( areEqual(length_term_i, length_term_j) ) { - Trace("strings-solve-debug") << "Case 2.2 : string lengths are equal" << std::endl; - Node eq = normal_forms[i][index_i].eqNode( normal_forms[j][index_j] ); - eq = Rewriter::rewrite( eq ); - Node length_eq = length_term_i.eqNode( length_term_j ); - std::vector< Node > temp_exp; - temp_exp.insert(temp_exp.end(), curr_exp.begin(), curr_exp.end() ); - temp_exp.push_back(length_eq); - Node eq_exp = temp_exp.empty() ? d_true : - temp_exp.size() == 1 ? temp_exp[0] : NodeManager::currentNM()->mkNode( kind::AND, temp_exp ); - Trace("strings-lemma") << "Strings: Infer " << eq << " from " << eq_exp << std::endl; - sendInfer( eq_exp, eq, "LengthEq" ); - return true; - } else if(( normal_forms[i][index_i].getKind()!=kind::CONST_STRING && index_i==normal_forms[i].size()-1 ) || - ( normal_forms[j][index_j].getKind()!=kind::CONST_STRING && index_j==normal_forms[j].size()-1 ) ) { - Trace("strings-solve-debug") << "Case 3 : at endpoint" << std::endl; - Node conc; - std::vector< Node > antec; - antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); - std::vector< Node > eqn; - for( unsigned r=0; r<2; r++ ) { - int index_k = r==0 ? index_i : index_j; - int k = r==0 ? i : j; - std::vector< Node > eqnc; - for( unsigned index_l=index_k; index_l antec; - Trace("strings-solve-debug") << "No loops detected." << std::endl; - if( normal_forms[i][index_i].getKind() == kind::CONST_STRING || - normal_forms[j][index_j].getKind() == kind::CONST_STRING) { - unsigned const_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? i : j; - unsigned const_index_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? index_i : index_j; - unsigned nconst_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? j : i; - unsigned nconst_index_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? index_j : index_i; - Node const_str = normal_forms[const_k][const_index_k]; - Node other_str = normal_forms[nconst_k][nconst_index_k]; - if( other_str.getKind() == kind::CONST_STRING ) { - unsigned len_short = const_str.getConst().size() <= other_str.getConst().size() ? const_str.getConst().size() : other_str.getConst().size(); - if( const_str.getConst().strncmp(other_str.getConst(), len_short) ) { - //same prefix - //k is the index of the string that is shorter - int k = const_str.getConst().size()().size() ? i : j; - int index_k = const_str.getConst().size()().size() ? index_i : index_j; - int l = const_str.getConst().size()().size() ? j : i; - int index_l = const_str.getConst().size()().size() ? index_j : index_i; - Node remainderStr = NodeManager::currentNM()->mkConst( normal_forms[l][index_l].getConst().substr(len_short) ); - Trace("strings-solve-debug-test") << "Break normal form of " << normal_forms[l][index_l] << " into " << normal_forms[k][index_k] << ", " << remainderStr << std::endl; - normal_forms[l].insert( normal_forms[l].begin()+index_l + 1, remainderStr ); - normal_forms[l][index_l] = normal_forms[k][index_k]; - success = true; - } else { - //curr_exp is conflict - antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); - Node ant = mkExplain( antec ); - sendLemma( ant, conc, "Conflict" ); - return true; - } + Node conc; + std::vector< Node > antec; + Trace("strings-solve-debug") << "No loops detected." << std::endl; + if( normal_forms[i][index_i].getKind() == kind::CONST_STRING || + normal_forms[j][index_j].getKind() == kind::CONST_STRING) { + unsigned const_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? i : j; + unsigned const_index_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? index_i : index_j; + unsigned nconst_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? j : i; + unsigned nconst_index_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? index_j : index_i; + Node const_str = normal_forms[const_k][const_index_k]; + Node other_str = normal_forms[nconst_k][nconst_index_k]; + if( other_str.getKind() == kind::CONST_STRING ) { + unsigned len_short = const_str.getConst().size() <= other_str.getConst().size() ? const_str.getConst().size() : other_str.getConst().size(); + if( const_str.getConst().strncmp(other_str.getConst(), len_short) ) { + //same prefix + //k is the index of the string that is shorter + int k = const_str.getConst().size()().size() ? i : j; + int index_k = const_str.getConst().size()().size() ? index_i : index_j; + int l = const_str.getConst().size()().size() ? j : i; + int index_l = const_str.getConst().size()().size() ? index_j : index_i; + Node remainderStr = NodeManager::currentNM()->mkConst( normal_forms[l][index_l].getConst().substr(len_short) ); + Trace("strings-solve-debug-test") << "Break normal form of " << normal_forms[l][index_l] << " into " << normal_forms[k][index_k] << ", " << remainderStr << std::endl; + normal_forms[l].insert( normal_forms[l].begin()+index_l + 1, remainderStr ); + normal_forms[l][index_l] = normal_forms[k][index_k]; + success = true; } else { - Assert( other_str.getKind()!=kind::STRING_CONCAT ); + //curr_exp is conflict antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); - Node firstChar = const_str.getConst().size() == 1 ? const_str : - NodeManager::currentNM()->mkConst( const_str.getConst().substr(0, 1) ); - //split the string - Node eq1 = Rewriter::rewrite( other_str.eqNode( d_emptyString ) ); - Node eq2 = mkSplitEq( "c_spt_$$", "created for v/c split", other_str, firstChar, false ); - d_pending_req_phase[ eq1 ] = true; - conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 ); - Trace("strings-solve-debug") << "Break normal form constant/variable " << std::endl; - Node ant = mkExplain( antec ); - sendLemma( ant, conc, "CST-SPLIT" ); + sendLemma( ant, conc, "Conflict" ); return true; } } else { - std::vector< Node > antec_new_lits; + Assert( other_str.getKind()!=kind::STRING_CONCAT ); antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); - - Node ldeq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j ).negate(); - if( d_equalityEngine.areDisequal( length_term_i, length_term_j, true ) ){ - antec.push_back( ldeq ); - }else{ - antec_new_lits.push_back(ldeq); - } - - //x!=e /\ y!=e - for(unsigned xory=0; xory<2; xory++) { - Node x = xory==0 ? normal_forms[i][index_i] : normal_forms[j][index_j]; - Node xgtz = x.eqNode( d_emptyString ).negate(); - if( areDisequal( x, d_emptyString ) ) { - antec.push_back( xgtz ); - } else { - antec_new_lits.push_back( xgtz ); - } - } - - //Node sk = NodeManager::currentNM()->mkSkolem( "v_spt_$$", normal_forms[i][index_i].getType(), "created for v/v split" ); - //Node eq1 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[i][index_i], - // NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[j][index_j], sk ) ) ); - //Node eq2 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[j][index_j], - // NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[i][index_i], sk ) ) ); - Node eq1 = mkSplitEq( "v_spt_l_$$", "created for v/v split", normal_forms[i][index_i], normal_forms[j][index_j], true ); - Node eq2 = mkSplitEq( "v_spt_r_$$", "created for v/v split", normal_forms[j][index_j], normal_forms[i][index_i], true ); + Node firstChar = const_str.getConst().size() == 1 ? const_str : + NodeManager::currentNM()->mkConst( const_str.getConst().substr(0, 1) ); + //split the string + Node eq1 = Rewriter::rewrite( other_str.eqNode( d_emptyString ) ); + Node eq2 = mkSplitEq( "c_spt_$$", "created for v/c split", other_str, firstChar, false ); + d_pending_req_phase[ eq1 ] = true; conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 ); + Trace("strings-solve-debug") << "Break normal form constant/variable " << std::endl; - Node ant = mkExplain( antec, antec_new_lits ); - sendLemma( ant, conc, "VAR-SPLIT" ); + Node ant = mkExplain( antec ); + sendLemma( ant, conc, "CST-SPLIT" ); return true; } + } else { + std::vector< Node > antec_new_lits; + antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); + + Node ldeq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j ).negate(); + if( d_equalityEngine.areDisequal( length_term_i, length_term_j, true ) ){ + antec.push_back( ldeq ); + }else{ + antec_new_lits.push_back(ldeq); + } + + //x!=e /\ y!=e + for(unsigned xory=0; xory<2; xory++) { + Node x = xory==0 ? normal_forms[i][index_i] : normal_forms[j][index_j]; + Node xgtz = x.eqNode( d_emptyString ).negate(); + if( areDisequal( x, d_emptyString ) ) { + antec.push_back( xgtz ); + } else { + antec_new_lits.push_back( xgtz ); + } + } + + //Node sk = NodeManager::currentNM()->mkSkolem( "v_spt_$$", normal_forms[i][index_i].getType(), "created for v/v split" ); + //Node eq1 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[i][index_i], + // NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[j][index_j], sk ) ) ); + //Node eq2 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[j][index_j], + // NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[i][index_i], sk ) ) ); + Node eq1 = mkSplitEq( "v_spt_l_$$", "created for v/v split", normal_forms[i][index_i], normal_forms[j][index_j], true ); + Node eq2 = mkSplitEq( "v_spt_r_$$", "created for v/v split", normal_forms[j][index_j], normal_forms[i][index_i], true ); + conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 ); + + Node ant = mkExplain( antec, antec_new_lits ); + sendLemma( ant, conc, "VAR-SPLIT" ); + return true; } } } @@ -1214,6 +1152,112 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms return false; } +bool TheoryStrings::processReverseNEq( std::vector< std::vector< Node > > &normal_forms, + std::vector< Node > &normal_form_src, std::vector< Node > &curr_exp, unsigned i, unsigned j ) { + //reverse normal form of i, j + std::reverse( normal_forms[i].begin(), normal_forms[i].end() ); + std::reverse( normal_forms[j].begin(), normal_forms[j].end() ); + + std::vector< Node > t_curr_exp; + t_curr_exp.insert( t_curr_exp.begin(), curr_exp.begin(), curr_exp.end() ); + unsigned index_i = 0; + unsigned index_j = 0; + bool ret = processSimpleNeq( normal_forms, normal_form_src, t_curr_exp, i, j, index_i, index_j ); + + //reverse normal form of i, j + std::reverse( normal_forms[i].begin(), normal_forms[i].end() ); + std::reverse( normal_forms[j].begin(), normal_forms[j].end() ); + + return ret; +} + +bool TheoryStrings::processSimpleNeq( std::vector< std::vector< Node > > &normal_forms, + std::vector< Node > &normal_form_src, std::vector< Node > &curr_exp, + unsigned i, unsigned j, unsigned& index_i, unsigned& index_j ) { + bool success; + do { + success = false; + //if we are at the end + if(index_i==normal_forms[i].size() || index_j==normal_forms[j].size() ) { + if( index_i==normal_forms[i].size() && index_j==normal_forms[j].size() ) { + //we're done + } else { + //the remainder must be empty + unsigned k = index_i==normal_forms[i].size() ? j : i; + unsigned index_k = index_i==normal_forms[i].size() ? index_j : index_i; + Node eq_exp = mkAnd( curr_exp ); + while(!d_conflict && index_k temp_exp; + temp_exp.insert(temp_exp.end(), curr_exp.begin(), curr_exp.end() ); + temp_exp.push_back(length_eq); + Node eq_exp = temp_exp.empty() ? d_true : + temp_exp.size() == 1 ? temp_exp[0] : NodeManager::currentNM()->mkNode( kind::AND, temp_exp ); + sendInfer( eq_exp, eq, "LengthEq" ); + return true; + } else if(( normal_forms[i][index_i].getKind()!=kind::CONST_STRING && index_i==normal_forms[i].size()-1 ) || + ( normal_forms[j][index_j].getKind()!=kind::CONST_STRING && index_j==normal_forms[j].size()-1 ) ) { + Trace("strings-solve-debug") << "Simple Case 3 : at endpoint" << std::endl; + Node conc; + std::vector< Node > antec; + antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); + std::vector< Node > eqn; + for( unsigned r=0; r<2; r++ ) { + int index_k = r==0 ? index_i : index_j; + int k = r==0 ? i : j; + std::vector< Node > eqnc; + for( unsigned index_l=index_k; index_l & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp ) { Trace("strings-process") << "Process equivalence class " << eqc << std::endl; @@ -1474,6 +1518,7 @@ void TheoryStrings::sendInfer( Node eq_exp, Node eq, const char * c ) { if( eq==d_false ){ sendLemma( eq_exp, eq, c ); }else{ + Trace("strings-lemma") << "Strings::Infer " << eq << " from " << eq_exp << std::endl; d_pending.push_back( eq ); d_pending_exp[eq] = eq_exp; d_infer.push_back(eq); @@ -1556,6 +1601,16 @@ Node TheoryStrings::mkExplain( std::vector< Node >& a, std::vector< Node >& an ) return ant; } +Node TheoryStrings::mkAnd( std::vector< Node >& a ) { + if( a.empty() ) { + return d_true; + } else if( a.size() == 1 ) { + return a[0]; + } else { + return NodeManager::currentNM()->mkNode( kind::AND, a ); + } +} + void TheoryStrings::getConcatVec( Node n, std::vector< Node >& c ) { if( n.getKind()==kind::STRING_CONCAT ){ for( unsigned i=0; i > &normal_forms, std::vector< std::vector< Node > > &normal_forms_exp, std::vector< Node > &normal_form_src); + bool processReverseNEq(std::vector< std::vector< Node > > &normal_forms, + std::vector< Node > &normal_form_src, std::vector< Node > &curr_exp, unsigned i, unsigned j ); + bool processSimpleNeq( std::vector< std::vector< Node > > &normal_forms, + std::vector< Node > &normal_form_src, std::vector< Node > &curr_exp, unsigned i, unsigned j, + unsigned& index_i, unsigned& index_j ); bool normalizeEquivalenceClass( Node n, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp ); bool normalizeDisequality( Node n1, Node n2 ); bool unrollStar( Node atom ); @@ -254,6 +259,8 @@ protected: /** mkExplain **/ Node mkExplain( std::vector< Node >& a ); Node mkExplain( std::vector< Node >& a, std::vector< Node >& an ); + /** mkAnd **/ + Node mkAnd( std::vector< Node >& a ); /** get concat vector */ void getConcatVec( Node n, std::vector< Node >& c ); -- 2.30.2