diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-10-21 10:47:52 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-10-21 10:47:52 +0200 |
| commit | 7e133dbb7c1adf077102d377d1f7eecae1640ee1 (patch) | |
| tree | 4423ff00d0957d65866e5151b776486f4c95e693 /src/theory/strings/theory_strings.h | |
| parent | cd119eedadb0431cfbcfc6c3ae037781ae849ee4 (diff) | |
Minor refactoring in strings related to length.
Diffstat (limited to 'src/theory/strings/theory_strings.h')
| -rw-r--r-- | src/theory/strings/theory_strings.h | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 125e1c1eb..40358649b 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -165,6 +165,7 @@ private: NodeSet d_loop_antec; NodeSet d_length_intro_vars; // preReg cache + NodeSet d_pregistered_terms_cache; NodeSet d_registered_terms_cache; // preprocess cache StringsPreprocess d_preproc; @@ -332,7 +333,7 @@ protected: void addToExplanation( Node lit, std::vector< Node >& exp ); //register term - bool registerTerm( Node n ); + void registerTerm( Node n, int effort ); //send lemma void sendLemma( Node ant, Node conc, const char * c ); void sendInfer( Node eq_exp, Node eq, const char * c ); |