diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-10-15 11:43:14 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-10-15 11:43:25 +0200 |
| commit | f4420f2a1f82ee4a2f86d6d4318286d21520e280 (patch) | |
| tree | 3fdca2248b22fe75bd16a2c2bdfcd159028c3f0b /src/theory/strings/theory_strings.h | |
| parent | 8d2144dcb7662baec8e2b744246b3bc77f37cce1 (diff) | |
Decompose string contains, minor refactoring.
Diffstat (limited to 'src/theory/strings/theory_strings.h')
| -rw-r--r-- | src/theory/strings/theory_strings.h | 12 |
1 files changed, 9 insertions, 3 deletions
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 ); |