Proper check for first-class types in datatype subfields (#7712)

Fixes two issues with our check for datatype subfields (isFunctionLike -> isFirstClass): functions should be allowed, RegLan should not.

Fixes cvc5/cvc5-projects#368. That issue now throws an error:

(error "Parse Error: proj-368.smt2:3.39: cannot use fields in datatypes that are not first class types

  (declare-datatype x ((_x (x8 RegLan))))
                                         ^
")
This adds a regression showing we allow functions as subfields.

diff --git a/src/expr/node_manager_template.cpp b/src/expr/node_manager_template.cpp
index a3e267d95de62c94572dd63a4bb9ba4031255204..b00d793225c1f9163448742aad5c7574a3a88244 100644 (file)
--- a/src/expr/node_manager_template.cpp
+++ b/src/expr/node_manager_template.cpp
@@ -692,9 +692,10 @@ std::vector<TypeNode> NodeManager::mkMutualDatatypeTypes(
         // This next one's a "hard" check, performed in non-debug builds
         // as well; the other ones should all be guaranteed by the
         // cvc5::DType class, but this actually needs to be checked.
-        if (selectorType.getRangeType().isFunctionLike())
+        if (!selectorType.getRangeType().isFirstClass())
         {
-          throw Exception("cannot put function-like things in datatypes");
+          throw Exception(
+              "cannot use fields in datatypes that are not first class types");
         }
       }
     }

diff --git a/src/theory/strings/regexp_enumerator.cpp b/src/theory/strings/regexp_enumerator.cpp
index 261d0008e3b68089ae57fdbe24d8f8dc016db6ee..63b7ee7c1d6cbe43eb56716c3742bb148c9cd985 100644 (file)
--- a/src/theory/strings/regexp_enumerator.cpp
+++ b/src/theory/strings/regexp_enumerator.cpp
@@ -20,7 +20,8 @@ namespace theory {
 namespace strings {
 
 RegExpEnumerator::RegExpEnumerator(TypeNode type, TypeEnumeratorProperties* tep)
-    : TypeEnumeratorBase<RegExpEnumerator>(type), d_senum(type, tep)
+    : TypeEnumeratorBase<RegExpEnumerator>(type),
+      d_senum(NodeManager::currentNM()->stringType(), tep)
 {
 }
 

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 2ed3ddb8b5220042eea033396db35a83954584d6..686c0ff6ee8d4ae8f0e1ce4e4b6636f2a55adf8d 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -631,6 +631,7 @@ set(regress_0_tests
   regress0/ho/bug_nodbuilding_interpreted_SYO042^1.p
   regress0/ho/cong-full-apply.smt2
   regress0/ho/cong.smt2
+  regress0/ho/datatype-field-ho.smt2
   regress0/ho/declare-fun-variants.smt2
   regress0/ho/def-fun-flatten.smt2
   regress0/ho/ext-finite-unsat.smt2

diff --git a/test/regress/regress0/ho/datatype-field-ho.smt2 b/test/regress/regress0/ho/datatype-field-ho.smt2
new file mode 100644 (file)
index 0000000..34a23ca
--- /dev/null
+++ b/test/regress/regress0/ho/datatype-field-ho.smt2
@@ -0,0 +1,7 @@
+(set-logic HO_ALL)
+(set-info :status sat)
+(declare-datatype x ((C (s (-> Int Int)))))
+(declare-fun x1 () x)
+(declare-fun x2 () x)
+(assert (distinct x1 x2))
+(check-sat)