Add regular expression elimination module (#2400)

[cvc5.git] / src / theory / strings / theory_strings.h

diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 2c0cb42aafddc76fba000b3ede65eecd22683bd4..c1bb1e0a067ad6e9eee0aa2a89bfae3d71854b7b 100644 (file)
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -22,6 +22,7 @@
 #include "context/cdhashset.h"
 #include "context/cdlist.h"
 #include "expr/attribute.h"
+#include "theory/strings/regexp_elim.h"
 #include "theory/strings/regexp_operation.h"
 #include "theory/strings/theory_strings_preprocess.h"
 #include "theory/theory.h"
@@ -618,10 +619,10 @@ private:
   NodeSet d_processed_memberships;
   // antecedant for why regexp membership must be true
   NodeNodeMap d_regexp_ant;
-  // membership length
-  //std::map< Node, bool > d_membership_length;
-  // regular expression operations
+  /** regular expression operation module */
   RegExpOpr d_regexp_opr;
+  /** regular expression elimination module */
+  RegExpElimination d_regexp_elim;
 
   CVC4::String getHeadConst( Node x );
   bool deriveRegExp( Node x, Node r, Node ant );