cprover
Loading...
Searching...
No Matches
smt_responses.h
Go to the documentation of this file.
1// Author: Diffblue Ltd.
2
3#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_RESPONSES_H
4#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_RESPONSES_H
5
6#include "smt_terms.h"
7#include <util/irep.h>
8
9class smt_responset : protected irept
10{
11public:
12 // smt_responset does not support the notion of an empty / null state. Use
13 // optionalt<smt_responset> instead if an empty response is required.
14 smt_responset() = delete;
15
16 using irept::pretty;
17
18 bool operator==(const smt_responset &) const;
19 bool operator!=(const smt_responset &) const;
20
21 template <typename sub_classt>
22 const sub_classt *cast() const &;
23
26};
27
33
35{
36public:
37 // smt_responset does not support the notion of an empty / null state. Use
38 // optionalt<smt_responset> instead if an empty response is required.
40
41 using irept::pretty;
42
43 bool operator==(const smt_check_sat_response_kindt &) const;
44 bool operator!=(const smt_check_sat_response_kindt &) const;
45
46 template <typename sub_classt>
47 const sub_classt *cast() const &;
48
57 {
58 protected:
59 storert();
61 static const smt_check_sat_response_kindt &downcast(const irept &);
62 };
63
64protected:
65 using irept::irept;
66};
67
73
79
85
87 : public smt_responset,
88 private smt_check_sat_response_kindt::storert<smt_check_sat_responset>
89{
90public:
92 const smt_check_sat_response_kindt &kind() const;
93};
94
96 : public smt_responset,
97 private smt_termt::storert<smt_get_value_responset>
98{
99public:
100 class valuation_pairt : private irept,
101 private smt_termt::storert<valuation_pairt>
102 {
103 public:
104 valuation_pairt() = delete;
105 valuation_pairt(smt_termt descriptor, smt_termt value);
106 valuation_pairt(irep_idt descriptor, const smt_termt &value);
107
108 using irept::pretty;
109
110 bool operator==(const valuation_pairt &) const;
111 bool operator!=(const valuation_pairt &) const;
112
113 const smt_termt &descriptor() const;
114 const smt_termt &value() const;
115
117 };
118
119 explicit smt_get_value_responset(std::vector<valuation_pairt> pairs);
120 std::vector<std::reference_wrapper<const valuation_pairt>> pairs() const;
121};
122
124{
125public:
127};
128
130{
131public:
132 explicit smt_error_responset(irep_idt message);
133 const irep_idt &message() const;
134};
135
136#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_RESPONSES_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
Class for adding the ability to up and down cast smt_check_sat_response_kindt to and from irept.
const sub_classt * cast() const &
smt_responset()=delete
bool operator!=(const smt_responset &) const
bool operator==(const smt_responset &) const
const sub_classt * cast() const &
Class for adding the ability to up and down cast smt_termt to and from irept.
Definition smt_terms.h:39
bool operator!=(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
bool operator==(const string_not_contains_constraintt &left, const string_not_contains_constraintt &right)