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/strings/theory_strings.h | |
| parent | 9833e6635f6b5bee825034715d15ad73e9955a88 (diff) | |
Fix strings preprocessing + incremental, fixes bug 682. Add initial infrastructure for str.contains inferences.
Diffstat (limited to 'src/theory/strings/theory_strings.h')
| -rw-r--r-- | src/theory/strings/theory_strings.h | 9 |
1 files changed, 7 insertions, 2 deletions
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, |