diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-03-17 13:17:12 -0500 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-03-17 13:22:08 -0500 |
| commit | 00f3fb686189c2ec7c5bf9e3700292c7c8ec45b5 (patch) | |
| tree | ba25bdbe1e63cabe8efafd1a0c1d1cf0cebd6439 /src/theory/strings/theory_strings.h | |
| parent | 52514303081e78c98e504980a50b76a04f4b8762 (diff) | |
hot fix for pre-reg term caching in strings
Diffstat (limited to 'src/theory/strings/theory_strings.h')
| -rw-r--r-- | src/theory/strings/theory_strings.h | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index c8a374893..902b902b6 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -157,6 +157,8 @@ private: // loop ant NodeSet d_loop_antec; NodeSet d_length_intro_vars; + // preReg cache + NodeSet d_prereg_cached; ///////////////////////////////////////////////////////////////////////////// // MODEL GENERATION @@ -194,8 +196,8 @@ private: std::map< Node, EqcInfo* > d_eqc_info; EqcInfo * getOrMakeEqcInfo( Node eqc, bool doMake = true ); //maintain which concat terms have the length lemma instantiated - NodeSet d_length_inst; - NodeBoolMap d_length_nodes; + NodeSet d_length_nodes; + NodeNodeMap d_length_inst; private: void mergeCstVec(std::vector< Node > &vec_strings); bool getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf, |