From 641c531bcb9df45ca6c19f3f9ccfad08afbe17de Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 30 Nov 2021 14:13:47 -0600 Subject: [PATCH] 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. --- src/expr/node_manager_template.cpp | 5 +++-- src/theory/strings/regexp_enumerator.cpp | 3 ++- test/regress/CMakeLists.txt | 1 + test/regress/regress0/ho/datatype-field-ho.smt2 | 7 +++++++ 4 files changed, 13 insertions(+), 3 deletions(-) create mode 100644 test/regress/regress0/ho/datatype-field-ho.smt2 diff --git a/src/expr/node_manager_template.cpp b/src/expr/node_manager_template.cpp index a3e267d95..b00d79322 100644 --- a/src/expr/node_manager_template.cpp +++ b/src/expr/node_manager_template.cpp @@ -692,9 +692,10 @@ std::vector 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 261d0008e..63b7ee7c1 100644 --- 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(type), d_senum(type, tep) + : TypeEnumeratorBase(type), + d_senum(NodeManager::currentNM()->stringType(), tep) { } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 2ed3ddb8b..686c0ff6e 100644 --- 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 index 000000000..34a23cabb --- /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) -- 2.30.2