From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Thu, 31 Mar 2022 21:27:39 +0000 (-0700)
Subject: Various fixes related to isDatatypeXXX checks. (#8473)
X-Git-Tag: cvc5-1.0.0~84
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bd45dc19adcfb3af6270e7e2373ea27f5b206205;p=cvc5.git

Various fixes related to isDatatypeXXX checks. (#8473)
---

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> 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.