From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 27 Mar 2020 15:23:42 +0000 (-0500)
Subject: Do not require that function sorts are first class internally (#4128)
X-Git-Tag: cvc5-1.0.0~3438
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a64866663f10db4ffadd2d48500cda05c4831f0e;p=cvc5.git

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

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 : ";
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index eced00c48..2e8f40fff 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -807,7 +807,7 @@ public:
    * @param range the range type
    * @returns the functional type domain -> range
    */
-  inline TypeNode mkFunctionType(const TypeNode& domain, const TypeNode& range);
+  TypeNode mkFunctionType(const TypeNode& domain, const TypeNode& range);
 
   /**
    * Make a function type with input types from
@@ -817,8 +817,8 @@ public:
    * @param range the range type
    * @returns the functional type (argTypes[0], ..., argTypes[n]) -> range
    */
-  inline TypeNode mkFunctionType(const std::vector<TypeNode>& argTypes,
-                                 const TypeNode& range);
+  TypeNode mkFunctionType(const std::vector<TypeNode>& argTypes,
+                          const TypeNode& range);
 
   /**
    * Make a function type with input types from
@@ -826,7 +826,7 @@ public:
    * <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have
    * at least 2 elements.
    */
-  inline TypeNode mkFunctionType(const std::vector<TypeNode>& sorts);
+  TypeNode mkFunctionType(const std::vector<TypeNode>& sorts);
 
   /**
    * Make a predicate type with input types from
@@ -834,7 +834,7 @@ public:
    * <code>BOOLEAN</code>. <code>sorts</code> must have at least one
    * element.
    */
-  inline TypeNode mkPredicateType(const std::vector<TypeNode>& sorts);
+  TypeNode mkPredicateType(const std::vector<TypeNode>& sorts);
 
   /**
    * Make a tuple type with types from
@@ -1086,52 +1086,6 @@ inline TypeNode NodeManager::builtinOperatorType() {
   return TypeNode(mkTypeConst<TypeConstant>(BUILTIN_OPERATOR_TYPE));
 }
 
-/** Make a function type from domain to range. */
-inline TypeNode NodeManager::mkFunctionType(const TypeNode& domain, const TypeNode& range) {
-  std::vector<TypeNode> sorts;
-  sorts.push_back(domain);
-  sorts.push_back(range);
-  return mkFunctionType(sorts);
-}
-
-inline 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);
-}
-
-inline TypeNode
-NodeManager::mkFunctionType(const std::vector<TypeNode>& sorts) {
-  Assert(sorts.size() >= 2);
-  std::vector<TypeNode> sortNodes;
-  for (unsigned i = 0; i < sorts.size(); ++ i) {
-    CheckArgument(sorts[i].isFirstClass(),
-                  sorts,
-                  "cannot create function types for argument types that are "
-                  "not first-class. Try option --uf-ho.");
-    sortNodes.push_back(sorts[i]);
-  }
-  CheckArgument(!sorts[sorts.size()-1].isFunction(), sorts[sorts.size()-1],
-                "must flatten function types");
-  return mkTypeNode(kind::FUNCTION_TYPE, sortNodes);
-}
-
-inline TypeNode
-NodeManager::mkPredicateType(const std::vector<TypeNode>& sorts) {
-  Assert(sorts.size() >= 1);
-  std::vector<TypeNode> sortNodes;
-  for (unsigned i = 0; i < sorts.size(); ++ i) {
-    CheckArgument(sorts[i].isFirstClass(),
-                  sorts,
-                  "cannot create predicate types for argument types that are "
-                  "not first-class. Try option --uf-ho.");
-    sortNodes.push_back(sorts[i]);
-  }
-  sortNodes.push_back(booleanType());
-  return mkTypeNode(kind::FUNCTION_TYPE, sortNodes);
-}
-
 inline TypeNode NodeManager::mkSExprType(const std::vector<TypeNode>& types) {
   std::vector<TypeNode> typeNodes;
   for (unsigned i = 0; i < types.size(); ++ i) {