From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 22 Feb 2022 19:11:45 +0000 (-0600)
Subject: Support some cases of isConst for regular expressions (#8114)
X-Git-Tag: cvc5-1.0.0~405
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=33fab4e47b9f5cc7dae76a30d7850a82bf8290d7;p=cvc5.git

Support some cases of isConst for regular expressions (#8114)

Fixes https://github.com/cvc5/cvc5/issues/8111.

Having `isConst` return true is required for some rare use cases of regular expressions, e.g. rewrite rule synthesis involving regular expression variables.
---

diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index d23e44cee..fcfefbb43 100644
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -141,11 +141,14 @@ typerule REGEXP_REPEAT "SimpleTypeRule<RRegExp, ARegExp>"
 typerule REGEXP_LOOP_OP "SimpleTypeRule<RBuiltinOperator>"
 typerule REGEXP_LOOP "SimpleTypeRule<RRegExp, ARegExp>"
 typerule REGEXP_COMPLEMENT "SimpleTypeRule<RRegExp, ARegExp>"
-typerule STRING_TO_REGEXP "SimpleTypeRule<RRegExp, AString>"
+typerule STRING_TO_REGEXP ::cvc5::theory::strings::StringToRegExpTypeRule
 typerule STRING_IN_REGEXP "SimpleTypeRule<RBool, AString, ARegExp>"
 typerule REGEXP_NONE "SimpleTypeRule<RRegExp>"
 typerule REGEXP_ALLCHAR "SimpleTypeRule<RRegExp>"
 
+# we return isConst for some regular expressions, including all that we enumerate
+construle STRING_TO_REGEXP ::cvc5::theory::strings::StringToRegExpTypeRule
+
 ### operators that apply to both strings and sequences
 
 typerule STRING_CONCAT ::cvc5::theory::strings::StringConcatTypeRule
diff --git a/src/theory/strings/theory_strings_type_rules.cpp b/src/theory/strings/theory_strings_type_rules.cpp
index c92502c40..965fee2b8 100644
--- a/src/theory/strings/theory_strings_type_rules.cpp
+++ b/src/theory/strings/theory_strings_type_rules.cpp
@@ -292,6 +292,27 @@ TypeNode RegExpRangeTypeRule::computeType(NodeManager* nodeManager,
   return nodeManager->regExpType();
 }
 
+TypeNode StringToRegExpTypeRule::computeType(NodeManager* nodeManager,
+                                             TNode n,
+                                             bool check)
+{
+  if (check)
+  {
+    if (!n[0].getType().isString())
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "expecting string term in string to regexp");
+    }
+  }
+  return nodeManager->regExpType();
+}
+
+bool StringToRegExpTypeRule::computeIsConst(NodeManager* nodeManager, TNode n)
+{
+  Assert(n.getKind() == kind::STRING_TO_REGEXP);
+  return n[0].isConst();
+}
+
 TypeNode ConstSequenceTypeRule::computeType(NodeManager* nodeManager,
                                             TNode n,
                                             bool check)
diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h
index 4631b33c7..5bc3ebd8b 100644
--- a/src/theory/strings/theory_strings_type_rules.h
+++ b/src/theory/strings/theory_strings_type_rules.h
@@ -93,6 +93,25 @@ public:
  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
+class StringToRegExpTypeRule
+{
+ public:
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+
+  /**
+   * Returns true if the argument to STRING_TO_REGEXP is a constant.
+   *
+   * In general, our implementation of isConst is incomplete for regular
+   * expressions, i.e. it is possible to return isConst for more regular
+   * expression terms.
+   *
+   * However, we at least require returning isConst true for STRING_TO_REGEXP
+   * applied to constant strings, as the regular expression enumerator uses
+   * these.
+   */
+  static bool computeIsConst(NodeManager* nodeManager, TNode n);
+};
+
 class ConstSequenceTypeRule
 {
  public: