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
15#include <solvers/prop/prop.h>
16
17// Shares variables between var == const tests for registered variables.
18// Gives ~15% memory savings on some programs using constant arrays
19// but seems to give a run-time penalty.
20// #define COMPACT_EQUAL_CONST
21
22
24{
25public:
26 explicit bv_utilst(propt &_prop):prop(_prop) { }
27
29
30 static bvt build_constant(const mp_integer &i, std::size_t width);
31
32 bvt incrementer(const bvt &op, literalt carry_in);
33 bvt inc(const bvt &op) { return incrementer(op, const_literal(true)); }
34 void incrementer(bvt &op, literalt carry_in, literalt &carry_out);
35
36 bvt negate(const bvt &op);
37 bvt negate_no_overflow(const bvt &op);
38 bvt absolute_value(const bvt &op);
39
40 // returns true iff unary minus will overflow
41 literalt overflow_negate(const bvt &op);
42
43 // bit-wise negation
44 static bvt inverted(const bvt &op);
45
47 const literalt a,
48 const literalt b,
49 const literalt carry_in,
52
53 bvt add_sub(const bvt &op0, const bvt &op1, bool subtract);
54 bvt add_sub(const bvt &op0, const bvt &op1, literalt subtract);
56 const bvt &op0,
57 const bvt &op1,
58 bool subtract,
59 representationt rep);
60
61 bvt add(const bvt &op0, const bvt &op1) { return add_sub(op0, op1, false); }
62 bvt sub(const bvt &op0, const bvt &op1) { return add_sub(op0, op1, true); }
63
64 literalt overflow_add(const bvt &op0, const bvt &op1, representationt rep);
65 literalt overflow_sub(const bvt &op0, const bvt &op1, representationt rep);
66 literalt carry_out(const bvt &op0, const bvt &op1, literalt carry_in);
67
68 enum class shiftt
69 {
71 };
72
73 static bvt shift(const bvt &op, const shiftt shift, std::size_t distance);
74 bvt shift(const bvt &op, const shiftt shift, const bvt &distance);
75
76 bvt unsigned_multiplier(const bvt &op0, const bvt &op1);
77 bvt signed_multiplier(const bvt &op0, const bvt &op1);
78 bvt multiplier(const bvt &op0, const bvt &op1, representationt rep);
80 const bvt &op0,
81 const bvt &op1,
82 representationt rep);
83
84 bvt divider(const bvt &op0, const bvt &op1, representationt rep)
85 {
86 bvt res, rem;
87 divider(op0, op1, res, rem, rep);
88 return res;
89 }
90
91 bvt remainder(const bvt &op0, const bvt &op1, representationt rep)
92 {
93 bvt res, rem;
94 divider(op0, op1, res, rem, rep);
95 return rem;
96 }
97
98 void divider(
99 const bvt &op0,
100 const bvt &op1,
101 bvt &res,
102 bvt &rem,
103 representationt rep);
104
105 void signed_divider(
106 const bvt &op0,
107 const bvt &op1,
108 bvt &res,
109 bvt &rem);
110
111 void unsigned_divider(
112 const bvt &op0,
113 const bvt &op1,
114 bvt &res,
115 bvt &rem);
116
117 #ifdef COMPACT_EQUAL_CONST
118 typedef std::set<bvt> equal_const_registeredt;
119 equal_const_registeredt equal_const_registered;
120 void equal_const_register(const bvt &var);
121
122 typedef std::pair<bvt, bvt> var_constant_pairt;
123 typedef std::map<var_constant_pairt, literalt> equal_const_cachet;
124 equal_const_cachet equal_const_cache;
125
126 literalt equal_const_rec(bvt &var, bvt &constant);
127 literalt equal_const(const bvt &var, const bvt &constant);
128 #endif
129
130
131 literalt equal(const bvt &op0, const bvt &op1);
132
133 static inline literalt sign_bit(const bvt &op)
134 {
135 return op[op.size()-1];
136 }
137
139 { return !prop.lor(op); }
140
142 { return prop.lor(op); }
143
145 {
146 bvt tmp=op;
147 tmp[tmp.size()-1]=!tmp[tmp.size()-1];
148 return is_zero(tmp);
149 }
150
151 literalt is_one(const bvt &op);
152
154 { return prop.land(op); }
155
157 bool or_equal,
158 const bvt &bv0,
159 const bvt &bv1,
160 representationt rep);
161
162 // id is one of ID_lt, le, gt, ge, equal, notequal
164 const bvt &bv0,
165 irep_idt id,
166 const bvt &bv1,
167 representationt rep);
168
169 literalt unsigned_less_than(const bvt &bv0, const bvt &bv1);
170 literalt signed_less_than(const bvt &bv0, const bvt &bv1);
171
172 static bool is_constant(const bvt &bv);
173
174 static bvt
175 extension(const bvt &bv, std::size_t new_size, representationt rep);
176
177 bvt sign_extension(const bvt &bv, std::size_t new_size)
178 {
179 return extension(bv, new_size, representationt::SIGNED);
180 }
181
182 bvt zero_extension(const bvt &bv, std::size_t new_size)
183 {
184 return extension(bv, new_size, representationt::UNSIGNED);
185 }
186
187 bvt zeros(std::size_t new_size) const
188 {
189 bvt result;
190 result.resize(new_size, const_literal(false));
191 return result;
192 }
193
194 void set_equal(const bvt &a, const bvt &b);
195
196 // if cond holds, a has to be equal to b
197 void cond_implies_equal(literalt cond, const bvt &a, const bvt &b);
198
199 bvt cond_negate(const bvt &bv, const literalt cond);
200
201 bvt select(literalt s, const bvt &a, const bvt &b);
202
203 // computes a[last:first]
204 static bvt extract(const bvt &a, std::size_t first, std::size_t last);
205
206 // extracts the n most significant bits
207 static bvt extract_msb(const bvt &a, std::size_t n);
208
209 // extracts the n least significant bits
210 static bvt extract_lsb(const bvt &a, std::size_t n);
211
212 // put a and b together, where a comes first (lower indices)
213 static bvt concatenate(const bvt &a, const bvt &b);
214
216 static bvt verilog_bv_normal_bits(const bvt &);
217
218protected:
220
221 void adder(
222 bvt &sum,
223 const bvt &op,
224 literalt carry_in,
226
228 bvt &sum,
229 const bvt &op,
230 bool subtract,
231 representationt rep);
232
233 void adder_no_overflow(bvt &sum, const bvt &op);
234
236 const bvt &op0, const bvt &op1);
237
239 const bvt &op0, const bvt &op1);
240
241 bvt cond_negate_no_overflow(const bvt &bv, const literalt cond);
242
243 bvt wallace_tree(const std::vector<bvt> &pps);
244};
245
246#endif // CPROVER_SOLVERS_FLATTENING_BV_UTILS_H
static bvt inverted(const bvt &op)
Definition bv_utils.cpp:577
literalt signed_less_than(const bvt &bv0, const bvt &bv1)
void adder_no_overflow(bvt &sum, const bvt &op, bool subtract, representationt rep)
Definition bv_utils.cpp:412
static bool is_constant(const bvt &bv)
literalt is_all_ones(const bvt &op)
Definition bv_utils.h:153
bvt wallace_tree(const std::vector< bvt > &pps)
Definition bv_utils.cpp:585
bv_utilst(propt &_prop)
Definition bv_utils.h:26
literalt is_not_zero(const bvt &op)
Definition bv_utils.h:141
static bvt verilog_bv_normal_bits(const bvt &)
literalt is_int_min(const bvt &op)
Definition bv_utils.h:144
static bvt extract_msb(const bvt &a, std::size_t n)
Definition bv_utils.cpp:54
void set_equal(const bvt &a, const bvt &b)
Definition bv_utils.cpp:31
static literalt sign_bit(const bvt &op)
Definition bv_utils.h:133
bvt multiplier_no_overflow(const bvt &op0, const bvt &op1, representationt rep)
Definition bv_utils.cpp:820
bvt add_sub_no_overflow(const bvt &op0, const bvt &op1, bool subtract, representationt rep)
Definition bv_utils.cpp:324
bvt add(const bvt &op0, const bvt &op1)
Definition bv_utils.h:61
bvt zero_extension(const bvt &bv, std::size_t new_size)
Definition bv_utils.h:182
void adder(bvt &sum, const bvt &op, literalt carry_in, literalt &carry_out)
Definition bv_utils.cpp:293
bvt absolute_value(const bvt &op)
Definition bv_utils.cpp:771
bvt select(literalt s, const bvt &a, const bvt &b)
If s is true, selects a otherwise selects b.
Definition bv_utils.cpp:92
static bvt build_constant(const mp_integer &i, std::size_t width)
Definition bv_utils.cpp:11
void signed_divider(const bvt &op0, const bvt &op1, bvt &res, bvt &rem)
Definition bv_utils.cpp:836
literalt is_zero(const bvt &op)
Definition bv_utils.h:138
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)
Definition bv_utils.cpp:740
literalt overflow_add(const bvt &op0, const bvt &op1, representationt rep)
Definition bv_utils.cpp:363
literalt is_one(const bvt &op)
Definition bv_utils.cpp:22
bvt cond_negate_no_overflow(const bvt &bv, const literalt cond)
Definition bv_utils.cpp:777
literalt overflow_sub(const bvt &op0, const bvt &op1, representationt rep)
Definition bv_utils.cpp:387
void cond_implies_equal(literalt cond, const bvt &a, const bvt &b)
bvt sign_extension(const bvt &bv, std::size_t new_size)
Definition bv_utils.h:177
literalt unsigned_less_than(const bvt &bv0, const bvt &bv1)
bvt signed_multiplier_no_overflow(const bvt &op0, const bvt &op1)
Definition bv_utils.cpp:784
bvt remainder(const bvt &op0, const bvt &op1, representationt rep)
Definition bv_utils.h:91
bvt incrementer(const bvt &op, literalt carry_in)
Definition bv_utils.cpp:569
bvt add_sub(const bvt &op0, const bvt &op1, bool subtract)
Definition bv_utils.cpp:335
static bvt shift(const bvt &op, const shiftt shift, std::size_t distance)
Definition bv_utils.cpp:477
literalt lt_or_le(bool or_equal, const bvt &bv0, const bvt &bv1, representationt rep)
To provide a bitwise model of < or <=.
literalt overflow_negate(const bvt &op)
Definition bv_utils.cpp:543
static bvt concatenate(const bvt &a, const bvt &b)
Definition bv_utils.cpp:76
representationt
Definition bv_utils.h:28
literalt full_adder(const literalt a, const literalt b, const literalt carry_in, literalt &carry_out)
Definition bv_utils.cpp:136
bvt negate_no_overflow(const bvt &op)
Definition bv_utils.cpp:537
bvt sub(const bvt &op0, const bvt &op1)
Definition bv_utils.h:62
static bvt extract(const bvt &a, std::size_t first, std::size_t last)
Definition bv_utils.cpp:38
bvt inc(const bvt &op)
Definition bv_utils.h:33
bvt unsigned_multiplier(const bvt &op0, const bvt &op1)
Definition bv_utils.cpp:631
bvt divider(const bvt &op0, const bvt &op1, representationt rep)
Definition bv_utils.h:84
void unsigned_divider(const bvt &op0, const bvt &op1, bvt &res, bvt &rem)
Definition bv_utils.cpp:889
bvt multiplier(const bvt &op0, const bvt &op1, representationt rep)
Definition bv_utils.cpp:806
bvt cond_negate(const bvt &bv, const literalt cond)
Definition bv_utils.cpp:758
literalt carry_out(const bvt &op0, const bvt &op1, literalt carry_in)
Definition bv_utils.cpp:309
bvt negate(const bvt &op)
Definition bv_utils.cpp:529
static bvt extension(const bvt &bv, std::size_t new_size, representationt rep)
Definition bv_utils.cpp:105
static bvt extract_lsb(const bvt &a, std::size_t n)
Definition bv_utils.cpp:66
literalt verilog_bv_has_x_or_z(const bvt &)
literalt carry(literalt a, literalt b, literalt c)
Definition bv_utils.cpp:227
bvt unsigned_multiplier_no_overflow(const bvt &op0, const bvt &op1)
Definition bv_utils.cpp:701
literalt rel(const bvt &bv0, irep_idt id, const bvt &bv1, representationt rep)
propt & prop
Definition bv_utils.h:219
bvt zeros(std::size_t new_size) const
Definition bv_utils.h:187
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
TO_BE_DOCUMENTED.
Definition prop.h:24
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
BigInt mp_integer
Definition smt_terms.h:12