diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-27 15:20:12 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-27 15:20:12 -0600 |
commit | a93b9c5a18bce93e2d66d1e98f13f69f0c193359 (patch) | |
tree | f0ed05495eaf7bfefdc12aabad559f4666fa09e4 /src/parser | |
parent | 0ad0496cd474a167973195d1ddc9322ada7f2b4e (diff) |
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.
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/smt2/smt2.cpp | 82 | ||||
-rw-r--r-- | 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<Expr> args; - std::vector<Type> cargs; - Expr op = purifySygusGTerm(term, ntsToUnres, args, cargs); + std::vector<api::Term> args; + std::vector<api::Sort> 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<SygusPrintCallback> spc; // callback prints as the expression - spc = std::make_shared<printer::SygusExprPrintCallback>(op, args); + spc = std::make_shared<printer::SygusExprPrintCallback>( + 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<Expr, Type>& ntsToUnres, - std::vector<Expr>& args, - std::vector<Type>& cargs) const +api::Term Smt2::purifySygusGTerm(api::Term term, + std::map<Expr, Type>& ntsToUnres, + std::vector<api::Term>& args, + std::vector<api::Sort>& cargs) const { Trace("parser-sygus2-debug") - << "purifySygusGTerm: " << term << " #nchild=" << term.getNumChildren() - << std::endl; - std::map<Expr, Type>::iterator itn = ntsToUnres.find(term); + << "purifySygusGTerm: " << term + << " #nchild=" << term.getExpr().getNumChildren() << std::endl; + std::map<Expr, Type>::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<Expr> 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<api::Term> 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<Expr, Type>& ntsToUnres, - std::vector<Expr>& args, - std::vector<Type>& cargs) const; + api::Term purifySygusGTerm(api::Term term, + std::map<Expr, Type>& ntsToUnres, + std::vector<api::Term>& args, + std::vector<api::Sort>& cargs) const; void addArithmeticOperators(); |