diff options
Diffstat (limited to 'src/theory/strings/theory_strings.h')
| -rw-r--r-- | src/theory/strings/theory_strings.h | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index bc53528f8..52bc37cb8 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -171,9 +171,6 @@ private: // extended functions inferences cache NodeSet d_extf_infer_cache; - bool doPreprocess( Node atom ); - - private: NodeSet d_congruent; std::map< Node, Node > d_eqc_to_const; @@ -244,6 +241,9 @@ private: void checkExtfInference( Node n, Node nr, int effort ); void collectVars( Node n, std::map< Node, std::vector< Node > >& vars, std::map< Node, bool >& visited ); Node getSymbolicDefinition( Node n, std::vector< Node >& exp ); + //check extf reduction + void checkExtfReduction( int effort ); + void checkReduction( Node atom, int pol, int effort ); //flat forms check void checkFlatForms(); Node checkCycles( Node eqc, std::vector< Node >& curr, std::vector< Node >& exp ); @@ -382,7 +382,6 @@ private: // Special String Functions NodeSet d_neg_ctn_eqlen; NodeSet d_neg_ctn_ulen; - NodeSet d_pos_ctn_cached; NodeSet d_neg_ctn_cached; //extended string terms and whether they have been reduced NodeBoolMap d_ext_func_terms; |