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 d23e44cee612da3c163a073d17cdf973f73c9a5c..fcfefbb43f03d7006ce8e1a7f231f73363c07c35 100644 (file)
--- 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 c92502c4052b20ab4809d5f019acab23323b995b..965fee2b846eb2050dfbfe3913b207ddf5e23037 100644 (file)
--- 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 4631b33c73db0db09a2d10390a0547a5482de169..5bc3ebd8b562cd49123414593103179734508fbe 100644 (file)
--- 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: