From: Tianyi Liang Date: Fri, 24 Jan 2014 21:39:13 +0000 (-0600) Subject: rev diseq X-Git-Tag: cvc5-1.0.0~7125^2 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1f82a19119fece6b78e393b33413a8f6e10441a6;p=cvc5.git rev diseq --- diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index d41359a88..effbbca2e 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -995,7 +995,7 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms do { //---------------------do simple stuff first - if( processSimpleNeq( normal_forms, normal_form_src, curr_exp, i, j, index_i, index_j, false ) ){ + if( processSimpleNEq( normal_forms, normal_form_src, curr_exp, i, j, index_i, index_j, false ) ){ //added a lemma, return return true; } @@ -1140,7 +1140,7 @@ bool TheoryStrings::processReverseNEq( std::vector< std::vector< Node > > &norma 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, true ); + bool ret = processSimpleNEq( normal_forms, normal_form_src, t_curr_exp, i, j, index_i, index_j, true ); //reverse normal form of i, j std::reverse( normal_forms[i].begin(), normal_forms[i].end() ); @@ -1149,7 +1149,7 @@ bool TheoryStrings::processReverseNEq( std::vector< std::vector< Node > > &norma return ret; } -bool TheoryStrings::processSimpleNeq( std::vector< std::vector< Node > > &normal_forms, +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 isRev ) { bool success; @@ -1349,7 +1349,8 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v } } -bool TheoryStrings::normalizeDisequality( Node ni, Node nj ) { +//return true for lemma, false if we succeed +bool TheoryStrings::processDeq( Node ni, Node nj ) { //Assert( areDisequal( ni, nj ) ); if( d_normal_forms[ni].size()>1 || d_normal_forms[nj].size()>1 ){ std::vector< Node > nfi; @@ -1357,106 +1358,75 @@ bool TheoryStrings::normalizeDisequality( Node ni, Node nj ) { std::vector< Node > nfj; nfj.insert( nfj.end(), d_normal_forms[nj].begin(), d_normal_forms[nj].end() ); + //int revRet = processReverseDeq( nfi, nfj, ni, nj ); + //if( revRet!=0 ){ + // return revRet==-1; + //} + + nfi.clear(); + nfi.insert( nfi.end(), d_normal_forms[ni].begin(), d_normal_forms[ni].end() ); + nfj.clear(); + nfj.insert( nfj.end(), d_normal_forms[nj].begin(), d_normal_forms[nj].end() ); + unsigned index = 0; while( index=nfi.size() || index>=nfj.size() ){ - std::vector< Node > ant; - //we have a conflict : because the lengths are equal, the remainder needs to be empty, which will lead to a conflict - Node lni = getLength( ni ); - Node lnj = getLength( nj ); - ant.push_back( lni.eqNode( lnj ) ); - ant.push_back( getLengthTerm( ni ).eqNode( d_normal_forms_base[ni] ) ); - ant.push_back( getLengthTerm( nj ).eqNode( d_normal_forms_base[nj] ) ); - ant.insert( ant.end(), d_normal_forms_exp[ni].begin(), d_normal_forms_exp[ni].end() ); - ant.insert( ant.end(), d_normal_forms_exp[nj].begin(), d_normal_forms_exp[nj].end() ); - std::vector< Node > cc; - std::vector< Node >& nfk = index>=nfi.size() ? nfj : nfi; - for( unsigned index_k=index; index_kmkNode( kind::AND, cc ); - conc = Rewriter::rewrite( conc ); - sendLemma(mkExplain( ant ), conc, "Disequality Normalize Empty"); - return true; + int ret = processSimpleDeq( nfi, nfj, ni, nj, index, false ); + if( ret!=0 ){ + return ret==-1; }else{ + Assert( index().size() < j.getConst().size() ? i.getConst().size() : j.getConst().size(); - String si = i.getConst().substr(0, len_short); - String sj = j.getConst().substr(0, len_short); - if(si == sj) { - if( i.getConst().size() < j.getConst().size() ) { - Node remainderStr = NodeManager::currentNM()->mkConst( j.getConst().substr(len_short) ); - Trace("strings-solve-debug-test") << "Break normal form of " << nfj[index] << " into " << nfi[index] << ", " << remainderStr << std::endl; - nfj.insert( nfj.begin() + index + 1, remainderStr ); - nfj[index] = nfi[index]; - } else { - Node remainderStr = NodeManager::currentNM()->mkConst( i.getConst().substr(len_short) ); - Trace("strings-solve-debug-test") << "Break normal form of " << nfi[index] << " into " << nfj[index] << ", " << remainderStr << std::endl; - nfi.insert( nfi.begin() + index + 1, remainderStr ); - nfi[index] = nfj[index]; - } - } else { - //conflict - return false; - } + Assert( i.getKind()!=kind::CONST_STRING || j.getKind()!=kind::CONST_STRING ); + Node li = getLength( i ); + Node lj = getLength( j ); + if( areDisequal(li, lj) ){ + //if( i.getKind()==kind::CONST_STRING || j.getKind()==kind::CONST_STRING ){ + + Trace("strings-solve") << "Non-Simple Case 1 : add lemma " << std::endl; + //must add lemma + std::vector< Node > antec; + std::vector< Node > antec_new_lits; + antec.insert( antec.end(), d_normal_forms_exp[ni].begin(), d_normal_forms_exp[ni].end() ); + antec.insert( antec.end(), d_normal_forms_exp[nj].begin(), d_normal_forms_exp[nj].end() ); + antec.push_back( ni.eqNode( nj ).negate() ); + antec_new_lits.push_back( li.eqNode( lj ).negate() ); + std::vector< Node > conc; + 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); + Node nemp = sk3.eqNode(d_emptyString).negate(); + conc.push_back(nemp); + Node lsk1 = getLength( sk1 ); + conc.push_back( lsk1.eqNode( li ) ); + Node lsk2 = getLength( sk2 ); + conc.push_back( lsk2.eqNode( lj ) ); + 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 ), "D-DISL-Split" ); + return true; + }else if( areEqual( li, lj ) ){ + Assert( !areDisequal( i, j ) ); + //splitting on demand : try to make them disequal + Node eq = i.eqNode( j ); + sendSplit( i, j, "D-EQL-Split" ); + eq = Rewriter::rewrite( eq ); + d_pending_req_phase[ eq ] = false; + return true; }else{ - Node li = getLength( i ); - Node lj = getLength( j ); - if( areDisequal(li, lj) ){ - //if( i.getKind()==kind::CONST_STRING || j.getKind()==kind::CONST_STRING ){ - - Trace("strings-solve") << "Case 2 : add lemma " << std::endl; - //must add lemma - std::vector< Node > antec; - std::vector< Node > antec_new_lits; - antec.insert( antec.end(), d_normal_forms_exp[ni].begin(), d_normal_forms_exp[ni].end() ); - antec.insert( antec.end(), d_normal_forms_exp[nj].begin(), d_normal_forms_exp[nj].end() ); - antec.push_back( ni.eqNode( nj ).negate() ); - antec_new_lits.push_back( li.eqNode( lj ).negate() ); - std::vector< Node > conc; - 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); - Node nemp = sk3.eqNode(d_emptyString).negate(); - conc.push_back(nemp); - Node lsk1 = getLength( sk1 ); - conc.push_back( lsk1.eqNode( li ) ); - Node lsk2 = getLength( sk2 ); - conc.push_back( lsk2.eqNode( lj ) ); - 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 ), "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: D-Remove - return false; - } else { - //splitting on demand : try to make them disequal - Node eq = i.eqNode( j ); - sendSplit( i, j, "D-EQL-Split" ); - eq = Rewriter::rewrite( eq ); - d_pending_req_phase[ eq ] = false; - return true; - } - }else{ - //splitting on demand : try to make lengths equal - Node eq = li.eqNode( lj ); - sendSplit( li, lj, "D-UNK-Split" ); - eq = Rewriter::rewrite( eq ); - d_pending_req_phase[ eq ] = true; - return true; - } + //splitting on demand : try to make lengths equal + Node eq = li.eqNode( lj ); + sendSplit( li, lj, "D-UNK-Split" ); + eq = Rewriter::rewrite( eq ); + d_pending_req_phase[ eq ] = true; + return true; } } index++; @@ -1467,6 +1437,92 @@ bool TheoryStrings::normalizeDisequality( Node ni, Node nj ) { return false; } +int TheoryStrings::processReverseDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj ) { + //reverse normal form of i, j + std::reverse( nfi.begin(), nfi.end() ); + std::reverse( nfj.begin(), nfj.end() ); + + unsigned index = 0; + int ret = processSimpleDeq( nfi, nfj, ni, nj, index, true ); + + //reverse normal form of i, j + std::reverse( nfi.begin(), nfi.end() ); + std::reverse( nfj.begin(), nfj.end() ); + + return ret; +} + +int TheoryStrings::processSimpleDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj, unsigned& index, bool isRev ) { + while( index=nfi.size() || index>=nfj.size() ){ + std::vector< Node > ant; + //we have a conflict : because the lengths are equal, the remainder needs to be empty, which will lead to a conflict + Node lni = getLength( ni ); + Node lnj = getLength( nj ); + ant.push_back( lni.eqNode( lnj ) ); + ant.push_back( getLengthTerm( ni ).eqNode( d_normal_forms_base[ni] ) ); + ant.push_back( getLengthTerm( nj ).eqNode( d_normal_forms_base[nj] ) ); + ant.insert( ant.end(), d_normal_forms_exp[ni].begin(), d_normal_forms_exp[ni].end() ); + ant.insert( ant.end(), d_normal_forms_exp[nj].begin(), d_normal_forms_exp[nj].end() ); + std::vector< Node > cc; + std::vector< Node >& nfk = index>=nfi.size() ? nfj : nfi; + for( unsigned index_k=index; index_kmkNode( kind::AND, cc ); + conc = Rewriter::rewrite( conc ); + sendLemma(mkExplain( ant ), conc, "Disequality Normalize Empty"); + return -1; + } else { + Node i = nfi[index]; + Node j = nfj[index]; + Trace("strings-solve-debug") << "...Processing " << i << " " << j << std::endl; + if( !areEqual( i, j ) ) { + if( i.getKind()==kind::CONST_STRING && j.getKind()==kind::CONST_STRING ) { + unsigned int len_short = i.getConst().size() < j.getConst().size() ? i.getConst().size() : j.getConst().size(); + bool isSameFix = isRev ? i.getConst().rstrncmp(j.getConst(), len_short): i.getConst().strncmp(j.getConst(), len_short); + if( isSameFix ) { + //same prefix/suffix + //k is the index of the string that is shorter + Node nk = i.getConst().size() < j.getConst().size() ? i : j; + Node nl = i.getConst().size() < j.getConst().size() ? j : i; + Node remainderStr; + if(isRev) { + int new_len = nl.getConst().size() - len_short; + remainderStr = NodeManager::currentNM()->mkConst( nl.getConst().substr(0, new_len) ); + Trace("strings-solve-debug-test") << "Rev. Break normal form of " << nl << " into " << nk << ", " << remainderStr << std::endl; + } else { + remainderStr = NodeManager::currentNM()->mkConst( j.getConst().substr(len_short) ); + Trace("strings-solve-debug-test") << "Break normal form of " << nl << " into " << nk << ", " << remainderStr << std::endl; + } + if( i.getConst().size() < j.getConst().size() ) { + nfj.insert( nfj.begin() + index + 1, remainderStr ); + nfj[index] = nfi[index]; + } else { + nfi.insert( nfi.begin() + index + 1, remainderStr ); + nfi[index] = nfj[index]; + } + } else { + return 1; + } + } else { + Node li = getLength( i ); + Node lj = getLength( j ); + if( areEqual( li, lj ) && areDisequal( i, j ) ) { + Trace("strings-solve") << "Simple Case 2 : found equal length disequal sub strings " << i << " " << j << std::endl; + //we are done: D-Remove + return 1; + }else{ + return 0; + } + } + } + index++; + } + } + return 0; +} + void TheoryStrings::addNormalFormPair( Node n1, Node n2 ) { if( !isNormalFormPair( n1, n2 ) ){ //Assert( !isNormalFormPair( n1, n2 ) ); @@ -1532,7 +1588,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; + Trace("strings-lemma") << "Strings::Infer " << eq << " from " << eq_exp << " by " << c << std::endl; d_pending.push_back( eq ); d_pending_exp[eq] = eq_exp; d_infer.push_back(eq); @@ -1844,7 +1900,7 @@ bool TheoryStrings::checkNormalForms() { Trace("strings-solve") << " against "; printConcat( d_normal_forms[cols[i][k]], "strings-solve" ); Trace("strings-solve") << "..." << std::endl; - if( normalizeDisequality( cols[i][j], cols[i][k] ) ){ + if( processDeq( cols[i][j], cols[i][k] ) ){ break; } } diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index e7f875157..1f69c81be 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -211,11 +211,13 @@ private: 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, + 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 isRev ); bool normalizeEquivalenceClass( Node n, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp ); - bool normalizeDisequality( Node n1, Node n2 ); + bool processDeq( Node n1, Node n2 ); + int processReverseDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj ); + int processSimpleDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj, unsigned& index, bool isRev ); bool unrollStar( Node atom ); bool checkLengths();