From f70674c2f0c6c1c55e3d7c5fed916fc1e7721ffe Mon Sep 17 00:00:00 2001 From: ajreynol Date: Sat, 16 Jul 2016 09:03:11 -0500 Subject: [PATCH] Refactor strings extf evaluation info. Ensure strings eager preprocess eliminates all extf symbols during ppRewrite. Add options stringGuessModel and stringUfReduct. Minor optimizations. --- src/options/strings_options | 4 + src/theory/strings/theory_strings.cpp | 309 ++++++++++-------- src/theory/strings/theory_strings.h | 64 ++-- .../strings/theory_strings_preprocess.cpp | 69 +++- .../strings/theory_strings_preprocess.h | 17 +- 5 files changed, 288 insertions(+), 175 deletions(-) diff --git a/src/options/strings_options b/src/options/strings_options index 136175d72..27739070d 100644 --- a/src/options/strings_options +++ b/src/options/strings_options @@ -63,6 +63,10 @@ option stringRExplainLemmas strings-rexplain-lemmas --strings-rexplain-lemmas bo regression explanations for string lemmas option stringMinPrefixExplain strings-min-prefix-explain --strings-min-prefix-explain bool :default true minimize explanations for prefix of normal forms in strings +option stringGuessModel strings-guess-model --strings-guess-model bool :default false + use model guessing to avoid string extended function reductions +option stringUfReduct strings-uf-reduct --strings-uf-reduct bool :default false + use uninterpreted functions when applying extended function reductions endmodule diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index e8459133e..e3dc0ac72 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -37,7 +37,7 @@ namespace CVC4 { namespace theory { namespace strings { -Node TheoryStrings::TermIndex::add( Node n, unsigned index, TheoryStrings* t, Node er, std::vector< Node >& c ) { +Node TheoryStrings::TermIndex::add( TNode n, unsigned index, TheoryStrings* t, Node er, std::vector< Node >& c ) { if( index==n.getNumChildren() ){ if( d_data.isNull() ){ d_data = n; @@ -45,7 +45,7 @@ Node TheoryStrings::TermIndex::add( Node n, unsigned index, TheoryStrings* t, No return d_data; }else{ Assert( indexgetRepresentative( n[index] ); + TNode nir = t->getRepresentative( n[index] ); //if it is empty, and doing CONCAT, ignore if( nir==er && n.getKind()==kind::STRING_CONCAT ){ return add( n, index+1, t, er, c ); @@ -81,6 +81,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, d_proxy_var_to_length(u), d_functionsTerms(c), d_ext_func_terms(c), + d_has_extf(c, false ), d_regexp_memberships(c), d_regexp_ucached(u), d_regexp_ccached(c), @@ -506,7 +507,7 @@ Node TheoryStrings::expandDefinition(LogicRequest &logicRequest, Node node) { void TheoryStrings::check(Effort e) { - if (done() && !fullEffort(e)) { + if (done() && e::iterator it = ti->d_children.begin(); it != ti->d_children.end(); ++it ){ + for( std::map< TNode, TermIndex >::iterator it = ti->d_children.begin(); it != ti->d_children.end(); ++it ){ std::map< Node, Node >::iterator itc = d_eqc_to_const.find( it->first ); if( itc!=d_eqc_to_const.end() ){ vecc.push_back( itc->second ); @@ -1228,45 +1235,55 @@ void TheoryStrings::checkConstantEquivalenceClasses( TermIndex* ti, std::vector< } } -void TheoryStrings::checkExtendedFuncsEval( int effort ) { +void TheoryStrings::checkExtfEval( int effort ) { Trace("strings-extf-list") << "Active extended functions, effort=" << effort << " : " << std::endl; - if( effort==0 ){ - d_extf_vars.clear(); - } - d_extf_pol.clear(); - d_extf_exp.clear(); - d_extf_info.clear(); + d_extf_info_tmp.clear(); + bool has_nreduce = false; 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 not already reduced if( (*it).second ){ Node n = (*it).first; - d_extf_pol[n] = 0; + + //setup information about extf + std::map< Node, ExtfInfo >::iterator iti = d_extf_info.find( n ); + Assert( iti!=d_extf_info.end() ); + d_extf_info_tmp[n].init(); + std::map< Node, ExtfInfoTmp >::iterator itit = d_extf_info_tmp.find( n ); + //get polarity if( n.getType().isBoolean() ){ if( areEqual( n, d_true ) ){ - d_extf_pol[n] = 1; + itit->second.d_pol = 1; }else if( areEqual( n, d_false ) ){ - d_extf_pol[n] = -1; + itit->second.d_pol = -1; } } - Trace("strings-extf-debug") << "Check extf " << n << ", pol = " << d_extf_pol[n] << "..." << std::endl; - if( effort==0 ){ - std::map< Node, bool > visited; - collectVars( n, d_extf_vars[n], visited ); + //compute rep vars map + for( unsigned j=0; jsecond.d_vars.size(); j++ ){ + Node nr = getRepresentative( iti->second.d_vars[j] ); + itit->second.d_rep_vars[nr].push_back( iti->second.d_vars[j] ); } + + Trace("strings-extf-debug") << "Check extf " << n << ", pol = " << itit->second.d_pol << ", effort=" << effort << "..." << std::endl; //build up a best current substitution for the variables in the term, exp is explanation for substitution 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 ){ + for( std::map< Node, std::vector< Node > >::iterator itv = itit->second.d_rep_vars.begin(); itv != itit->second.d_rep_vars.end(); ++itv ){ Node nr = itv->first; std::map< Node, Node >::iterator itc = d_eqc_to_const.find( nr ); Node s; Node b; Node e; - if( itc!=d_eqc_to_const.end() ){ + if( effort>=3 ){ + //model values + s = d_valuation.getModel()->getRepresentative( nr ); + }else if( itc!=d_eqc_to_const.end() ){ + //constant equivalence classes b = d_eqc_to_const_base[nr]; s = itc->second; e = d_eqc_to_const_exp[nr]; - }else if( effort>0 ){ + }else if( effort>=1 && effort<3 ){ + //normal forms b = d_normal_forms_base[nr]; std::vector< Node > expt; s = getNormalString( b, expt ); @@ -1278,80 +1295,92 @@ 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, d_extf_exp[n] ); + if( !b.isNull() ){ + addToExplanation( itv->second[i], b, itit->second.d_exp ); + } Trace("strings-extf-debug") << " " << itv->second[i] << " --> " << s << std::endl; added = true; } } - if( added ){ - addToExplanation( e, d_extf_exp[n] ); + if( added && !e.isNull() ){ + addToExplanation( e, itit->second.d_exp ); } } } Node to_reduce; if( !var.empty() ){ + //do substitution, evaluate Node nr = n.substitute( var.begin(), var.end(), sub.begin(), sub.end() ); Node nrc = Rewriter::rewrite( nr ); + //if rewrites to a constant, then do the inference and mark as reduced if( nrc.isConst() ){ - //mark as reduced - d_ext_func_terms[n] = false; - Trace("strings-extf-debug") << " resolvable by evaluation..." << std::endl; - std::vector< Node > exps; - Trace("strings-extf-debug") << " get symbolic definition..." << std::endl; - Node nrs = getSymbolicDefinition( nr, exps ); - if( !nrs.isNull() ){ - Trace("strings-extf-debug") << " rewrite " << nrs << "..." << std::endl; - nrs = Rewriter::rewrite( nrs ); - //ensure the symbolic form is non-trivial - if( nrs.isConst() ){ - Trace("strings-extf-debug") << " symbolic definition is trivial..." << std::endl; - nrs = Node::null(); - } - }else{ - Trace("strings-extf-debug") << " could not infer symbolic definition." << std::endl; - } - Node conc; - if( !nrs.isNull() ){ - Trace("strings-extf-debug") << " symbolic def : " << nrs << std::endl; - if( !areEqual( nrs, nrc ) ){ - //infer symbolic unit - if( n.getType().isBoolean() ){ - conc = nrc==d_true ? nrs : nrs.negate(); - }else{ - conc = nrs.eqNode( nrc ); + if( effort<3 ){ + d_ext_func_terms[n] = false; + Trace("strings-extf-debug") << " resolvable by evaluation..." << std::endl; + std::vector< Node > exps; + Trace("strings-extf-debug") << " get symbolic definition..." << std::endl; + Node nrs = getSymbolicDefinition( nr, exps ); + if( !nrs.isNull() ){ + Trace("strings-extf-debug") << " rewrite " << nrs << "..." << std::endl; + nrs = Rewriter::rewrite( nrs ); + //ensure the symbolic form is non-trivial + if( nrs.isConst() ){ + Trace("strings-extf-debug") << " symbolic definition is trivial..." << std::endl; + nrs = Node::null(); } - d_extf_exp[n].clear(); + }else{ + Trace("strings-extf-debug") << " could not infer symbolic definition." << std::endl; } - }else{ - if( !areEqual( n, nrc ) ){ - if( n.getType().isBoolean() ){ - if( areEqual( n, nrc==d_true ? d_false : d_true ) ){ - d_extf_exp[n].push_back( nrc==d_true ? n.negate() : n ); - conc = d_false; + Node conc; + if( !nrs.isNull() ){ + Trace("strings-extf-debug") << " symbolic def : " << nrs << std::endl; + if( !areEqual( nrs, nrc ) ){ + //infer symbolic unit + if( n.getType().isBoolean() ){ + conc = nrc==d_true ? nrs : nrs.negate(); }else{ - conc = nrc==d_true ? n : n.negate(); + conc = nrs.eqNode( nrc ); + } + itit->second.d_exp.clear(); + } + }else{ + if( !areEqual( n, nrc ) ){ + if( n.getType().isBoolean() ){ + if( areEqual( n, nrc==d_true ? d_false : d_true ) ){ + itit->second.d_exp.push_back( nrc==d_true ? n.negate() : n ); + conc = d_false; + }else{ + conc = nrc==d_true ? n : n.negate(); + } + }else{ + conc = n.eqNode( nrc ); } - }else{ - conc = n.eqNode( nrc ); } } - } - if( !conc.isNull() ){ - Trace("strings-extf") << " resolve extf : " << nr << " -> " << nrc << std::endl; - sendInference( d_extf_exp[n], conc, effort==0 ? "EXTF" : "EXTF-N", true ); - if( d_conflict ){ - Trace("strings-extf-debug") << " conflict, return." << std::endl; - return; + if( !conc.isNull() ){ + Trace("strings-extf") << " resolve extf : " << nr << " -> " << nrc << std::endl; + sendInference( itit->second.d_exp, conc, effort==0 ? "EXTF" : "EXTF-N", true ); + if( d_conflict ){ + Trace("strings-extf-debug") << " conflict, return." << std::endl; + return; + } + } + }else{ + //check if it is already equal, if so, mark as reduced. Otherwise, do nothing. + if( areEqual( n, nrc ) ){ + Trace("strings-extf") << " resolved extf, since satisfied by model: " << n << std::endl; + itit->second.d_model_active = false; } } - }else if( ( nrc.getKind()==kind::OR && d_extf_pol[n]==-1 ) || ( nrc.getKind()==kind::AND && d_extf_pol[n]==1 ) ){ - //infer the consequence of each + //if it reduces to a conjunction, infer each and reduce + }else if( ( nrc.getKind()==kind::OR && itit->second.d_pol==-1 ) || ( nrc.getKind()==kind::AND && itit->second.d_pol==1 ) ){ + Assert( effort<3 ); d_ext_func_terms[n] = false; - d_extf_exp[n].push_back( d_extf_pol[n]==-1 ? n.negate() : n ); + itit->second.d_exp.push_back( itit->second.d_pol==-1 ? n.negate() : n ); Trace("strings-extf-debug") << " decomposable..." << std::endl; - Trace("strings-extf") << " resolve extf : " << nr << " -> " << nrc << ", pol = " << d_extf_pol[n] << std::endl; + Trace("strings-extf") << " resolve extf : " << nr << " -> " << nrc << ", pol = " << itit->second.d_pol << std::endl; for( unsigned i=0; isecond.d_exp, itit->second.d_pol==-1 ? nrc[i].negate() : nrc[i], effort==0 ? "EXTF_d" : "EXTF_d-N" ); } }else{ to_reduce = nrc; @@ -1360,14 +1389,15 @@ void TheoryStrings::checkExtendedFuncsEval( int effort ) { to_reduce = n; } if( !to_reduce.isNull() ){ + Assert( effort<3 ); if( effort==1 ){ Trace("strings-extf") << " cannot rewrite extf : " << to_reduce << std::endl; } - checkExtfInference( n, to_reduce, effort ); + checkExtfInference( n, to_reduce, itit->second, effort ); if( Trace.isOn("strings-extf-list") ){ Trace("strings-extf-list") << " * " << to_reduce; - if( d_extf_pol[n]!=0 ){ - Trace("strings-extf-list") << ", pol = " << d_extf_pol[n]; + if( itit->second.d_pol!=0 ){ + Trace("strings-extf-list") << ", pol = " << itit->second.d_pol; } if( n!=to_reduce ){ Trace("strings-extf-list") << ", from " << n; @@ -1375,63 +1405,66 @@ void TheoryStrings::checkExtendedFuncsEval( int effort ) { Trace("strings-extf-list") << std::endl; } } + if( d_ext_func_terms[n] && itit->second.d_model_active ){ + has_nreduce = true; + } }else{ Trace("strings-extf-debug") << " already reduced " << (*it).first << std::endl; } } + d_has_extf = has_nreduce; } -void TheoryStrings::checkExtfInference( Node n, Node nr, int effort ){ +void TheoryStrings::checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int effort ){ //make additional inferences that do not contribute to the reduction of n, but may help show a refutation - int n_pol = d_extf_pol[n]; - if( n_pol!=0 ){ + if( in.d_pol!=0 ){ //add original to explanation - d_extf_exp[n].push_back( n_pol==1 ? n : n.negate() ); + in.d_exp.push_back( in.d_pol==1 ? n : n.negate() ); //d_extf_infer_cache stores whether we have made the inferences associated with a node n, // this may need to be generalized if multiple inferences apply if( nr.getKind()==kind::STRING_IN_REGEXP ){ - if( n_pol==1 && nr[1].getKind()==kind::REGEXP_RANGE ){ + if( in.d_pol==1 && nr[1].getKind()==kind::REGEXP_RANGE ){ if( d_extf_infer_cache.find( nr )==d_extf_infer_cache.end() ){ d_extf_infer_cache.insert( nr ); //length of first argument is one Node conc = d_one.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, nr[0]) ); - sendInference( d_extf_exp[n], conc, "RE-Range-Len", true ); + sendInference( in.d_exp, conc, "RE-Range-Len", true ); } } }else 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( ( in.d_pol==1 && nr[1].getKind()==kind::STRING_CONCAT ) || ( in.d_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 - int index = n_pol==1 ? 1 : 0; + int index = in.d_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] ); + //Node exp_n = mkAnd( exp ); 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; - sendInference( d_extf_exp[n], n_pol==1 ? conc : conc.negate(), "CTN_Decompose" ); + sendInference( in.d_exp, in.d_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() ){ + bool pol = in.d_pol==1; + if( std::find( d_extf_info_tmp[nr[0]].d_ctn[pol].begin(), d_extf_info_tmp[nr[0]].d_ctn[pol].end(), nr[1] )==d_extf_info_tmp[nr[0]].d_ctn[pol].end() ){ Trace("strings-extf-debug") << " store contains info : " << nr[0] << " " << pol << " " << nr[1] << std::endl; - d_extf_info[nr[0]].d_ctn[pol].push_back( nr[1] ); - d_extf_info[nr[0]].d_ctn_from[pol].push_back( n ); + d_extf_info_tmp[nr[0]].d_ctn[pol].push_back( nr[1] ); + d_extf_info_tmp[nr[0]].d_ctn_from[pol].push_back( n ); //transitive closure for contains bool opol = !pol; - for( unsigned i=0; imkNode( kind::STRING_STRCTN, pol ? nr[1] : onr, pol ? onr : nr[1] ); conc = Rewriter::rewrite( conc ); bool do_infer = false; @@ -1442,12 +1475,12 @@ void TheoryStrings::checkExtfInference( Node n, Node nr, int effort ){ } if( do_infer ){ conc = conc.negate(); - std::vector< Node > exp; - exp.insert( exp.end(), d_extf_exp[n].begin(), d_extf_exp[n].end() ); - Node ofrom = d_extf_info[nr[0]].d_ctn_from[opol][i]; - Assert( d_extf_exp.find( ofrom )!=d_extf_exp.end() ); - exp.insert( exp.end(), d_extf_exp[ofrom].begin(), d_extf_exp[ofrom].end() ); - sendInference( exp, conc, "CTN_Trans" ); + std::vector< Node > exp_c; + exp_c.insert( exp_c.end(), in.d_exp.begin(), in.d_exp.end() ); + Node ofrom = d_extf_info_tmp[nr[0]].d_ctn_from[opol][i]; + Assert( d_extf_info_tmp.find( ofrom )!=d_extf_info_tmp.end() ); + exp_c.insert( exp_c.end(), d_extf_info_tmp[ofrom].d_exp.begin(), d_extf_info_tmp[ofrom].d_exp.end() ); + sendInference( exp_c, conc, "CTN_Trans" ); } } }else{ @@ -1459,7 +1492,7 @@ void TheoryStrings::checkExtfInference( Node n, Node nr, int effort ){ } } -void TheoryStrings::collectVars( Node n, std::map< Node, std::vector< Node > >& vars, std::map< Node, bool >& visited ) { +void TheoryStrings::collectVars( Node n, std::vector< Node >& vars, std::map< Node, bool >& visited ) { if( !n.isConst() ){ if( visited.find( n )==visited.end() ){ visited[n] = true; @@ -1468,8 +1501,9 @@ void TheoryStrings::collectVars( Node n, std::map< Node, std::vector< Node > >& collectVars( n[i], vars, visited ); } }else{ - Node nr = getRepresentative( n ); - vars[nr].push_back( n ); + //Node nr = getRepresentative( n ); + //vars[nr].push_back( n ); + vars.push_back( n ); } } } @@ -1748,7 +1782,7 @@ void TheoryStrings::checkFlatForms() { if( !hasProcessed() ){ // simple extended func reduction Trace("strings-process") << "Check extended function reduction effort=1..." << std::endl; - checkExtfReduction( 1 ); + checkExtfReductions( 1 ); Trace("strings-process") << "Done check extended function reduction" << std::endl; } } @@ -1883,7 +1917,7 @@ void TheoryStrings::checkNormalForms(){ } Trace("strings-nf") << std::endl; } - checkExtendedFuncsEval( 1 ); + checkExtfEval( 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() ){ @@ -3558,8 +3592,7 @@ Node TheoryStrings::ppRewrite(TNode atom) { if( !options::stringLazyPreproc() ){ //eager preprocess here std::vector< Node > new_nodes; - std::map< Node, Node > visited; - Node ret = d_preproc.simplifyRec( atom, new_nodes, visited ); + Node ret = d_preproc.processAssertion( atom, new_nodes ); if( ret!=atom ){ Trace("strings-ppr") << " rewrote " << atom << " -> " << ret << ", with " << new_nodes.size() << " lemmas." << std::endl; for( unsigned i=0; i& vi n.getKind() == kind::STRING_ITOS || n.getKind() == kind::STRING_U16TOS || n.getKind() == kind::STRING_U32TOS || n.getKind() == kind::STRING_STOI || n.getKind() == kind::STRING_STOU16 || n.getKind() == kind::STRING_STOU32 || n.getKind() == kind::STRING_STRREPL || n.getKind() == kind::STRING_STRCTN ){ - if( d_ext_func_terms.find( n )==d_ext_func_terms.end() ){ - Trace("strings-extf-debug2") << "Found extended function : " << n << std::endl; - Assert( options::stringLazyPreproc() ); - d_ext_func_terms[n] = true; - } + addExtendedFuncTerm( n ); } for( unsigned i=0; i& vi } } +void TheoryStrings::addExtendedFuncTerm( Node n ) { + if( d_ext_func_terms.find( n )==d_ext_func_terms.end() ){ + Trace("strings-extf-debug2") << "Found extended function : " << n << std::endl; + Assert( n.getKind()==kind::STRING_IN_REGEXP || options::stringLazyPreproc() ); + d_ext_func_terms[n] = true; + d_has_extf = true; + std::map< Node, bool > visited; + collectVars( n, d_extf_info[n].d_vars, visited ); + } +} + // Stats TheoryStrings::Statistics::Statistics(): d_splits("TheoryStrings::NumOfSplitOnDemands", 0), @@ -3979,8 +4019,9 @@ void TheoryStrings::checkMemberships() { if( (*it).second ){ Node n = (*it).first; if( n.getKind()==kind::STRING_IN_REGEXP ) { - bool pol = d_extf_pol[n]==1; - Assert( d_extf_pol[n]==1 || d_extf_pol[n]==-1 ); + Assert( d_extf_info_tmp.find( n )!=d_extf_info_tmp.end() ); + Assert( d_extf_info_tmp[n].d_pol==1 || d_extf_info_tmp[n].d_pol==-1 ); + bool pol = d_extf_info_tmp[n].d_pol==1; Trace("strings-process-debug") << " add membership : " << n << ", pol = " << pol << std::endl; addMembership( pol ? n : n.negate() ); } diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index c4a3e85cd..99abd94ce 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -194,8 +194,8 @@ private: class TermIndex { public: Node d_data; - std::map< Node, TermIndex > d_children; - Node add( Node n, unsigned index, TheoryStrings* t, Node er, std::vector< Node >& c ); + std::map< TNode, TermIndex > d_children; + Node add( TNode n, unsigned index, TheoryStrings* t, Node er, std::vector< Node >& c ); void clear(){ d_children.clear(); } }; std::map< Kind, TermIndex > d_term_index; @@ -245,18 +245,53 @@ private: NodeNodeMap d_proxy_var_to_length; /** All the function terms that the theory has seen */ context::CDList d_functionsTerms; +private: + //extended string terms, map to whether they are active + NodeBoolMap d_ext_func_terms; + //any non-reduced extended functions exist + context::CDO< bool > d_has_extf; + // static information about extf + class ExtfInfo { + public: + //all variables in this term + std::vector< Node > d_vars; + }; + // non-static information about extf + class ExtfInfoTmp { + public: + void init(){ + d_pol = 0; + d_model_active = true; + } + // list of terms that something (does not) contain and their explanation + std::map< bool, std::vector< Node > > d_ctn; + std::map< bool, std::vector< Node > > d_ctn_from; + //polarity + int d_pol; + //explanation + std::vector< Node > d_exp; + //reps -> list of variables + std::map< Node, std::vector< Node > > d_rep_vars; + //false if it is reduced in the model + bool d_model_active; + }; + std::map< Node, ExtfInfo > d_extf_info; + std::map< Node, ExtfInfoTmp > d_extf_info_tmp; + //collect extended operator terms + void collectExtendedFuncTerms( Node n, std::map< Node, bool >& visited ); + void addExtendedFuncTerm( Node n ); private: //initial check void checkInit(); void checkConstantEquivalenceClasses( TermIndex* ti, std::vector< Node >& vecc ); //extended functions evaluation check - void checkExtendedFuncsEval( int effort = 0 ); - void checkExtfInference( Node n, Node nr, int effort ); - void collectVars( Node n, std::map< Node, std::vector< Node > >& vars, std::map< Node, bool >& visited ); + void checkExtfEval( int effort = 0 ); + void checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int effort ); + void collectVars( Node n, std::vector< Node >& vars, std::map< Node, bool >& visited ); Node getSymbolicDefinition( Node n, std::vector< Node >& exp ); //check extf reduction - void checkExtfReduction( int effort ); - void checkReduction( Node atom, int pol, int effort ); + void checkExtfReductions( int effort ); + void checkExtfReduction( Node atom, int pol, int effort ); //flat forms check void checkFlatForms(); Node checkCycles( Node eqc, std::vector< Node >& curr, std::vector< Node >& exp ); @@ -391,21 +426,6 @@ protected: void printConcat( std::vector< Node >& n, const char * c ); void inferSubstitutionProxyVars( Node n, std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& unproc ); -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; - // list of terms that something (does not) contain and their explanation - class ExtfInfo { - public: - std::map< bool, std::vector< Node > > d_ctn; - std::map< bool, std::vector< Node > > d_ctn_from; - }; - std::map< Node, int > d_extf_pol; - 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 ); // Symbolic Regular Expression private: diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 51feb15e6..e8f1b879a 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -38,24 +38,34 @@ StringsPreprocess::~StringsPreprocess(){ } -Node StringsPreprocess::getUfForNode( Node n ) { - //TODO: use this for eager preprocess - Kind k = n.getKind(); - std::map< Kind, Node >::iterator it = d_uf.find( k ); - if( it==d_uf.end() ){ +Node StringsPreprocess::getUfForNode( Kind k, Node n, unsigned id ) { + std::map< unsigned, Node >::iterator it = d_uf[k].find( id ); + if( it==d_uf[k].end() ){ std::vector< TypeNode > types; for( unsigned i=0; imkFunctionType( types, n.getType() ); Node f = NodeManager::currentNM()->mkSkolem( "sop", typ, "op created for string op" ); - d_uf[k] = f; + d_uf[k][id] = f; return f; }else{ return it->second; } } +//pro: congruence possible, con: introduces UF/requires theory combination +// currently hurts performance +//TODO: for all skolems below +Node StringsPreprocess::getUfAppForNode( Kind k, Node n, unsigned id ) { + std::vector< Node > children; + children.push_back( getUfForNode( k, n, id ) ); + for( unsigned i=0; imkNode( kind::APPLY_UF, children ); +} + //returns an n such that t can be replaced by n, under the assumption of lemmas in new_nodes Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { @@ -64,7 +74,12 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node retNode = t; if( t.getKind() == kind::STRING_SUBSTR ) { - Node skt = NodeManager::currentNM()->mkSkolem( "sst", NodeManager::currentNM()->stringType(), "created for substr" ); + Node skt; + if( options::stringUfReduct() ){ + skt = getUfAppForNode( kind::STRING_SUBSTR, t ); + }else{ + skt = NodeManager::currentNM()->mkSkolem( "sst", NodeManager::currentNM()->stringType(), "created for substr" ); + } Node t12 = NodeManager::currentNM()->mkNode( kind::PLUS, t[1], t[2] ); Node lt0 = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ); //start point is greater than or equal zero @@ -74,7 +89,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { //length is positive Node c3 = NodeManager::currentNM()->mkNode( kind::GT, t[2], d_zero ); Node cond = NodeManager::currentNM()->mkNode( kind::AND, c1, c2, c3 ); - + Node sk1 = NodeManager::currentNM()->mkSkolem( "ss1", NodeManager::currentNM()->stringType(), "created for substr" ); Node sk2 = NodeManager::currentNM()->mkSkolem( "ss2", NodeManager::currentNM()->stringType(), "created for substr" ); Node b11 = t[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, skt, sk2 ) ); @@ -94,7 +109,12 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node sk2 = NodeManager::currentNM()->mkSkolem( "io2", NodeManager::currentNM()->stringType(), "created for indexof" ); Node sk3 = NodeManager::currentNM()->mkSkolem( "io3", NodeManager::currentNM()->stringType(), "created for indexof" ); Node sk4 = NodeManager::currentNM()->mkSkolem( "io4", NodeManager::currentNM()->stringType(), "created for indexof" ); - Node skk = NodeManager::currentNM()->mkSkolem( "iok", NodeManager::currentNM()->integerType(), "created for indexof" ); + Node skk; + if( options::stringUfReduct() ){ + skk = getUfAppForNode( kind::STRING_STRIDOF, t ); + }else{ + skk = NodeManager::currentNM()->mkSkolem( "iok", NodeManager::currentNM()->integerType(), "created for indexof" ); + } Node st = NodeManager::currentNM()->mkNode( kind::STRING_SUBSTR, t[0], t[2], NodeManager::currentNM()->mkNode( kind::MINUS, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ), t[2] ) ); Node eq = st.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk2, sk3, sk4 ) ); new_nodes.push_back( eq ); @@ -139,8 +159,12 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { // NodeManager::currentNM()->mkNode(kind::GEQ, t[0], d_zero), // t[0], NodeManager::currentNM()->mkNode(kind::UMINUS, t[0]))); Node num = t[0]; - //Node pret = NodeManager::currentNM()->mkNode(kind::STRING_ITOS, num); - Node pret = NodeManager::currentNM()->mkSkolem( "itost", NodeManager::currentNM()->stringType(), "created for itos" ); + Node pret; + if( options::stringUfReduct() ){ + pret = NodeManager::currentNM()->mkNode(kind::STRING_ITOS, num); + }else{ + pret = NodeManager::currentNM()->mkSkolem( "itost", NodeManager::currentNM()->stringType(), "created for itos" ); + } Node lenp = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, pret); Node nonneg = NodeManager::currentNM()->mkNode(kind::GEQ, t[0], d_zero); @@ -246,8 +270,14 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { retNode = pret; } else if( t.getKind() == kind::STRING_STOI || t.getKind() == kind::STRING_STOU16 || t.getKind() == kind::STRING_STOU32 ) { Node str = t[0]; + Node pret; + if( options::stringUfReduct() ){ + pret = getUfAppForNode( kind::STRING_STOI, t ); + }else{ + pret = NodeManager::currentNM()->mkSkolem( "stoit", NodeManager::currentNM()->integerType(), "created for stoi" ); + } //Node pret = NodeManager::currentNM()->mkNode(kind::STRING_STOI, str); - Node pret = NodeManager::currentNM()->mkSkolem( "stoit", NodeManager::currentNM()->integerType(), "created for stoi" ); + //Node pret = getUfAppForNode( kind::STRING_STOI, t ); Node lenp = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, str); Node negone = NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) ); @@ -434,6 +464,21 @@ Node StringsPreprocess::simplifyRec( Node t, std::vector< Node > & new_nodes, st } } +Node StringsPreprocess::processAssertion( Node n, std::vector< Node > &new_nodes ) { + std::map< Node, Node > visited; + std::vector< Node > new_nodes_curr; + Node ret = simplifyRec( n, new_nodes_curr, visited ); + while( !new_nodes_curr.empty() ){ + Node curr = new_nodes_curr.back(); + new_nodes_curr.pop_back(); + std::vector< Node > new_nodes_tmp; + curr = simplifyRec( curr, new_nodes_tmp, visited ); + new_nodes_curr.insert( new_nodes_curr.end(), new_nodes_tmp.begin(), new_nodes_tmp.end() ); + new_nodes.push_back( curr ); + } + return ret; +} + void StringsPreprocess::processAssertions( std::vector< Node > &vec_node ){ std::map< Node, Node > visited; for( unsigned i=0; i d_uf; + std::map< Kind, std::map< unsigned, Node > > d_uf; //get UF for node - Node getUfForNode( Node n ); + Node getUfForNode( Kind k, Node n, unsigned id = 0 ); + Node getUfAppForNode( Kind k, Node n, unsigned id = 0 ); + //recursive simplify + Node simplifyRec( Node t, std::vector< Node > &new_nodes, std::map< Node, Node >& visited ); public: StringsPreprocess( context::UserContext* u ); ~StringsPreprocess(); - //simplify a node + //returns a node that is equivalent to t under assumptions in new_nodes Node simplify( Node t, std::vector< Node > &new_nodes ); - //recursive simplify - Node simplifyRec( Node t, std::vector< Node > &new_nodes, std::map< Node, Node >& visited ); - //simplify each node in vec_node - void processAssertions(std::vector< Node > &vec_node); + //process assertion: guarentees to remove all extf + Node processAssertion( Node n, std::vector< Node > &new_nodes ); + //proces assertions: guarentees to remove all extf, rewrite in place + void processAssertions( std::vector< Node > &vec_node ); }; }/* CVC4::theory::strings namespace */ -- 2.30.2