cprover
bv_utils.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: 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 <map>
14 #include <set>
15 
16 #include <util/mp_arith.h>
17 
18 #include <solvers/prop/prop.h>
19 
20 // Shares variables between var == const tests for registered variables.
21 // Gives ~15% memory savings on some programs using constant arrays
22 // but seems to give a run-time penalty.
23 // #define COMPACT_EQUAL_CONST
24 
25 
26 class bv_utilst
27 {
28 public:
29  explicit bv_utilst(propt &_prop):prop(_prop) { }
30 
31  enum class representationt { SIGNED, UNSIGNED };
32 
33  bvt build_constant(const mp_integer &i, std::size_t width);
34 
35  bvt incrementer(const bvt &op, literalt carry_in);
36  bvt inc(const bvt &op) { return incrementer(op, const_literal(true)); }
37  void incrementer(bvt &op, literalt carry_in, literalt &carry_out);
38 
39  bvt negate(const bvt &op);
40  bvt negate_no_overflow(const bvt &op);
41  bvt absolute_value(const bvt &op);
42 
43  // returns true iff unary minus will overflow
44  literalt overflow_negate(const bvt &op);
45 
46  // bit-wise negation
47  bvt inverted(const bvt &op);
48 
50  const literalt a,
51  const literalt b,
52  const literalt carry_in,
55 
56  bvt add_sub(const bvt &op0, const bvt &op1, bool subtract);
57  bvt add_sub(const bvt &op0, const bvt &op1, literalt subtract);
59  const bvt &op0,
60  const bvt &op1,
61  bool subtract,
62  representationt rep);
63 
64  bvt add(const bvt &op0, const bvt &op1) { return add_sub(op0, op1, false); }
65  bvt sub(const bvt &op0, const bvt &op1) { return add_sub(op0, op1, true); }
66 
67  literalt overflow_add(const bvt &op0, const bvt &op1, representationt rep);
68  literalt overflow_sub(const bvt &op0, const bvt &op1, representationt rep);
69  literalt carry_out(const bvt &op0, const bvt &op1, literalt carry_in);
70 
71  enum class shiftt
72  {
74  };
75 
76  bvt shift(const bvt &op, const shiftt shift, std::size_t distance);
77  bvt shift(const bvt &op, const shiftt shift, const bvt &distance);
78 
79  bvt unsigned_multiplier(const bvt &op0, const bvt &op1);
80  bvt signed_multiplier(const bvt &op0, const bvt &op1);
81  bvt multiplier(const bvt &op0, const bvt &op1, representationt rep);
83  const bvt &op0,
84  const bvt &op1,
85  representationt rep);
86 
87  bvt divider(const bvt &op0, const bvt &op1, representationt rep)
88  {
89  bvt res, rem;
90  divider(op0, op1, res, rem, rep);
91  return res;
92  }
93 
94  bvt remainder(const bvt &op0, const bvt &op1, representationt rep)
95  {
96  bvt res, rem;
97  divider(op0, op1, res, rem, rep);
98  return rem;
99  }
100 
101  void divider(
102  const bvt &op0,
103  const bvt &op1,
104  bvt &res,
105  bvt &rem,
106  representationt rep);
107 
108  void signed_divider(
109  const bvt &op0,
110  const bvt &op1,
111  bvt &res,
112  bvt &rem);
113 
114  void unsigned_divider(
115  const bvt &op0,
116  const bvt &op1,
117  bvt &res,
118  bvt &rem);
119 
120  #ifdef COMPACT_EQUAL_CONST
121  typedef std::set<bvt> equal_const_registeredt;
122  equal_const_registeredt equal_const_registered;
123  void equal_const_register(const bvt &var);
124 
125  typedef std::pair<bvt, bvt> var_constant_pairt;
126  typedef std::map<var_constant_pairt, literalt> equal_const_cachet;
127  equal_const_cachet equal_const_cache;
128 
129  literalt equal_const_rec(bvt &var, bvt &constant);
130  literalt equal_const(const bvt &var, const bvt &constant);
131  #endif
132 
133 
134  literalt equal(const bvt &op0, const bvt &op1);
135 
136  static inline literalt sign_bit(const bvt &op)
137  {
138  return op[op.size()-1];
139  }
140 
141  literalt is_zero(const bvt &op)
142  { return !prop.lor(op); }
143 
145  { return prop.lor(op); }
146 
148  {
149  bvt tmp=op;
150  tmp[tmp.size()-1]=!tmp[tmp.size()-1];
151  return is_zero(tmp);
152  }
153 
154  literalt is_one(const bvt &op);
155 
157  { return prop.land(op); }
158 
160  bool or_equal,
161  const bvt &bv0,
162  const bvt &bv1,
163  representationt rep);
164 
165  // id is one of ID_lt, le, gt, ge, equal, notequal
166  literalt rel(
167  const bvt &bv0,
168  irep_idt id,
169  const bvt &bv1,
170  representationt rep);
171 
172  literalt unsigned_less_than(const bvt &bv0, const bvt &bv1);
173  literalt signed_less_than(const bvt &bv0, const bvt &bv1);
174 
175  bool is_constant(const bvt &bv);
176 
177  bvt extension(const bvt &bv, std::size_t new_size, representationt rep);
178 
179  bvt sign_extension(const bvt &bv, std::size_t new_size)
180  {
181  return extension(bv, new_size, representationt::SIGNED);
182  }
183 
184  bvt zero_extension(const bvt &bv, std::size_t new_size)
185  {
186  return extension(bv, new_size, representationt::UNSIGNED);
187  }
188 
189  bvt zeros(std::size_t new_size) const
190  {
191  bvt result;
192  result.resize(new_size, const_literal(false));
193  return result;
194  }
195 
196  void set_equal(const bvt &a, const bvt &b);
197 
198  // if cond holds, a has to be equal to b
199  void cond_implies_equal(literalt cond, const bvt &a, const bvt &b);
200 
201  bvt cond_negate(const bvt &bv, const literalt cond);
202 
203  bvt select(literalt s, const bvt &a, const bvt &b);
204 
205  // computes a[last:first]
206  static bvt extract(const bvt &a, std::size_t first, std::size_t last);
207 
208  // extracts the n most significant bits
209  static bvt extract_msb(const bvt &a, std::size_t n);
210 
211  // extracts the n least significant bits
212  static bvt extract_lsb(const bvt &a, std::size_t n);
213 
214  // put a and b together, where a comes first (lower indices)
215  bvt concatenate(const bvt &a, const bvt &b) const;
216 
218  bvt verilog_bv_normal_bits(const bvt &);
219 
220 protected:
222 
223  void adder(
224  bvt &sum,
225  const bvt &op,
226  literalt carry_in,
228 
229  void adder_no_overflow(
230  bvt &sum,
231  const bvt &op,
232  bool subtract,
233  representationt rep);
234 
235  void adder_no_overflow(bvt &sum, const bvt &op);
236 
238  const bvt &op0, const bvt &op1);
239 
241  const bvt &op0, const bvt &op1);
242 
243  bvt cond_negate_no_overflow(const bvt &bv, const literalt cond);
244 
245  bvt wallace_tree(const std::vector<bvt> &pps);
246 };
247 
248 #endif // CPROVER_SOLVERS_FLATTENING_BV_UTILS_H
bv_utilst::shiftt::SHIFT_LEFT
@ SHIFT_LEFT
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bv_utilst::cond_negate_no_overflow
bvt cond_negate_no_overflow(const bvt &bv, const literalt cond)
Definition: bv_utils.cpp:781
mp_arith.h
bv_utilst::extract_lsb
static bvt extract_lsb(const bvt &a, std::size_t n)
Definition: bv_utils.cpp:70
bv_utilst::cond_implies_equal
void cond_implies_equal(literalt cond, const bvt &a, const bvt &b)
Definition: bv_utils.cpp:1321
bv_utilst::carry
literalt carry(literalt a, literalt b, literalt c)
Definition: bv_utils.cpp:231
bv_utilst::full_adder
literalt full_adder(const literalt a, const literalt b, const literalt carry_in, literalt &carry_out)
Definition: bv_utils.cpp:140
bv_utilst::inc
bvt inc(const bvt &op)
Definition: bv_utils.h:36
bv_utilst::is_not_zero
literalt is_not_zero(const bvt &op)
Definition: bv_utils.h:144
bv_utilst::carry_out
literalt carry_out(const bvt &op0, const bvt &op1, literalt carry_in)
Definition: bv_utils.cpp:313
bvt
std::vector< literalt > bvt
Definition: literal.h:201
bv_utilst::negate_no_overflow
bvt negate_no_overflow(const bvt &op)
Definition: bv_utils.cpp:541
bv_utilst::adder_no_overflow
void adder_no_overflow(bvt &sum, const bvt &op, bool subtract, representationt rep)
Definition: bv_utils.cpp:416
bv_utilst::signed_multiplier
bvt signed_multiplier(const bvt &op0, const bvt &op1)
Definition: bv_utils.cpp:744
bv_utilst::shiftt::SHIFT_ARIGHT
@ SHIFT_ARIGHT
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
bv_utilst::representationt::UNSIGNED
@ UNSIGNED
bv_utilst::set_equal
void set_equal(const bvt &a, const bvt &b)
Definition: bv_utils.cpp:35
bv_utilst::sign_extension
bvt sign_extension(const bvt &bv, std::size_t new_size)
Definition: bv_utils.h:179
bv_utilst::signed_divider
void signed_divider(const bvt &op0, const bvt &op1, bvt &res, bvt &rem)
Definition: bv_utils.cpp:840
propt::lor
virtual literalt lor(literalt a, literalt b)=0
bv_utilst::prop
propt & prop
Definition: bv_utils.h:221
bv_utilst::incrementer
bvt incrementer(const bvt &op, literalt carry_in)
Definition: bv_utils.cpp:573
bv_utilst::inverted
bvt inverted(const bvt &op)
Definition: bv_utils.cpp:581
bv_utilst::absolute_value
bvt absolute_value(const bvt &op)
Definition: bv_utils.cpp:775
bv_utilst::zeros
bvt zeros(std::size_t new_size) const
Definition: bv_utils.h:189
bv_utilst::unsigned_multiplier
bvt unsigned_multiplier(const bvt &op0, const bvt &op1)
Definition: bv_utils.cpp:635
propt::land
virtual literalt land(literalt a, literalt b)=0
bv_utilst::select
bvt select(literalt s, const bvt &a, const bvt &b)
If s is true, selects a otherwise selects b.
Definition: bv_utils.cpp:96
bv_utilst
Definition: bv_utils.h:27
bv_utilst::shift
bvt shift(const bvt &op, const shiftt shift, std::size_t distance)
Definition: bv_utils.cpp:481
bv_utilst::unsigned_less_than
literalt unsigned_less_than(const bvt &bv0, const bvt &bv1)
Definition: bv_utils.cpp:1271
bv_utilst::unsigned_divider
void unsigned_divider(const bvt &op0, const bvt &op1, bvt &res, bvt &rem)
Definition: bv_utils.cpp:893
bv_utilst::is_int_min
literalt is_int_min(const bvt &op)
Definition: bv_utils.h:147
bv_utilst::add
bvt add(const bvt &op0, const bvt &op1)
Definition: bv_utils.h:64
bv_utilst::representationt::SIGNED
@ SIGNED
bv_utilst::representationt
representationt
Definition: bv_utils.h:31
bv_utilst::cond_negate
bvt cond_negate(const bvt &bv, const literalt cond)
Definition: bv_utils.cpp:762
bv_utilst::overflow_sub
literalt overflow_sub(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.cpp:391
prop.h
const_literal
literalt const_literal(bool value)
Definition: literal.h:188
bv_utilst::overflow_add
literalt overflow_add(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.cpp:367
bv_utilst::signed_multiplier_no_overflow
bvt signed_multiplier_no_overflow(const bvt &op0, const bvt &op1)
Definition: bv_utils.cpp:788
bv_utilst::bv_utilst
bv_utilst(propt &_prop)
Definition: bv_utils.h:29
bv_utilst::unsigned_multiplier_no_overflow
bvt unsigned_multiplier_no_overflow(const bvt &op0, const bvt &op1)
Definition: bv_utils.cpp:705
bv_utilst::lt_or_le
literalt lt_or_le(bool or_equal, const bvt &bv0, const bvt &bv1, representationt rep)
To provide a bitwise model of < or <=.
Definition: bv_utils.cpp:1152
bv_utilst::add_sub
bvt add_sub(const bvt &op0, const bvt &op1, bool subtract)
Definition: bv_utils.cpp:339
bv_utilst::wallace_tree
bvt wallace_tree(const std::vector< bvt > &pps)
Definition: bv_utils.cpp:589
bv_utilst::remainder
bvt remainder(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.h:94
bv_utilst::multiplier_no_overflow
bvt multiplier_no_overflow(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.cpp:824
bv_utilst::build_constant
bvt build_constant(const mp_integer &i, std::size_t width)
Definition: bv_utils.cpp:15
bv_utilst::rel
literalt rel(const bvt &bv0, irep_idt id, const bvt &bv1, representationt rep)
Definition: bv_utils.cpp:1290
bv_utilst::shiftt
shiftt
Definition: bv_utils.h:72
propt
TO_BE_DOCUMENTED.
Definition: prop.h:25
bv_utilst::negate
bvt negate(const bvt &op)
Definition: bv_utils.cpp:533
bv_utilst::is_all_ones
literalt is_all_ones(const bvt &op)
Definition: bv_utils.h:156
bv_utilst::overflow_negate
literalt overflow_negate(const bvt &op)
Definition: bv_utils.cpp:547
bv_utilst::shiftt::ROTATE_RIGHT
@ ROTATE_RIGHT
bv_utilst::sign_bit
static literalt sign_bit(const bvt &op)
Definition: bv_utils.h:136
bv_utilst::concatenate
bvt concatenate(const bvt &a, const bvt &b) const
Definition: bv_utils.cpp:80
bv_utilst::extension
bvt extension(const bvt &bv, std::size_t new_size, representationt rep)
Definition: bv_utils.cpp:109
literalt
Definition: literal.h:26
bv_utilst::divider
bvt divider(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.h:87
bv_utilst::extract
static bvt extract(const bvt &a, std::size_t first, std::size_t last)
Definition: bv_utils.cpp:42
bv_utilst::signed_less_than
literalt signed_less_than(const bvt &bv0, const bvt &bv1)
Definition: bv_utils.cpp:1283
bv_utilst::shiftt::SHIFT_LRIGHT
@ SHIFT_LRIGHT
bv_utilst::multiplier
bvt multiplier(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.cpp:810
bv_utilst::extract_msb
static bvt extract_msb(const bvt &a, std::size_t n)
Definition: bv_utils.cpp:58
bv_utilst::verilog_bv_normal_bits
bvt verilog_bv_normal_bits(const bvt &)
Definition: bv_utils.cpp:1359
bv_utilst::adder
void adder(bvt &sum, const bvt &op, literalt carry_in, literalt &carry_out)
Definition: bv_utils.cpp:297
bv_utilst::add_sub_no_overflow
bvt add_sub_no_overflow(const bvt &op0, const bvt &op1, bool subtract, representationt rep)
Definition: bv_utils.cpp:328
bv_utilst::equal
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
Definition: bv_utils.cpp:1113
bv_utilst::is_zero
literalt is_zero(const bvt &op)
Definition: bv_utils.h:141
bv_utilst::shiftt::ROTATE_LEFT
@ ROTATE_LEFT
bv_utilst::verilog_bv_has_x_or_z
literalt verilog_bv_has_x_or_z(const bvt &)
Definition: bv_utils.cpp:1344
bv_utilst::is_one
literalt is_one(const bvt &op)
Definition: bv_utils.cpp:26
bv_utilst::zero_extension
bvt zero_extension(const bvt &bv, std::size_t new_size)
Definition: bv_utils.h:184
bv_utilst::sub
bvt sub(const bvt &op0, const bvt &op1)
Definition: bv_utils.h:65
bv_utilst::is_constant
bool is_constant(const bvt &bv)
Definition: bv_utils.cpp:1312