cprover
smt_commands.h
Go to the documentation of this file.
1 // Author: Diffblue Ltd.
2 
3 #ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_COMMANDS_H
4 #define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_COMMANDS_H
5 
9 #include <util/irep.h>
10 
12 
13 class smt_commandt : protected irept
14 {
15 public:
16  // smt_commandt does not support the notion of an empty / null state. Use
17  // optionalt<smt_commandt> instead if an empty command is required.
18  smt_commandt() = delete;
19 
20  using irept::pretty;
21 
22  bool operator==(const smt_commandt &) const;
23  bool operator!=(const smt_commandt &) const;
24 
27 
28 protected:
29  using irept::irept;
30 };
31 
33  private smt_termt::storert<smt_assert_commandt>
34 {
35 public:
37  const smt_termt &condition() const;
38 };
39 
41 {
42 public:
44 };
45 
47  : public smt_commandt,
48  private smt_sortt::storert<smt_declare_function_commandt>,
49  private smt_termt::storert<smt_declare_function_commandt>
50 {
51 public:
54  std::vector<smt_sortt> parameter_sorts);
55  const smt_identifier_termt &identifier() const;
56  const smt_sortt &return_sort() const;
57  std::vector<std::reference_wrapper<const smt_sortt>> parameter_sorts() const;
58 
59 private:
62 };
63 
65  : public smt_commandt,
66  private smt_termt::storert<smt_define_function_commandt>
67 {
68 public:
71  std::vector<smt_identifier_termt> parameters,
73  const smt_identifier_termt &identifier() const;
74  std::vector<std::reference_wrapper<const smt_identifier_termt>>
75  parameters() const;
76  const smt_sortt &return_sort() const;
77  const smt_termt &definition() const;
78 };
79 
81 {
82 public:
84 };
85 
87  protected smt_termt::storert<smt_assert_commandt>
88 {
89 public:
91  const smt_termt &descriptor() const;
92 };
93 
95 {
96 public:
97  explicit smt_push_commandt(std::size_t levels);
98  size_t levels() const;
99 };
100 
102 {
103 public:
104  explicit smt_pop_commandt(std::size_t levels);
105  size_t levels() const;
106 };
107 
109  : public smt_commandt,
110  private smt_logict::storert<smt_set_logic_commandt>
111 {
112 public:
114  const smt_logict &logic() const;
115 };
116 
118  : public smt_commandt,
119  private smt_optiont::storert<smt_set_option_commandt>
120 {
121 public:
123  const smt_optiont &option() const;
124 };
125 
127 {
128 public:
129 #define COMMAND_ID(the_id) \
130  virtual void visit(const smt_##the_id##_commandt &) = 0;
131 #include "smt_commands.def"
132 #undef COMMAND_ID
133 };
134 
138 {
139 private:
140  std::vector<smt_sortt> parameter_sorts;
142 
143 public:
144  explicit smt_command_functiont(
145  const smt_declare_function_commandt &function_declaration);
146  explicit smt_command_functiont(
147  const smt_define_function_commandt &function_definition);
148  irep_idt identifier() const;
149  smt_sortt return_sort(const std::vector<smt_termt> &arguments) const;
150  void validate(const std::vector<smt_termt> &arguments) const;
151 };
152 
153 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_COMMANDS_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:383
irept()=default
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
smt_assert_commandt(smt_termt condition)
const smt_termt & condition() const
A function generated from a command.
Definition: smt_commands.h:138
std::vector< smt_sortt > parameter_sorts
Definition: smt_commands.h:140
irep_idt identifier() const
smt_command_functiont(const smt_declare_function_commandt &function_declaration)
smt_sortt return_sort(const std::vector< smt_termt > &arguments) const
smt_identifier_termt _identifier
Definition: smt_commands.h:141
void validate(const std::vector< smt_termt > &arguments) const
void accept(smt_command_const_downcast_visitort &) const
bool operator==(const smt_commandt &) const
bool operator!=(const smt_commandt &) const
smt_commandt()=delete
const smt_identifier_termt & identifier() const
smt_declare_function_commandt(smt_identifier_termt identifier, std::vector< smt_sortt > parameter_sorts)
const smt_sortt & return_sort() const
std::vector< std::reference_wrapper< const smt_sortt > > parameter_sorts() const
const smt_termt & definition() const
const smt_identifier_termt & identifier() const
smt_define_function_commandt(irep_idt identifier, std::vector< smt_identifier_termt > parameters, smt_termt definition)
std::vector< std::reference_wrapper< const smt_identifier_termt > > parameters() const
const smt_sortt & return_sort() const
const smt_termt & descriptor() const
smt_get_value_commandt(smt_termt descriptor)
Stores identifiers in unescaped and unquoted form.
Definition: smt_terms.h:81
Class for adding the ability to up and down cast smt_logict to and from irept.
Definition: smt_logics.h:32
Class for adding the ability to up and down cast smt_optiont to and from irept.
Definition: smt_options.h:32
size_t levels() const
smt_pop_commandt(std::size_t levels)
size_t levels() const
smt_push_commandt(std::size_t levels)
const smt_logict & logic() const
smt_set_logic_commandt(smt_logict logic)
smt_set_option_commandt(smt_optiont option)
const smt_optiont & option() const
Class for adding the ability to up and down cast smt_sortt to and from irept.
Definition: smt_sorts.h:39
Class for adding the ability to up and down cast smt_termt to and from irept.
Definition: smt_terms.h:39