diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-09-27 17:52:51 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-09-27 17:52:51 -0400 |
commit | b72ebc42011e4d55b28b807d362694447448c4e8 (patch) | |
tree | a0fd1285a5fdd17b65f43658b33f9e22d70d50af /src/theory/strings/theory_strings.cpp | |
parent | e277b4d220a1d15ac32f6e4fc5f06e88f55b7f68 (diff) | |
parent | a1b32a49ef01d61bb82936f13cb76c5efa4bb42f (diff) |
Merge branch 'master' of github.com:tiliang/CVC4
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 1350 |
1 files changed, 888 insertions, 462 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 33bee4135..7d5edd0f7 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -23,8 +23,11 @@ #include "theory/model.h" #include "smt/logic_exception.h" #include "theory/strings/options.h" +#include "theory/strings/type_enumerator.h" #include <cmath> +#define STR_UNROLL_INDUCTION + using namespace std; using namespace CVC4::context; @@ -43,7 +46,10 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu d_ind_map1(c), d_ind_map2(c), d_ind_map_exp(c), - d_ind_map_lemma(c) + d_ind_map_lemma(c), + //d_lit_to_decide_index( c, 0 ), + //d_lit_to_decide( c ), + d_lit_to_unroll( c ) { // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP); @@ -60,6 +66,46 @@ TheoryStrings::~TheoryStrings() { } +Node TheoryStrings::getRepresentative( Node t ) { + if( d_equalityEngine.hasTerm( t ) ){ + return d_equalityEngine.getRepresentative( t ); + }else{ + return t; + } +} + +bool TheoryStrings::hasTerm( Node a ){ + return d_equalityEngine.hasTerm( a ); +} + +bool TheoryStrings::areEqual( Node a, Node b ){ + if( a==b ){ + return true; + }else if( hasTerm( a ) && hasTerm( b ) ){ + return d_equalityEngine.areEqual( a, b ); + }else{ + return false; + } +} + +bool TheoryStrings::areDisequal( Node a, Node b ){ + if( hasTerm( a ) && hasTerm( b ) ){ + return d_equalityEngine.areDisequal( a, b, false ); + }else{ + return false; + } +} + +Node TheoryStrings::getLength( Node t ) { + EqcInfo * ei = getOrMakeEqcInfo( t ); + Node length_term = ei->d_length_term; + if( length_term.isNull()) { + //typically shouldnt be necessary + length_term = t; + } + return NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, length_term ); +} + void TheoryStrings::setMasterEqualityEngine(eq::EqualityEngine* eq) { d_equalityEngine.setMasterEqualityEngine(eq); } @@ -71,6 +117,20 @@ void TheoryStrings::addSharedTerm(TNode t) { Debug("strings") << "TheoryStrings::addSharedTerm() finished" << std::endl; } +EqualityStatus TheoryStrings::getEqualityStatus(TNode a, TNode b) { + if( d_equalityEngine.hasTerm(a) && d_equalityEngine.hasTerm(b) ){ + if (d_equalityEngine.areEqual(a, b)) { + // The terms are implied to be equal + return EQUALITY_TRUE; + } + if (d_equalityEngine.areDisequal(a, b, false)) { + // The terms are implied to be dis-equal + return EQUALITY_FALSE; + } + } + return EQUALITY_UNKNOWN; +} + void TheoryStrings::propagate(Effort e) { // direct propagation now @@ -108,7 +168,7 @@ Node TheoryStrings::explain( TNode literal ){ std::vector< TNode > assumptions; explain( literal, assumptions ); if( assumptions.empty() ){ - return NodeManager::currentNM()->mkConst( true ); + return d_true; }else if( assumptions.size()==1 ){ return assumptions[0]; }else{ @@ -122,33 +182,114 @@ Node TheoryStrings::explain( TNode literal ){ void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) { - /* + Trace("strings-model") << "TheoryStrings : Collect model info, fullModel = " << fullModel << std::endl; + Trace("strings-model") << "TheoryStrings : assertEqualityEngine." << std::endl; + m->assertEqualityEngine( &d_equalityEngine ); // Generate model - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); - while( !eqcs_i.isFinished() ) { - Node eqc = (*eqcs_i); - //if eqc.getType is string - if (eqc.getType().isString()) { - EqcInfo* ei = getOrMakeEqcInfo( eqc ); + std::vector< Node > nodes; + getEquivalenceClasses( nodes ); + std::map< Node, Node > processed; + std::vector< std::vector< Node > > col; + std::vector< Node > lts; + seperateByLength( nodes, col, lts ); + //step 1 : get all values for known lengths + std::vector< Node > lts_values; + //std::map< Node, bool > values_used; + for( unsigned i=0; i<col.size(); i++ ){ + Trace("strings-model") << "Checking length for " << col[i][0] << " (length is " << lts[i] << ")" << std::endl; + if( lts[i].isConst() ){ + lts_values.push_back( lts[i] ); + //values_used[ lts[i] ] = true; + }else{ + //get value for lts[i]; + if( !lts[i].isNull() ){ + Node v = d_valuation.getModelValue(lts[i]); + //Node v = m->getValue(lts[i]); + Trace("strings-model") << "Model value for " << lts[i] << " is " << v << std::endl; + lts_values.push_back( v ); + //values_used[ v ] = true; + }else{ + Trace("strings-model-warn") << "No length for eqc " << col[i][0] << std::endl; + Assert( false ); + lts_values.push_back( Node::null() ); + } + } + } + ////step 2 : assign arbitrary values for unknown lengths? + //for( unsigned i=0; i<col.size(); i++ ){ + // if( + //} + Trace("strings-model") << "Assign to equivalence classes..." << std::endl; + //step 3 : assign values to equivalence classes that are pure variables + for( unsigned i=0; i<col.size(); i++ ){ + std::vector< Node > pure_eq; + Trace("strings-model") << "The equivalence classes "; + for( unsigned j=0; j<col[i].size(); j++ ) { + Trace("strings-model") << col[i][j] << " "; + //check if col[i][j] has only variables + EqcInfo* ei = getOrMakeEqcInfo( col[i][j], false ); Node cst = ei ? ei->d_const_term : Node::null(); - if( !cst.isNull() ){ - //print out - Trace("strings-model-debug") << cst << std::endl; - }else{ - //is there a length term? - // is there a value for it? if so, assign a constant via enumerator - // otherwise: error - //otherwise: assign a new unique length, then assign a constant via enumerator - } - }else{ - //should be length eqc - //if no constant, error - } - - ++eqcs_i; - } -*/ - //TODO: not done + if( cst.isNull() ){ + Assert( d_normal_forms.find( col[i][j] )!=d_normal_forms.end() ); + if( d_normal_forms[col[i][j]].size()==1 ){//&& d_normal_forms[col[i][j]][0]==col[i][j] ){ + pure_eq.push_back( col[i][j] ); + } + }else{ + processed[col[i][j]] = cst; + } + } + Trace("strings-model") << "have length " << lts_values[i] << std::endl; + + Trace("strings-model") << "Need to assign values of length " << lts_values[i] << " to equivalence classes "; + for( unsigned j=0; j<pure_eq.size(); j++ ){ + Trace("strings-model") << pure_eq[j] << " "; + } + Trace("strings-model") << std::endl; + + //use type enumerator + StringEnumeratorLength sel(lts_values[i].getConst<Rational>().getNumerator().toUnsignedInt()); + for( unsigned j=0; j<pure_eq.size(); j++ ){ + Assert( !sel.isFinished() ); + Node c = *sel; + while( d_equalityEngine.hasTerm( c ) ){ + ++sel; + Assert( !sel.isFinished() ); + c = *sel; + } + ++sel; + Trace("strings-model") << "*** Assigned constant " << c << " for " << pure_eq[j] << std::endl; + processed[pure_eq[j]] = c; + m->assertEquality( pure_eq[j], c, true ); + } + } + Trace("strings-model") << "String Model : Finished." << std::endl; + //step 4 : assign constants to all other equivalence classes + for( unsigned i=0; i<nodes.size(); i++ ){ + if( processed.find( nodes[i] )==processed.end() ){ + Assert( d_normal_forms.find( nodes[i] )!=d_normal_forms.end() ); + Trace("strings-model") << "Construct model for " << nodes[i] << " based on normal form "; + for( unsigned j=0; j<d_normal_forms[nodes[i]].size(); j++ ) { + if( j>0 ) Trace("strings-model") << " ++ "; + Trace("strings-model") << d_normal_forms[nodes[i]][j]; + Node r = getRepresentative( d_normal_forms[nodes[i]][j] ); + if( !r.isConst() && processed.find( r )==processed.end() ){ + Trace("strings-model") << "(UNPROCESSED)"; + } + } + Trace("strings-model") << std::endl; + std::vector< Node > nc; + for( unsigned j=0; j<d_normal_forms[nodes[i]].size(); j++ ) { + Node r = getRepresentative( d_normal_forms[nodes[i]][j] ); + Assert( r.isConst() || processed.find( r )!=processed.end() ); + nc.push_back(r.isConst() ? r : processed[r]); + } + Node cc = mkConcat( nc ); + Assert( cc.getKind()==kind::CONST_STRING ); + Trace("strings-model") << "*** Determined constant " << cc << " for " << nodes[i] << std::endl; + processed[nodes[i]] = cc; + m->assertEquality( nodes[i], cc, true ); + } + } } ///////////////////////////////////////////////////////////////////////////// @@ -167,11 +308,12 @@ void TheoryStrings::preRegisterTerm(TNode n) { break; default: if(n.getKind() == kind::VARIABLE || n.getKind()==kind::SKOLEM) { - Node n_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n); - Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational( 0 ) ); - Node n_len_geq_zero = NodeManager::currentNM()->mkNode( kind::GEQ, n_len, zero); - Trace("strings-lemma") << "Strings: Add lemma " << n_len_geq_zero << std::endl; - d_out->lemma(n_len_geq_zero); + 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_geq_zero = NodeManager::currentNM()->mkNode( kind::GEQ, n_len, d_zero); + Trace("strings-lemma") << "Strings: Add lemma " << n_len_geq_zero << std::endl; + d_out->lemma(n_len_geq_zero); + } } if (n.getType().isBoolean()) { // Get triggered for both equal and dis-equal @@ -184,22 +326,14 @@ void TheoryStrings::preRegisterTerm(TNode n) { } } -void TheoryStrings::dealPositiveWordEquation(TNode n) { - Trace("strings-pwe") << "Deal Positive Word Equation: " << n << endl; - Node node = n; - - // length left = length right - //Node n_left = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, n[0]); - //Node n_right = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, n[1]); - if(node[0].getKind() == kind::CONST_STRING) { - } else if(node[0].getKind() == kind::STRING_CONCAT) { - } -} - void TheoryStrings::check(Effort e) { bool polarity; TNode atom; + if( !done() && !hasTerm( d_emptyString ) ){ + preRegisterTerm( d_emptyString ); + } + // Trace("strings-process") << "Theory of strings, check : " << e << std::endl; Trace("strings-check") << "Theory of strings, check : " << e << std::endl; while ( !done() && !d_conflict) @@ -213,33 +347,16 @@ void TheoryStrings::check(Effort e) { polarity = fact.getKind() != kind::NOT; atom = polarity ? fact : fact[0]; if (atom.getKind() == kind::EQUAL) { - //head - //if(atom[0].getKind() == kind::CONST_STRING) { - //if(atom[1].getKind() == kind::STRING_CONCAT) { - //} - //} - //tail d_equalityEngine.assertEquality(atom, polarity, fact); } else { d_equalityEngine.assertPredicate(atom, polarity, fact); } - switch(atom.getKind()) { - case kind::EQUAL: - if(polarity) { - //if(atom[0].isString() && atom[1].isString()) { - //dealPositiveWordEquation(atom); - //} - } else { - // TODO: Word Equation negaitive - } - break; - case kind::STRING_IN_REGEXP: - // TODO: membership - break; - default: - //possibly error - break; - } +#ifdef STR_UNROLL_INDUCTION + //check if it is a literal to unroll? + if( d_lit_to_unroll.find( atom )!=d_lit_to_unroll.end() ){ + Trace("strings-ind") << "Strings-ind : Possibly unroll for : " << atom << ", polarity = " << polarity << std::endl; + } +#endif } doPendingFacts(); @@ -266,6 +383,7 @@ void TheoryStrings::check(Effort e) { 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: Add lemma " << eq << std::endl; @@ -298,10 +416,13 @@ void TheoryStrings::check(Effort e) { } if( !addedLemma ){ addedLemma = checkNormalForms(); + Trace("strings-process") << "Done check normal forms, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; if(!d_conflict && !addedLemma) { addedLemma = checkCardinality(); + Trace("strings-process") << "Done check cardinality, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; if( !d_conflict && !addedLemma ){ addedLemma = checkInductiveEquations(); + Trace("strings-process") << "Done check inductive equations, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; } } } @@ -386,7 +507,6 @@ void TheoryStrings::eqNotifyPreMerge(TNode t1, TNode t2){ Node n = (*eqc_i); if( n.getKind()==kind::STRING_LENGTH ){ if( !hasTerm( d_emptyString ) || !areEqual(n[0], d_emptyString ) ){ - Trace("strings-debug") << "Processing possible inference." << n << std::endl; //apply the rule length(n[0])==0 => n[0] == "" Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, n[0], d_emptyString ); d_pending.push_back( eq ); @@ -426,7 +546,9 @@ void TheoryStrings::doPendingFacts() { bool polarity = fact.getKind() != kind::NOT; TNode atom = polarity ? fact : fact[0]; if (atom.getKind() == kind::EQUAL) { - d_equalityEngine.assertEquality( atom, polarity, exp ); + Assert( d_equalityEngine.hasTerm( atom[0] ) ); + Assert( d_equalityEngine.hasTerm( atom[1] ) ); + d_equalityEngine.assertEquality( atom, polarity, exp ); }else{ d_equalityEngine.assertPredicate( atom, polarity, exp ); } @@ -435,6 +557,20 @@ void TheoryStrings::doPendingFacts() { d_pending.clear(); d_pending_exp.clear(); } +void TheoryStrings::doPendingLemmas() { + if( !d_conflict && !d_lemma_cache.empty() ){ + for( unsigned i=0; i<d_lemma_cache.size(); i++ ){ + Trace("strings-pending") << "Process pending lemma : " << d_lemma_cache[i] << std::endl; + d_out->lemma( d_lemma_cache[i] ); + } + for( std::map< Node, bool >::iterator it = d_pending_req_phase.begin(); it != d_pending_req_phase.end(); ++it ){ + Trace("strings-pending") << "Require phase : " << it->first << ", polarity = " << it->second << std::endl; + d_out->requirePhase( it->first, it->second ); + } + d_lemma_cache.clear(); + d_pending_req_phase.clear(); + } +} void TheoryStrings::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, std::vector< Node > &normal_form_src) { @@ -519,15 +655,19 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v //nf.push_back( eqc ); if( eqc.getKind()==kind::STRING_CONCAT ){ for( unsigned i=0; i<eqc.getNumChildren(); i++ ){ - nf.push_back( eqc[i] ); + if( !d_equalityEngine.hasTerm(d_emptyString) || !d_equalityEngine.areEqual( eqc[i], d_emptyString ) ){ + nf.push_back( eqc[i] ); + } } - }else{ + }else if( !d_equalityEngine.hasTerm(d_emptyString) || !d_equalityEngine.areEqual( eqc, d_emptyString ) ){ nf.push_back( eqc ); } Trace("strings-process") << "Return process equivalence class " << eqc << " : already visited." << std::endl; } else if (d_equalityEngine.hasTerm(d_emptyString) && d_equalityEngine.areEqual( eqc, d_emptyString )){ //do nothing Trace("strings-process") << "Return process equivalence class " << eqc << " : empty." << std::endl; + d_normal_forms[eqc].clear(); + d_normal_forms_exp[eqc].clear(); } else { visited.push_back( eqc ); if(d_normal_forms.find(eqc)==d_normal_forms.end() ){ @@ -547,10 +687,7 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v unsigned i = 0; //unify each normal form > 0 with normal_forms[0] for( unsigned j=1; j<normal_forms.size(); j++ ) { - std::vector< Node > loop_eqs_x; - std::vector< Node > loop_eqs_y; - std::vector< Node > loop_eqs_z; - std::vector< Node > loop_exps; + Trace("strings-solve") << "Process normal form #0 against #" << j << "..." << std::endl; if( isNormalFormPair( normal_form_src[i], normal_form_src[j] ) ){ Trace("strings-solve") << "Already normalized (in cache)." << std::endl; @@ -573,10 +710,6 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v 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] ); - //add loop equations that we've accumulated - for( unsigned r=0; r<loop_eqs_x.size(); r++ ){ - addInductiveEquation( loop_eqs_x[r], loop_eqs_y[r], loop_eqs_z[r], loop_exps[r] ); - } }else{ //the remainder must be empty unsigned k = index_i==normal_forms[i].size() ? j : i; @@ -585,7 +718,7 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v //can infer that this string must be empty Node eq_exp; if( curr_exp.empty() ) { - eq_exp = NodeManager::currentNM()->mkConst(true); + eq_exp = d_true; } else if( curr_exp.size() == 1 ) { eq_exp = curr_exp[0]; } else { @@ -593,7 +726,7 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v } Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, d_emptyString, normal_forms[k][index_k] ); Trace("strings-lemma") << "Strings : Infer " << eq << " from " << eq_exp << std::endl; - //d_equalityEngine.assertEquality( eq, true, eq_exp ); + Assert( !d_equalityEngine.areEqual( d_emptyString, normal_forms[k][index_k] ) ); d_pending.push_back( eq ); d_pending_exp[eq] = eq_exp; d_infer.push_back(eq); @@ -616,19 +749,8 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v index_i++; success = true; }else{ - EqcInfo * ei = getOrMakeEqcInfo( normal_forms[i][index_i] ); - Node length_term_i = ei->d_length_term; - if( length_term_i.isNull()) { - //typically shouldnt be necessary - length_term_i = normal_forms[i][index_i]; - } - length_term_i = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, length_term_i ); - EqcInfo * ej = getOrMakeEqcInfo( normal_forms[j][index_j] ); - Node length_term_j = ej->d_length_term; - if( length_term_j.isNull()) { - length_term_j = normal_forms[j][index_j]; - } - length_term_j = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, length_term_j ); + Node length_term_i = getLength( normal_forms[i][index_i] ); + Node length_term_j = getLength( normal_forms[j][index_j] ); //check if length(normal_forms[i][index]) == length(normal_forms[j][index]) if( areEqual(length_term_i, length_term_j) ){ Trace("strings-solve-debug") << "Case 2 : string lengths are equal" << std::endl; @@ -637,7 +759,7 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v std::vector< Node > temp_exp; temp_exp.insert(temp_exp.end(), curr_exp.begin(), curr_exp.end() ); temp_exp.push_back(NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j )); - Node eq_exp = temp_exp.empty() ? NodeManager::currentNM()->mkConst(true) : + 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; //d_equalityEngine.assertEquality( eq, true, eq_exp ); @@ -646,17 +768,34 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v d_infer.push_back(eq); d_infer_exp.push_back(eq_exp); return; - }else{ - Trace("strings-solve-debug") << "Case 3 : must compare strings" << std::endl; - bool sendLemma = false; - Node loop_x; - Node loop_y; - Node loop_z; + }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 > antec_new_lits; + 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<normal_forms[k].size(); index_l++ ){ + eqnc.push_back( normal_forms[k][index_l] ); + } + eqn.push_back( mkConcat( eqnc ) ); + } + conc = eqn[0].eqNode( eqn[1] ); + Node ant = mkExplain( antec, antec_new_lits ); + sendLemma( ant, conc, "Endpoint" ); + return; + }else{ + Trace("strings-solve-debug") << "Case 4 : must compare strings" << std::endl; Node conc; std::vector< Node > antec; std::vector< Node > antec_new_lits; //check for loops - Trace("strings-loop") << "Check for loops i,j = " << (index_i+1) << "/" << normal_forms[i].size() << " " << (index_j+1) << "/" << normal_forms[j].size() << std::endl; + //Trace("strings-loop") << "Check for loops i,j = " << (index_i+1) << "/" << normal_forms[i].size() << " " << (index_j+1) << "/" << normal_forms[j].size() << std::endl; int has_loop[2] = { -1, -1 }; for( unsigned r=0; r<2; r++ ){ int index = (r==0 ? index_i : index_j); @@ -680,128 +819,88 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v int other_index = has_loop[0]!=-1 ? index_j : index_i; Trace("strings-loop") << "Detected possible loop for " << normal_forms[loop_n_index][loop_index]; Trace("strings-loop") << " ... " << normal_forms[other_n_index][other_index] << std::endl; + //we have x * s1 * .... * sm = t1 * ... * tn * x * r1 * ... * rp //check if - //t1 * ... * tn = n[loop_n_index][index]....n[loop_n_index][loop_lindex-1] = y * z + //t1 * ... * tn = n[loop_n_index][index]....n[loop_n_index][loop_index-1] = y * z // and //s1 * ... * sk = n[other_n_index][other_index+1].....n[other_n_index][k+1] = z * y // for some y,z,k - int found_size_y = -1; - for( int size_y = 0; size_y<(loop_index-index); size_y++ ){ - int size_z = (loop_index-index)-size_y; - bool success = true; - //check for z - for( int r = 0; r<size_z; r++ ){ - if( other_index+1+r >= (int)normal_forms[other_n_index].size() || - normal_forms[other_n_index][other_index+1+r]!=normal_forms[loop_n_index][index+size_y+r] ) { - success = false; - break; - } - } - //check for y - if( success ){ - for( int r=0; r<size_y; r++ ){ - if( other_index+1+r >= (int)normal_forms[other_n_index].size() || - normal_forms[other_n_index][other_index+1+size_y+r]!=normal_forms[loop_n_index][index+r] ) { - success = false; - break; - } - } - if( success ){ - found_size_y = size_y; - break; - } - } - } - if( found_size_y==-1 ){ - //need to break - Node sk_y= NodeManager::currentNM()->mkSkolem( "ldssym_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); - Node sk_z= NodeManager::currentNM()->mkSkolem( "ldssym_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); - sendLemma = true; - antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); - //t1 * ... * tn = y * z - std::vector< Node > c1c; - //n[loop_n_index][index]....n[loop_n_index][loop_lindex-1] - for( int r=index; r<=loop_index-1; r++ ) { - c1c.push_back( normal_forms[loop_n_index][r] ); - } - Node conc1 = c1c.size()>1 ? NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, c1c ) : - c1c.size()==1 ? c1c[0] : d_emptyString; - conc1 = NodeManager::currentNM()->mkNode( kind::EQUAL, conc1, - NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk_y, sk_z ) ); - std::vector< Node > c2c; - //s1 * ... * sk = n[other_n_index][other_index+1].....n[other_n_index][k+1] - for( int r=other_index+1; r < (int)normal_forms[other_n_index].size(); r++ ) { - c2c.push_back( normal_forms[other_n_index][r] ); - } - Node left2 = c2c.size()>1 ? NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, c2c ) : - c2c.size()==1 ? c2c[0] : d_emptyString; - std::vector< Node > c3c; - c3c.push_back( sk_z ); - c3c.push_back( sk_y ); - //r1 * ... * rk = n[loop_n_index][loop_index+1]....n[loop_n_index][loop_index-1] - for( int r=loop_index+1; r < (int)normal_forms[loop_n_index].size(); r++ ) { - c3c.push_back( normal_forms[loop_n_index][r] ); - } - Node conc2 = NodeManager::currentNM()->mkNode( kind::EQUAL, left2, - NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, c3c ) ); - Node sk_y_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_y ); - Node sk_z_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_z ); - Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational( 0 ) ); - //Node sk_y_len_geq_zero = NodeManager::currentNM()->mkNode( kind::GEQ, sk_y_len, zero); - //Node sk_z_len_geq_zero = NodeManager::currentNM()->mkNode( kind::GEQ, sk_z_len, zero); - conc = NodeManager::currentNM()->mkNode( kind::AND, conc1, conc2 );//, sk_y_len_geq_zero, sk_z_len_geq_zero ); - loop_x = normal_forms[other_n_index][other_index]; - loop_y = sk_y; - loop_z = sk_z; - //we will be done - addNormalFormPair( normal_form_src[i], normal_form_src[j] ); - } else { - // x = (yz)*y - Trace("strings-loop") << "We have that " << normal_forms[loop_n_index][loop_index] << " = ("; - loop_eqs_x.push_back( normal_forms[loop_n_index][loop_index] ); - for( unsigned r=0; r<2; r++ ){ - //print y - std::vector< Node > yc; - for( int rr = 0; rr<found_size_y; rr++ ){ - if( rr>0 ) Trace("strings-loop") << "."; - Trace("strings-loop") << normal_forms[loop_n_index][index+rr]; - yc.push_back( normal_forms[loop_n_index][index+rr] ); - } - if( r==0 ){ - loop_eqs_y.push_back( mkConcat( yc ) ); - Trace("strings-loop") <<".."; - //print z - int found_size_z = (loop_index-index)-found_size_y; - std::vector< Node > zc; - for( int rr = 0; rr<found_size_z; rr++ ){ - if( rr>0 ) Trace("strings-loop") << "."; - Trace("strings-loop") << normal_forms[loop_n_index][index+found_size_y+rr]; - zc.push_back( normal_forms[loop_n_index][index+found_size_y+rr] ); - } - Trace("strings-loop") << ")*"; - loop_eqs_z.push_back( mkConcat( zc ) ); - } - } - Trace("strings-loop") << std::endl; - if( loop_n_index==(int)i ){ - index_j += (loop_index+1)-index_i; - index_i = loop_index+1; - }else{ - index_i += (loop_index+1)-index_j; - index_j = loop_index+1; - } - success = true; - std::vector< Node > empty_vec; - loop_exps.push_back( mkExplain( antec, empty_vec ) ); - } + Trace("strings-loop") << "Must add lemma." << std::endl; + //need to break + Node sk_y= NodeManager::currentNM()->mkSkolem( "ysym_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); + Node sk_z= NodeManager::currentNM()->mkSkolem( "zsym_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); + + antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); + //require that x is non-empty + Node x_empty = normal_forms[loop_n_index][loop_index].eqNode( d_emptyString ); + x_empty = Rewriter::rewrite( x_empty ); + //if( d_equalityEngine.hasTerm( d_emptyString ) && d_equalityEngine.areDisequal( normal_forms[loop_n_index][loop_index], d_emptyString, true ) ){ + // antec.push_back( x_empty.negate() ); + //}else{ + antec_new_lits.push_back( x_empty.negate() ); + //} + d_pending_req_phase[ x_empty ] = true; + + + //t1 * ... * tn = y * z + std::vector< Node > c1c; + //n[loop_n_index][index]....n[loop_n_index][loop_lindex-1] + for( int r=index; r<=loop_index-1; r++ ) { + c1c.push_back( normal_forms[loop_n_index][r] ); + } + Node conc1 = mkConcat( c1c ); + conc1 = NodeManager::currentNM()->mkNode( kind::EQUAL, conc1, + NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk_y, sk_z ) ); + std::vector< Node > c2c; + //s1 * ... * sk = n[other_n_index][other_index+1].....n[other_n_index][k+1] + for( int r=other_index+1; r < (int)normal_forms[other_n_index].size(); r++ ) { + c2c.push_back( normal_forms[other_n_index][r] ); + } + Node left2 = mkConcat( c2c ); + std::vector< Node > c3c; + c3c.push_back( sk_z ); + c3c.push_back( sk_y ); + //r1 * ... * rk = n[loop_n_index][loop_index+1]....n[loop_n_index][loop_index-1] + for( int r=loop_index+1; r < (int)normal_forms[loop_n_index].size(); r++ ) { + c3c.push_back( normal_forms[loop_n_index][r] ); + } + Node conc2 = NodeManager::currentNM()->mkNode( kind::EQUAL, left2, + mkConcat( c3c ) ); + + Node sk_y_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_y ); + //Node sk_z_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_z ); + //Node len_y_eq_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_y_len, d_zero); + //Node len_z_eq_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_z_len, d_zero); + //Node len_y_eq_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_y, d_emptyString); + //Node zz_imp_yz = NodeManager::currentNM()->mkNode( kind::IMPLIES, len_z_eq_zero, len_y_eq_zero); + + //Node z_neq_empty = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_z, d_emptyString).negate(); + //Node len_x_gt_len_y = NodeManager::currentNM()->mkNode( kind::GT, + // NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, normal_forms[other_n_index][other_index]), + // sk_y_len ); + Node ant = mkExplain( antec, antec_new_lits ); + conc = NodeManager::currentNM()->mkNode( kind::AND, conc1, conc2 );//, x_eq_y_rest );// , z_neq_empty //, len_x_gt_len_y + + //Node x_eq_empty = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[other_n_index][other_index], d_emptyString); + //conc = NodeManager::currentNM()->mkNode( kind::OR, x_eq_empty, conc ); + + //we will be done + addNormalFormPair( normal_form_src[i], normal_form_src[j] ); + sendLemma( ant, conc, "Loop" ); + addInductiveEquation( normal_forms[other_n_index][other_index], sk_y, sk_z, ant, "Loop Induction" ); + return; }else{ - Trace("strings-loop") << "No loops detected." << std::endl; + 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) { - Node const_str = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? normal_forms[i][index_i] : normal_forms[j][index_j]; - Node other_str = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? normal_forms[j][index_j] : normal_forms[i][index_i]; + 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<String>().size() <= other_str.getConst<String>().size() ? const_str.getConst<String>().size() : other_str.getConst<String>().size(); if( const_str.getConst<String>().strncmp(other_str.getConst<String>(), len_short) ) { @@ -811,77 +910,64 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v int index_k = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? index_i : index_j; int l = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? j : i; int index_l = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? index_j : index_i; - Node remainderStr = NodeManager::currentNM()->mkConst( const_str.getConst<String>().substr(len_short) ); - Trace("strings-solve-debug") << "Break normal form of " << normal_forms[l][index_l] << " into " << normal_forms[k][index_k] << ", " << remainderStr << std::endl; + Node remainderStr = NodeManager::currentNM()->mkConst( normal_forms[l][index_l].getConst<String>().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 - sendLemma = true; antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); + Node ant = mkExplain( antec, antec_new_lits ); + sendLemma( ant, conc, "Conflict" ); + return; } } else { Assert( other_str.getKind()!=kind::STRING_CONCAT ); antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); - Node firstChar = const_str.getConst<String>().size() == 1 ? const_str : - NodeManager::currentNM()->mkConst( const_str.getConst<String>().substr(0, 1) ); - //split the string - Node sk = NodeManager::currentNM()->mkSkolem( "ssym_$$", normal_forms[i][index_i].getType(), "created for split" ); - // |sk| >= 0 - Node sk_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk ); - Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational( 0 ) ); - //Node sk_len_geq_zero = NodeManager::currentNM()->mkNode( kind::GEQ, sk_len, zero); - - Node eq1 = NodeManager::currentNM()->mkNode( kind::EQUAL, other_str, d_emptyString ); - Node eq2_m = NodeManager::currentNM()->mkNode( kind::EQUAL, other_str, - NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, firstChar, sk ) ); - Node eq2 = eq2_m;//NodeManager::currentNM()->mkNode( kind::AND, eq2_m, sk_len_geq_zero ); - conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 ); + Node firstChar = const_str.getConst<String>().size() == 1 ? const_str : + NodeManager::currentNM()->mkConst( const_str.getConst<String>().substr(0, 1) ); + //split the string + Node sk = NodeManager::currentNM()->mkSkolem( "ssym_$$", normal_forms[i][index_i].getType(), "created for split" ); + + Node eq1 = NodeManager::currentNM()->mkNode( kind::EQUAL, other_str, d_emptyString ); + Node eq2_m = NodeManager::currentNM()->mkNode( kind::EQUAL, other_str, + NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, firstChar, sk ) ); + Node eq2 = eq2_m;//NodeManager::currentNM()->mkNode( kind::AND, eq2_m, sk_len_geq_zero ); + conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 ); Trace("strings-solve-debug") << "Break normal form constant/variable " << std::endl; - sendLemma = true; + + Node ant = mkExplain( antec, antec_new_lits ); + sendLemma( ant, conc, "Constant Split" ); + return; } }else{ 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); - } - Node sk = NodeManager::currentNM()->mkSkolem( "ssym_$$", normal_forms[i][index_i].getType(), "created for split" ); - Node eq1 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[i][index_i], - NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[j][index_j], sk ) ); - Node eq2 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[j][index_j], - NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[i][index_i], sk ) ); - conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 ); - sendLemma = true; - // |sk| > 0 - Node sk_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk ); - Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational( 0 ) ); - Node sk_gt_zero = NodeManager::currentNM()->mkNode( kind::GT, sk_len, zero); - Trace("strings-lemma") << "Strings lemma : " << sk_gt_zero << std::endl; - //d_out->lemma(sk_gt_zero); - d_lemma_cache.push_back( sk_gt_zero ); - } - } - Trace("strings-solve-debug2") << "sendLemma/success : " << sendLemma << " " << success << std::endl; - if( sendLemma ){ - Node ant = mkExplain( antec, antec_new_lits ); - if( conc.isNull() ){ - d_out->conflict(ant); - Trace("strings-conflict") << "Strings conflict : " << ant << std::endl; - d_conflict = true; - }else{ - Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, ant, conc ); - Trace("strings-lemma") << "Strings compare lemma : " << lem << std::endl; - //d_out->lemma(lem); - d_lemma_cache.push_back( lem ); - } - if( !loop_y.isNull() ){ - addInductiveEquation( loop_x, loop_y, loop_z, ant ); + + 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); + } + Node sk = NodeManager::currentNM()->mkSkolem( "ssym_$$", normal_forms[i][index_i].getType(), "created for split" ); + Node eq1 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[i][index_i], + NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[j][index_j], sk ) ); + Node eq2 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[j][index_j], + NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[i][index_i], sk ) ); + conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 ); + // |sk| > 0 + //Node sk_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk ); + //Node sk_gt_zero = NodeManager::currentNM()->mkNode( kind::GT, sk_len, d_zero); + Node sk_gt_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, d_emptyString).negate(); + Trace("strings-lemma") << "Strings lemma : " << sk_gt_zero << std::endl; + //d_out->lemma(sk_gt_zero); + d_lemma_cache.push_back( sk_gt_zero ); + + Node ant = mkExplain( antec, antec_new_lits ); + sendLemma( ant, conc, "Split" ); + return; } - return; } } } @@ -918,22 +1004,66 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v visited.pop_back(); } } -bool TheoryStrings::hasTerm( Node a ){ - return d_equalityEngine.hasTerm( a ); -} -bool TheoryStrings::areEqual( Node a, Node b ){ - if( a==b ){ - return true; - }else if( hasTerm( a ) && hasTerm( b ) ){ - return d_equalityEngine.areEqual( a, b ); - }else{ - return false; - } +bool TheoryStrings::normalizeDisequality( Node ni, Node nj ) { + //Assert( areDisequal( ni, nj ) ); + if( d_normal_forms[ni].size()>1 || d_normal_forms[nj].size()>1 ){ + unsigned index = 0; + while( index<d_normal_forms[ni].size() ){ + Node i = d_normal_forms[ni][index]; + Node j = d_normal_forms[nj][index]; + Trace("strings-solve-debug") << "...Processing " << i << " " << j << std::endl; + if( !areEqual( i, j ) ){ + Node li = getLength( i ); + Node lj = getLength( j ); + if( !areEqual(li, lj) ){ + 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 ) ); + std::vector< Node > conc; + Node sk1 = NodeManager::currentNM()->mkSkolem( "w1sym_$$", ni.getType(), "created for disequality normalization" ); + Node sk2 = NodeManager::currentNM()->mkSkolem( "w2sym_$$", ni.getType(), "created for disequality normalization" ); + Node sk3 = NodeManager::currentNM()->mkSkolem( "w3sym_$$", ni.getType(), "created for disequality normalization" ); + Node sk4 = NodeManager::currentNM()->mkSkolem( "w4sym_$$", ni.getType(), "created for disequality normalization" ); + Node sk5 = NodeManager::currentNM()->mkSkolem( "w5sym_$$", ni.getType(), "created for disequality normalization" ); + Node w1w2w3 = NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2, sk3 ); + Node w1w4w5 = NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk4, sk5 ); + Node s_eq_w1w2w3 = NodeManager::currentNM()->mkNode( kind::EQUAL, ni, w1w2w3 ); + conc.push_back( s_eq_w1w2w3 ); + Node t_eq_w1w4w5 = NodeManager::currentNM()->mkNode( kind::EQUAL, nj, w1w4w5 ); + conc.push_back( t_eq_w1w4w5 ); + Node w2_neq_w4 = sk2.eqNode( sk4 ).negate(); + conc.push_back( w2_neq_w4 ); + Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational( 1 ) ); + Node w2_len_one = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2), one); + conc.push_back( w2_len_one ); + Node w4_len_one = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk4), one); + conc.push_back( w4_len_one ); + + //Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2), + // NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk4) ); + //conc.push_back( eq ); + sendLemma( mkExplain( antec, antec_new_lits ), NodeManager::currentNM()->mkNode( kind::AND, conc ), "Disequality Normalize" ); + return true; + }else if( areDisequal( i, j ) ){ + Trace("strings-solve") << "Case 1 : found equal length disequal sub strings " << i << " " << j << std::endl; + //we are done + return false; + } + } + index++; + } + Assert( false ); + } + return false; } void TheoryStrings::addNormalFormPair( Node n1, Node n2 ) { - //Trace("strings-debug") << "add normal form pair. " << n1 << " " << n2 << std::endl; if( !isNormalFormPair( n1, n2 ) ){ NodeList* lst; NodeListMap::iterator nf_i = d_nf_pairs.find( n1 ); @@ -945,11 +1075,17 @@ void TheoryStrings::addNormalFormPair( Node n1, Node n2 ) { lst = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false, ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) ); d_nf_pairs.insertDataFromContextMemory( n1, lst ); + Trace("strings-nf") << "Create cache for " << n1 << std::endl; }else{ lst = (*nf_i).second; } + Trace("strings-nf") << "Add normal form pair : " << n1 << " " << n2 << std::endl; lst->push_back( n2 ); - } + Assert( isNormalFormPair( n1, n2 ) ); + }else{ + Trace("strings-nf-debug") << "Already a normal form pair " << n1 << " " << n2 << std::endl; + } + } bool TheoryStrings::isNormalFormPair( Node n1, Node n2 ) { //TODO: modulo equality? @@ -971,8 +1107,39 @@ bool TheoryStrings::isNormalFormPair2( Node n1, Node n2 ) { return false; } -void TheoryStrings::addInductiveEquation( Node x, Node y, Node z, Node exp ) { +bool TheoryStrings::addInductiveEquation( Node x, Node y, Node z, Node exp, const char * c ) { Trace("strings-solve-debug") << "add inductive equation for " << x << " = (" << y << " " << z << ")* " << y << std::endl; +#ifdef STR_UNROLL_INDUCTION + Node w = NodeManager::currentNM()->mkSkolem( "wsym_$$", x.getType(), "created for induction" ); + Node x_eq_y_w = NodeManager::currentNM()->mkNode( kind::EQUAL, x, + NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, y, w ) ); + Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, x_eq_y_w ); + Trace("strings-lemma") << "Strings " << c << " lemma : " << lem << std::endl; + d_lemma_cache.push_back( lem ); + + //add initial induction + Node lit1 = w.eqNode( d_emptyString ); + lit1 = Rewriter::rewrite( lit1 ); + Node wp = NodeManager::currentNM()->mkSkolem( "wpsym_$$", x.getType(), "created for induction" ); + Node lit2 = w.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, z, y, wp ) ); + lit2 = Rewriter::rewrite( lit2 ); + Node split_lem = NodeManager::currentNM()->mkNode( kind::OR, lit1, lit2 ); + Trace("strings-ind") << "Strings : Lemma " << c << " for unrolling " << split_lem << std::endl; + Trace("strings-lemma") << "Strings : Lemma " << c << " for unrolling " << split_lem << std::endl; + d_lemma_cache.push_back( split_lem ); + + //d_lit_to_decide.push_back( lit1 ); + d_lit_to_unroll[lit2] = true; + d_pending_req_phase[lit1] = true; + d_pending_req_phase[lit2] = false; + + x = w; + std::vector< Node > skc; + skc.push_back( y ); + skc.push_back( z ); + y = d_emptyString; + z = mkConcat( skc ); +#endif NodeListMap::iterator itr_x_y = d_ind_map1.find(x); NodeList* lst1; @@ -1008,10 +1175,38 @@ void TheoryStrings::addInductiveEquation( Node x, Node y, Node z, Node exp ) { lst1->push_back( y ); lst2->push_back( z ); lste->push_back( exp ); +#ifdef STR_UNROLL_INDUCTION + return true; +#else + return false; +#endif +} + +void TheoryStrings::sendLemma( Node ant, Node conc, const char * c ) { + if( conc.isNull() ){ + d_out->conflict(ant); + Trace("strings-conflict") << "CONFLICT : Strings conflict : " << ant << std::endl; + d_conflict = true; + }else{ + Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, ant, conc ); + Trace("strings-lemma") << "Strings " << c << " lemma : " << lem << std::endl; + d_lemma_cache.push_back( lem ); + } +} + +void TheoryStrings::sendSplit( Node a, Node b, const char * c ) { + Node eq = a.eqNode( b ); + eq = Rewriter::rewrite( eq ); + Node neq = NodeManager::currentNM()->mkNode( kind::NOT, eq ); + Node lemma_or = NodeManager::currentNM()->mkNode( kind::OR, eq, neq ); + Trace("strings-lemma") << "Strings " << c << " split lemma : " << lemma_or << std::endl; + d_lemma_cache.push_back(lemma_or); + d_pending_req_phase[eq] = true; } Node TheoryStrings::mkConcat( std::vector< Node >& c ) { - return c.size()>1 ? NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, c ) : ( c.size()==1 ? c[0] : d_emptyString ); + Node cc = c.size()>1 ? NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, c ) : ( c.size()==1 ? c[0] : d_emptyString ); + return Rewriter::rewrite( cc ); } Node TheoryStrings::mkExplain( std::vector< Node >& a, std::vector< Node >& an ) { @@ -1028,176 +1223,228 @@ Node TheoryStrings::mkExplain( std::vector< Node >& a, std::vector< Node >& an ) Assert( hasTerm(a[i][0][1]) ); Assert( d_equalityEngine.areDisequal(a[i][0][0], a[i][0][1], true) ); } + unsigned ps = antec_exp.size(); explain(a[i], antec_exp); - Trace("strings-solve-debug") << "Done." << std::endl; + Trace("strings-solve-debug") << "Done, explanation was : " << std::endl; + for( unsigned j=ps; j<antec_exp.size(); j++ ){ + Trace("strings-solve-debug") << " " << antec_exp[j] << std::endl; + } + Trace("strings-solve-debug") << std::endl; } for( unsigned i=0; i<an.size(); i++ ){ + Trace("strings-solve-debug") << "Add to explanation (new literal) " << an[i] << std::endl; antec_exp.push_back(an[i]); } Node ant; if( antec_exp.empty() ) { - ant = NodeManager::currentNM()->mkConst(true); + ant = d_true; } else if( antec_exp.size()==1 ) { ant = antec_exp[0]; } else { ant = NodeManager::currentNM()->mkNode( kind::AND, antec_exp ); } + ant = Rewriter::rewrite( ant ); return ant; } bool TheoryStrings::checkNormalForms() { Trace("strings-process") << "Normalize equivalence classes...." << std::endl; - eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator( &d_equalityEngine ); - while( !eqcs2_i.isFinished() ){ - Node eqc = (*eqcs2_i); - //if (eqc.getType().isString()) { - eq::EqClassIterator eqc2_i = eq::EqClassIterator( eqc, &d_equalityEngine ); - Trace("strings-eqc") << "Eqc( " << eqc << " ) : "; - while( !eqc2_i.isFinished() ) { - Trace("strings-eqc") << (*eqc2_i) << " "; - ++eqc2_i; + eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator( &d_equalityEngine ); + for( unsigned t=0; t<2; t++ ){ + Trace("strings-eqc") << (t==0 ? "STRINGS:" : "OTHER:") << std::endl; + while( !eqcs2_i.isFinished() ){ + Node eqc = (*eqcs2_i); + bool print = (t==0 && eqc.getType().isString() ) || (t==1 && !eqc.getType().isString() ); + if (print) { + eq::EqClassIterator eqc2_i = eq::EqClassIterator( eqc, &d_equalityEngine ); + Trace("strings-eqc") << "Eqc( " << eqc << " ) : "; + while( !eqc2_i.isFinished() ) { + if( (*eqc2_i)!=eqc ){ + Trace("strings-eqc") << (*eqc2_i) << " "; + } + ++eqc2_i; + } + Trace("strings-eqc") << std::endl; + } + ++eqcs2_i; + } + Trace("strings-eqc") << std::endl; + } + Trace("strings-eqc") << std::endl; + for( NodeListMap::const_iterator it = d_nf_pairs.begin(); it != d_nf_pairs.end(); ++it ){ + NodeList* lst = (*it).second; + NodeList::const_iterator it2 = lst->begin(); + Trace("strings-nf") << (*it).first << " has been unified with "; + while( it2!=lst->end() ){ + Trace("strings-nf") << (*it2); + ++it2; + } + Trace("strings-nf") << std::endl; + } + Trace("strings-nf") << std::endl; + Trace("strings-nf") << "Current inductive equations : " << std::endl; + for( NodeListMap::const_iterator it = d_ind_map1.begin(); it != d_ind_map1.end(); ++it ){ + Node x = (*it).first; + NodeList* lst1 = (*it).second; + NodeList* lst2 = (*d_ind_map2.find(x)).second; + NodeList::const_iterator i1 = lst1->begin(); + NodeList::const_iterator i2 = lst2->begin(); + while( i1!=lst1->end() ){ + Node y = *i1; + Node z = *i2; + Trace("strings-nf") << "Inductive equation : " << x << " = ( " << y << " ++ " << z << " ) * " << y << std::endl; + ++i1; + ++i2; } - Trace("strings-eqc") << std::endl; - //} - ++eqcs2_i; - } + } - bool addedFact = false; + bool addedFact; do { + Trace("strings-process") << "Check Normal Forms........next round" << std::endl; //calculate normal forms for each equivalence class, possibly adding splitting lemmas d_normal_forms.clear(); d_normal_forms_exp.clear(); std::map< Node, Node > nf_to_eqc; std::map< Node, Node > eqc_to_exp; - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); - d_lemma_cache.clear(); - while( !eqcs_i.isFinished() ){ - Node eqc = (*eqcs_i); - //if eqc.getType is string - if (eqc.getType().isString()) { - Trace("strings-process") << "Verify normal forms are the same for " << eqc << std::endl; - std::vector< Node > visited; - std::vector< Node > nf; - std::vector< Node > nf_exp; - normalizeEquivalenceClass(eqc, visited, nf, nf_exp); - if( d_conflict ){ - return true; - }else if ( d_pending.empty() && d_lemma_cache.empty() ){ - Node nf_term; - if( nf.size()==0 ){ - nf_term = d_emptyString; - }else if( nf.size()==1 ) { - nf_term = nf[0]; - } else { - nf_term = NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, nf ); - } - nf_term = Rewriter::rewrite( nf_term ); - Trace("strings-debug") << "Make nf_term_exp..." << std::endl; - Node nf_term_exp = nf_exp.empty() ? NodeManager::currentNM()->mkConst(true) : - nf_exp.size()==1 ? nf_exp[0] : NodeManager::currentNM()->mkNode( kind::AND, nf_exp ); - if( nf_to_eqc.find(nf_term)!=nf_to_eqc.end() ){ - //Trace("strings-debug") << "Merge because of normal form : " << eqc << " and " << nf_to_eqc[nf_term] << " both have normal form " << nf_term << std::endl; - //two equivalence classes have same normal form, merge - Node eq_exp = NodeManager::currentNM()->mkNode( kind::AND, nf_term_exp, eqc_to_exp[nf_to_eqc[nf_term]] ); - Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, eqc, nf_to_eqc[nf_term] ); - Trace("strings-lemma") << "Strings (by normal forms) : Infer " << eq << " from " << eq_exp << std::endl; - //d_equalityEngine.assertEquality( eq, true, eq_exp ); - d_pending.push_back( eq ); - d_pending_exp[eq] = eq_exp; - d_infer.push_back(eq); - d_infer_exp.push_back(eq_exp); - }else{ - nf_to_eqc[nf_term] = eqc; - eqc_to_exp[eqc] = nf_term_exp; - } - } - Trace("strings-process") << "Done verifying normal forms are the same for " << eqc << std::endl; - } - ++eqcs_i; - } + d_lemma_cache.clear(); + d_pending_req_phase.clear(); + //get equivalence classes + std::vector< Node > eqcs; + getEquivalenceClasses( eqcs ); + for( unsigned i=0; i<eqcs.size(); i++ ){ + Node eqc = eqcs[i]; + Trace("strings-process") << "- Verify normal forms are the same for " << eqc << std::endl; + std::vector< Node > visited; + std::vector< Node > nf; + std::vector< Node > nf_exp; + normalizeEquivalenceClass(eqc, visited, nf, nf_exp); + if( d_conflict ){ + return true; + }else if ( d_pending.empty() && d_lemma_cache.empty() ){ + Node nf_term; + if( nf.size()==0 ){ + nf_term = d_emptyString; + }else if( nf.size()==1 ) { + nf_term = nf[0]; + } else { + nf_term = NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, nf ); + } + nf_term = Rewriter::rewrite( nf_term ); + Trace("strings-debug") << "Make nf_term_exp..." << std::endl; + Node nf_term_exp = nf_exp.empty() ? d_true : + nf_exp.size()==1 ? nf_exp[0] : NodeManager::currentNM()->mkNode( kind::AND, nf_exp ); + if( nf_to_eqc.find(nf_term)!=nf_to_eqc.end() ){ + //Trace("strings-debug") << "Merge because of normal form : " << eqc << " and " << nf_to_eqc[nf_term] << " both have normal form " << nf_term << std::endl; + //two equivalence classes have same normal form, merge + Node eq_exp = NodeManager::currentNM()->mkNode( kind::AND, nf_term_exp, eqc_to_exp[nf_to_eqc[nf_term]] ); + Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, eqc, nf_to_eqc[nf_term] ); + Trace("strings-lemma") << "Strings (by normal forms) : Infer " << eq << " from " << eq_exp << std::endl; + //d_equalityEngine.assertEquality( eq, true, eq_exp ); + d_pending.push_back( eq ); + d_pending_exp[eq] = eq_exp; + d_infer.push_back(eq); + d_infer_exp.push_back(eq_exp); + }else{ + nf_to_eqc[nf_term] = eqc; + eqc_to_exp[eqc] = nf_term_exp; + } + } + Trace("strings-process") << "Done verifying normal forms are the same for " << eqc << std::endl; + } + + Trace("strings-nf-debug") << "**** Normal forms are : " << std::endl; + for( std::map< Node, Node >::iterator it = nf_to_eqc.begin(); it != nf_to_eqc.end(); ++it ){ + Trace("strings-nf-debug") << " normal_form(" << it->second << ") = " << it->first << std::endl; + } + Trace("strings-nf-debug") << std::endl; addedFact = !d_pending.empty(); doPendingFacts(); - if( !d_conflict ){ - for( unsigned i=0; i<d_lemma_cache.size(); i++ ){ - Trace("strings-pending") << "Process pending lemma : " << d_lemma_cache[i] << std::endl; - d_out->lemma( d_lemma_cache[i] ); - } - if( !d_lemma_cache.empty() ){ - d_lemma_cache.clear(); - return true; - } - } - } while (!d_conflict && addedFact); - return false; + } while ( !d_conflict && d_lemma_cache.empty() && addedFact ); + + + //process disequalities between equivalence classes + if( !d_conflict && d_lemma_cache.empty() ){ + std::vector< Node > eqcs; + getEquivalenceClasses( eqcs ); + std::vector< std::vector< Node > > cols; + std::vector< Node > lts; + seperateByLength( eqcs, cols, lts ); + for( unsigned i=0; i<cols.size(); i++ ){ + if( cols[i].size()>1 && d_lemma_cache.empty() ){ + Trace("strings-solve") << "- Verify disequalities are processed for "; + printConcat( d_normal_forms[cols[i][0]], "strings-solve" ); + Trace("strings-solve") << "..." << std::endl; + //must ensure that normal forms are disequal + for( unsigned j=1; j<cols[i].size(); j++ ){ + if( !d_equalityEngine.areDisequal( cols[i][0], cols[i][j], false ) ){ + sendSplit( cols[i][0], cols[i][j], "Disequality Normalization" ); + break; + }else{ + Trace("strings-solve") << " against "; + printConcat( d_normal_forms[cols[i][j]], "strings-solve" ); + Trace("strings-solve") << "..." << std::endl; + if( normalizeDisequality( cols[i][0], cols[i][j] ) ){ + break; + } + } + } + } + } + } + + //flush pending lemmas + if( !d_conflict && !d_lemma_cache.empty() ){ + doPendingLemmas(); + return true; + }else{ + return false; + } } bool TheoryStrings::checkCardinality() { int cardinality = options::stringCharCardinality(); Trace("strings-solve-debug2") << "get cardinality: " << cardinality << endl; - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); - unsigned leqc_counter = 0; - std::map< Node, unsigned > eqc_to_leqc; - std::map< unsigned, Node > leqc_to_eqc; - std::map< unsigned, std::vector< Node > > eqc_to_strings; - while( !eqcs_i.isFinished() ){ - Node eqc = (*eqcs_i); - //if eqc.getType is string - if (eqc.getType().isString()) { - EqcInfo* ei = getOrMakeEqcInfo( eqc, true ); - Node lt = ei->d_length_term; - if( !lt.isNull() ){ - lt = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt ); - Node r = d_equalityEngine.getRepresentative( lt ); - if( eqc_to_leqc.find( r )==eqc_to_leqc.end() ){ - eqc_to_leqc[r] = leqc_counter; - leqc_to_eqc[leqc_counter] = r; - leqc_counter++; - } - eqc_to_strings[ eqc_to_leqc[r] ].push_back( eqc ); - }else{ - eqc_to_strings[leqc_counter].push_back( eqc ); - leqc_counter++; - } - } - ++eqcs_i; - } - for( std::map< unsigned, std::vector< Node > >::iterator it = eqc_to_strings.begin(); it != eqc_to_strings.end(); ++it ){ - Node lr = leqc_to_eqc[it->first]; - Trace("string-cardinality") << "Number of strings with length equal to " << lr << " is " << it->second.size() << std::endl; + std::vector< Node > eqcs; + getEquivalenceClasses( eqcs ); + + std::vector< std::vector< Node > > cols; + std::vector< Node > lts; + seperateByLength( eqcs, cols, lts ); + + for( unsigned i = 0; i<cols.size(); ++i ){ + Node lr = lts[i]; + Trace("string-cardinality") << "Number of strings with length equal to " << lr << " is " << cols[i].size() << std::endl; // size > c^k - double k = std::log( it->second.size() ) / log((double) cardinality); + double k = std::log( cols[i].size() ) / log((double) cardinality); unsigned int int_k = (unsigned int)k; Node k_node = NodeManager::currentNM()->mkConst( ::CVC4::Rational( int_k ) ); //double c_k = pow ( (double)cardinality, (double)lr ); - if( it->second.size() > 1 ) { + if( cols[i].size() > 1 ) { bool allDisequal = true; - for( std::vector< Node >::iterator itr1 = it->second.begin(); - itr1 != it->second.end(); ++itr1) { + for( std::vector< Node >::iterator itr1 = cols[i].begin(); + itr1 != cols[i].end(); ++itr1) { for( std::vector< Node >::iterator itr2 = itr1 + 1; - itr2 != it->second.end(); ++itr2) { + itr2 != cols[i].end(); ++itr2) { if(!d_equalityEngine.areDisequal( *itr1, *itr2, false )) { allDisequal = false; // add split lemma - Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, *itr1, *itr2 ); - Node neq = NodeManager::currentNM()->mkNode( kind::NOT, eq ); - Node lemma_or = NodeManager::currentNM()->mkNode( kind::OR, eq, neq ); - Trace("strings-lemma") << "Strings split lemma : " << lemma_or << std::endl; - d_out->lemma(lemma_or); - return true; + sendSplit( *itr1, *itr2, "Cardinality" ); + doPendingLemmas(); + return true; } } } if(allDisequal) { EqcInfo* ei = getOrMakeEqcInfo( lr, true ); - Trace("string-cardinality") << "Previous cardinality used for " << lr << " is " << ei->d_cardinality_lem_k << std::endl; - if( int_k > ei->d_cardinality_lem_k.get() ){ + Trace("string-cardinality") << "Previous cardinality used for " << lr << " is " << ((int)ei->d_cardinality_lem_k.get()-1) << std::endl; + if( int_k+1 > ei->d_cardinality_lem_k.get() ){ //add cardinality lemma - Node dist = NodeManager::currentNM()->mkNode( kind::DISTINCT, it->second ); + Node dist = NodeManager::currentNM()->mkNode( kind::DISTINCT, cols[i] ); std::vector< Node > vec_node; vec_node.push_back( dist ); - for( std::vector< Node >::iterator itr1 = it->second.begin(); - itr1 != it->second.end(); ++itr1) { + for( std::vector< Node >::iterator itr1 = cols[i].begin(); + itr1 != cols[i].end(); ++itr1) { Node len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, *itr1 ); if( len!=lr ){ Node len_eq_lr = NodeManager::currentNM()->mkNode( kind::EQUAL, lr, len ); @@ -1205,13 +1452,24 @@ bool TheoryStrings::checkCardinality() { } } Node antc = NodeManager::currentNM()->mkNode( kind::AND, vec_node ); - Node len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, it->second[0] ); + Node len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, cols[i][0] ); Node cons = NodeManager::currentNM()->mkNode( kind::GT, len, k_node ); + /* + sendLemma( antc, cons, "Cardinality" ); + ei->d_cardinality_lem_k.set( int_k+1 ); + if( !d_lemma_cache.empty() ){ + doPendingLemmas(); + return true; + } + */ Node lemma = NodeManager::currentNM()->mkNode( kind::IMPLIES, antc, cons ); - Trace("strings-lemma") << "Strings cardinaliry lemma : " << lemma << std::endl; - d_out->lemma(lemma); - ei->d_cardinality_lem_k.set( k ); - return true; + lemma = Rewriter::rewrite( lemma ); + ei->d_cardinality_lem_k.set( int_k+1 ); + if( lemma!=d_true ){ + Trace("strings-lemma") << "Strings cardinality lemma : " << lemma << std::endl; + d_out->lemma(lemma); + return true; + } } } } @@ -1219,67 +1477,235 @@ bool TheoryStrings::checkCardinality() { return false; } +int TheoryStrings::gcd ( int a, int b ) { + int c; + while ( a != 0 ) { + c = a; a = b%a; b = c; + } + return b; +} + bool TheoryStrings::checkInductiveEquations() { bool hasEq = false; - Trace("strings-ind") << "We are sat, with these inductive equations : " << std::endl; - for( NodeListMap::const_iterator it = d_ind_map1.begin(); it != d_ind_map1.end(); ++it ){ - Node x = (*it).first; - NodeList* lst1 = (*it).second; - NodeList* lst2 = (*d_ind_map2.find(x)).second; - NodeList* lste = (*d_ind_map_exp.find(x)).second; - NodeList* lstl = (*d_ind_map_lemma.find(x)).second; - NodeList::const_iterator i1 = lst1->begin(); - NodeList::const_iterator i2 = lst2->begin(); - NodeList::const_iterator ie = lste->begin(); - NodeList::const_iterator il = lstl->begin(); - while( i1!=lst1->end() ){ - Node y = *i1; - Node z = *i2; - Node exp = *ie; - Trace("strings-ind") << "Inductive equation : " << x << " = ( " << y << "..." << z << " )* " << y << std::endl; - if( il==lstl->end() ) { - Trace("strings-ind") << "Add length lemma..." << std::endl; - Node lemma_len; - if( y.getKind()!=kind::STRING_CONCAT || z.getKind()!=kind::STRING_CONCAT ) { - Node len_x = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, x ); - Node len_y = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, y ); - lemma_len = NodeManager::currentNM()->mkNode( kind::GEQ, len_x, len_y ); - } else { - // both constants - Node len_x = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, x ); - Node sk = NodeManager::currentNM()->mkSkolem( "argsym_$$", NodeManager::currentNM()->integerType(), "created for length inductive lemma" ); - Node len_y = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, y ); - Node len_z = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, z ); - Node len_y_plus_len_z = NodeManager::currentNM()->mkNode( kind::PLUS, len_y, len_z ); - Node y_p_z_t_a = NodeManager::currentNM()->mkNode( kind::MULT, len_y_plus_len_z, sk ); - Node y_p_z_t_a_p_y = NodeManager::currentNM()->mkNode( kind::PLUS, y_p_z_t_a, len_y ); - lemma_len = NodeManager::currentNM()->mkNode( kind::EQUAL, y_p_z_t_a_p_y, len_x ); - Node sk_geq_zero = NodeManager::currentNM()->mkNode( kind::GEQ, sk, d_zero ); - lemma_len = NodeManager::currentNM()->mkNode( kind::AND, lemma_len, sk_geq_zero ); - } - lemma_len = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, lemma_len ); - Trace("strings-lemma") << "Strings: Add lemma " << lemma_len << std::endl; - d_out->lemma(lemma_len); - lstl->push_back( d_true ); - return true; - } - - ++i1; - ++i2; - ++ie; - ++il; - hasEq = true; - } - } + if(d_ind_map1.size() != 0){ + Trace("strings-ind") << "We are sat, with these inductive equations : " << std::endl; + for( NodeListMap::const_iterator it = d_ind_map1.begin(); it != d_ind_map1.end(); ++it ){ + Node x = (*it).first; + Trace("strings-ind-debug") << "Check eq for " << x << std::endl; + NodeList* lst1 = (*it).second; + NodeList* lst2 = (*d_ind_map2.find(x)).second; + NodeList* lste = (*d_ind_map_exp.find(x)).second; + //NodeList* lstl = (*d_ind_map_lemma.find(x)).second; + NodeList::const_iterator i1 = lst1->begin(); + NodeList::const_iterator i2 = lst2->begin(); + NodeList::const_iterator ie = lste->begin(); + //NodeList::const_iterator il = lstl->begin(); + while( i1!=lst1->end() ){ + Node y = *i1; + Node z = *i2; + //Trace("strings-ind-debug") << "Check y=" << y << " , z=" << z << std::endl; + //if( il==lstl->end() ) { + std::vector< Node > nf_y, nf_z, exp_y, exp_z; + + //getFinalNormalForm( y, nf_y, exp_y); + //getFinalNormalForm( z, nf_z, exp_z); + //std::vector< Node > vec_empty; + //Node nexp_y = mkExplain( exp_y, vec_empty ); + //Trace("strings-ind-debug") << "Check nexp_y=" << nexp_y << std::endl; + //Node nexp_z = mkExplain( exp_z, vec_empty ); + + //Node exp = *ie; + //Trace("strings-ind-debug") << "Check exp=" << exp << std::endl; + + //exp = NodeManager::currentNM()->mkNode( kind::AND, exp, nexp_y, nexp_z ); + //exp = Rewriter::rewrite( exp ); + + Trace("strings-ind") << "Inductive equation : " << x << " = ( " << y << " ++ " << z << " )* " << y << std::endl; + /* + for( std::vector< Node >::const_iterator itr = nf_y.begin(); itr != nf_y.end(); ++itr) { + Trace("strings-ind") << (*itr) << " "; + } + Trace("strings-ind") << " ++ "; + for( std::vector< Node >::const_iterator itr = nf_z.begin(); itr != nf_z.end(); ++itr) { + Trace("strings-ind") << (*itr) << " "; + } + Trace("strings-ind") << " )* "; + for( std::vector< Node >::const_iterator itr = nf_y.begin(); itr != nf_y.end(); ++itr) { + Trace("strings-ind") << (*itr) << " "; + } + Trace("strings-ind") << std::endl; + */ + /* + Trace("strings-ind") << "Explanation is : " << exp << std::endl; + std::vector< Node > nf_yz; + nf_yz.insert( nf_yz.end(), nf_y.begin(), nf_y.end() ); + nf_yz.insert( nf_yz.end(), nf_z.begin(), nf_z.end() ); + std::vector< std::vector< Node > > cols; + std::vector< Node > lts; + seperateByLength( nf_yz, cols, lts ); + Trace("strings-ind") << "This can be grouped into collections : " << std::endl; + for( unsigned j=0; j<cols.size(); j++ ){ + Trace("strings-ind") << " : "; + for( unsigned k=0; k<cols[j].size(); k++ ){ + Trace("strings-ind") << cols[j][k] << " "; + } + Trace("strings-ind") << std::endl; + } + Trace("strings-ind") << std::endl; + + Trace("strings-ind") << "Add length lemma..." << std::endl; + std::vector< int > co; + co.push_back(0); + for(unsigned int k=0; k<lts.size(); ++k) { + if(lts[k].isConst() && lts[k].getType().isInteger()) { + int len = lts[k].getConst<Rational>().getNumerator().toUnsignedInt(); + co[0] += cols[k].size() * len; + } else { + co.push_back( cols[k].size() ); + } + } + int g_co = co[0]; + for(unsigned k=1; k<co.size(); ++k) { + g_co = gcd(g_co, co[k]); + } + Node lemma_len; + // both constants + Node len_x = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, x ); + Node sk = NodeManager::currentNM()->mkSkolem( "argsym_$$", NodeManager::currentNM()->integerType(), "created for length inductive lemma" ); + Node g_co_node = NodeManager::currentNM()->mkConst( CVC4::Rational(g_co) ); + Node sk_m_gcd = NodeManager::currentNM()->mkNode( kind::MULT, g_co_node, sk ); + Node len_y = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, y ); + Node sk_m_g_p_y = NodeManager::currentNM()->mkNode( kind::PLUS, sk_m_gcd, len_y ); + lemma_len = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_m_g_p_y, len_x ); + //Node sk_geq_zero = NodeManager::currentNM()->mkNode( kind::GEQ, sk, d_zero ); + //lemma_len = NodeManager::currentNM()->mkNode( kind::AND, lemma_len, sk_geq_zero ); + lemma_len = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, lemma_len ); + Trace("strings-lemma") << "Strings: Add lemma " << lemma_len << std::endl; + d_out->lemma(lemma_len); + lstl->push_back( d_true ); + return true;*/ + //} + ++i1; + ++i2; + ++ie; + //++il; + if( !d_equalityEngine.hasTerm( d_emptyString ) || !d_equalityEngine.areEqual( y, d_emptyString ) || !d_equalityEngine.areEqual( x, d_emptyString ) ){ + hasEq = true; + } + } + } + } if( hasEq ){ + Trace("strings-ind") << "It is incomplete." << std::endl; d_out->setIncomplete(); - } + }else{ + Trace("strings-ind") << "We can answer SAT." << std::endl; + } return false; } +void TheoryStrings::getEquivalenceClasses( std::vector< Node >& eqcs ) { + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); + while( !eqcs_i.isFinished() ) { + Node eqc = (*eqcs_i); + //if eqc.getType is string + if (eqc.getType().isString()) { + eqcs.push_back( eqc ); + } + ++eqcs_i; + } +} + +void TheoryStrings::getFinalNormalForm( Node n, std::vector< Node >& nf, std::vector< Node >& exp ) { + if( n!=d_emptyString ){ + if( n.getKind()==kind::STRING_CONCAT ){ + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + getFinalNormalForm( n[i], nf, exp ); + } + }else{ + Trace("strings-debug") << "Get final normal form " << n << std::endl; + Assert( d_equalityEngine.hasTerm( n ) ); + Node nr = d_equalityEngine.getRepresentative( n ); + EqcInfo *eqc_n = getOrMakeEqcInfo( nr, false ); + Node nc = eqc_n ? eqc_n->d_const_term.get() : Node::null(); + if( !nc.isNull() ){ + nf.push_back( nc ); + if( n!=nc ){ + exp.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, n, nc ) ); + } + }else{ + Assert( d_normal_forms.find( nr )!=d_normal_forms.end() ); + if( d_normal_forms[nr][0]==nr ){ + Assert( d_normal_forms[nr].size()==1 ); + nf.push_back( nr ); + if( n!=nr ){ + exp.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, n, nr ) ); + } + }else{ + for( unsigned i=0; i<d_normal_forms[nr].size(); i++ ){ + Assert( d_normal_forms[nr][i]!=nr ); + getFinalNormalForm( d_normal_forms[nr][i], nf, exp ); + } + exp.insert( exp.end(), d_normal_forms_exp[nr].begin(), d_normal_forms_exp[nr].end() ); + } + } + Trace("strings-ind-nf") << "The final normal form of " << n << " is " << nf << std::endl; + } + } +} +void TheoryStrings::seperateByLength( std::vector< Node >& n, std::vector< std::vector< Node > >& cols, + std::vector< Node >& lts ) { + unsigned leqc_counter = 0; + std::map< Node, unsigned > eqc_to_leqc; + std::map< unsigned, Node > leqc_to_eqc; + std::map< unsigned, std::vector< Node > > eqc_to_strings; + for( unsigned i=0; i<n.size(); i++ ){ + Node eqc = n[i]; + Assert( d_equalityEngine.getRepresentative(eqc)==eqc ); + EqcInfo* ei = getOrMakeEqcInfo( eqc, false ); + Node lt = ei ? ei->d_length_term : Node::null(); + if( !lt.isNull() ){ + lt = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt ); + Node r = d_equalityEngine.getRepresentative( lt ); + if( eqc_to_leqc.find( r )==eqc_to_leqc.end() ){ + eqc_to_leqc[r] = leqc_counter; + leqc_to_eqc[leqc_counter] = r; + leqc_counter++; + } + eqc_to_strings[ eqc_to_leqc[r] ].push_back( eqc ); + }else{ + eqc_to_strings[leqc_counter].push_back( eqc ); + leqc_counter++; + } + } + for( std::map< unsigned, std::vector< Node > >::iterator it = eqc_to_strings.begin(); it != eqc_to_strings.end(); ++it ){ + std::vector< Node > vec; + vec.insert( vec.end(), it->second.begin(), it->second.end() ); + lts.push_back( leqc_to_eqc[it->first] ); + cols.push_back( vec ); + } +} +void TheoryStrings::printConcat( std::vector< Node >& n, const char * c ) { + for( unsigned i=0; i<n.size(); i++ ){ + if( i>0 ) Trace(c) << " ++ "; + Trace(c) << n[i]; + } +} +/* +Node TheoryStrings::getNextDecisionRequest() { + if( d_lit_to_decide_index.get()<d_lit_to_decide.size() ){ + Node l = d_lit_to_decide[d_lit_to_decide_index.get()]; + d_lit_to_decide_index.set( d_lit_to_decide_index.get() + 1 ); + Trace("strings-ind") << "Strings-ind : decide on " << l << std::endl; + return l; + }else{ + return Node::null(); + } +} +*/ }/* CVC4::theory::strings namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ |