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.

diff --git a/src/api/checks.h b/src/api/checks.h
index c2869f463538b85b22c7be70ee78e9b85e7f1c32..d5408d3129252cc150054df7dcc7b3f9f67b993c 100644 (file)
--- 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 2d5ed36fb4766a51115f129e009998a406572ea5..fdd7e5f5a784403ce9f11d5a7b2db9825ba3cefd 100644 (file)
--- 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 8b0d6d7f70991da1d31d7f80c1bc62066e6d5606..8cf4fbccd3c73b206ff74457f96ae37a23fb4fe8 100644 (file)
--- 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 ac25ede143ba085b863145f89aa7d33a8256a83d..aaa9d60f0788ba0a966a9474f006dae26372f33e 100644 (file)
--- 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 e1184a829b0870deb0914ed11936609e44d6cd25..8d2edaffea7e2072bda6e4358acf696fdcd183f0 100644 (file)
--- 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 e5589f81e7a991f42e646c30618fe8fcab564063..18a8f9cc88380014c9d3d30bd35d54a5902621b4 100644 (file)
--- 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 e52bd61031a1d0f908ab8f1b480e1180c80477f5..625af9342e22c060b5da4befbec9a2040d0b70c9 100644 (file)
--- 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());
 }