Eliminate APPLY kind (#2976)

3 files changed, 10 insertions, 45 deletions

diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index 3313a684f..15891dfad 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -289,9 +289,6 @@ constant BUILTIN \
     "expr/kind.h" \
     "the kind of expressions representing built-in operators"
 
-variable FUNCTION "a defined function"
-parameterized APPLY FUNCTION 0: "application of a defined function"
-
 operator EQUAL 2 "equality (two parameters only, sorts must match)"
 operator DISTINCT 2: "disequality (N-ary, sorts must match)"
 variable VARIABLE "a variable (not permitted in bindings)"
@@ -332,7 +329,6 @@ well-founded SEXPR_TYPE \
     "::CVC4::theory::builtin::SExprProperties::mkGroundTerm(%TYPE%)" \
     "theory/builtin/theory_builtin_type_rules.h"
 
-typerule APPLY ::CVC4::theory::builtin::ApplyTypeRule
 typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule
 typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule
 typerule SEXPR ::CVC4::theory::builtin::SExprTypeRule
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 2c726d12f..db427d21e 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -31,44 +31,6 @@ namespace CVC4 {
 namespace theory {
 namespace builtin {
 
-class ApplyTypeRule {
- public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    TNode f = n.getOperator();
-    TypeNode fType = f.getType(check);
-    if( !fType.isFunction() && n.getNumChildren() > 0 ) {
-      throw TypeCheckingExceptionPrivate(n, "operator does not have function type");
-    }
-    if( check ) {
-      if(fType.isFunction()) {
-        if(n.getNumChildren() != fType.getNumChildren() - 1) {
-          throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the function type");
-        }
-        TNode::iterator argument_it = n.begin();
-        TNode::iterator argument_it_end = n.end();
-        TypeNode::iterator argument_type_it = fType.begin();
-        for(; argument_it != argument_it_end; ++argument_it, ++argument_type_it) {
-          if(!(*argument_it).getType().isComparableTo(*argument_type_it)) {
-            std::stringstream ss;
-            ss << "argument types do not match the function type:\n"
-               << "argument:  " << *argument_it << "\n"
-               << "has type:  " << (*argument_it).getType() << "\n"
-               << "not equal: " << *argument_type_it;
-            throw TypeCheckingExceptionPrivate(n, ss.str());
-          }
-        }
-      } else {
-        if( n.getNumChildren() > 0 ) {
-          throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the function type");
-        }
-      }
-    }
-    return fType.isFunction() ? fType.getRangeType() : fType;
-  }
-};/* class ApplyTypeRule */
-
-
 class EqualityTypeRule {
  public:
   inline static TypeNode computeType(NodeManager* nodeManager,
diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp
index 5d3a92cdc..be87b7e8d 100644
--- a/src/theory/datatypes/datatypes_rewriter.cpp
+++ b/src/theory/datatypes/datatypes_rewriter.cpp
@@ -191,8 +191,6 @@ Kind DatatypesRewriter::getOperatorKindForSygusBuiltin(Node op)
   Assert(op.getKind() != BUILTIN);
   if (op.getKind() == LAMBDA)
   {
-    // we use APPLY_UF instead of APPLY, since the rewriter for APPLY_UF
-    // does beta-reduction but does not for APPLY
     return APPLY_UF;
   }
   TypeNode tn = op.getType();
@@ -247,7 +245,16 @@ Node DatatypesRewriter::mkSygusTerm(const Datatype& dt,
   Kind ok = NodeManager::operatorToKind(op);
   if (ok != UNDEFINED_KIND)
   {
-    ret = NodeManager::currentNM()->mkNode(ok, schildren);
+    if (ok == APPLY_UF && schildren.size() == 1)
+    {
+      // This case is triggered for defined constant symbols. In this case,
+      // we return the operator itself instead of an APPLY_UF node.
+      ret = schildren[0];
+    }
+    else
+    {
+      ret = NodeManager::currentNM()->mkNode(ok, schildren);
+    }
     Trace("dt-sygus-util") << "...return (op) " << ret << std::endl;
     return ret;
   }