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 <map>
13 #include <unordered_map>
14 
16 #include <util/std_expr.h>
17 
18 #include "smt2_tokenizer.h"
19 
21 {
22 public:
23  explicit smt2_parsert(std::istream &_in)
24  : exit(false), smt2_tokenizer(_in), parenthesis_level(0)
25  {
27  setup_sorts();
29  }
30 
31  void parse()
32  {
34  }
35 
36  struct idt
37  {
38  using kindt = enum { VARIABLE, BINDING, PARAMETER };
39 
40  idt(kindt _kind, const exprt &expr)
41  : kind(_kind), type(expr.type()), definition(expr)
42  {
43  }
44 
48  std::vector<irep_idt> parameters;
49  };
50 
51  using id_mapt=std::map<irep_idt, idt>;
53 
54  struct named_termt
55  {
58  named_termt(const exprt &_term, const symbol_exprt &_name)
59  : term(_term), name(_name)
60  {
61  }
62 
65  };
66 
67  using named_termst = std::map<irep_idt, named_termt>;
69 
70  bool exit;
71 
73  {
75  }
76 
78  {
79  return smt2_tokenizer.error();
80  }
81 
83  void skip_to_end_of_list();
84 
85 protected:
87  // we extend next_token to track the parenthesis level
88  std::size_t parenthesis_level;
90 
91  // for let/quantifier bindings, function parameters
92  using renaming_mapt=std::map<irep_idt, irep_idt>;
94  using renaming_counterst=std::map<irep_idt, unsigned>;
96  irep_idt add_fresh_id(const irep_idt &, idt::kindt, const exprt &);
97  void add_unique_id(const irep_idt &, const exprt &);
98  irep_idt rename_id(const irep_idt &) const;
99 
101  {
103  std::vector<irep_idt> parameters;
104 
105  explicit signature_with_parameter_idst(const typet &_type) : type(_type)
106  {
107  }
108 
110  const typet &_type,
111  const std::vector<irep_idt> &_parameters)
112  : type(_type), parameters(_parameters)
113  {
114  PRECONDITION(
115  (_type.id() == ID_mathematical_function &&
116  to_mathematical_function_type(_type).domain().size() ==
117  _parameters.size()) ||
118  (_type.id() != ID_mathematical_function && _parameters.empty()));
119  }
120  };
121 
122  // expressions
123  std::unordered_map<std::string, std::function<exprt()>> expressions;
124  void setup_expressions();
125  exprt expression();
128  const irep_idt &,
129  const exprt::operandst &);
139 
143  const symbol_exprt &function,
144  const exprt::operandst &op);
145 
148 
151 
152  // sorts
153  typet sort();
154  std::unordered_map<std::string, std::function<typet()>> sorts;
155  void setup_sorts();
156 
157  // hashtable for all commands
158  std::unordered_map<std::string, std::function<void()>> commands;
159 
160  void command_sequence();
161  void command(const std::string &);
162  void ignore_command();
163  void setup_commands();
164 };
165 
166 #endif // CPROVER_SOLVERS_SMT2_SMT2_PARSER_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
const irep_idt & id() const
Definition: irep.h:407
irep_idt add_fresh_id(const irep_idt &, idt::kindt, const exprt &)
exprt function_application_ieee_float_op(const irep_idt &, const exprt::operandst &)
std::size_t parenthesis_level
Definition: smt2_parser.h:88
void command(const std::string &)
std::map< irep_idt, named_termt > named_termst
Definition: smt2_parser.h:67
exprt::operandst operands()
std::map< irep_idt, unsigned > renaming_counterst
Definition: smt2_parser.h:94
renaming_mapt renaming_map
Definition: smt2_parser.h:93
void command_sequence()
Definition: smt2_parser.cpp:43
exprt binary(irep_idt, const exprt::operandst &)
void skip_to_end_of_list()
This skips tokens until all bracketed expressions are closed.
Definition: smt2_parser.cpp:36
std::unordered_map< std::string, std::function< exprt()> > expressions
Definition: smt2_parser.h:123
smt2_parsert(std::istream &_in)
Definition: smt2_parser.h:23
void add_unique_id(const irep_idt &, const exprt &)
typet function_signature_declaration()
named_termst named_terms
Definition: smt2_parser.h:68
id_mapt id_map
Definition: smt2_parser.h:52
std::unordered_map< std::string, std::function< void()> > commands
Definition: smt2_parser.h:158
void setup_sorts()
exprt function_application()
exprt cast_bv_to_unsigned(const exprt &)
Apply typecast to unsignedbv to given expression.
exprt::operandst cast_bv_to_signed(const exprt::operandst &)
Apply typecast to signedbv to expressions in vector.
exprt multi_ary(irep_idt, const exprt::operandst &)
std::map< irep_idt, idt > id_mapt
Definition: smt2_parser.h:51
irep_idt rename_id(const irep_idt &) const
std::map< irep_idt, irep_idt > renaming_mapt
Definition: smt2_parser.h:92
void ignore_command()
Definition: smt2_parser.cpp:88
exprt quantifier_expression(irep_idt)
exprt function_application_ieee_float_eq(const exprt::operandst &)
exprt let_expression()
signature_with_parameter_idst function_signature_definition()
exprt function_application_fp(const exprt::operandst &)
void parse()
Definition: smt2_parser.h:31
exprt expression()
renaming_counterst renaming_counters
Definition: smt2_parser.h:95
void setup_expressions()
exprt binary_predicate(irep_idt, const exprt::operandst &)
smt2_tokenizert::tokent next_token()
Definition: smt2_parser.cpp:24
smt2_tokenizert::smt2_errort error(const std::string &message)
Definition: smt2_parser.h:72
std::unordered_map< std::string, std::function< typet()> > sorts
Definition: smt2_parser.h:154
smt2_tokenizert::smt2_errort error()
Definition: smt2_parser.h:77
smt2_tokenizert smt2_tokenizer
Definition: smt2_parser.h:86
exprt unary(irep_idt, const exprt::operandst &)
void setup_commands()
smt2_errort error(const std::string &message)
generate an error exception, pre-filled with a message
enum { NONE, END_OF_FILE, STRING_LITERAL, NUMERAL, SYMBOL, KEYWORD, OPEN, CLOSE } tokent
Expression to hold a symbol (variable)
Definition: std_expr.h:81
The type of an expression, extends irept.
Definition: type.h:28
Mathematical types.
const mathematical_function_typet & to_mathematical_function_type(const typet &type)
Cast a typet to a mathematical_function_typet.
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
static const char * message(const statust &status)
Makes a status message string from a status.
API to expression classes.
std::vector< irep_idt > parameters
Definition: smt2_parser.h:48
idt(kindt _kind, const exprt &expr)
Definition: smt2_parser.h:40
enum { VARIABLE, BINDING, PARAMETER } kindt
Definition: smt2_parser.h:38
named_termt(const exprt &_term, const symbol_exprt &_name)
Default-constructing a symbol_exprt is deprecated, thus make sure we always construct a named_termt f...
Definition: smt2_parser.h:58
signature_with_parameter_idst(const typet &_type, const std::vector< irep_idt > &_parameters)
Definition: smt2_parser.h:109
signature_with_parameter_idst(const typet &_type)
Definition: smt2_parser.h:105