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/smt2/smt2.h | |
| 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/smt2/smt2.h')
| -rw-r--r-- | src/parser/smt2/smt2.h | 8 |
1 files changed, 4 insertions, 4 deletions
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(); |