cprover
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 {
10 public:
11  // Relational operator class declarations
12  struct unsigned_less_thant final
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  };
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  };
68 
69  struct signed_greater_thant final
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 
130  struct unsigned_remaindert final
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  };
138 
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
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)