diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-24 01:40:17 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-24 01:42:26 -0400 |
| commit | 7736abe3b9c898033737865f033cc5cfe0f7922f (patch) | |
| tree | 8a1903164e4300b606beb9b64d663f3d2946709c /src/theory/strings/theory_strings.h | |
| parent | c948e9517b7b5f0bacb055ab2ad320f889c3fb49 (diff) | |
Squashed commit of the following:
* Fix a bug in intersection
* merging...
* add delayed length lemmas
* PreRegisterTerm is changed.
* Bug fix for string-opt2
* PreRegisterTerm is changed.
* add delayed length lemmas
* Bug fix for string-opt2
* PreRegisterTerm is changed.
* Bug fix for string-opt2
* PreRegisterTerm is changed.
* Bug fix for string-opt2
* PreRegisterTerm is changed.
Diffstat (limited to 'src/theory/strings/theory_strings.h')
| -rw-r--r-- | src/theory/strings/theory_strings.h | 15 |
1 files changed, 13 insertions, 2 deletions
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 2a33b400e..de5f62b1a 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -164,7 +164,11 @@ private: NodeSet d_loop_antec; NodeSet d_length_intro_vars; // preReg cache - NodeSet d_prereg_cached; + NodeSet d_registed_terms_cache; + // term cache + std::vector< Node > d_terms_cache; + void collectTerm( Node n ); + void appendTermLemma(); ///////////////////////////////////////////////////////////////////////////// // MODEL GENERATION @@ -271,12 +275,19 @@ protected: void doPendingFacts(); void doPendingLemmas(); + //register term + bool registerTerm( Node n ); + //send lemma 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 ); /** mkConcat **/ inline Node mkConcat( Node n1, Node n2 ); - inline Node mkConcat( std::vector< Node >& c ); + inline Node mkConcat( Node n1, Node n2, Node n3 ); + inline Node mkConcat( const std::vector< Node >& c ); + //mkSkolem + inline Node mkSkolemS(const char * c, int isLenSplit = 0); + //inline Node mkSkolemI(const char * c); /** mkExplain **/ Node mkExplain( std::vector< Node >& a ); Node mkExplain( std::vector< Node >& a, std::vector< Node >& an ); |