diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-07-26 15:15:46 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-07-26 15:15:57 -0500 |
| commit | 608bf149dda6dcb546445ead3eb98241f64b8876 (patch) | |
| tree | b204c165a1ba1c3d0aca1132f5e2255082be20d1 /src/theory/strings/theory_strings.h | |
| parent | 319bbda7ad32e6e9ee009c27003f6f1c0a8d7b20 (diff) | |
Minor improvements to strings related to constant splitting, including a few options (disabled by default).
Diffstat (limited to 'src/theory/strings/theory_strings.h')
| -rw-r--r-- | src/theory/strings/theory_strings.h | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index b8959f003..b4d7ce889 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -300,8 +300,8 @@ private: Node checkCycles( Node eqc, std::vector< Node >& curr, std::vector< Node >& exp ); //normal forms check void checkNormalForms(); - bool normalizeEquivalenceClass( Node n ); - bool getNormalForms( Node &eqc, std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src, + void normalizeEquivalenceClass( Node n ); + void getNormalForms( Node &eqc, std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src, std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend); bool detectLoop(std::vector< std::vector< Node > > &normal_forms, int i, int j, int index, int &loop_in_i, int &loop_in_j); @@ -311,13 +311,14 @@ private: int i, int j, int loop_n_index, int other_n_index, int loop_index, int index); bool processNEqc( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src, - std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend ); + std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend, + int effort ); bool processReverseNEq( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src, std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend, - unsigned i, unsigned j ); + unsigned i, unsigned j, unsigned& index, unsigned rproc ); bool processSimpleNEq( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src, std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend, - unsigned i, unsigned j, unsigned& index, bool isRev ); + unsigned i, unsigned j, unsigned& index, bool isRev, unsigned rproc ); bool processDeq( Node n1, Node n2 ); int processReverseDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj ); int processSimpleDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj, unsigned& index, bool isRev ); @@ -328,6 +329,8 @@ private: std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend, unsigned i, unsigned j, int index_i, int index_j, bool isRev, std::vector< Node >& curr_exp ); + Node collectConstantStringAt( std::vector< Node >& vec, int& index, bool isRev ); + //check membership constraints Node mkRegExpAntec(Node atom, Node ant); Node normalizeRegexp(Node r); |