diff options
Diffstat (limited to 'src/parser/parser.cpp')
| -rw-r--r-- | src/parser/parser.cpp | 17 |
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()) { |