GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/parser/parse_op.h Lines: 2 2 100.0 %
Date: 2021-03-22 Branches: 3 6 50.0 %

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