diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-10-11 15:35:14 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-10-11 15:35:14 +0200 |
commit | c6179b1922e0366acec51eec24a2023d21354030 (patch) | |
tree | 57804bae2910c556e704b2aa0fc3408ead7897b3 /src/theory | |
parent | 9833e6635f6b5bee825034715d15ad73e9955a88 (diff) |
Fix strings preprocessing + incremental, fixes bug 682. Add initial infrastructure for str.contains inferences.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 56 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.h | 9 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 10 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_preprocess.h | 7 |
4 files changed, 66 insertions, 16 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index f4019450d..997c47776 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -68,7 +68,9 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu d_loop_antec(u), d_length_intro_vars(u), d_registered_terms_cache(u), + d_preproc(u), d_preproc_cache(u), + d_extf_infer_cache(c), d_proxy_var(u), d_proxy_var_to_length(u), d_neg_ctn_eqlen(u), @@ -2054,8 +2056,8 @@ void TheoryStrings::sendInfer( Node eq_exp, Node eq, const char * c ) { Trace("strings-assert") << "(assert (=> " << eq_exp << " " << eq << ")) ; infer " << c << 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); + d_infer.push_back( eq ); + d_infer_exp.push_back( eq_exp ); } } @@ -3832,12 +3834,20 @@ void TheoryStrings::checkExtendedFuncsEval( int effort ) { for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){ if( (*it).second ){ Node n = (*it).first; + int n_pol = 0; + if( n.getType().isBoolean() ){ + if( areEqual( n, d_true ) ){ + n_pol = 1; + }else if( areEqual( n, d_false ) ){ + n_pol = -1; + } + } Trace("strings-extf-debug") << "Check extf " << n << "..." << std::endl; if( effort==0 ){ std::map< Node, bool > visited; collectVars( n, d_extf_vars[n], visited ); } - //build up a best current substitution for the variables in the term + //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; @@ -3873,7 +3883,7 @@ void TheoryStrings::checkExtendedFuncsEval( int effort ) { } } } - + Node to_reduce; if( !var.empty() ){ Node nr = n.substitute( var.begin(), var.end(), sub.begin(), sub.end() ); Node nrc = Rewriter::rewrite( nr ); @@ -3929,16 +3939,46 @@ void TheoryStrings::checkExtendedFuncsEval( int effort ) { return; } } + }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 ); + Trace("strings-extf-debug") << " decomposable..." << std::endl; + Trace("strings-extf") << " resolve extf : " << nr << " -> " << nrc << ", pol = " << n_pol << std::endl; + for( unsigned i=0; i<nrc.getNumChildren(); i++ ){ + sendInfer( mkAnd( exp ), n_pol==-1 ? nrc[i].negate() : nrc[i], effort==0 ? "EXTF_d" : "EXTF_d-N" ); + } //}else if( hasTerm( nrc ) && !areEqual( nrc, n ) ){ // Trace("strings-extf-debug") << "Reduction inference : " << nrc << " " << n << std::endl; TODO? }else{ - if( effort==1 ){ - Trace("strings-extf") << " cannot rewrite extf : " << nrc << std::endl; - } + to_reduce = nrc; } }else{ + to_reduce = n; + } + if( !to_reduce.isNull() ){ + //TODO + //checkExtfInference( n, to_reduce, n_pol, exp, effort ); if( effort==1 ){ - Trace("strings-extf") << " cannot rewrite extf : " << n << std::endl; + Trace("strings-extf") << " cannot rewrite extf : " << to_reduce << std::endl; + } + } + } + } +} + +void TheoryStrings::checkExtfInference( Node n, Node nr, int n_pol, std::vector< Node >& exp, 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 ) ){ + //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; + for( unsigned i=0; i<nr[index].getNumChildren(); i++ ){ + //TODO + } } } } diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 7e09a8e5b..af06519c0 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -157,7 +157,7 @@ private: std::vector< Node > d_pending; std::vector< Node > d_lemma_cache; std::map< Node, bool > d_pending_req_phase; - /** inferences */ + /** inferences: maintained to ensure ref count for internally introduced nodes */ NodeList d_infer; NodeList d_infer_exp; /** normal forms */ @@ -177,6 +177,8 @@ private: // preprocess cache StringsPreprocess d_preproc; NodeBoolMap d_preproc_cache; + // extended functions inferences cache + NodeSet d_extf_infer_cache; bool doPreprocess( Node atom ); bool hasProcessed(); @@ -277,6 +279,7 @@ 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 collectVars( Node n, std::map< Node, std::vector< Node > >& vars, std::map< Node, bool >& visited ); void checkNormalForms(); Node checkCycles( Node eqc, std::vector< Node >& curr, std::vector< Node >& exp ); @@ -319,6 +322,8 @@ public: void eqNotifyPostMerge(TNode t1, TNode t2); /** called when two equivalence classes are made disequal */ void eqNotifyDisequal(TNode t1, TNode t2, TNode reason); + /** get preprocess */ + StringsPreprocess * getPreprocess() { return &d_preproc; } protected: /** compute care graph */ void computeCareGraph(); @@ -360,7 +365,7 @@ 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 ); - + enum { sk_id_c_spt, sk_id_vc_spt, diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 4e2b00fb1..b2b7bac5e 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -25,7 +25,7 @@ namespace CVC4 { namespace theory { namespace strings { -StringsPreprocess::StringsPreprocess() { +StringsPreprocess::StringsPreprocess( context::UserContext* u ) : d_cache( u ){ //Constants d_zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) ); } @@ -119,7 +119,9 @@ void StringsPreprocess::processRegExp( Node s, Node r, std::vector< Node > &ret bool StringsPreprocess::checkStarPlus( Node t ) { if( t.getKind() != kind::REGEXP_STAR && t.getKind() != kind::REGEXP_PLUS ) { for( unsigned i = 0; i<t.getNumChildren(); ++i ) { - if( checkStarPlus(t[i]) ) return true; + if( checkStarPlus(t[i]) ){ + return true; + } } return false; } else { @@ -151,7 +153,7 @@ int StringsPreprocess::checkFixLenVar( Node t ) { return ret; } Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes, bool during_pp ) { - std::hash_map<TNode, Node, TNodeHashFunction>::const_iterator i = d_cache.find(t); + NodeNodeMap::const_iterator i = d_cache.find(t); if(i != d_cache.end()) { return (*i).second.isNull() ? t : (*i).second; } @@ -568,7 +570,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes, bool d } Node StringsPreprocess::decompose(Node t, std::vector< Node > & new_nodes, bool during_pp) { - std::hash_map<TNode, Node, TNodeHashFunction>::const_iterator i = d_cache.find(t); + NodeNodeMap::const_iterator i = d_cache.find(t); if(i != d_cache.end()) { return (*i).second.isNull() ? t : (*i).second; } diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h index 1255d93e0..a5ba1f615 100644 --- a/src/theory/strings/theory_strings_preprocess.h +++ b/src/theory/strings/theory_strings_preprocess.h @@ -23,14 +23,17 @@ #include "util/hash.h" #include "theory/theory.h" #include "theory/rewriter.h" +#include "context/cdchunk_list.h" +#include "context/cdhashmap.h" namespace CVC4 { namespace theory { namespace strings { class StringsPreprocess { + typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap; // NOTE: this class is NOT context-dependent - std::hash_map<TNode, Node, TNodeHashFunction> d_cache; + NodeNodeMap d_cache; //Constants Node d_zero; private: @@ -39,7 +42,7 @@ private: void processRegExp( Node s, Node r, std::vector< Node > &ret ); Node simplify( Node t, std::vector< Node > &new_nodes, bool during_pp ); public: - StringsPreprocess(); + StringsPreprocess( context::UserContext* u ); Node decompose( Node t, std::vector< Node > &new_nodes, bool during_pp = false ); void simplify(std::vector< Node > &vec_node); |