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
smt2_parsert::command
void command(const std::string &)
Definition: smt2_parser.cpp:1236
smt2_parsert::quantifier_expression
exprt quantifier_expression(irep_idt)
Definition: smt2_parser.cpp:241
smt2_parsert::setup_sorts
void setup_sorts()
Definition: smt2_parser.cpp:1105
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
smt2_parsert::rename_id
irep_idt rename_id(const irep_idt &) const
Definition: smt2_parser.cpp:169
smt2_parsert::setup_commands
void setup_commands()
Definition: smt2_parser.cpp:1248
smt2_parsert::error
smt2_tokenizert::smt2_errort error(const std::string &message)
Definition: smt2_parser.h:72
smt2_parsert::renaming_counters
renaming_counterst renaming_counters
Definition: smt2_parser.h:95
smt2_parsert::error
smt2_tokenizert::smt2_errort error()
Definition: smt2_parser.h:77
smt2_tokenizert::tokent
enum { NONE, END_OF_FILE, STRING_LITERAL, NUMERAL, SYMBOL, KEYWORD, OPEN, CLOSE } tokent
Definition: smt2_tokenizer.h:68
typet
The type of an expression, extends irept.
Definition: type.h:29
smt2_parsert::sorts
std::unordered_map< std::string, std::function< typet()> > sorts
Definition: smt2_parser.h:154
smt2_parsert::expressions
std::unordered_map< std::string, std::function< exprt()> > expressions
Definition: smt2_parser.h:123
smt2_parsert::ignore_command
void ignore_command()
Definition: smt2_parser.cpp:86
smt2_parsert::function_application
exprt function_application()
Definition: smt2_parser.cpp:489
smt2_parsert::add_fresh_id
irep_idt add_fresh_id(const irep_idt &, idt::kindt, const exprt &)
Definition: smt2_parser.cpp:131
smt2_parsert
Definition: smt2_parser.h:21
smt2_parsert::signature_with_parameter_idst::signature_with_parameter_idst
signature_with_parameter_idst(const typet &_type, const std::vector< irep_idt > &_parameters)
Definition: smt2_parser.h:109
smt2_parsert::idt::parameters
std::vector< irep_idt > parameters
Definition: smt2_parser.h:48
smt2_parsert::binary
exprt binary(irep_idt, const exprt::operandst &)
Definition: smt2_parser.cpp:403
to_mathematical_function_type
const mathematical_function_typet & to_mathematical_function_type(const typet &type)
Cast a typet to a mathematical_function_typet.
Definition: mathematical_types.h:119
exprt
Base class for all expressions.
Definition: expr.h:53
smt2_tokenizert::error
smt2_errort error(const std::string &message)
generate an error exception, pre-filled with a message
Definition: smt2_tokenizer.h:95
smt2_parsert::parse
void parse()
Definition: smt2_parser.h:31
smt2_parsert::idt::definition
exprt definition
Definition: smt2_parser.h:47
smt2_parsert::commands
std::unordered_map< std::string, std::function< void()> > commands
Definition: smt2_parser.h:158
smt2_parsert::named_terms
named_termst named_terms
Definition: smt2_parser.h:68
smt2_parsert::idt::kind
kindt kind
Definition: smt2_parser.h:45
smt2_tokenizert
Definition: smt2_tokenizer.h:18
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
smt2_parsert::function_signature_definition
signature_with_parameter_idst function_signature_definition()
Definition: smt2_parser.cpp:1161
smt2_parsert::sort
typet sort()
Definition: smt2_parser.cpp:1060
smt2_parsert::exit
bool exit
Definition: smt2_parser.h:70
smt2_parsert::add_unique_id
void add_unique_id(const irep_idt &, const exprt &)
Definition: smt2_parser.cpp:155
smt2_parsert::multi_ary
exprt multi_ary(irep_idt, const exprt::operandst &)
Definition: smt2_parser.cpp:358
smt2_parsert::unary
exprt unary(irep_idt, const exprt::operandst &)
Definition: smt2_parser.cpp:395
smt2_parsert::idt::type
typet type
Definition: smt2_parser.h:46
smt2_parsert::command_sequence
void command_sequence()
Definition: smt2_parser.cpp:41
mathematical_types.h
Mathematical types.
message
static const char * message(const static_verifier_resultt::statust &status)
Makes a status message string from a status.
Definition: static_verifier.cpp:74
smt2_parsert::parenthesis_level
std::size_t parenthesis_level
Definition: smt2_parser.h:88
smt2_parsert::renaming_mapt
std::map< irep_idt, irep_idt > renaming_mapt
Definition: smt2_parser.h:92
smt2_parsert::function_signature_declaration
typet function_signature_declaration()
Definition: smt2_parser.cpp:1202
smt2_parsert::function_application_fp
exprt function_application_fp(const exprt::operandst &)
Definition: smt2_parser.cpp:462
smt2_parsert::let_expression
exprt let_expression()
Definition: smt2_parser.cpp:179
smt2_parsert::setup_expressions
void setup_expressions()
Definition: smt2_parser.cpp:807
smt2_tokenizer.h
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
smt2_parsert::binary_predicate
exprt binary_predicate(irep_idt, const exprt::operandst &)
Definition: smt2_parser.cpp:379
smt2_parsert::named_termt::named_termt
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
smt2_parsert::named_termt
Definition: smt2_parser.h:55
smt2_parsert::function_application_ieee_float_op
exprt function_application_ieee_float_op(const irep_idt &, const exprt::operandst &)
Definition: smt2_parser.cpp:433
smt2_parsert::cast_bv_to_signed
exprt::operandst cast_bv_to_signed(const exprt::operandst &)
Apply typecast to signedbv to expressions in vector.
Definition: smt2_parser.cpp:323
irept::id
const irep_idt & id() const
Definition: irep.h:418
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
smt2_parsert::renaming_map
renaming_mapt renaming_map
Definition: smt2_parser.h:93
smt2_parsert::signature_with_parameter_idst::signature_with_parameter_idst
signature_with_parameter_idst(const typet &_type)
Definition: smt2_parser.h:105
smt2_parsert::id_mapt
std::map< irep_idt, idt > id_mapt
Definition: smt2_parser.h:51
smt2_parsert::signature_with_parameter_idst
Definition: smt2_parser.h:101
smt2_parsert::named_termst
std::map< irep_idt, named_termt > named_termst
Definition: smt2_parser.h:67
smt2_parsert::function_application_ieee_float_eq
exprt function_application_ieee_float_eq(const exprt::operandst &)
Definition: smt2_parser.cpp:414
smt2_parsert::expression
exprt expression()
Definition: smt2_parser.cpp:736
smt2_tokenizert::smt2_errort
Definition: smt2_tokenizer.h:27
smt2_parsert::cast_bv_to_unsigned
exprt cast_bv_to_unsigned(const exprt &)
Apply typecast to unsignedbv to given expression.
Definition: smt2_parser.cpp:346
smt2_parsert::idt
Definition: smt2_parser.h:37
smt2_parsert::idt::kindt
enum { VARIABLE, BINDING, PARAMETER } kindt
Definition: smt2_parser.h:38
smt2_parsert::signature_with_parameter_idst::type
typet type
Definition: smt2_parser.h:102
smt2_parsert::next_token
smt2_tokenizert::tokent next_token()
Definition: smt2_parser.cpp:22
smt2_parsert::renaming_counterst
std::map< irep_idt, unsigned > renaming_counterst
Definition: smt2_parser.h:94
smt2_parsert::signature_with_parameter_idst::parameters
std::vector< irep_idt > parameters
Definition: smt2_parser.h:103
smt2_parsert::operands
exprt::operandst operands()
Definition: smt2_parser.cpp:119
smt2_parsert::smt2_tokenizer
smt2_tokenizert smt2_tokenizer
Definition: smt2_parser.h:86
smt2_parsert::idt::idt
idt(kindt _kind, const exprt &expr)
Definition: smt2_parser.h:40
std_expr.h
API to expression classes.
smt2_parsert::id_map
id_mapt id_map
Definition: smt2_parser.h:52
smt2_parsert::skip_to_end_of_list
void skip_to_end_of_list()
This skips tokens until all bracketed expressions are closed.
Definition: smt2_parser.cpp:34
smt2_parsert::named_termt::name
symbol_exprt name
Definition: smt2_parser.h:64
smt2_parsert::smt2_parsert
smt2_parsert(std::istream &_in)
Definition: smt2_parser.h:23
smt2_parsert::named_termt::term
exprt term
Definition: smt2_parser.h:63