diff options
Diffstat (limited to 'src/parser/smt2/smt2.cpp')
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index d52dd948b..71ba81124 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Kshitij Bansal, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -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; } |