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
smt2_parsert::command
virtual void command(const std::string &)
Definition: smt2_parser.cpp:1164
smt2_parsert::quantifier_expression
exprt quantifier_expression(irep_idt)
Definition: smt2_parser.cpp:218
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
smt2_parsert::rename_id
irep_idt rename_id(const irep_idt &) const
Definition: smt2_parser.cpp:139
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
smt2_parsert::renaming_counters
renaming_counterst renaming_counters
Definition: smt2_parser.h:73
smt2_tokenizert::tokent
enum { NONE, END_OF_FILE, STRING_LITERAL, NUMERAL, SYMBOL, KEYWORD, OPEN, CLOSE } tokent
Definition: smt2_tokenizer.h:73
typet
The type of an expression, extends irept.
Definition: type.h:27
smt2_parsert::ignore_command
void ignore_command()
Definition: smt2_parser.cpp:78
smt2_parsert::function_application
exprt function_application()
Definition: smt2_parser.cpp:448
smt2_parsert::next_token
tokent next_token() override
Definition: smt2_parser.cpp:19
smt2_parsert
Definition: smt2_parser.h:18
nil_typet
The NIL type, i.e., an invalid type, no value.
Definition: std_types.h:39
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:86
smt2_parsert::idt::parameters
std::vector< irep_idt > parameters
Definition: smt2_parser.h:40
smt2_parsert::binary
exprt binary(irep_idt, const exprt::operandst &)
Definition: smt2_parser.cpp:379
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:120
exprt
Base class for all expressions.
Definition: expr.h:54
smt2_parsert::idt::definition
exprt definition
Definition: smt2_parser.h:39
smt2_parsert::named_terms
named_termst named_terms
Definition: smt2_parser.h:53
smt2_tokenizert
Definition: smt2_tokenizer.h:18
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:143
smt2_parsert::function_signature_definition
signature_with_parameter_idst function_signature_definition()
Definition: smt2_parser.cpp:1087
smt2_parsert::sort
typet sort()
Definition: smt2_parser.cpp:1003
smt2_parsert::exit
bool exit
Definition: smt2_parser.h:55
smt2_parsert::multi_ary
exprt multi_ary(irep_idt, const exprt::operandst &)
Definition: smt2_parser.cpp:334
smt2_parsert::unary
exprt unary(irep_idt, const exprt::operandst &)
Definition: smt2_parser.cpp:371
smt2_parsert::idt::type
typet type
Definition: smt2_parser.h:38
smt2_parsert::command_sequence
void command_sequence()
Definition: smt2_parser.cpp:38
smt2_parsert::parenthesis_level
std::size_t parenthesis_level
Definition: smt2_parser.h:62
smt2_parsert::renaming_mapt
std::map< irep_idt, irep_idt > renaming_mapt
Definition: smt2_parser.h:70
smt2_parsert::function_signature_declaration
typet function_signature_declaration()
Definition: smt2_parser.cpp:1130
smt2_parsert::function_application_fp
exprt function_application_fp(const exprt::operandst &)
Definition: smt2_parser.cpp:419
smt2_parsert::let_expression
exprt let_expression()
Definition: smt2_parser.cpp:149
smt2_tokenizer.h
smt2_parsert::binary_predicate
exprt binary_predicate(irep_idt, const exprt::operandst &)
Definition: smt2_parser.cpp:355
smt2_parsert::idt::idt
idt()
Definition: smt2_parser.h:34
smt2_parsert::named_termt
Definition: smt2_parser.h:46
smt2_parsert::function_application_ieee_float_op
exprt function_application_ieee_float_op(const irep_idt &, const exprt::operandst &)
Definition: smt2_parser.cpp:390
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:299
irept::id
const irep_idt & id() const
Definition: irep.h:259
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:57
smt2_parsert::renaming_map
renaming_mapt renaming_map
Definition: smt2_parser.h:71
smt2_parsert::signature_with_parameter_idst::signature_with_parameter_idst
signature_with_parameter_idst(const typet &_type)
Definition: smt2_parser.h:82
smt2_parsert::id_mapt
std::map< irep_idt, idt > id_mapt
Definition: smt2_parser.h:43
smt2_parsert::get_fresh_id
irep_idt get_fresh_id(const irep_idt &)
Definition: smt2_parser.cpp:119
smt2_parsert::signature_with_parameter_idst
Definition: smt2_parser.h:77
smt2_parsert::named_termst
std::map< irep_idt, named_termt > named_termst
Definition: smt2_parser.h:52
smt2_parsert::expression
exprt expression()
Definition: smt2_parser.cpp:912
smt2_parsert::cast_bv_to_unsigned
exprt cast_bv_to_unsigned(const exprt &)
Apply typecast to unsignedbv to given expression.
Definition: smt2_parser.cpp:322
smt2_parsert::idt
Definition: smt2_parser.h:32
smt2_parsert::signature_with_parameter_idst::type
typet type
Definition: smt2_parser.h:79
smt2_parsert::renaming_counterst
std::map< irep_idt, unsigned > renaming_counterst
Definition: smt2_parser.h:72
smt2_parsert::signature_with_parameter_idst::parameters
std::vector< irep_idt > parameters
Definition: smt2_parser.h:80
smt2_parsert::parse
bool parse() override
Definition: smt2_parser.h:26
smt2_parsert::operands
exprt::operandst operands()
Definition: smt2_parser.cpp:107
std_expr.h
smt2_parsert::id_map
id_mapt id_map
Definition: smt2_parser.h:44
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:31
smt2_parsert::named_termt::name
symbol_exprt name
Definition: smt2_parser.h:49
smt2_parsert::smt2_parsert
smt2_parsert(std::istream &_in)
Definition: smt2_parser.h:21
smt2_parsert::named_termt::term
exprt term
Definition: smt2_parser.h:48