Do not require that function sorts are first class internally (#4128)

This PR removes the requirement in the NodeManager that argument types to the function sort are first class.

Notice that the new API does this check (as it should): https://github.com/CVC4/CVC4/blob/master/src/api/cvc4cpp.cpp#L2633

Moreover, SyGuS v2 internally requires constructing function types having arguments that are not first class (e.g. regular expression type). This is required to update the regression https://github.com/CVC4/CVC4/blob/master/test/regress/regress1/sygus/re-concat.sy to SyGuS v2.

FYI @abdoo8080 .

1 files changed, 36 insertions, 0 deletions

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 5d409f748..16ffd8306 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -575,6 +575,42 @@ TypeNode NodeManager::RecTypeCache::getRecordType( NodeManager * nm, const Recor
   }
 }
 
+TypeNode NodeManager::mkFunctionType(const std::vector<TypeNode>& sorts)
+{
+  Assert(sorts.size() >= 2);
+  CheckArgument(!sorts[sorts.size() - 1].isFunction(),
+                sorts[sorts.size() - 1],
+                "must flatten function types");
+  return mkTypeNode(kind::FUNCTION_TYPE, sorts);
+}
+
+TypeNode NodeManager::mkPredicateType(const std::vector<TypeNode>& sorts)
+{
+  Assert(sorts.size() >= 1);
+  std::vector<TypeNode> sortNodes;
+  sortNodes.insert(sortNodes.end(), sorts.begin(), sorts.end());
+  sortNodes.push_back(booleanType());
+  return mkFunctionType(sortNodes);
+}
+
+TypeNode NodeManager::mkFunctionType(const TypeNode& domain,
+                                     const TypeNode& range)
+{
+  std::vector<TypeNode> sorts;
+  sorts.push_back(domain);
+  sorts.push_back(range);
+  return mkFunctionType(sorts);
+}
+
+TypeNode NodeManager::mkFunctionType(const std::vector<TypeNode>& argTypes,
+                                     const TypeNode& range)
+{
+  Assert(argTypes.size() >= 1);
+  std::vector<TypeNode> sorts(argTypes);
+  sorts.push_back(range);
+  return mkFunctionType(sorts);
+}
+
 TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) {
   std::vector< TypeNode > ts;
   Debug("tuprec-debug") << "Make tuple type : ";