cprover
Loading...
Searching...
No Matches
smt_bit_vector_theory.h
Go to the documentation of this file.
1// Author: Diffblue Ltd.
2
3#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_BIT_VECTOR_THEORY_H
4#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_BIT_VECTOR_THEORY_H
5
7
9{
10public:
11 // Relational operator class declarations
13 {
14 static const char *identifier();
15 static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
16 static void validate(const smt_termt &lhs, const smt_termt &rhs);
17 };
20
22 {
23 static const char *identifier();
24 static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
25 static void validate(const smt_termt &lhs, const smt_termt &rhs);
26 };
30
32 {
33 static const char *identifier();
34 static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
35 static void validate(const smt_termt &lhs, const smt_termt &rhs);
36 };
39
41 {
42 static const char *identifier();
43 static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
44 static void validate(const smt_termt &lhs, const smt_termt &rhs);
45 };
47 unsigned_greater_than_or_equalt>
49
50 struct signed_less_thant final
51 {
52 static const char *identifier();
53 static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
54 static void validate(const smt_termt &lhs, const smt_termt &rhs);
55 };
58
60 {
61 static const char *identifier();
62 static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
63 static void validate(const smt_termt &lhs, const smt_termt &rhs);
64 };
70 {
71 static const char *identifier();
72 static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
73 static void validate(const smt_termt &lhs, const smt_termt &rhs);
74 };
77
79 {
80 static const char *identifier();
81 static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
82 static void validate(const smt_termt &lhs, const smt_termt &rhs);
83 };
87
88 struct addt final
89 {
90 static const char *identifier();
91 static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
92 static void validate(const smt_termt &lhs, const smt_termt &rhs);
93 };
95
96 struct subtractt final
97 {
98 static const char *identifier();
99 static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
100 static void validate(const smt_termt &lhs, const smt_termt &rhs);
101 };
103
104 struct multiplyt final
105 {
106 static const char *identifier();
107 static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
108 static void validate(const smt_termt &lhs, const smt_termt &rhs);
109 };
111
112 struct unsigned_dividet final
113 {
114 static const char *identifier();
115 static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
116 static void validate(const smt_termt &lhs, const smt_termt &rhs);
117 };
120
121 struct signed_dividet final
122 {
123 static const char *identifier();
124 static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
125 static void validate(const smt_termt &lhs, const smt_termt &rhs);
126 };
129
131 {
132 static const char *identifier();
133 static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
134 static void validate(const smt_termt &lhs, const smt_termt &rhs);
135 };
139 struct signed_remaindert final
140 {
141 static const char *identifier();
142 static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
143 static void validate(const smt_termt &lhs, const smt_termt &rhs);
144 };
147
148 struct negatet final
149 {
150 static const char *identifier();
151 static smt_sortt return_sort(const smt_termt &operand);
152 static void validate(const smt_termt &operand);
153 };
155};
156
157#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_BIT_VECTOR_THEORY_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
static const smt_function_application_termt::factoryt< unsigned_less_than_or_equalt > unsigned_less_than_or_equal
static const smt_function_application_termt::factoryt< signed_less_than_or_equalt > signed_less_than_or_equal
static const smt_function_application_termt::factoryt< addt > add
static const smt_function_application_termt::factoryt< signed_greater_than_or_equalt > signed_greater_than_or_equal
static const smt_function_application_termt::factoryt< unsigned_greater_thant > unsigned_greater_than
static const smt_function_application_termt::factoryt< unsigned_remaindert > unsigned_remainder
static const smt_function_application_termt::factoryt< unsigned_greater_than_or_equalt > unsigned_greater_than_or_equal
static const smt_function_application_termt::factoryt< multiplyt > multiply
static const smt_function_application_termt::factoryt< signed_less_thant > signed_less_than
static const smt_function_application_termt::factoryt< signed_greater_thant > signed_greater_than
static const smt_function_application_termt::factoryt< negatet > negate
static const smt_function_application_termt::factoryt< unsigned_dividet > unsigned_divide
static const smt_function_application_termt::factoryt< unsigned_less_thant > unsigned_less_than
static const smt_function_application_termt::factoryt< signed_dividet > signed_divide
static const smt_function_application_termt::factoryt< signed_remaindert > signed_remainder
static const smt_function_application_termt::factoryt< subtractt > subtract
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static void validate(const smt_termt &operand)
static smt_sortt return_sort(const smt_termt &operand)
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)