From a93b9c5a18bce93e2d66d1e98f13f69f0c193359 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 27 Feb 2020 15:20:12 -0600 Subject: [PATCH] Update purifySygusGTerm to the new API (#3830) Towards parser migration. (Partially) updates the central function used for synth-fun in sygus v2 to the new API. It also removes an optimization for "pure operators" from the v2 parser that is incompatible with the new API. --- src/parser/smt2/smt2.cpp | 82 +++++++++++++--------------------------- src/parser/smt2/smt2.h | 8 ++-- 2 files changed, 31 insertions(+), 59 deletions(-) diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index ff155d0f9..48c1c96c7 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1460,83 +1460,55 @@ void Smt2::addSygusConstructorTerm(Datatype& dt, // should be treated as distinct terms. // Notice that let expressions are forbidden in the input syntax of term, so // this does not lead to exponential behavior with respect to input size. - std::vector args; - std::vector cargs; - Expr op = purifySygusGTerm(term, ntsToUnres, args, cargs); + std::vector args; + std::vector cargs; + api::Term op = purifySygusGTerm(api::Term(term), ntsToUnres, args, cargs); + std::stringstream ssCName; + ssCName << op.getKind(); Trace("parser-sygus2") << "Purified operator " << op << ", #args/cargs=" << args.size() << "/" << cargs.size() << std::endl; std::shared_ptr spc; // callback prints as the expression - spc = std::make_shared(op, args); + spc = std::make_shared( + op.getExpr(), api::termVectorToExprs(args)); if (!args.empty()) { - bool pureVar = false; - if (op.getNumChildren() == args.size()) - { - pureVar = true; - for (unsigned i = 0, nchild = op.getNumChildren(); i < nchild; i++) - { - if (op[i] != args[i]) - { - pureVar = false; - break; - } - } - } - Trace("parser-sygus2") << "Pure var is " << pureVar - << ", hasOp=" << op.hasOperator() << std::endl; - if (pureVar && op.hasOperator()) - { - // optimization: use just the operator if it an application to only vars - op = op.getOperator(); - } - else - { - Expr lbvl = getExprManager()->mkExpr(kind::BOUND_VAR_LIST, args); - // its operator is a lambda - op = getExprManager()->mkExpr(kind::LAMBDA, lbvl, op); - } - } - Trace("parser-sygus2") << "Generated operator " << op << std::endl; - std::stringstream ss; - ss << op.getKind(); - dt.addSygusConstructor(op, ss.str(), cargs, spc); + api::Term lbvl = d_solver->mkTerm(api::BOUND_VAR_LIST, args); + // its operator is a lambda + op = d_solver->mkTerm(api::LAMBDA, lbvl, op); + } + Trace("parser-sygus2") << "addSygusConstructor: operator " << op + << std::endl; + dt.addSygusConstructor( + op.getExpr(), ssCName.str(), api::sortVectorToTypes(cargs), spc); } -Expr Smt2::purifySygusGTerm(Expr term, - std::map& ntsToUnres, - std::vector& args, - std::vector& cargs) const +api::Term Smt2::purifySygusGTerm(api::Term term, + std::map& ntsToUnres, + std::vector& args, + std::vector& cargs) const { Trace("parser-sygus2-debug") - << "purifySygusGTerm: " << term << " #nchild=" << term.getNumChildren() - << std::endl; - std::map::iterator itn = ntsToUnres.find(term); + << "purifySygusGTerm: " << term + << " #nchild=" << term.getExpr().getNumChildren() << std::endl; + std::map::iterator itn = ntsToUnres.find(term.getExpr()); if (itn != ntsToUnres.end()) { - Expr ret = getExprManager()->mkBoundVar(term.getType()); + api::Term ret = d_solver->mkVar(term.getSort()); Trace("parser-sygus2-debug") << "...unresolved non-terminal, intro " << ret << std::endl; - args.push_back(ret); + args.push_back(ret.getExpr()); cargs.push_back(itn->second); return ret; } - std::vector pchildren; - // To test whether the operator should be passed to mkExpr below, we check - // whether this term is parameterized. This includes APPLY_UF terms and BV - // extraction terms, but excludes applications of most interpreted symbols - // like PLUS. - if (term.isParameterized()) - { - pchildren.push_back(term.getOperator()); - } + std::vector pchildren; bool childChanged = false; for (unsigned i = 0, nchild = term.getNumChildren(); i < nchild; i++) { Trace("parser-sygus2-debug") << "......purify child " << i << " : " << term[i] << std::endl; - Expr ptermc = purifySygusGTerm(term[i], ntsToUnres, args, cargs); + api::Term ptermc = purifySygusGTerm(term[i], ntsToUnres, args, cargs); pchildren.push_back(ptermc); childChanged = childChanged || ptermc != term[i]; } @@ -1545,7 +1517,7 @@ Expr Smt2::purifySygusGTerm(Expr term, Trace("parser-sygus2-debug") << "...no child changed" << std::endl; return term; } - Expr nret = getExprManager()->mkExpr(term.getKind(), pchildren); + api::Term nret = d_solver->mkTerm(term.getOp(), pchildren); Trace("parser-sygus2-debug") << "...child changed, return " << nret << std::endl; return nret; diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 35ac781f5..53ebf5929 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -602,10 +602,10 @@ class Smt2 : public Parser * by a lambda), and cargs contains the types of the arguments of the * sygus constructor. */ - Expr purifySygusGTerm(Expr term, - std::map& ntsToUnres, - std::vector& args, - std::vector& cargs) const; + api::Term purifySygusGTerm(api::Term term, + std::map& ntsToUnres, + std::vector& args, + std::vector& cargs) const; void addArithmeticOperators(); -- 2.30.2