Function types are always first-class (#6167)

This eliminates one of the dependencies of TypeNode on options. In particular, this makes it so that function types are always considered first-class.

This change makes it so that higher-order types can always be constructed; logic exceptions should occur if they are used in constraints.

7 files changed, 102 insertions, 50 deletions

diff --git a/src/api/checks.h b/src/api/checks.h
index c2869f463..d5408d312 100644
--- a/src/api/checks.h
+++ b/src/api/checks.h
@@ -429,16 +429,18 @@ namespace api {
 /**
  * Codomain sort check for member functions of class Solver.
  * Check if codomain sort is not null, associated with this solver, and a
- * first-class sort.
+ * first-class, non-function sort.
  */
-#define CVC4_API_SOLVER_CHECK_CODOMAIN_SORT(sort)                         \
-  do                                                                      \
-  {                                                                       \
-    CVC4_API_ARG_CHECK_NOT_NULL(sort);                                    \
-    CVC4_API_CHECK(this == sort.d_solver)                                 \
-        << "Given sort is not associated with this solver";               \
-    CVC4_API_ARG_CHECK_EXPECTED(sort.isFirstClass(), sort)                \
-        << "first-class sort as codomain sort";                           \
+#define CVC4_API_SOLVER_CHECK_CODOMAIN_SORT(sort)           \
+  do                                                        \
+  {                                                         \
+    CVC4_API_ARG_CHECK_NOT_NULL(sort);                      \
+    CVC4_API_CHECK(this == sort.d_solver)                   \
+        << "Given sort is not associated with this solver"; \
+    CVC4_API_ARG_CHECK_EXPECTED(sort.isFirstClass(), sort)  \
+        << "first-class sort as codomain sort";             \
+    CVC4_API_ARG_CHECK_EXPECTED(!sort.isFunction(), sort)   \
+        << "function sort as codomain sort";                \
   } while (0)
 
 /* Term checks. ------------------------------------------------------------- */
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 2d5ed36fb..fdd7e5f5a 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -31,8 +31,6 @@
 #include "expr/node_manager_attributes.h"
 #include "expr/skolem_manager.h"
 #include "expr/type_checker.h"
-#include "options/options.h"
-#include "options/smt_options.h"
 #include "util/resource_manager.h"
 #include "util/statistics_registry.h"
 
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 8b0d6d7f7..8cf4fbccd 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -20,9 +20,7 @@
 #include "expr/node_manager_attributes.h"
 #include "expr/type_properties.h"
 #include "options/base_options.h"
-#include "options/expr_options.h"
 #include "options/quantifiers_options.h"
-#include "options/uf_options.h"
 #include "theory/type_enumerator.h"
 
 using namespace std;
@@ -286,13 +284,10 @@ bool TypeNode::isClosedEnumerable()
 }
 
 bool TypeNode::isFirstClass() const {
-  return ( getKind() != kind::FUNCTION_TYPE || options::ufHo() ) && 
-         getKind() != kind::CONSTRUCTOR_TYPE &&
-         getKind() != kind::SELECTOR_TYPE &&
-         getKind() != kind::TESTER_TYPE &&
-         getKind() != kind::SEXPR_TYPE &&
-         ( getKind() != kind::TYPE_CONSTANT ||
-           getConst<TypeConstant>() != REGEXP_TYPE );
+  return getKind() != kind::CONSTRUCTOR_TYPE && getKind() != kind::SELECTOR_TYPE
+         && getKind() != kind::TESTER_TYPE && getKind() != kind::SEXPR_TYPE
+         && (getKind() != kind::TYPE_CONSTANT
+             || getConst<TypeConstant>() != REGEXP_TYPE);
 }
 
 bool TypeNode::isWellFounded() const {
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index ac25ede14..aaa9d60f0 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -210,7 +210,9 @@ TrustNode TheoryUF::ppRewrite(TNode node, std::vector<SkolemLemma>& lems)
 {
   Trace("uf-exp-def") << "TheoryUF::ppRewrite: expanding definition : " << node
                       << std::endl;
-  if( node.getKind()==kind::HO_APPLY ){
+  Kind k = node.getKind();
+  if (k == kind::HO_APPLY)
+  {
     if( !options::ufHo() ){
       std::stringstream ss;
       ss << "Partial function applications are not supported in default mode, try --uf-ho.";
@@ -224,6 +226,18 @@ TrustNode TheoryUF::ppRewrite(TNode node, std::vector<SkolemLemma>& lems)
       return TrustNode::mkTrustRewrite(node, ret, nullptr);
     }
   }
+  else if (k == kind::APPLY_UF)
+  {
+    // check for higher-order
+    // logic exception if higher-order is not enabled
+    if (isHigherOrderType(node.getOperator().getType()) && !options::ufHo())
+    {
+      std::stringstream ss;
+      ss << "UF received an application whose operator has higher-order type "
+         << node << ", which is not supported by default, try --uf-ho";
+      throw LogicException(ss.str());
+    }
+  }
   return TrustNode::null();
 }
 
@@ -239,23 +253,30 @@ void TheoryUF::preRegisterTerm(TNode node)
   //Assert( node.getKind()!=kind::APPLY_UF || !options::ufHo() );
   Assert(node.getKind() != kind::HO_APPLY || options::ufHo());
 
-  switch (node.getKind()) {
-  case kind::EQUAL:
-    // Add the trigger for equality
-    d_equalityEngine->addTriggerPredicate(node);
-    break;
-  case kind::APPLY_UF:
-  case kind::HO_APPLY:
-    // Maybe it's a predicate
-    if (node.getType().isBoolean()) {
-      // Get triggered for both equal and dis-equal
+  Kind k = node.getKind();
+  switch (k)
+  {
+    case kind::EQUAL:
+      // Add the trigger for equality
       d_equalityEngine->addTriggerPredicate(node);
-    } else {
-      // Function applications/predicates
-      d_equalityEngine->addTerm(node);
+      break;
+    case kind::APPLY_UF:
+    case kind::HO_APPLY:
+    {
+      // Maybe it's a predicate
+      if (node.getType().isBoolean())
+      {
+        // Get triggered for both equal and dis-equal
+        d_equalityEngine->addTriggerPredicate(node);
+      }
+      else
+      {
+        // Function applications/predicates
+        d_equalityEngine->addTerm(node);
+      }
+      // Remember the function and predicate terms
+      d_functionsTerms.push_back(node);
     }
-    // Remember the function and predicate terms
-    d_functionsTerms.push_back(node);
     break;
   case kind::CARDINALITY_CONSTRAINT:
   case kind::COMBINED_CARDINALITY_CONSTRAINT:
@@ -648,6 +669,28 @@ void TheoryUF::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
   }
 }
 
+bool TheoryUF::isHigherOrderType(TypeNode tn)
+{
+  Assert(tn.isFunction());
+  std::map<TypeNode, bool>::iterator it = d_isHoType.find(tn);
+  if (it != d_isHoType.end())
+  {
+    return it->second;
+  }
+  bool ret = false;
+  const std::vector<TypeNode>& argTypes = tn.getArgTypes();
+  for (const TypeNode& tnc : argTypes)
+  {
+    if (tnc.isFunction())
+    {
+      ret = true;
+      break;
+    }
+  }
+  d_isHoType[tn] = ret;
+  return ret;
+}
+
 } /* namespace CVC4::theory::uf */
 } /* namespace CVC4::theory */
 } /* namespace CVC4 */
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index e1184a829..8d2edaffe 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -162,7 +162,12 @@ private:
                     const TNodeTrie* t2,
                     unsigned arity,
                     unsigned depth);
-
+  /**
+   * Is t a higher order type? A higher-order type is a function type having
+   * an argument type that is also a function type. This is used for checking
+   * logic exceptions.
+   */
+  bool isHigherOrderType(TypeNode tn);
   TheoryUfRewriter d_rewriter;
   /** Proof rule checker */
   UfProofRuleChecker d_ufProofChecker;
@@ -172,6 +177,8 @@ private:
   TheoryInferenceManager d_im;
   /** The notify class */
   NotifyClass d_notify;
+  /** Cache for isHigherOrderType */
+  std::map<TypeNode, bool> d_isHoType;
 };/* class TheoryUF */
 
 }/* CVC4::theory::uf namespace */
diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp
index e5589f81e..18a8f9cc8 100644
--- a/test/unit/api/solver_black.cpp
+++ b/test/unit/api/solver_black.cpp
@@ -200,7 +200,11 @@ TEST_F(TestApiBlackSolver, mkFunctionSort)
                                           d_solver.getIntegerSort()));
   Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
                                          d_solver.getIntegerSort());
-  ASSERT_THROW(d_solver.mkFunctionSort(funSort, d_solver.getIntegerSort()),
+  // function arguments are allowed
+  ASSERT_NO_THROW(d_solver.mkFunctionSort(funSort, d_solver.getIntegerSort()));
+  // non-first-class arguments are not allowed
+  Sort reSort = d_solver.getRegExpSort();
+  ASSERT_THROW(d_solver.mkFunctionSort(reSort, d_solver.getIntegerSort()),
                CVC4ApiException);
   ASSERT_THROW(d_solver.mkFunctionSort(d_solver.getIntegerSort(), funSort),
                CVC4ApiException);
@@ -209,10 +213,10 @@ TEST_F(TestApiBlackSolver, mkFunctionSort)
       d_solver.getIntegerSort()));
   Sort funSort2 = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
                                           d_solver.getIntegerSort());
-  ASSERT_THROW(
+  // function arguments are allowed
+  ASSERT_NO_THROW(
       d_solver.mkFunctionSort({funSort2, d_solver.mkUninterpretedSort("u")},
-                              d_solver.getIntegerSort()),
-      CVC4ApiException);
+                              d_solver.getIntegerSort()));
   ASSERT_THROW(d_solver.mkFunctionSort({d_solver.getIntegerSort(),
                                         d_solver.mkUninterpretedSort("u")},
                                        funSort2),
@@ -248,8 +252,9 @@ TEST_F(TestApiBlackSolver, mkPredicateSort)
   ASSERT_THROW(d_solver.mkPredicateSort({}), CVC4ApiException);
   Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
                                          d_solver.getIntegerSort());
-  ASSERT_THROW(d_solver.mkPredicateSort({d_solver.getIntegerSort(), funSort}),
-               CVC4ApiException);
+  // functions as arguments are allowed
+  ASSERT_NO_THROW(
+      d_solver.mkPredicateSort({d_solver.getIntegerSort(), funSort}));
 
   Solver slv;
   ASSERT_THROW(slv.mkPredicateSort({d_solver.getIntegerSort()}),
@@ -954,8 +959,8 @@ TEST_F(TestApiBlackSolver, declareFun)
   ASSERT_NO_THROW(
       d_solver.declareFun("f3", {bvSort, d_solver.getIntegerSort()}, bvSort));
   ASSERT_THROW(d_solver.declareFun("f2", {}, funSort), CVC4ApiException);
-  ASSERT_THROW(d_solver.declareFun("f4", {bvSort, funSort}, bvSort),
-               CVC4ApiException);
+  // functions as arguments is allowed
+  ASSERT_NO_THROW(d_solver.declareFun("f4", {bvSort, funSort}, bvSort));
   ASSERT_THROW(d_solver.declareFun("f5", {bvSort, bvSort}, funSort),
                CVC4ApiException);
   Solver slv;
@@ -1007,8 +1012,8 @@ TEST_F(TestApiBlackSolver, defineFun)
   ASSERT_THROW(d_solver.defineFun("fff", {b1}, bvSort, v3), CVC4ApiException);
   ASSERT_THROW(d_solver.defineFun("ffff", {b1}, funSort2, v3),
                CVC4ApiException);
-  ASSERT_THROW(d_solver.defineFun("fffff", {b1, b3}, bvSort, v1),
-               CVC4ApiException);
+  // b3 has function sort, which is allowed as an argument
+  ASSERT_NO_THROW(d_solver.defineFun("fffff", {b1, b3}, bvSort, v1));
   ASSERT_THROW(d_solver.defineFun(f1, {v1, b11}, v1), CVC4ApiException);
   ASSERT_THROW(d_solver.defineFun(f1, {b1}, v1), CVC4ApiException);
   ASSERT_THROW(d_solver.defineFun(f1, {b1, b11}, v2), CVC4ApiException);
@@ -1078,8 +1083,8 @@ TEST_F(TestApiBlackSolver, defineFunRec)
                CVC4ApiException);
   ASSERT_THROW(d_solver.defineFunRec("ffff", {b1}, funSort2, v3),
                CVC4ApiException);
-  ASSERT_THROW(d_solver.defineFunRec("fffff", {b1, b3}, bvSort, v1),
-               CVC4ApiException);
+  // b3 has function sort, which is allowed as an argument
+  ASSERT_NO_THROW(d_solver.defineFunRec("fffff", {b1, b3}, bvSort, v1));
   ASSERT_THROW(d_solver.defineFunRec(f1, {b1}, v1), CVC4ApiException);
   ASSERT_THROW(d_solver.defineFunRec(f1, {b1, b11}, v2), CVC4ApiException);
   ASSERT_THROW(d_solver.defineFunRec(f1, {b1, b11}, v3), CVC4ApiException);
diff --git a/test/unit/api/sort_black.cpp b/test/unit/api/sort_black.cpp
index e52bd6103..625af9342 100644
--- a/test/unit/api/sort_black.cpp
+++ b/test/unit/api/sort_black.cpp
@@ -230,7 +230,9 @@ TEST_F(TestApiBlackSort, isFirstClass)
   Sort fun_sort = d_solver.mkFunctionSort(d_solver.getRealSort(),
                                           d_solver.getIntegerSort());
   ASSERT_TRUE(d_solver.getIntegerSort().isFirstClass());
-  ASSERT_FALSE(fun_sort.isFirstClass());
+  ASSERT_TRUE(fun_sort.isFirstClass());
+  Sort reSort = d_solver.getRegExpSort();
+  ASSERT_FALSE(reSort.isFirstClass());
   ASSERT_NO_THROW(Sort().isFirstClass());
 }