diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-13 23:31:13 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-13 23:31:13 -0600 |
commit | 08289dd911aff28110baf0fd815fd912f8b76fd3 (patch) | |
tree | 74cb9775532373b6f24e54bfaf471dc1ef0bae24 /src/parser/parser.h | |
parent | d84d67018234bb6bb24dd9183a888892c3bfd4d7 (diff) |
Update sygus v1 parser to use ParseOp utility (#3756)
Diffstat (limited to 'src/parser/parser.h')
-rw-r--r-- | src/parser/parser.h | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/src/parser/parser.h b/src/parser/parser.h index 642b81fb0..b0ef2328f 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -29,6 +29,7 @@ #include "expr/kind.h" #include "expr/symbol_table.h" #include "parser/input.h" +#include "parser/parse_op.h" #include "parser/parser_exception.h" #include "util/unsafe_interrupt_exception.h" @@ -58,7 +59,8 @@ public: gterm_ignore, }; Type d_type; - Expr d_expr; + /** The parsed operator */ + ParseOp d_op; std::vector< Expr > d_let_vars; unsigned d_gterm_type; std::string d_name; @@ -367,11 +369,12 @@ public: virtual Expr getExpressionForNameAndType(const std::string& name, Type t); /** - * Returns the kind that should be used for applications of expression fun, where - * fun has "function-like" type, i.e. where checkFunctionLike(fun) returns true. - * Returns a parse error if fun does not have function-like type. + * Returns the kind that should be used for applications of expression fun. + * This is a generalization of ExprManager::operatorToKind that also + * handles variables whose types are "function-like", i.e. where + * checkFunctionLike(fun) returns true. * - * For example, this function returns + * For examples of the latter, this function returns * APPLY_UF if fun has function type, * APPLY_CONSTRUCTOR if fun has constructor type. */ |