From bd45dc19adcfb3af6270e7e2373ea27f5b206205 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Thu, 31 Mar 2022 14:27:39 -0700 Subject: [PATCH] Various fixes related to isDatatypeXXX checks. (#8473) --- src/expr/node_manager_template.cpp | 4 ++++ src/expr/symbol_table.cpp | 5 ----- src/expr/type_node.cpp | 6 ++++-- src/theory/quantifiers/sygus/sygus_abduct.cpp | 2 +- src/theory/quantifiers/sygus/sygus_interpol.cpp | 2 +- 5 files changed, 10 insertions(+), 9 deletions(-) diff --git a/src/expr/node_manager_template.cpp b/src/expr/node_manager_template.cpp index 7ab63bc78..a1fdc48fb 100644 --- a/src/expr/node_manager_template.cpp +++ b/src/expr/node_manager_template.cpp @@ -1271,6 +1271,10 @@ Kind NodeManager::getKindForFunction(TNode fun) { return kind::APPLY_TESTER; } + else if (tn.isDatatypeUpdater()) + { + return kind::APPLY_UPDATER; + } return kind::UNDEFINED_KIND; } diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp index ae5ef34f6..a55e52d2e 100644 --- a/src/expr/symbol_table.cpp +++ b/src/expr/symbol_table.cpp @@ -251,11 +251,6 @@ bool OverloadedTypeTrie::markOverloaded(const string& name, cvc5::Term obj) argTypes = t.getDatatypeConstructorDomainSorts(); rangeType = t.getDatatypeConstructorCodomainSort(); } - else if (t.isDatatypeTester()) - { - argTypes.push_back(t.getDatatypeTesterDomainSort()); - rangeType = t.getDatatypeTesterCodomainSort(); - } else if (t.isDatatypeSelector()) { argTypes.push_back(t.getDatatypeSelectorDomainSort()); diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index d86f197e5..1278e9bf2 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -356,7 +356,8 @@ std::vector TypeNode::getArgTypes() const { } else { - Assert(isFunction() || isDatatypeConstructor() || isDatatypeSelector()); + Assert(isFunction() || isDatatypeConstructor() || isDatatypeSelector() + || isDatatypeUpdater()); for (uint32_t i = 0, i_end = getNumChildren() - 1; i < i_end; ++i) { args.push_back((*this)[i]); @@ -698,7 +699,8 @@ TypeNode TypeNode::getRangeType() const { return NodeManager::currentNM()->booleanType(); } - Assert(isFunction() || isDatatypeConstructor() || isDatatypeSelector()) + Assert(isFunction() || isDatatypeConstructor() || isDatatypeSelector() + || isDatatypeUpdater()) << "Cannot get range type of " << *this; return (*this)[getNumChildren() - 1]; } diff --git a/src/theory/quantifiers/sygus/sygus_abduct.cpp b/src/theory/quantifiers/sygus/sygus_abduct.cpp index f2a065b1f..4de4f40af 100644 --- a/src/theory/quantifiers/sygus/sygus_abduct.cpp +++ b/src/theory/quantifiers/sygus/sygus_abduct.cpp @@ -62,7 +62,7 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name, { TypeNode tn = s.getType(); if (tn.isDatatypeConstructor() || tn.isDatatypeSelector() - || tn.isDatatypeTester()) + || tn.isDatatypeTester() || tn.isDatatypeUpdater()) { // datatype symbols should be considered interpreted symbols here, not // (higher-order) variables. diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp index 64ac9d49a..e7a0aaa59 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.cpp +++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp @@ -66,7 +66,7 @@ void SygusInterpol::createVariables(bool needsShared) { TypeNode tn = s.getType(); if (tn.isDatatypeConstructor() || tn.isDatatypeSelector() - || tn.isDatatypeTester()) + || tn.isDatatypeTester() || tn.isDatatypeUpdater()) { // datatype symbols should be considered interpreted symbols here, not // (higher-order) variables. -- 2.30.2