Various fixes related to isDatatypeXXX checks. (#8473)

diff --git a/src/expr/node_manager_template.cpp b/src/expr/node_manager_template.cpp
index 7ab63bc785bc2aa3abc0cbd7f985fd836d0ab076..a1fdc48fbc3ed1b7b4fafe1b9be1a794c18c1c1b 100644 (file)
--- 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 ae5ef34f6a8705f89b336c1867f6edf2c0e44abf..a55e52d2ea69f83af45f35b0b7883d9f5075c882 100644 (file)
--- 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 d86f197e54fc26577c912787aca81b8547df267f..1278e9bf24be37b3431e87f046c67bb45db469e3 100644 (file)
--- 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 f2a065b1f57bc4dde5d8850b3d88e2c2122b87ef..4de4f40afc63c028f2553be7e813019f80dfd5d3 100644 (file)
--- 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 64ac9d49ae531916e82bb853b15f4eb1e22be510..e7a0aaa59b2460ab93e18b08b667f581cf5eb23e 100644 (file)
--- 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.