cprover
Loading...
Searching...
No Matches
bv_utils.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9
10#ifndef CPROVER_SOLVERS_FLATTENING_BV_UTILS_H
11#define CPROVER_SOLVERS_FLATTENING_BV_UTILS_H
12
13#include <util/mp_arith.h>
14#include <util/nodiscard.h>
15
16#include <solvers/prop/prop.h>
17
18// Shares variables between var == const tests for registered variables.
19// Gives ~15% memory savings on some programs using constant arrays
20// but seems to give a run-time penalty.
21// #define COMPACT_EQUAL_CONST
22
23
25{
26public:
27 explicit bv_utilst(propt &_prop):prop(_prop) { }
28
30
31 static bvt build_constant(const mp_integer &i, std::size_t width);
32
33 bvt incrementer(const bvt &op, literalt carry_in);
34 bvt inc(const bvt &op) { return incrementer(op, const_literal(true)); }
35 void incrementer(bvt &op, literalt carry_in, literalt &carry_out);
36
37 bvt negate(const bvt &op);
38 bvt negate_no_overflow(const bvt &op);
39 bvt absolute_value(const bvt &op);
40
41 // returns true iff unary minus will overflow
42 literalt overflow_negate(const bvt &op);
43
44 // bit-wise negation
45 static bvt inverted(const bvt &op);
46
48 const literalt a,
49 const literalt b,
50 const literalt carry_in,
53
54 bvt add_sub(const bvt &op0, const bvt &op1, bool subtract);
55 bvt add_sub(const bvt &op0, const bvt &op1, literalt subtract);
57 const bvt &op0,
58 const bvt &op1,
59 bool subtract,
60 representationt rep);
62 const bvt &op0,
63 const bvt &op1,
64 bool subtract,
65 representationt rep);
66
67 bvt add(const bvt &op0, const bvt &op1) { return add_sub(op0, op1, false); }
68 bvt sub(const bvt &op0, const bvt &op1) { return add_sub(op0, op1, true); }
69
70 literalt overflow_add(const bvt &op0, const bvt &op1, representationt rep);
71 literalt overflow_sub(const bvt &op0, const bvt &op1, representationt rep);
72 literalt carry_out(const bvt &op0, const bvt &op1, literalt carry_in);
73
78
79 static bvt shift(const bvt &op, const shiftt shift, std::size_t distance);
80 bvt shift(const bvt &op, const shiftt shift, const bvt &distance);
81
82 bvt unsigned_multiplier(const bvt &op0, const bvt &op1);
83 bvt signed_multiplier(const bvt &op0, const bvt &op1);
84 bvt multiplier(const bvt &op0, const bvt &op1, representationt rep);
86 const bvt &op0,
87 const bvt &op1,
88 representationt rep);
89
90 bvt divider(const bvt &op0, const bvt &op1, representationt rep)
91 {
92 bvt res, rem;
93 divider(op0, op1, res, rem, rep);
94 return res;
95 }
96
97 bvt remainder(const bvt &op0, const bvt &op1, representationt rep)
98 {
99 bvt res, rem;
100 divider(op0, op1, res, rem, rep);
101 return rem;
102 }
103
104 void divider(
105 const bvt &op0,
106 const bvt &op1,
107 bvt &res,
108 bvt &rem,
109 representationt rep);
110
111 void signed_divider(
112 const bvt &op0,
113 const bvt &op1,
114 bvt &res,
115 bvt &rem);
116
117 void unsigned_divider(
118 const bvt &op0,
119 const bvt &op1,
120 bvt &res,
121 bvt &rem);
122
123 #ifdef COMPACT_EQUAL_CONST
124 typedef std::set<bvt> equal_const_registeredt;
125 equal_const_registeredt equal_const_registered;
126 void equal_const_register(const bvt &var);
127
128 typedef std::pair<bvt, bvt> var_constant_pairt;
129 typedef std::map<var_constant_pairt, literalt> equal_const_cachet;
130 equal_const_cachet equal_const_cache;
131
132 literalt equal_const_rec(bvt &var, bvt &constant);
133 literalt equal_const(const bvt &var, const bvt &constant);
134 #endif
135
136
137 literalt equal(const bvt &op0, const bvt &op1);
138
139 static inline literalt sign_bit(const bvt &op)
140 {
141 return op[op.size()-1];
142 }
143
145 { return !prop.lor(op); }
146
148 { return prop.lor(op); }
149
151 {
152 bvt tmp=op;
153 tmp[tmp.size()-1]=!tmp[tmp.size()-1];
154 return is_zero(tmp);
155 }
156
157 literalt is_one(const bvt &op);
158
160 { return prop.land(op); }
161
163 bool or_equal,
164 const bvt &bv0,
165 const bvt &bv1,
166 representationt rep);
167
168 // id is one of ID_lt, le, gt, ge, equal, notequal
170 const bvt &bv0,
171 irep_idt id,
172 const bvt &bv1,
173 representationt rep);
174
175 literalt unsigned_less_than(const bvt &bv0, const bvt &bv1);
176 literalt signed_less_than(const bvt &bv0, const bvt &bv1);
177
178 static bool is_constant(const bvt &bv);
179
180 static bvt
181 extension(const bvt &bv, std::size_t new_size, representationt rep);
182
183 static bvt sign_extension(const bvt &bv, std::size_t new_size)
184 {
185 return extension(bv, new_size, representationt::SIGNED);
186 }
187
188 static bvt zero_extension(const bvt &bv, std::size_t new_size)
189 {
190 return extension(bv, new_size, representationt::UNSIGNED);
191 }
192
193 static bvt zeros(std::size_t new_size)
194 {
195 return bvt(new_size, const_literal(false));
196 }
197
198 void set_equal(const bvt &a, const bvt &b);
199
200 // if cond holds, a has to be equal to b
201 void cond_implies_equal(literalt cond, const bvt &a, const bvt &b);
202
203 bvt cond_negate(const bvt &bv, const literalt cond);
204
205 bvt select(literalt s, const bvt &a, const bvt &b);
206
207 // computes a[last:first]
208 static bvt extract(const bvt &a, std::size_t first, std::size_t last);
209
210 // extracts the n most significant bits
211 static bvt extract_msb(const bvt &a, std::size_t n);
212
213 // extracts the n least significant bits
214 static bvt extract_lsb(const bvt &a, std::size_t n);
215
216 // put a and b together, where a comes first (lower indices)
217 static bvt concatenate(const bvt &a, const bvt &b);
218
220 static bvt verilog_bv_normal_bits(const bvt &);
221
222protected:
224
227 NODISCARD std::pair<bvt, literalt>
228 adder(const bvt &op0, const bvt &op1, literalt carry_in);
229
231 const bvt &op0,
232 const bvt &op1,
233 bool subtract,
234 representationt rep);
235
236 NODISCARD bvt adder_no_overflow(const bvt &op0, const bvt &op1);
237
239 const bvt &op0, const bvt &op1);
240
242 const bvt &op0, const bvt &op1);
243
244 bvt cond_negate_no_overflow(const bvt &bv, const literalt cond);
245
246 bvt wallace_tree(const std::vector<bvt> &pps);
247 bvt dadda_tree(const std::vector<bvt> &pps);
248};
249
250#endif // CPROVER_SOLVERS_FLATTENING_BV_UTILS_H
static bvt inverted(const bvt &op)
Definition bv_utils.cpp:636
literalt signed_less_than(const bvt &bv0, const bvt &bv1)
static bool is_constant(const bvt &bv)
NODISCARD std::pair< bvt, literalt > adder(const bvt &op0, const bvt &op1, literalt carry_in)
Return the sum and carry-out when adding op0 and op1 under initial carry carry_in.
Definition bv_utils.cpp:296
literalt is_all_ones(const bvt &op)
Definition bv_utils.h:159
bvt wallace_tree(const std::vector< bvt > &pps)
Definition bv_utils.cpp:644
bv_utilst(propt &_prop)
Definition bv_utils.h:27
literalt is_not_zero(const bvt &op)
Definition bv_utils.h:147
static bvt verilog_bv_normal_bits(const bvt &)
literalt is_int_min(const bvt &op)
Definition bv_utils.h:150
static bvt extract_msb(const bvt &a, std::size_t n)
Definition bv_utils.cpp:56
void set_equal(const bvt &a, const bvt &b)
Definition bv_utils.cpp:33
static literalt sign_bit(const bvt &op)
Definition bv_utils.h:139
bvt multiplier_no_overflow(const bvt &op0, const bvt &op1, representationt rep)
bvt add_sub_no_overflow(const bvt &op0, const bvt &op1, bool subtract, representationt rep)
Definition bv_utils.cpp:327
bvt add(const bvt &op0, const bvt &op1)
Definition bv_utils.h:67
static bvt zero_extension(const bvt &bv, std::size_t new_size)
Definition bv_utils.h:188
bvt absolute_value(const bvt &op)
bvt select(literalt s, const bvt &a, const bvt &b)
If s is true, selects a otherwise selects b.
Definition bv_utils.cpp:94
static bvt build_constant(const mp_integer &i, std::size_t width)
Definition bv_utils.cpp:13
void signed_divider(const bvt &op0, const bvt &op1, bvt &res, bvt &rem)
literalt is_zero(const bvt &op)
Definition bv_utils.h:144
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
bvt signed_multiplier(const bvt &op0, const bvt &op1)
literalt overflow_add(const bvt &op0, const bvt &op1, representationt rep)
Definition bv_utils.cpp:426
literalt is_one(const bvt &op)
Definition bv_utils.cpp:24
bvt cond_negate_no_overflow(const bvt &bv, const literalt cond)
literalt overflow_sub(const bvt &op0, const bvt &op1, representationt rep)
Definition bv_utils.cpp:450
void cond_implies_equal(literalt cond, const bvt &a, const bvt &b)
literalt unsigned_less_than(const bvt &bv0, const bvt &bv1)
bvt signed_multiplier_no_overflow(const bvt &op0, const bvt &op1)
bvt remainder(const bvt &op0, const bvt &op1, representationt rep)
Definition bv_utils.h:97
bvt incrementer(const bvt &op, literalt carry_in)
Definition bv_utils.cpp:628
bvt add_sub(const bvt &op0, const bvt &op1, bool subtract)
Definition bv_utils.cpp:336
static bvt shift(const bvt &op, const shiftt shift, std::size_t distance)
Definition bv_utils.cpp:536
literalt lt_or_le(bool or_equal, const bvt &bv0, const bvt &bv1, representationt rep)
literalt overflow_negate(const bvt &op)
Definition bv_utils.cpp:602
static bvt concatenate(const bvt &a, const bvt &b)
Definition bv_utils.cpp:78
representationt
Definition bv_utils.h:29
literalt full_adder(const literalt a, const literalt b, const literalt carry_in, literalt &carry_out)
Definition bv_utils.cpp:138
bvt negate_no_overflow(const bvt &op)
Definition bv_utils.cpp:596
bvt sub(const bvt &op0, const bvt &op1)
Definition bv_utils.h:68
static bvt extract(const bvt &a, std::size_t first, std::size_t last)
Definition bv_utils.cpp:40
bvt inc(const bvt &op)
Definition bv_utils.h:34
bvt unsigned_multiplier(const bvt &op0, const bvt &op1)
Definition bv_utils.cpp:918
bvt divider(const bvt &op0, const bvt &op1, representationt rep)
Definition bv_utils.h:90
void unsigned_divider(const bvt &op0, const bvt &op1, bvt &res, bvt &rem)
bvt multiplier(const bvt &op0, const bvt &op1, representationt rep)
bvt cond_negate(const bvt &bv, const literalt cond)
bvt dadda_tree(const std::vector< bvt > &pps)
Definition bv_utils.cpp:691
literalt carry_out(const bvt &op0, const bvt &op1, literalt carry_in)
Definition bv_utils.cpp:312
bvt negate(const bvt &op)
Definition bv_utils.cpp:588
static bvt extension(const bvt &bv, std::size_t new_size, representationt rep)
Definition bv_utils.cpp:107
static bvt extract_lsb(const bvt &a, std::size_t n)
Definition bv_utils.cpp:68
literalt verilog_bv_has_x_or_z(const bvt &)
literalt carry(literalt a, literalt b, literalt c)
Definition bv_utils.cpp:229
bvt unsigned_multiplier_no_overflow(const bvt &op0, const bvt &op1)
Definition bv_utils.cpp:963
static bvt zeros(std::size_t new_size)
Definition bv_utils.h:193
literalt rel(const bvt &bv0, irep_idt id, const bvt &bv1, representationt rep)
propt & prop
Definition bv_utils.h:223
NODISCARD bvt adder_no_overflow(const bvt &op0, const bvt &op1, bool subtract, representationt rep)
Definition bv_utils.cpp:475
static bvt sign_extension(const bvt &bv, std::size_t new_size)
Definition bv_utils.h:183
bvt saturating_add_sub(const bvt &op0, const bvt &op1, bool subtract, representationt rep)
Definition bv_utils.cpp:357
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
TO_BE_DOCUMENTED.
Definition prop.h:25
virtual literalt land(literalt a, literalt b)=0
virtual literalt lor(literalt a, literalt b)=0
std::vector< literalt > bvt
Definition literal.h:201
literalt const_literal(bool value)
Definition literal.h:188
#define NODISCARD
Definition nodiscard.h:22
BigInt mp_integer
Definition smt_terms.h:18