diff options
Diffstat (limited to 'src/parser/smt2/smt2.cpp')
-rw-r--r-- | src/parser/smt2/smt2.cpp | 9 |
1 files changed, 5 insertions, 4 deletions
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; } |