Eliminate APPLY kind (#2976)

1 files changed, 6 insertions, 11 deletions

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index bc88166d3..28489154a 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -128,23 +128,18 @@ Expr Parser::getExpressionForNameAndType(const std::string& name, Type t) {
   }
   // now, post-process the expression
   assert( !expr.isNull() );
-  if(isDefinedFunction(expr)) {
-    // defined functions/constants are wrapped in an APPLY so that they are
-    // expanded into their definition, e.g. during SmtEnginePrivate::expandDefinitions
-    expr = getExprManager()->mkExpr(CVC4::kind::APPLY, expr);
-  }else{
-    Type te = expr.getType();
-    if(te.isConstructor() && ConstructorType(te).getArity() == 0) {
-      // nullary constructors have APPLY_CONSTRUCTOR kind with no children
-      expr = getExprManager()->mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, expr);
-    }
+  Type te = expr.getType();
+  if (te.isConstructor() && ConstructorType(te).getArity() == 0)
+  {
+    // nullary constructors have APPLY_CONSTRUCTOR kind with no children
+    expr = getExprManager()->mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, expr);
   }
   return expr;
 }
 
 Kind Parser::getKindForFunction(Expr fun) {
   if(isDefinedFunction(fun)) {
-    return APPLY;
+    return APPLY_UF;
   }
   Type t = fun.getType();
   if(t.isConstructor()) {