1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Mathias Preiner |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS |
8 |
|
* in the top-level source directory and their institutional affiliations. |
9 |
|
* All rights reserved. See the file COPYING in the top-level source |
10 |
|
* directory for licensing information. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Definitions of parsed operators. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "cvc5parser_public.h" |
17 |
|
|
18 |
|
#ifndef CVC5__PARSER__PARSE_OP_H |
19 |
|
#define CVC5__PARSER__PARSE_OP_H |
20 |
|
|
21 |
|
#include <string> |
22 |
|
|
23 |
|
#include "api/cpp/cvc5.h" |
24 |
|
|
25 |
|
namespace cvc5 { |
26 |
|
|
27 |
|
/** A parsed operator |
28 |
|
* |
29 |
|
* The purpose of this struct is to store information regarding a parsed term |
30 |
|
* that might not be ready to associate with an expression. |
31 |
|
* |
32 |
|
* While parsing terms in smt2, we may store a combination of one or more of |
33 |
|
* the following to track how to process this term: |
34 |
|
* (1) A kind. |
35 |
|
* (2) A string name. |
36 |
|
* (3) An expression expr. |
37 |
|
* (4) A type t. |
38 |
|
* (5) An operator object. |
39 |
|
* |
40 |
|
* Examples: |
41 |
|
* |
42 |
|
* - For declared functions f that we have not yet looked up in a symbol table, |
43 |
|
* we store (2). We may store a name in a state if f is overloaded and we have |
44 |
|
* not yet parsed its arguments to know how to disambiguate f. |
45 |
|
* - For tuple selectors (_ tupSel n), we store (1) and (3). Kind is set to |
46 |
|
* APPLY_SELECTOR, and expr is set to n, which is to be interpreted by the |
47 |
|
* caller as the n^th generic tuple selector. We do this since there is no |
48 |
|
* AST expression representing generic tuple select, and we do not have enough |
49 |
|
* type information at this point to know the type of the tuple we will be |
50 |
|
* selecting from. |
51 |
|
* - For array constant specifications prior to type ascription e.g. when we |
52 |
|
* have parsed "const", we store (1), setting the kind to STORE_ALL. |
53 |
|
* - For array constant specifications (as const (Array T1 T2)), we store (1) |
54 |
|
* and (4), where kind is set to STORE_ALL and type is set to (Array T1 T2). |
55 |
|
* When parsing this as an operator e.g. ((as const (Array T1 T2)) t), we |
56 |
|
* interpret this operator by converting the next parsed constant of type T2 to |
57 |
|
* an Array of type (Array T1 T2) over that constant. |
58 |
|
*/ |
59 |
11570922 |
struct ParseOp |
60 |
|
{ |
61 |
11520807 |
ParseOp(api::Kind k = api::NULL_EXPR) : d_kind(k) {} |
62 |
|
/** The kind associated with the parsed operator, if it exists */ |
63 |
|
api::Kind d_kind; |
64 |
|
/** The name associated with the parsed operator, if it exists */ |
65 |
|
std::string d_name; |
66 |
|
/** The expression associated with the parsed operator, if it exists */ |
67 |
|
api::Term d_expr; |
68 |
|
/** The type associated with the parsed operator, if it exists */ |
69 |
|
api::Sort d_type; |
70 |
|
/** The operator associated with the parsed operator, if it exists */ |
71 |
|
api::Op d_op; |
72 |
|
|
73 |
|
/* Return true if this is equal to 'p'. */ |
74 |
|
bool operator==(const ParseOp& p) const |
75 |
|
{ |
76 |
|
return d_kind == p.d_kind && d_name == p.d_name && d_expr == p.d_expr |
77 |
|
&& d_type == p.d_type && d_op == p.d_op; |
78 |
|
} |
79 |
|
}; |
80 |
|
|
81 |
|
std::ostream& operator<<(std::ostream& os, const ParseOp& p); |
82 |
|
|
83 |
|
} // namespace cvc5 |
84 |
|
|
85 |
|
#endif /* CVC5__PARSER__PARSE_OP_H */ |