diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-26 13:39:06 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-26 13:39:06 -0600 |
| commit | 135f99f365920097ce48be87cb77fb1144d446a3 (patch) | |
| tree | 9a83a6c90aafca0de217a1fee3fd943199926ee2 /src/theory/strings/theory_strings.h | |
| parent | a1135ca591276f6d02b3632bc77a3934ded2d2af (diff) | |
Refactoring of inferences in strings. Add several options.
Diffstat (limited to 'src/theory/strings/theory_strings.h')
| -rw-r--r-- | src/theory/strings/theory_strings.h | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index fef2983fd..63098552d 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -174,7 +174,7 @@ private: NodeBoolMap d_preproc_cache; // extended functions inferences cache NodeSet d_extf_infer_cache; - + std::vector< Node > d_empty_vec; private: NodeSet d_congruent; std::map< Node, Node > d_eqc_to_const; @@ -337,6 +337,8 @@ protected: //register term void registerTerm( Node n, int effort ); //send lemma + void sendInference( std::vector< Node >& exp, std::vector< Node >& exp_n, Node eq, const char * c, bool asLemma = false ); + void sendInference( std::vector< Node >& exp, Node eq, const char * c, bool asLemma = false ); void sendLemma( Node ant, Node conc, const char * c ); void sendInfer( Node eq_exp, Node eq, const char * c ); void sendSplit( Node a, Node b, const char * c, bool preq = true ); |