From: ajreynol Date: Thu, 15 Oct 2015 09:43:14 +0000 (+0200) Subject: Decompose string contains, minor refactoring. X-Git-Tag: cvc5-1.0.0~6208 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f4420f2a1f82ee4a2f86d6d4318286d21520e280;p=cvc5.git Decompose string contains, minor refactoring. --- diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 997c47776..fc8df8bbc 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -632,19 +632,23 @@ void TheoryStrings::check(Effort e) { checkExtendedFuncsEval(); Trace("strings-process") << "Done check extended functions eval, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl; if( !hasProcessed() ){ - checkNormalForms(); - Trace("strings-process") << "Done check normal forms, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl; + checkFlatForms(); + Trace("strings-process") << "Done check flat forms, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl; if( !hasProcessed() ){ - if( options::stringEagerLen() ){ - checkLengthsEqc(); - Trace("strings-process") << "Done check lengths, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl; - } + checkNormalForms(); + Trace("strings-process") << "Done check normal forms, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl; if( !hasProcessed() ){ - checkExtendedFuncs(); - Trace("strings-process") << "Done check extended functions, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl; + if( options::stringEagerLen() ){ + checkLengthsEqc(); + Trace("strings-process") << "Done check lengths, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl; + } if( !hasProcessed() ){ - checkCardinality(); - Trace("strings-process") << "Done check cardinality, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl; + checkExtendedFuncs(); + Trace("strings-process") << "Done check extended functions, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl; + if( !hasProcessed() ){ + checkCardinality(); + Trace("strings-process") << "Done check cardinality, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl; + } } } } @@ -2267,8 +2271,8 @@ void TheoryStrings::getConcatVec( Node n, std::vector< Node >& c ) { } void TheoryStrings::debugPrintFlatForms( const char * tc ){ - for( unsigned k=0; k1 ){ Trace( tc ) << "EQC [" << eqc << "]" << std::endl; }else{ @@ -2307,24 +2311,25 @@ void TheoryStrings::debugPrintFlatForms( const char * tc ){ Trace( tc ) << std::endl; } -void TheoryStrings::checkNormalForms() { - +void TheoryStrings::checkFlatForms() { //first check for cycles, while building ordering of equivalence classes d_eqc.clear(); d_flat_form.clear(); d_flat_form_index.clear(); Trace("strings-process") << "Check equivalence classes cycles...." << std::endl; - d_eqcs.clear(); - for( unsigned i=0; i eqc; + eqc.insert( eqc.end(), d_strings_eqc.begin(), d_strings_eqc.end() ); + d_strings_eqc.clear(); + for( unsigned i=0; i curr; std::vector< Node > exp; - checkCycles( d_strings_eqc[i], curr, exp ); + checkCycles( eqc[i], curr, exp ); if( hasProcessed() ){ return; } } Trace("strings-process-debug") << "Done check cycles, lemmas = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << std::endl; - if( !hasProcessed() ){ //debug print flat forms if( Trace.isOn("strings-ff") ){ @@ -2332,8 +2337,8 @@ void TheoryStrings::checkNormalForms() { debugPrintFlatForms( "strings-ff" ); } //inferences without recursively expanding flat forms - for( unsigned k=0; k::iterator itc = d_eqc_to_const.find( eqc ); if( itc!=d_eqc_to_const.end() ){ @@ -2492,67 +2497,62 @@ void TheoryStrings::checkNormalForms() { } } } + } +} - if( !hasProcessed() ){ - //get equivalence classes - //d_eqcs.clear(); - //getEquivalenceClasses( d_eqcs ); - Trace("strings-process") << "Normalize equivalence classes...." << 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; - for( unsigned i=0; i visited; - 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; - } else if ( d_pending.empty() && d_lemma_cache.empty() ) { - Node nf_term = mkConcat( nf ); - 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 - nf_exp.push_back( eqc_to_exp[nf_to_eqc[nf_term]] ); - Node eq = eqc.eqNode( nf_to_eqc[nf_term] ); - sendInfer( mkAnd( nf_exp ), eq, "Normal_Form" ); - //d_equalityEngine.assertEquality( eq, true, eq_exp ); - } else { - nf_to_eqc[nf_term] = eqc; - eqc_to_exp[eqc] = mkAnd( nf_exp ); - } - } - Trace("strings-process-debug") << "Done verifying normal forms are the same for " << eqc << std::endl; - } - - if(Trace.isOn("strings-nf")) { - Trace("strings-nf") << "**** 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") << " N[" << it->second << "] = " << it->first << std::endl; - } - Trace("strings-nf") << std::endl; +void TheoryStrings::checkNormalForms() { + Trace("strings-process") << "Normalize equivalence classes...." << 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; + for( unsigned i=0; i visited; + 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; + } else if ( d_pending.empty() && d_lemma_cache.empty() ) { + Node nf_term = mkConcat( nf ); + 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 + nf_exp.push_back( eqc_to_exp[nf_to_eqc[nf_term]] ); + Node eq = eqc.eqNode( nf_to_eqc[nf_term] ); + sendInfer( mkAnd( nf_exp ), eq, "Normal_Form" ); + } else { + nf_to_eqc[nf_term] = eqc; + eqc_to_exp[eqc] = mkAnd( nf_exp ); } + } + Trace("strings-process-debug") << "Done verifying normal forms are the same for " << eqc << std::endl; + } - if( !hasProcessed() ){ - checkExtendedFuncsEval( 1 ); - Trace("strings-process-debug") << "Done check extended functions re-eval, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl; - if( !hasProcessed() ){ - if( !options::stringEagerLen() ){ - checkLengthsEqc(); - if( hasProcessed() ){ - return; - } - } - //process disequalities between equivalence classes - checkDeqNF(); - Trace("strings-process-debug") << "Done check disequalities, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl; + if(Trace.isOn("strings-nf")) { + Trace("strings-nf") << "**** 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") << " N[" << it->second << "] = " << it->first << std::endl; + } + Trace("strings-nf") << std::endl; + } + if( !hasProcessed() ){ + checkExtendedFuncsEval( 1 ); + Trace("strings-process-debug") << "Done check extended functions re-eval, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl; + if( !hasProcessed() ){ + if( !options::stringEagerLen() ){ + checkLengthsEqc(); + if( hasProcessed() ){ + return; } } + //process disequalities between equivalence classes + checkDeqNF(); + Trace("strings-process-debug") << "Done check disequalities, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl; } } Trace("strings-solve") << "Finished check normal forms, #lemmas = " << d_lemma_cache.size() << ", conflict = " << d_conflict << std::endl; @@ -2562,7 +2562,7 @@ Node TheoryStrings::checkCycles( Node eqc, std::vector< Node >& curr, std::vecto if( std::find( curr.begin(), curr.end(), eqc )!=curr.end() ){ // a loop return eqc; - }else if( std::find( d_eqcs.begin(), d_eqcs.end(), eqc )==d_eqcs.end() ){ + }else if( std::find( d_strings_eqc.begin(), d_strings_eqc.end(), eqc )==d_strings_eqc.end() ){ curr.push_back( eqc ); //look at all terms in this equivalence class eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); @@ -2625,7 +2625,7 @@ Node TheoryStrings::checkCycles( Node eqc, std::vector< Node >& curr, std::vecto } curr.pop_back(); //now we can add it to the list of equivalence classes - d_eqcs.push_back( eqc ); + d_strings_eqc.push_back( eqc ); }else{ //already processed } @@ -2653,14 +2653,14 @@ void TheoryStrings::checkDeqNF() { // sendSplit( cols[i][j], cols[i][k], "D-NORM", true ); // return; //}else{ - Trace("strings-solve") << "- Compare " << cols[i][j] << " "; - printConcat( d_normal_forms[cols[i][j]], "strings-solve" ); - Trace("strings-solve") << " against " << cols[i][k] << " "; - printConcat( d_normal_forms[cols[i][k]], "strings-solve" ); - Trace("strings-solve") << "..." << std::endl; - if( processDeq( cols[i][j], cols[i][k] ) ){ - return; - } + Trace("strings-solve") << "- Compare " << cols[i][j] << " "; + printConcat( d_normal_forms[cols[i][j]], "strings-solve" ); + Trace("strings-solve") << " against " << cols[i][k] << " "; + printConcat( d_normal_forms[cols[i][k]], "strings-solve" ); + Trace("strings-solve") << "..." << std::endl; + if( processDeq( cols[i][j], cols[i][k] ) ){ + return; + } //} } } @@ -3830,6 +3830,8 @@ void TheoryStrings::checkExtendedFuncsEval( int effort ) { if( effort==0 ){ d_extf_vars.clear(); } + d_extf_exp.clear(); + d_extf_info.clear(); Trace("strings-extf-debug") << "Checking " << d_ext_func_terms.size() << " extended functions." << std::endl; for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){ if( (*it).second ){ @@ -3848,7 +3850,6 @@ void TheoryStrings::checkExtendedFuncsEval( int effort ) { collectVars( n, d_extf_vars[n], visited ); } //build up a best current substitution for the variables in the term, exp is explanation for substitution - std::vector< Node > exp; std::vector< Node > var; std::vector< Node > sub; for( std::map< Node, std::vector< Node > >::iterator itv = d_extf_vars[n].begin(); itv != d_extf_vars[n].end(); ++itv ){ @@ -3873,13 +3874,13 @@ void TheoryStrings::checkExtendedFuncsEval( int effort ) { if( itv->second[i]!=s ){ var.push_back( itv->second[i] ); sub.push_back( s ); - addToExplanation( itv->second[i], b, exp ); + addToExplanation( itv->second[i], b, d_extf_exp[n] ); Trace("strings-extf-debug") << " " << itv->second[i] << " --> " << s << std::endl; added = true; } } - if( added && !e.isNull() ){ - exp.push_back( e ); + if( added ){ + addToExplanation( e, d_extf_exp[n] ); } } } @@ -3915,12 +3916,12 @@ void TheoryStrings::checkExtendedFuncsEval( int effort ) { }else{ conc = nrs.eqNode( nrc ); } - exp.clear(); + d_extf_exp[n].clear(); } }else{ if( !areEqual( n, nrc ) ){ if( n.getType().isBoolean() ){ - exp.push_back( nrc==d_true ? n.negate() : n ); + d_extf_exp[n].push_back( nrc==d_true ? n.negate() : n ); conc = d_false; }else{ conc = n.eqNode( nrc ); @@ -3929,10 +3930,10 @@ void TheoryStrings::checkExtendedFuncsEval( int effort ) { } if( !conc.isNull() ){ Trace("strings-extf") << " resolve extf : " << nr << " -> " << nrc << std::endl; - if( n.getType().isInteger() || exp.empty() ){ - sendLemma( mkExplain( exp ), conc, effort==0 ? "EXTF" : "EXTF-N" ); + if( n.getType().isInteger() || d_extf_exp[n].empty() ){ + sendLemma( mkExplain( d_extf_exp[n] ), conc, effort==0 ? "EXTF" : "EXTF-N" ); }else{ - sendInfer( mkAnd( exp ), conc, effort==0 ? "EXTF" : "EXTF-N" ); + sendInfer( mkAnd( d_extf_exp[n] ), conc, effort==0 ? "EXTF" : "EXTF-N" ); } if( d_conflict ){ Trace("strings-extf-debug") << " conflict, return." << std::endl; @@ -3942,14 +3943,12 @@ void TheoryStrings::checkExtendedFuncsEval( int effort ) { }else if( ( nrc.getKind()==kind::OR && n_pol==-1 ) || ( nrc.getKind()==kind::AND && n_pol==1 ) ){ //infer the consequence of each d_ext_func_terms[n] = false; - exp.push_back( n_pol==-1 ? n.negate() : n ); + d_extf_exp[n].push_back( n_pol==-1 ? n.negate() : n ); Trace("strings-extf-debug") << " decomposable..." << std::endl; Trace("strings-extf") << " resolve extf : " << nr << " -> " << nrc << ", pol = " << n_pol << std::endl; for( unsigned i=0; i& exp, int effort ){ +void TheoryStrings::checkExtfInference( Node n, Node nr, int n_pol, int effort ){ if( n_pol!=0 ){ - if( d_extf_infer_cache.find( nr )==d_extf_infer_cache.end() ){ - d_extf_infer_cache.insert( nr ); - if( nr.getKind()==kind::STRING_STRCTN ){ - if( ( n_pol==1 && nr[1].getKind()==kind::STRING_CONCAT ) || ( n_pol==-1 && nr[0].getKind()==kind::STRING_CONCAT ) ){ + //add original to explanation + d_extf_exp[n].push_back( n_pol==1 ? n : n.negate() ); + if( nr.getKind()==kind::STRING_STRCTN ){ + if( ( n_pol==1 && nr[1].getKind()==kind::STRING_CONCAT ) || ( n_pol==-1 && nr[0].getKind()==kind::STRING_CONCAT ) ){ + if( d_extf_infer_cache.find( nr )==d_extf_infer_cache.end() ){ + d_extf_infer_cache.insert( nr ); //one argument does (not) contain each of the components of the other argument - exp.push_back( n_pol==1 ? n : n.negate() ); int index = n_pol==1 ? 1 : 0; + std::vector< Node > children; + children.push_back( nr[0] ); + children.push_back( nr[1] ); + Node exp_n = mkAnd( d_extf_exp[n] ); for( unsigned i=0; imkNode( kind::STRING_STRCTN, children ); + //can mark as reduced, since model for n => model for conc + d_ext_func_terms[conc] = false; + sendInfer( exp_n, n_pol==1 ? conc : conc.negate(), "CTN_Decompose" ); } } + }else{ + //store this (reduced) assertion + Assert( effort==0 || nr[0]==getRepresentative( nr[0] ) ); + bool pol = n_pol==1; + if( std::find( d_extf_info[nr[0]].d_ctn[pol].begin(), d_extf_info[nr[0]].d_ctn[pol].end(), nr[1] )==d_extf_info[nr[0]].d_ctn[pol].end() ){ + d_extf_info[nr[0]].d_ctn[pol].push_back( nr[1] ); + d_extf_info[nr[0]].d_ctn_from[pol].push_back( n ); + }else{ + Trace("strings-extf-debug") << " redundant." << std::endl; + d_ext_func_terms[n] = false; + } } } } diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index af06519c0..b2864656a 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -201,8 +201,6 @@ private: void clear(){ d_children.clear(); } }; std::map< Kind, TermIndex > d_term_index; - // (ordered) strings eqc to process - std::vector< Node > d_eqcs; //list of non-congruent concat terms in each eqc std::map< Node, std::vector< Node > > d_eqc; std::map< Node, std::vector< Node > > d_flat_form; @@ -279,8 +277,9 @@ private: void checkInit(); void checkConstantEquivalenceClasses( TermIndex* ti, std::vector< Node >& vecc ); void checkExtendedFuncsEval( int effort = 0 ); - void checkExtfInference( Node n, Node nr, int n_pol, std::vector< Node >& exp, int effort ); + void checkExtfInference( Node n, Node nr, int n_pol, int effort ); void collectVars( Node n, std::map< Node, std::vector< Node > >& vars, std::map< Node, bool >& visited ); + void checkFlatForms(); void checkNormalForms(); Node checkCycles( Node eqc, std::vector< Node >& curr, std::vector< Node >& exp ); void checkDeqNF(); @@ -388,6 +387,13 @@ private: //extended string terms and whether they have been reduced NodeBoolMap d_ext_func_terms; std::map< Node, std::map< Node, std::vector< Node > > > d_extf_vars; + class ExtfInfo { + public: + std::map< bool, std::vector< Node > > d_ctn; + std::map< bool, std::vector< Node > > d_ctn_from; + }; + std::map< Node, std::vector< Node > > d_extf_exp; + std::map< Node, ExtfInfo > d_extf_info; //collect extended operator terms void collectExtendedFuncTerms( Node n, std::map< Node, bool >& visited ); diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h index a5ba1f615..08fe478c4 100644 --- a/src/theory/strings/theory_strings_preprocess.h +++ b/src/theory/strings/theory_strings_preprocess.h @@ -32,7 +32,6 @@ namespace strings { class StringsPreprocess { typedef context::CDHashMap NodeNodeMap; - // NOTE: this class is NOT context-dependent NodeNodeMap d_cache; //Constants Node d_zero;