From 19a93d5e0f924c70e7f77719e0310c730c8fbc61 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 29 Apr 2019 20:27:20 -0500
Subject: Eliminate APPLY kind (#2976)

---
 src/parser/parser.cpp    | 17 ++++++-----------
 src/parser/smt2/Smt2.g   |  2 +-
 src/parser/smt2/smt2.cpp |  9 +++++----
 3 files changed, 12 insertions(+), 16 deletions(-)

(limited to 'src/parser')

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()) {
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 75df38637..9ba7f4b2e 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -2091,7 +2091,7 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
              // however, we need to apply partial version since we don't have the internal selector available
              aargs.push_back( MK_EXPR( CVC4::kind::APPLY_SELECTOR, dtc[i].getSelector(), expr ) );
            }
-           patexprs.push_back( MK_EXPR( CVC4::kind::APPLY, aargs ) );
+           patexprs.push_back( MK_EXPR( CVC4::kind::APPLY_UF, aargs ) );
            patconds.push_back( MK_EXPR( CVC4::kind::APPLY_TESTER, dtc.getTester(), expr ) );
          }
          RPAREN_TOK 
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 47da10f42..71ba81124 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -859,7 +859,9 @@ Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, st
           children.push_back( it->second );
         }
       }
-      Kind sk = sop.getKind() != kind::BUILTIN ? kind::APPLY : getExprManager()->operatorToKind(sop);
+      Kind sk = sop.getKind() != kind::BUILTIN
+                    ? kind::APPLY_UF
+                    : getExprManager()->operatorToKind(sop);
       Debug("parser-sygus") << ": operator " << sop << " with " << sop.getKind() << " " << sk << std::endl;
       Expr e = getExprManager()->mkExpr( sk, children );
       Debug("parser-sygus") << ": constructed " << e << ", which has type " << e.getType() << std::endl;
@@ -1072,7 +1074,7 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
         }
         children.insert(children.end(), largs.begin(), largs.end());
         Kind sk = ops[i].getKind() != kind::BUILTIN
-                      ? kind::APPLY
+                      ? kind::APPLY_UF
                       : getExprManager()->operatorToKind(ops[i]);
         Expr body = getExprManager()->mkExpr(sk, children);
         // replace by lambda
@@ -1131,14 +1133,13 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
             std::vector<Expr> largs;
             Expr lbvl = makeSygusBoundVarList(dt, i, ftypes, largs);
             largs.insert(largs.begin(), ops[i]);
-            Expr body = getExprManager()->mkExpr(kind::APPLY, largs);
+            Expr body = getExprManager()->mkExpr(kind::APPLY_UF, largs);
             ops[i] = getExprManager()->mkExpr(kind::LAMBDA, lbvl, body);
             Debug("parser-sygus") << "  ...replace op : " << ops[i]
                                   << std::endl;
           }
           else
           {
-            ops[i] = getExprManager()->mkExpr(kind::APPLY, ops[i]);
             Debug("parser-sygus") << "  ...replace op : " << ops[i]
                                   << std::endl;
           }
-- 
cgit v1.2.3