diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-01 09:08:46 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-08-01 09:08:46 -0500 |
commit | 79881c196e29ef341166e7a31c1183e8b537d069 (patch) | |
tree | 25466cceb67c54895bf012fd745dd864d356b153 /src/theory/strings/regexp_operation.h | |
parent | 7537ff075dbb2d814d722d2d72586ce78235467c (diff) |
Regular expression intersection modes (#3134)
Diffstat (limited to 'src/theory/strings/regexp_operation.h')
-rw-r--r-- | src/theory/strings/regexp_operation.h | 24 |
1 files changed, 23 insertions, 1 deletions
diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h index 8f9541e91..cb35b37c6 100644 --- a/src/theory/strings/regexp_operation.h +++ b/src/theory/strings/regexp_operation.h @@ -33,6 +33,25 @@ namespace CVC4 { namespace theory { namespace strings { +/** + * Information on whether regular expressions contain constants or re.allchar. + * + * The order of this enumeration matters: the larger the value, the more + * possible regular expressions could fit the description. + */ +enum RegExpConstType +{ + // the regular expression doesn't contain variables or re.allchar or re.range + RE_C_CONRETE_CONSTANT, + // the regular expression doesn't contain variables, but may contain + // re.allchar or re.range + RE_C_CONSTANT, + // the regular expression may contain variables + RE_C_VARIABLE, + // the status of the regular expression is unknown (used internally) + RE_C_UNKNOWN, +}; + class RegExpOpr { typedef std::pair< Node, CVC4::String > PairNodeStr; typedef std::set< Node > SetNodes; @@ -58,7 +77,8 @@ class RegExpOpr { std::map<PairNodeStr, Node> d_dv_cache; std::map<PairNodeStr, std::pair<Node, int> > d_deriv_cache; std::map<Node, std::pair<Node, int> > d_compl_cache; - std::map<Node, bool> d_cstre_cache; + /** cache mapping regular expressions to whether they contain constants */ + std::unordered_map<Node, RegExpConstType, NodeHashFunction> d_constCache; std::map<Node, std::pair<std::set<unsigned>, std::set<Node> > > d_cset_cache; std::map<Node, std::pair<std::set<unsigned>, std::set<Node> > > d_fset_cache; std::map<PairNodes, Node> d_inter_cache; @@ -96,6 +116,8 @@ class RegExpOpr { * are such that t is a constant (or rewrites to one). */ bool checkConstRegExp( Node r ); + /** get the constant type for regular expression r */ + RegExpConstType getRegExpConstType(Node r); void simplify(Node t, std::vector< Node > &new_nodes, bool polarity); int delta( Node r, Node &exp ); int derivativeS( Node r, CVC4::String c, Node &retNode ); |