Simplify making function types (#6447)

Previously, we were conditionally checking whether a function was "flat" e.g. did not have a function type as the range type.

The original motivation for this was to catch cases where the user made a declare-fun that had function return type, which is not permitted. All these checks are already done at the API level https://github.com/CVC4/CVC4/blob/master/src/api/cpp/cvc5_checks.h#L441.

However, internally we should have no such restriction. This is required for simplifying the LFSC term processor.

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 70f221091e07e9f57cf653fd2c61198dda07d407..591413a8aa8064d438afb102827b90db933dd425 100644 (file)
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -763,44 +763,37 @@ TypeNode NodeManager::RecTypeCache::getRecordType( NodeManager * nm, const Recor
       nm, rec, index + 1);
 }
 
-TypeNode NodeManager::mkFunctionType(const std::vector<TypeNode>& sorts,
-                                     bool reqFlat)
+TypeNode NodeManager::mkFunctionType(const std::vector<TypeNode>& sorts)
 {
   Assert(sorts.size() >= 2);
-  CheckArgument(!reqFlat || !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,
-                                      bool reqFlat)
+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, reqFlat);
+  return mkFunctionType(sortNodes);
 }
 
 TypeNode NodeManager::mkFunctionType(const TypeNode& domain,
-                                     const TypeNode& range,
-                                     bool reqFlat)
+                                     const TypeNode& range)
 {
   std::vector<TypeNode> sorts;
   sorts.push_back(domain);
   sorts.push_back(range);
-  return mkFunctionType(sorts, reqFlat);
+  return mkFunctionType(sorts);
 }
 
 TypeNode NodeManager::mkFunctionType(const std::vector<TypeNode>& argTypes,
-                                     const TypeNode& range,
-                                     bool reqFlat)
+                                     const TypeNode& range)
 {
   Assert(argTypes.size() >= 1);
   std::vector<TypeNode> sorts(argTypes);
   sorts.push_back(range);
-  return mkFunctionType(sorts, reqFlat);
+  return mkFunctionType(sorts);
 }
 
 TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) {

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 6cda50075fb29b0a8fe24dd6c0af59211650df63..1208069555586f3f22b714cc38ac2793d17c7818 100644 (file)
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -846,15 +846,10 @@ class NodeManager
    *
    * @param domain the domain type
    * @param range the range type
-   * @param reqFlat If true, we require flat function types, e.g. the
-   * range type cannot be a function. User-generated function types and those
-   * used in solving must be flat, although some use cases (e.g. LFSC proof
-   * conversion) require non-flat function types.
    * @returns the functional type domain -> range
    */
   TypeNode mkFunctionType(const TypeNode& domain,
-                          const TypeNode& range,
-                          bool reqFlat = true);
+                          const TypeNode& range);
 
   /**
    * Make a function type with input types from
@@ -862,12 +857,10 @@ class NodeManager
    *
    * @param argTypes the domain is a tuple (argTypes[0], ..., argTypes[n])
    * @param range the range type
-   * @param reqFlat Same as above
    * @returns the functional type (argTypes[0], ..., argTypes[n]) -> range
    */
   TypeNode mkFunctionType(const std::vector<TypeNode>& argTypes,
-                          const TypeNode& range,
-                          bool reqFlat = true);
+                          const TypeNode& range);
 
   /**
    * Make a function type with input types from
@@ -877,10 +870,9 @@ class NodeManager
    *
    * @param sorts The argument and range sort of the function type, where the
    * range type is the last in this vector.
-   * @param reqFlat Same as above
+   * @return the function type
    */
-  TypeNode mkFunctionType(const std::vector<TypeNode>& sorts,
-                          bool reqFlat = true);
+  TypeNode mkFunctionType(const std::vector<TypeNode>& sorts);
 
   /**
    * Make a predicate type with input types from
@@ -888,8 +880,7 @@ class NodeManager
    * <code>BOOLEAN</code>. <code>sorts</code> must have at least one
    * element.
    */
-  TypeNode mkPredicateType(const std::vector<TypeNode>& sorts,
-                           bool reqFlat = true);
+  TypeNode mkPredicateType(const std::vector<TypeNode>& sorts);
 
   /**
    * Make a tuple type with types from