diff options
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 ); |