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
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
smt_push_commandt
Definition: smt_commands.h:95
smt_set_logic_commandt
Definition: smt_commands.h:111
smt_define_function_commandt::return_sort
const smt_sortt & return_sort() const
Definition: smt_commands.cpp:114
smt_identifier_termt
Stores identifiers in unescaped and unquoted form.
Definition: smt_terms.h:81
smt_pop_commandt::levels
size_t levels() const
Definition: smt_commands.cpp:152
smt_pop_commandt::smt_pop_commandt
smt_pop_commandt(std::size_t levels)
Definition: smt_commands.cpp:146
smt_define_function_commandt::definition
const smt_termt & definition() const
Definition: smt_commands.cpp:119
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
smt_define_function_commandt::smt_define_function_commandt
smt_define_function_commandt(irep_idt identifier, std::vector< smt_identifier_termt > parameters, smt_termt definition)
Definition: smt_commands.cpp:80
smt_command_functiont::parameter_sorts
std::vector< smt_sortt > parameter_sorts
Definition: smt_commands.h:140
smt_termt
Definition: smt_terms.h:16
smt_assert_commandt::smt_assert_commandt
smt_assert_commandt(smt_termt condition)
Definition: smt_commands.cpp:23
smt_set_option_commandt
Definition: smt_commands.h:120
smt_check_sat_commandt::smt_check_sat_commandt
smt_check_sat_commandt()
Definition: smt_commands.cpp:37
smt_define_function_commandt
Definition: smt_commands.h:67
smt_get_value_commandt::descriptor
const smt_termt & descriptor() const
Definition: smt_commands.cpp:130
smt_define_function_commandt::parameters
std::vector< std::reference_wrapper< const smt_identifier_termt > > parameters() const
Definition: smt_commands.cpp:106
smt_sortt::storert
Class for adding the ability to up and down cast smt_sortt to and from irept.
Definition: smt_sorts.h:39
smt_commandt::accept
void accept(smt_command_const_downcast_visitort &) const
Definition: smt_commands.cpp:192
smt_set_option_commandt::option
const smt_optiont & option() const
Definition: smt_commands.cpp:174
smt_command_functiont::return_sort
smt_sortt return_sort(const std::vector< smt_termt > &arguments) const
Definition: smt_commands.cpp:227
irept::irept
irept()=default
smt_commandt::operator==
bool operator==(const smt_commandt &) const
Definition: smt_commands.cpp:13
smt_define_function_commandt::identifier
const smt_identifier_termt & identifier() const
Definition: smt_commands.cpp:99
smt_exit_commandt
Definition: smt_commands.h:81
smt_optiont::storert
Class for adding the ability to up and down cast smt_optiont to and from irept.
Definition: smt_options.h:32
smt_push_commandt::smt_push_commandt
smt_push_commandt(std::size_t levels)
Definition: smt_commands.cpp:135
smt_declare_function_commandt::smt_declare_function_commandt
smt_declare_function_commandt(smt_identifier_termt identifier, std::vector< smt_sortt > parameter_sorts)
Definition: smt_commands.cpp:42
smt_declare_function_commandt
Definition: smt_commands.h:50
smt_command_const_downcast_visitort
Definition: smt_commands.h:127
smt_check_sat_commandt
Definition: smt_commands.h:41
smt_command_functiont::_identifier
smt_identifier_termt _identifier
Definition: smt_commands.h:141
smt_pop_commandt
Definition: smt_commands.h:102
smt_sortt
Definition: smt_sorts.h:18
smt_exit_commandt::smt_exit_commandt
smt_exit_commandt()
Definition: smt_commands.cpp:76
smt_assert_commandt::condition
const smt_termt & condition() const
Definition: smt_commands.cpp:32
smt_command_functiont::smt_command_functiont
smt_command_functiont(const smt_declare_function_commandt &function_declaration)
Definition: smt_commands.cpp:202
smt_set_logic_commandt::smt_set_logic_commandt
smt_set_logic_commandt(smt_logict logic)
Definition: smt_commands.cpp:157
smt_commandt
Definition: smt_commands.h:14
smt_command_functiont::identifier
irep_idt identifier() const
Definition: smt_commands.cpp:222
smt_get_value_commandt::smt_get_value_commandt
smt_get_value_commandt(smt_termt descriptor)
Definition: smt_commands.cpp:124
smt_commandt::smt_commandt
smt_commandt()=delete
smt_declare_function_commandt::return_sort
const smt_sortt & return_sort() const
Definition: smt_commands.cpp:63
smt_command_functiont::validate
void validate(const std::vector< smt_termt > &arguments) const
Definition: smt_commands.cpp:233
smt_declare_function_commandt::parameter_sorts
std::vector< std::reference_wrapper< const smt_sortt > > parameter_sorts() const
Definition: smt_commands.cpp:69
smt_logict::storert
Class for adding the ability to up and down cast smt_logict to and from irept.
Definition: smt_logics.h:32
smt_declare_function_commandt::identifier
const smt_identifier_termt & identifier() const
Definition: smt_commands.cpp:57
smt_termt::storert
Class for adding the ability to up and down cast smt_termt to and from irept.
Definition: smt_terms.h:39
smt_logics.h
smt_get_value_commandt
Definition: smt_commands.h:88
smt_options.h
smt_assert_commandt
Definition: smt_commands.h:34
smt_set_option_commandt::smt_set_option_commandt
smt_set_option_commandt(smt_optiont option)
Definition: smt_commands.cpp:168
smt_logict
Definition: smt_logics.h:11
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:383
smt_set_logic_commandt::logic
const smt_logict & logic() const
Definition: smt_commands.cpp:163
smt_push_commandt::levels
size_t levels() const
Definition: smt_commands.cpp:141
smt_commandt::operator!=
bool operator!=(const smt_commandt &) const
Definition: smt_commands.cpp:18
smt_terms.h
smt_command_functiont
A function generated from a command.
Definition: smt_commands.h:138
smt_optiont
Definition: smt_options.h:11
irep.h