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.

1 files changed, 59 insertions, 16 deletions

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 */