From c36b44a0ae17a721179a2432bc8eb4c6e64a18b8 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Thu, 3 Oct 2013 10:48:25 -0500 Subject: [PATCH] adds some fixes. it solves kaluza problems --- src/theory/strings/theory_strings.cpp | 1221 ++++++++++++++----------- src/theory/strings/theory_strings.h | 16 +- 2 files changed, 705 insertions(+), 532 deletions(-) diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 291af408b..a0058954d 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -96,14 +96,18 @@ bool TheoryStrings::areDisequal( Node a, Node b ){ } } -Node TheoryStrings::getLength( Node t ) { - EqcInfo * ei = getOrMakeEqcInfo( t ); - Node length_term = ei->d_length_term; +Node TheoryStrings::getLengthTerm( Node t ) { + EqcInfo * ei = getOrMakeEqcInfo( t, false ); + Node length_term = ei ? ei->d_length_term : Node::null(); if( length_term.isNull()) { //typically shouldnt be necessary length_term = t; } - return NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, length_term ); + return length_term; +} + +Node TheoryStrings::getLength( Node t ) { + return NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, getLengthTerm( t ) ); } void TheoryStrings::setMasterEqualityEngine(eq::EqualityEngine* eq) { @@ -194,23 +198,29 @@ void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) { seperateByLength( nodes, col, lts ); //step 1 : get all values for known lengths std::vector< Node > lts_values; - //std::map< Node, bool > values_used; + std::map< unsigned, bool > values_used; for( unsigned i=0; i0 ) Trace("strings-model") << ", "; + Trace("strings-model") << col[i][j]; + } + Trace("strings-model") << " } (length is " << lts[i] << ")" << std::endl; if( lts[i].isConst() ){ lts_values.push_back( lts[i] ); - //values_used[ lts[i] ] = true; + unsigned lvalue = lts[i].getConst().getNumerator().toUnsignedInt(); + values_used[ lvalue ] = 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; + unsigned lvalue = v.getConst().getNumerator().toUnsignedInt(); + values_used[ lvalue ] = true; }else{ - Trace("strings-model-warn") << "No length for eqc " << col[i][0] << std::endl; - Assert( false ); + //Trace("strings-model-warn") << "No length for eqc " << col[i][0] << std::endl; + //Assert( false ); lts_values.push_back( Node::null() ); } } @@ -240,26 +250,39 @@ void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) { } 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().getNumerator().toUnsignedInt()); - for( unsigned j=0; jmkConst( Rational( lvalue ) ); + values_used[ lvalue ] = true; + } + Trace("strings-model") << "Need to assign values of length " << lts_values[i] << " to equivalence classes "; + for( unsigned j=0; j().getNumerator().toUnsignedInt()); + for( unsigned j=0; jassertEquality( pure_eq[j], c, true ); } - ++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; @@ -363,65 +386,21 @@ void TheoryStrings::check(Effort e) { bool addedLemma = false; if( e == EFFORT_FULL && !d_conflict ) { - 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, true ); - //get the constant for the equivalence class - //int c_len = ...; - eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); - while( !eqc_i.isFinished() ){ - Node n = (*eqc_i); - //if n is concat, and - //if n has not instantiatied the concat..length axiom - //then, add lemma - if( n.getKind() == kind::STRING_CONCAT || n.getKind() == kind::CONST_STRING ){ - if( d_length_inst.find(n)==d_length_inst.end() ){ - 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 term lemma " << eq << std::endl; - d_out->lemma(eq); - Node skl = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk ); - Node lsum; - if( n.getKind() == kind::STRING_CONCAT ){ - //add lemma - std::vector node_vec; - for( unsigned i=0; imkNode( kind::STRING_LENGTH, n[i] ); - node_vec.push_back(lni); - } - lsum = NodeManager::currentNM()->mkNode( kind::PLUS, node_vec ); - }else{ - //add lemma - lsum = NodeManager::currentNM()->mkConst( ::CVC4::Rational( n.getConst().size() ) ); - } - Node ceq = NodeManager::currentNM()->mkNode( kind::EQUAL, skl, lsum ); - ceq = Rewriter::rewrite(ceq); - Trace("strings-lemma") << "Strings: Add length lemma " << ceq << std::endl; - d_out->lemma(ceq); - addedLemma = true; - } - } - ++eqc_i; - } - } - ++eqcs_i; - } + addedLemma = checkLengths(); + Trace("strings-process") << "Done check (constant) lengths, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; 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; + addedLemma = checkLengthsEqc(); + Trace("strings-process") << "Done check lengths, 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; + } } } } @@ -430,7 +409,7 @@ void TheoryStrings::check(Effort e) { Trace("strings-process") << "Theory of strings, done check : " << e << std::endl; } -TheoryStrings::EqcInfo::EqcInfo( context::Context* c ) : d_const_term(c), d_length_term(c), d_cardinality_lem_k(c) { +TheoryStrings::EqcInfo::EqcInfo( context::Context* c ) : d_const_term(c), d_length_term(c), d_cardinality_lem_k(c), d_normalized_length(c) { } @@ -492,6 +471,9 @@ void TheoryStrings::eqNotifyPreMerge(TNode t1, TNode t2){ if( e2->d_cardinality_lem_k.get()>e1->d_cardinality_lem_k.get() ) { e1->d_cardinality_lem_k.set( e2->d_cardinality_lem_k ); } + if( !e2->d_normalized_length.get().isNull() ){ + e1->d_normalized_length.set( e2->d_normalized_length ); + } } if( hasTerm( d_zero ) ){ Node leqc; @@ -572,16 +554,17 @@ void TheoryStrings::doPendingLemmas() { } } -void TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf, +bool 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) { // EqcItr eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); while( !eqc_i.isFinished() ) { Node n = (*eqc_i); - Trace("strings-process") << "Process term " << n << std::endl; + Trace("strings-process-debug") << "Get Normal Form : Process term " << n << std::endl; if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT ) { std::vector nf_n; std::vector nf_exp_n; + bool result = true; if( n.getKind() == kind::CONST_STRING ){ if( n!=d_emptyString ) { nf_n.push_back( n ); @@ -591,37 +574,88 @@ void TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std Node nr = d_equalityEngine.getRepresentative( n[i] ); std::vector< Node > nf_temp; std::vector< Node > nf_exp_temp; - Trace("strings-process") << "Normalizing subterm " << n[i] << " = " << nr << std::endl; - normalizeEquivalenceClass( nr, visited, nf_temp, nf_exp_temp ); + Trace("strings-process-debug") << "Normalizing subterm " << n[i] << " = " << nr << std::endl; + bool nresult = normalizeEquivalenceClass( nr, visited, nf_temp, nf_exp_temp ); if( d_conflict || !d_pending.empty() || !d_lemma_cache.empty() ) { - return; - } - if( nf.size()!=1 || nf[0]!=d_emptyString ) { - for( unsigned r=0; rmkNode( kind::EQUAL, n[i], nr ) ); + return true; } + //successfully computed normal form + if( nf.size()!=1 || nf[0]!=d_emptyString ) { + for( unsigned r=0; rmkNode( kind::EQUAL, n[i], nr ) ); + } + if( !nresult ){ + //Trace("strings-process-debug") << "....Caused already asserted + for( unsigned j=i+1; j1 ){ + result = false; + break; + } + } } } - normal_forms.push_back(nf_n); - normal_forms_exp.push_back(nf_exp_n); - normal_form_src.push_back(n); + 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 "; + printConcat(nf_n,"strings-process-debug"); + Trace("strings-process-debug") << "..." << std::endl; + for( unsigned i=0; i ant; + if( nf_n[i]!=n ){ + ant.push_back( nf_n[i].eqNode( n ) ); + } + ant.insert( ant.end(), nf_exp_n.begin(), nf_exp_n.end() ); + std::vector< Node > cc; + for( unsigned j=0; j empty_vec; + Node conc = cc.size()==1 ? cc[0] : NodeManager::currentNM()->mkNode( kind::AND, cc ); + sendLemma( mkExplain( ant ), conc, "Component" ); + return true; + } + } + } + if( !result ){ + //we have a normal form that will cause a component lemma at a higher level + normal_forms.clear(); + normal_forms_exp.clear(); + normal_form_src.clear(); + } + normal_forms.push_back(nf_n); + normal_forms_exp.push_back(nf_exp_n); + normal_form_src.push_back(n); + if( !result ){ + return false; + } + }else{ + Node nn = nf_n.size()==0 ? d_emptyString : nf_n[0]; + //Assert( areEqual( nf_n[0], eqc ) ); + if( !areEqual( nn, eqc ) ){ + std::vector< Node > ant; + 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" ); + return true; + } + } } - /* should we add these? - else { - //var/sk? - std::vector nf_n; - std::vector nf_exp_n; - nf_n.push_back(n); - normal_forms.push_back(nf_n); - normal_forms_exp.push_back(nf_exp_n); - normal_form_src.push_back(n); - }*/ ++eqc_i; } @@ -647,29 +681,36 @@ void TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std Trace("strings-solve") << std::endl; } } + return true; } //nf_exp is conjunction -void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp ) { +bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp ) { Trace("strings-process") << "Process equivalence class " << eqc << std::endl; if( std::find( visited.begin(), visited.end(), eqc )!=visited.end() ){ - //nf.push_back( eqc ); + nf.push_back( eqc ); + /* if( eqc.getKind()==kind::STRING_CONCAT ){ for( unsigned i=0; i t = s1 * ... * sn // normal form for each non-variable term in this eqc (s1...sn) @@ -679,337 +720,336 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v // record terms for each normal form (t) std::vector< Node > normal_form_src; //Get Normal Forms - getNormalForms(eqc, visited, nf, normal_forms, normal_forms_exp, normal_form_src); + result = getNormalForms(eqc, visited, nf, normal_forms, normal_forms_exp, normal_form_src); if( d_conflict || !d_pending.empty() || !d_lemma_cache.empty() ) { - return; - } - - unsigned i = 0; - //unify each normal form > 0 with normal_forms[0] - for( unsigned j=1; j curr_exp; - 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] ) ); - //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 - { - 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; - while(!d_conflict && index_kmkNode( kind::AND, curr_exp ); - } - 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; - 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); - d_infer_exp.push_back(eq_exp); - index_k++; - } - } - }else { - Trace("strings-solve-debug") << "Process " << normal_forms[i][index_i] << " ... " << normal_forms[j][index_j] << std::endl; - if(areEqual(normal_forms[i][index_i],normal_forms[j][index_j])){ - Trace("strings-solve-debug") << "Case 1 : strings are equal" << std::endl; - //terms are equal, continue - if( normal_forms[i][index_i]!=normal_forms[j][index_j] ){ - Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL,normal_forms[i][index_i], - normal_forms[j][index_j]); - Trace("strings-solve-debug") << "Add to explanation : " << eq << std::endl; - curr_exp.push_back(eq); - } - index_j++; - index_i++; - success = 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) && - 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 ); - if( !areEqual(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; - }else{ - Trace("strings-solve-debug") << "Case 2.2 : string lengths are explicitly equal" << std::endl; - //lengths are already equal, do unification - Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[i][index_i], normal_forms[j][index_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 ); + return true; + }else if( result ){ + unsigned i = 0; + //unify each normal form > 0 with normal_forms[0] + for( unsigned j=1; j curr_exp; + 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] ) ); + //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 + { + 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; + while(!d_conflict && index_kmkNode( kind::AND, curr_exp ); + } + 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; + 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); d_infer_exp.push_back(eq_exp); - return; - } - }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_lmkNode( kind::EQUAL,normal_forms[i][index_i], + normal_forms[j][index_j]); + Trace("strings-solve-debug") << "Add to explanation : " << eq << std::endl; + curr_exp.push_back(eq); } + index_j++; + index_i++; + success = true; }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; - int has_loop[2] = { -1, -1 }; - for( unsigned r=0; r<2; r++ ){ - int index = (r==0 ? index_i : index_j); - int other_index = (r==0 ? index_j : index_i ); - int n_index = (r==0 ? i : j); - int other_n_index = (r==0 ? j : i); - if( normal_forms[other_n_index][other_index].getKind() != kind::CONST_STRING ) { - for( unsigned lp = index+1; lpmkNode( kind::EQUAL, length_term_i, length_term_j ); + if( !areEqual(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{ + Trace("strings-solve-debug") << "Case 2.2 : string lengths are explicitly equal" << std::endl; + //lengths are already equal, do unification + Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[i][index_i], normal_forms[j][index_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; + d_pending.push_back( eq ); + d_pending_exp[eq] = eq_exp; + d_infer.push_back(eq); + d_infer_exp.push_back(eq_exp); + return true; } - Trace("strings-loop") << std::endl; - Trace("strings-loop") << " ... R= "; - for(int lp=loop_index+1; lp<(int)normal_forms[loop_n_index].size(); ++lp) { - if(lp != loop_index+1) Trace("strings-loop") << " ++ "; - Trace("strings-loop") << normal_forms[loop_n_index][lp]; - } - Trace("strings-loop") << 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_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 - - 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" ); - + }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() ); - //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] ); + 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_lmkNode( 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] ); + if( areEqual( eqn[0], eqn[1] ) ){ + addNormalFormPair( normal_form_src[i], normal_form_src[j] ); + }else{ + conc = eqn[0].eqNode( eqn[1] ); + Node ant = mkExplain( antec, antec_new_lits ); + sendLemma( ant, conc, "Endpoint" ); + return true; } - 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] ); + }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; + int has_loop[2] = { -1, -1 }; + for( unsigned r=0; r<2; r++ ){ + int index = (r==0 ? index_i : index_j); + int other_index = (r==0 ? index_j : index_i ); + int n_index = (r==0 ? i : j); + int other_n_index = (r==0 ? j : i); + if( normal_forms[other_n_index][other_index].getKind() != kind::CONST_STRING ) { + for( unsigned lp = index+1; lpmkNode( 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-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() ); + if( has_loop[0]!=-1 || has_loop[1]!=-1 ){ + int loop_n_index = has_loop[0]!=-1 ? i : j; + int other_n_index = has_loop[0]!=-1 ? j : i; + int loop_index = has_loop[0]!=-1 ? has_loop[0] : has_loop[1]; + int index = has_loop[0]!=-1 ? index_i : index_j; + 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") << " ... (X)= " << normal_forms[other_n_index][other_index] << std::endl; + + Trace("strings-loop") << " ... T(Y.Z)= "; + for(int lp=index; lpmkSkolem( "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 true; + }else{ + 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, antec_new_lits ); + sendLemma( ant, conc, "Conflict" ); + return true; + } + } else { + Assert( other_str.getKind()!=kind::STRING_CONCAT ); + 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 sk = NodeManager::currentNM()->mkSkolem( "ssym_$$", normal_forms[i][index_i].getType(), "created for v/c split" ); + + Node eq1 = NodeManager::currentNM()->mkNode( kind::EQUAL, other_str, d_emptyString ); + Node eq2 = NodeManager::currentNM()->mkNode( kind::EQUAL, other_str, + NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, firstChar, sk ) ); + 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, "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().size() == 1 ? const_str : - NodeManager::currentNM()->mkConst( const_str.getConst().substr(0, 1) ); - //split the string - Node sk = NodeManager::currentNM()->mkSkolem( "ssym_$$", normal_forms[i][index_i].getType(), "created for v/c split" ); - - Node eq1 = NodeManager::currentNM()->mkNode( kind::EQUAL, other_str, d_emptyString ); - Node eq2 = NodeManager::currentNM()->mkNode( kind::EQUAL, other_str, - NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, firstChar, sk ) ); + sendLemma( ant, conc, "Constant Split" ); + return true; + } + }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 v/v 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 ); - Trace("strings-solve-debug") << "Break normal form constant/variable " << std::endl; + // |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, "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); + sendLemma( ant, conc, "Split" ); + return true; } - Node sk = NodeManager::currentNM()->mkSkolem( "ssym_$$", normal_forms[i][index_i].getType(), "created for v/v 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; - } - } - } - } - } - }while(success); - } - } + } + } + } + } + }while(success); + } + } + } //construct the normal form if( normal_forms.empty() ){ @@ -1025,18 +1065,19 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v } Trace("strings-solve-debug2") << "just take the first normal form ... done" << std::endl; } - //if( visited.empty() ){ - //TODO : cache? - //} + + d_normal_forms_base[eqc] = normal_form_src.empty() ? eqc : normal_form_src[0]; d_normal_forms[eqc].insert( d_normal_forms[eqc].end(), nf.begin(), nf.end() ); d_normal_forms_exp[eqc].insert( d_normal_forms_exp[eqc].end(), nf_exp.begin(), nf_exp.end() ); - Trace("strings-process") << "Return process equivalence class " << eqc << " : returned." << std::endl; + Trace("strings-process") << "Return process equivalence class " << eqc << " : returned, size = " << nf.size() << std::endl; }else{ - Trace("strings-process") << "Return process equivalence class " << eqc << " : already computed." << std::endl; + Trace("strings-process") << "Return process equivalence class " << eqc << " : already computed, size = " << d_normal_forms[eqc].size() << std::endl; nf.insert( nf.end(), d_normal_forms[eqc].begin(), d_normal_forms[eqc].end() ); nf_exp.insert( nf_exp.end(), d_normal_forms_exp[eqc].begin(), d_normal_forms_exp[eqc].end() ); + result = true; } visited.pop_back(); + return result; } } @@ -1049,104 +1090,125 @@ bool TheoryStrings::normalizeDisequality( Node ni, Node nj ) { nfj.insert( nfj.end(), d_normal_forms[nj].begin(), d_normal_forms[nj].end() ); unsigned index = 0; - while( 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]; + 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; + }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(); + 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 { - 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; - } - }else{ - Node li = getLength( i ); - Node lj = getLength( j ); - if( areDisequal(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 ).negate() ); - std::vector< Node > conc; - Node sk1 = NodeManager::currentNM()->mkSkolem( "xpdsym_$$", ni.getType(), "created for disequality normalization" ); - Node sk2 = NodeManager::currentNM()->mkSkolem( "ypdsym_$$", ni.getType(), "created for disequality normalization" ); - Node sk3 = NodeManager::currentNM()->mkSkolem( "zpdsym_$$", ni.getType(), "created for disequality normalization" ); - 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 ) ) ) ); - - /* - 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 c = NodeManager::currentNM()->mkNode( kind::AND, conc ); - */ - //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( 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 + //conflict return false; - } else { - //splitting on demand : try to make them disequal - Node eq = i.eqNode( j ); - sendSplit( i, j, "Disequality : disequal terms" ); + } + }else{ + Node li = getLength( i ); + Node lj = getLength( j ); + if( areDisequal(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 ).negate() ); + std::vector< Node > conc; + Node sk1 = NodeManager::currentNM()->mkSkolem( "xpdsym_$$", ni.getType(), "created for disequality normalization" ); + Node sk2 = NodeManager::currentNM()->mkSkolem( "ypdsym_$$", ni.getType(), "created for disequality normalization" ); + Node sk3 = NodeManager::currentNM()->mkSkolem( "zpdsym_$$", ni.getType(), "created for disequality normalization" ); + 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 ) ) ) ); + + /* + 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 c = NodeManager::currentNM()->mkNode( kind::AND, conc ); + */ + //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( 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 + return false; + } else { + //splitting on demand : try to make them disequal + Node eq = i.eqNode( j ); + sendSplit( i, j, "Disequality : disequal terms" ); + 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, "Disequality : equal length" ); eq = Rewriter::rewrite( eq ); - d_pending_req_phase[ eq ] = false; + d_pending_req_phase[ eq ] = true; return true; } - }else{ - //splitting on demand : try to make lengths equal - Node eq = li.eqNode( lj ); - sendSplit( li, lj, "Disequality : equal length" ); - eq = Rewriter::rewrite( eq ); - d_pending_req_phase[ eq ] = true; - return true; } } + index++; } - index++; } Assert( false ); } @@ -1273,7 +1335,7 @@ bool TheoryStrings::addInductiveEquation( Node x, Node y, Node z, Node exp, cons } void TheoryStrings::sendLemma( Node ant, Node conc, const char * c ) { - if( conc.isNull() ){ + if( conc.isNull() || conc==d_false ){ d_out->conflict(ant); Trace("strings-conflict") << "CONFLICT : Strings conflict : " << ant << std::endl; d_conflict = true; @@ -1306,6 +1368,11 @@ Node TheoryStrings::mkConcat( std::vector< Node >& c ) { return Rewriter::rewrite( cc ); } +Node TheoryStrings::mkExplain( std::vector< Node >& a ) { + std::vector< Node > an; + return mkExplain( a, an ); +} + Node TheoryStrings::mkExplain( std::vector< Node >& a, std::vector< Node >& an ) { std::vector< TNode > antec_exp; for( unsigned i=0; i& a, std::vector< Node >& an ) return ant; } +bool TheoryStrings::checkLengths() { + bool addedLemma = false; + 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, true ); + //get the constant for the equivalence class + //int c_len = ...; + eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); + while( !eqc_i.isFinished() ){ + Node n = (*eqc_i); + //if n is concat, and + //if n has not instantiatied the concat..length axiom + //then, add lemma + if( n.getKind() == kind::CONST_STRING ){ //n.getKind() == kind::STRING_CONCAT || + if( d_length_inst.find(n)==d_length_inst.end() ){ + 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 term lemma " << eq << std::endl; + d_out->lemma(eq); + Node skl = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk ); + Node lsum; + if( n.getKind() == kind::STRING_CONCAT ){ + //add lemma + std::vector node_vec; + for( unsigned i=0; imkNode( kind::STRING_LENGTH, n[i] ); + node_vec.push_back(lni); + } + lsum = NodeManager::currentNM()->mkNode( kind::PLUS, node_vec ); + }else{ + //add lemma + lsum = NodeManager::currentNM()->mkConst( ::CVC4::Rational( n.getConst().size() ) ); + } + Node ceq = NodeManager::currentNM()->mkNode( kind::EQUAL, skl, lsum ); + ceq = Rewriter::rewrite(ceq); + Trace("strings-lemma") << "Strings: Add length lemma " << ceq << std::endl; + d_out->lemma(ceq); + addedLemma = true; + } + } + ++eqc_i; + } + } + ++eqcs_i; + } + return addedLemma; +} + bool TheoryStrings::checkNormalForms() { Trace("strings-process") << "Normalize equivalence classes...." << std::endl; eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator( &d_equalityEngine ); @@ -1354,14 +1476,20 @@ bool TheoryStrings::checkNormalForms() { 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 << " ) : "; + 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; + Trace("strings-eqc") << " } " << std::endl; + EqcInfo * ei = getOrMakeEqcInfo( eqc, false ); + if( ei ){ + Trace("strings-eqc-debug") << "* Length term : " << ei->d_length_term.get() << std::endl; + Trace("strings-eqc-debug") << "* Cardinality lemma k : " << ei->d_cardinality_lem_k.get() << std::endl; + Trace("strings-eqc-debug") << "* Normalization length lemma : " << ei->d_normalized_length.get() << std::endl; + } } ++eqcs2_i; } @@ -1415,6 +1543,7 @@ bool TheoryStrings::checkNormalForms() { std::vector< Node > nf; std::vector< Node > nf_exp; normalizeEquivalenceClass(eqc, visited, nf, nf_exp); + Trace("strings-debug") << "Finished normalizing eqc..." << std::endl; if( d_conflict ){ return true; }else if ( d_pending.empty() && d_lemma_cache.empty() ){ @@ -1498,6 +1627,42 @@ bool TheoryStrings::checkNormalForms() { } } +bool TheoryStrings::checkLengthsEqc() { + bool addedLemma = false; + std::vector< Node > nodes; + getEquivalenceClasses( nodes ); + for( unsigned i=0; i1 ){ + Trace("strings-process-debug") << "Process length constraints for " << nodes[i] << std::endl; + //check if there is a length term for this equivalence class + EqcInfo* ei = getOrMakeEqcInfo( nodes[i], false ); + Node lt = ei ? ei->d_length_term : Node::null(); + if( !lt.isNull() ){ + Node llt = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt ); + //now, check if length normalization has occurred + if( ei->d_normalized_length.get().isNull() ){ + //if not, add the lemma + std::vector< Node > ant; + ant.insert( ant.end(), d_normal_forms_exp[nodes[i]].begin(), d_normal_forms_exp[nodes[i]].end() ); + ant.push_back( d_normal_forms_base[nodes[i]].eqNode( lt ) ); + Node lc = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, mkConcat( d_normal_forms[nodes[i]] ) ); + lc = Rewriter::rewrite( lc ); + Node eq = llt.eqNode( lc ); + ei->d_normalized_length.set( eq ); + sendLemma( mkExplain( ant ), eq, "Length Normalization" ); + addedLemma = true; + } + } + }else{ + Trace("strings-process-debug") << "Do not process length constraints for " << nodes[i] << " " << d_normal_forms[nodes[i]].size() << std::endl; + } + } + if( addedLemma ){ + doPendingLemmas(); + } + return addedLemma; +} + bool TheoryStrings::checkCardinality() { int cardinality = options::stringCharCardinality(); Trace("strings-solve-debug2") << "get cardinality: " << cardinality << endl; diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 52c7288a8..16c3d4876 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -50,6 +50,7 @@ class TheoryStrings : public Theory { bool hasTerm( Node a ); bool areEqual( Node a, Node b ); bool areDisequal( Node a, Node b ); + Node getLengthTerm( Node t ); Node getLength( Node t ); public: @@ -131,6 +132,10 @@ class TheoryStrings : public Theory { /** inferences */ NodeList d_infer; NodeList d_infer_exp; + /** normal forms */ + std::map< Node, Node > d_normal_forms_base; + std::map< Node, std::vector< Node > > d_normal_forms; + std::map< Node, std::vector< Node > > d_normal_forms_exp; //map of pairs of terms that have the same normal form NodeListMap d_nf_pairs; void addNormalFormPair( Node n1, Node n2 ); @@ -179,6 +184,8 @@ class TheoryStrings : public Theory { context::CDO< Node > d_const_term; context::CDO< Node > d_length_term; context::CDO< unsigned > d_cardinality_lem_k; + // 1 = added length lemma + context::CDO< Node > d_normalized_length; }; /** map from representatives to information necessary for equivalence classes */ std::map< Node, EqcInfo* > d_eqc_info; @@ -186,14 +193,14 @@ class TheoryStrings : public Theory { //maintain which concat terms have the length lemma instantiatied std::map< Node, bool > d_length_inst; private: - std::map< Node, std::vector< Node > > d_normal_forms; - std::map< Node, std::vector< Node > > d_normal_forms_exp; - void getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf, + bool getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< std::vector< Node > > &normal_forms, std::vector< std::vector< Node > > &normal_forms_exp, std::vector< Node > &normal_form_src); - void normalizeEquivalenceClass( Node n, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp ); + bool normalizeEquivalenceClass( Node n, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp ); bool normalizeDisequality( Node n1, Node n2 ); + bool checkLengths(); bool checkNormalForms(); + bool checkLengthsEqc(); bool checkCardinality(); bool checkInductiveEquations(); int gcd(int a, int b); @@ -225,6 +232,7 @@ protected: Node mkConcat( Node n1, Node n2 ); Node mkConcat( std::vector< Node >& c ); /** mkExplain **/ + Node mkExplain( std::vector< Node >& a ); Node mkExplain( std::vector< Node >& a, std::vector< Node >& an ); //get equivalence classes -- 2.30.2