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/parse_op.h | |
parent | d84d67018234bb6bb24dd9183a888892c3bfd4d7 (diff) |
Update sygus v1 parser to use ParseOp utility (#3756)
Diffstat (limited to 'src/parser/parse_op.h')
-rw-r--r-- | src/parser/parse_op.h | 93 |
1 files changed, 93 insertions, 0 deletions
diff --git a/src/parser/parse_op.h b/src/parser/parse_op.h new file mode 100644 index 000000000..2465bf324 --- /dev/null +++ b/src/parser/parse_op.h @@ -0,0 +1,93 @@ +/********************* */ +/*! \file parse_op.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Definitions of parsed operators. + **/ + +#include "cvc4parser_public.h" + +#ifndef CVC4__PARSER__PARSE_OP_H +#define CVC4__PARSER__PARSE_OP_H + +#include <string> + +#include "expr/expr.h" +#include "expr/kind.h" + +namespace CVC4 { + +/** A parsed operator + * + * The purpose of this struct is to store information regarding a parsed term + * that might not be ready to associate with an expression. + * + * While parsing terms in smt2, we may store a combination of one or more of + * the following to track how to process this term: + * (1) A kind. + * (2) A string name. + * (3) An expression expr. + * (4) A type t. + * + * Examples: + * + * - For declared functions f that we have not yet looked up in a symbol table, + * we store (2). We may store a name in a state if f is overloaded and we have + * not yet parsed its arguments to know how to disambiguate f. + * - For tuple selectors (_ tupSel n), we store (1) and (3). Kind is set to + * APPLY_SELECTOR, and expr is set to n, which is to be interpreted by the + * caller as the n^th generic tuple selector. We do this since there is no + * AST expression representing generic tuple select, and we do not have enough + * type information at this point to know the type of the tuple we will be + * selecting from. + * - For array constant specifications prior to type ascription e.g. when we + * have parsed "const", we store (1), setting the kind to STORE_ALL. + * - For array constant specifications (as const (Array T1 T2)), we store (1) + * and (4), where kind is set to STORE_ALL and type is set to (Array T1 T2). + * When parsing this as an operator e.g. ((as const (Array T1 T2)) t), we + * interpret this operator by converting the next parsed constant of type T2 to + * an Array of type (Array T1 T2) over that constant. + */ +struct CVC4_PUBLIC ParseOp +{ + ParseOp() : d_kind(kind::NULL_EXPR) {} + /** The kind associated with the parsed operator, if it exists */ + Kind d_kind; + /** The name associated with the parsed operator, if it exists */ + std::string d_name; + /** The expression associated with the parsed operator, if it exists */ + Expr d_expr; + /** The type associated with the parsed operator, if it exists */ + Type d_type; + + /* Return true if this is equal to 'p'. */ + bool operator==(const ParseOp& p) const + { + return d_kind == p.d_kind && d_name == p.d_name && d_expr == p.d_expr + && d_type == p.d_type; + } +}; + +inline std::ostream& operator<<(std::ostream& os, const ParseOp& p) +{ + if (!p.d_expr.isNull()) + { + return os << p.d_expr; + } + else if (p.d_kind != kind::NULL_EXPR) + { + return os << p.d_kind; + } + return os << "ParseOp::unknown"; +} + +} // namespace CVC4 + +#endif /* CVC4__PARSER__PARSE_OP_H */ |