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),
23  exit(false)
24  {
25  }
26 
27  bool parse() override
28  {
30  return !ok;
31  }
32 
33  struct idt
34  {
36  {
37  }
38 
41  };
42 
43  using id_mapt=std::map<irep_idt, idt>;
45 
46 protected:
47  bool exit;
48  void command_sequence();
49 
50  virtual void command(const std::string &);
51 
52  // for let/quantifier bindings, function parameters
53  using renaming_mapt=std::map<irep_idt, irep_idt>;
55  using renaming_counterst=std::map<irep_idt, unsigned>;
58  irep_idt rename_id(const irep_idt &) const;
59 
60  void ignore_command();
61  exprt expression();
63  typet sort();
71 
75  const irep_idt &identifier,
76  const exprt::operandst &op);
77 
80 
83 };
84 
85 #endif // CPROVER_SOLVERS_SMT2_SMT2_PARSER_H
The type of an expression.
Definition: type.h:22
renaming_mapt renaming_map
Definition: smt2_parser.h:54
typet function_signature_declaration()
exprt quantifier_expression(irep_idt)
irep_idt get_fresh_id(const irep_idt &)
Definition: smt2_parser.cpp:94
bool parse() override
Definition: smt2_parser.h:27
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()
Definition: smt2_parser.cpp:82
renaming_counterst renaming_counters
Definition: smt2_parser.h:56
exprt binary_predicate(irep_idt, const exprt::operandst &)
void ignore_command()
Definition: smt2_parser.cpp:53
API to expression classes.
std::map< irep_idt, irep_idt > renaming_mapt
Definition: smt2_parser.h:53
irep_idt rename_id(const irep_idt &) const
exprt let_expression()
typet function_signature_definition()
exprt expression()
id_mapt id_map
Definition: smt2_parser.h:44
std::vector< exprt > operandst
Definition: expr.h:45
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:55
virtual void command(const std::string &)
exprt binary(irep_idt, const exprt::operandst &)
Base class for all expressions.
Definition: expr.h:42
The NIL type.
Definition: std_types.h:44
exprt::operandst cast_bv_to_signed(const exprt::operandst &)
Apply typecast to signedbv to expressions in vector.
exprt function_application()
smt2_parsert(std::istream &_in)
Definition: smt2_parser.h:21
void command_sequence()
Definition: smt2_parser.cpp:13