cprover
Loading...
Searching...
No Matches
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
13class smt_commandt : protected irept
14{
15public:
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
28protected:
29 using irept::irept;
30};
31
33 private smt_termt::storert<smt_assert_commandt>
34{
35public:
37 const smt_termt &condition() const;
38};
39
41{
42public:
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{
51public:
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
59private:
62};
63
65 : public smt_commandt,
66 private smt_termt::storert<smt_define_function_commandt>
67{
68public:
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{
82public:
84};
85
87 protected smt_termt::storert<smt_assert_commandt>
88{
89public:
99 const smt_termt &descriptor() const;
100};
101
103{
104public:
105 explicit smt_push_commandt(std::size_t levels);
106 size_t levels() const;
107};
108
110{
111public:
112 explicit smt_pop_commandt(std::size_t levels);
113 size_t levels() const;
114};
115
117 : public smt_commandt,
118 private smt_logict::storert<smt_set_logic_commandt>
119{
120public:
122 const smt_logict &logic() const;
123};
124
126 : public smt_commandt,
127 private smt_optiont::storert<smt_set_option_commandt>
128{
129public:
131 const smt_optiont &option() const;
132};
133
135{
136public:
137#define COMMAND_ID(the_id) \
138 virtual void visit(const smt_##the_id##_commandt &) = 0;
139#include "smt_commands.def"
140#undef COMMAND_ID
141};
142
146{
147private:
148 std::vector<smt_sortt> parameter_sorts;
150
151public:
152 explicit smt_command_functiont(
154 explicit smt_command_functiont(
156 irep_idt identifier() const;
157 smt_sortt return_sort(const std::vector<smt_termt> &arguments) const;
158 void validate(const std::vector<smt_termt> &arguments) const;
159};
160
161#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_COMMANDS_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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:372
irept()=default
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition irep.cpp:495
const smt_termt & condition() const
A function generated from a command.
std::vector< smt_sortt > parameter_sorts
irep_idt identifier() const
smt_sortt return_sort(const std::vector< smt_termt > &arguments) const
smt_identifier_termt _identifier
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
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
std::vector< std::reference_wrapper< const smt_identifier_termt > > parameters() const
const smt_sortt & return_sort() const
const smt_termt & descriptor() const
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
size_t levels() const
const smt_logict & logic() const
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