diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-30 11:57:58 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-08-30 11:57:58 -0500 |
commit | bc0c0b8b9ea77e8e4e328dbe66a4582fa7883eda (patch) | |
tree | 4f43e20e294ade551676847668ceb424d44bab4f /src/theory/strings/theory_strings.h | |
parent | 3eac9d04c5d4bfba81142d4a5fe91b86590b32ae (diff) |
Add regular expression elimination module (#2400)
Diffstat (limited to 'src/theory/strings/theory_strings.h')
-rw-r--r-- | src/theory/strings/theory_strings.h | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 2c0cb42aa..c1bb1e0a0 100644 --- 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 ); |