cprover
smt2_parser.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_SOLVERS_SMT2_SMT2_PARSER_H
10 #define CPROVER_SOLVERS_SMT2_SMT2_PARSER_H
11 
12 #include <stack>
13 
14 #include <util/std_expr.h>
15 
16 #include "smt2_tokenizer.h"
17 
19 {
20 public:
21  explicit smt2_parsert(std::istream &_in)
22  : smt2_tokenizert(_in), exit(false), parenthesis_level(0)
23  {
24  }
25 
26  bool parse() override
27  {
29  return false;
30  }
31 
32  struct idt
33  {
35  {
36  }
37 
40  std::vector<irep_idt> parameters;
41  };
42 
43  using id_mapt=std::map<irep_idt, idt>;
45 
46  struct named_termt
47  {
50  };
51 
52  using named_termst = std::map<irep_idt, named_termt>;
54 
55  bool exit;
56 
58  void skip_to_end_of_list();
59 
60 protected:
61  // we override next_token to track the parenthesis level
62  std::size_t parenthesis_level;
63  tokent next_token() override;
64 
65  void command_sequence();
66 
67  virtual void command(const std::string &);
68 
69  // for let/quantifier bindings, function parameters
70  using renaming_mapt=std::map<irep_idt, irep_idt>;
72  using renaming_counterst=std::map<irep_idt, unsigned>;
75  irep_idt rename_id(const irep_idt &) const;
76 
78  {
80  std::vector<irep_idt> parameters;
81 
82  explicit signature_with_parameter_idst(const typet &_type) : type(_type)
83  {
84  }
85 
87  const typet &_type,
88  const std::vector<irep_idt> &_parameters)
89  : type(_type), parameters(_parameters)
90  {
92  (_type.id() == ID_mathematical_function &&
93  to_mathematical_function_type(_type).domain().size() ==
94  _parameters.size()) ||
95  (_type.id() != ID_mathematical_function && _parameters.empty()));
96  }
97  };
98 
99  void ignore_command();
100  exprt expression();
103  const irep_idt &,
104  const exprt::operandst &);
106  typet sort();
109  signature_with_parameter_idst function_signature_definition();
114 
118  const irep_idt &identifier,
119  const exprt::operandst &op);
120 
123 
126 };
127 
128 #endif // CPROVER_SOLVERS_SMT2_SMT2_PARSER_H
The type of an expression, extends irept.
Definition: type.h:27
void skip_to_end_of_list()
This skips tokens until all bracketed expressions are closed.
Definition: smt2_parser.cpp:31
std::size_t parenthesis_level
Definition: smt2_parser.h:62
renaming_mapt renaming_map
Definition: smt2_parser.h:71
typet function_signature_declaration()
exprt quantifier_expression(irep_idt)
irep_idt get_fresh_id(const irep_idt &)
bool parse() override
Definition: smt2_parser.h:26
std::map< irep_idt, named_termt > named_termst
Definition: smt2_parser.h:52
const mathematical_function_typet & to_mathematical_function_type(const typet &type)
Cast a typet to a mathematical_function_typet.
exprt cast_bv_to_unsigned(const exprt &)
Apply typecast to unsignedbv to given expression.
std::map< irep_idt, idt > id_mapt
Definition: smt2_parser.h:43
exprt::operandst operands()
const irep_idt & id() const
Definition: irep.h:259
signature_with_parameter_idst(const typet &_type, const std::vector< irep_idt > &_parameters)
Definition: smt2_parser.h:86
renaming_counterst renaming_counters
Definition: smt2_parser.h:73
exprt binary_predicate(irep_idt, const exprt::operandst &)
exprt function_application_ieee_float_op(const irep_idt &, const exprt::operandst &)
void ignore_command()
Definition: smt2_parser.cpp:78
tokent next_token() override
Definition: smt2_parser.cpp:19
API to expression classes.
std::map< irep_idt, irep_idt > renaming_mapt
Definition: smt2_parser.h:70
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
irep_idt rename_id(const irep_idt &) const
exprt let_expression()
enum { NONE, END_OF_FILE, STRING_LITERAL, NUMERAL, SYMBOL, KEYWORD, OPEN, CLOSE } tokent
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
exprt expression()
id_mapt id_map
Definition: smt2_parser.h:44
std::vector< exprt > operandst
Definition: expr.h:57
exprt multi_ary(irep_idt, const exprt::operandst &)
exprt unary(irep_idt, const exprt::operandst &)
std::map< irep_idt, unsigned > renaming_counterst
Definition: smt2_parser.h:72
virtual void command(const std::string &)
exprt binary(irep_idt, const exprt::operandst &)
Base class for all expressions.
Definition: expr.h:54
named_termst named_terms
Definition: smt2_parser.h:53
signature_with_parameter_idst(const typet &_type)
Definition: smt2_parser.h:82
signature_with_parameter_idst function_signature_definition()
The NIL type, i.e., an invalid type, no value.
Definition: std_types.h:39
exprt::operandst cast_bv_to_signed(const exprt::operandst &)
Apply typecast to signedbv to expressions in vector.
std::vector< irep_idt > parameters
Definition: smt2_parser.h:40
exprt function_application()
Expression to hold a symbol (variable)
Definition: std_expr.h:143
smt2_parsert(std::istream &_in)
Definition: smt2_parser.h:21
void command_sequence()
Definition: smt2_parser.cpp:38
exprt function_application_fp(const exprt::operandst &)