Regular expression intersection modes (#3134)

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