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  static 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  static 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  static 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  static bool is_constant(const bvt &bv);
176 
177  static bvt
178  extension(const bvt &bv, std::size_t new_size, representationt rep);
179 
180  bvt sign_extension(const bvt &bv, std::size_t new_size)
181  {
182  return extension(bv, new_size, representationt::SIGNED);
183  }
184 
185  bvt zero_extension(const bvt &bv, std::size_t new_size)
186  {
187  return extension(bv, new_size, representationt::UNSIGNED);
188  }
189 
190  bvt zeros(std::size_t new_size) const
191  {
192  bvt result;
193  result.resize(new_size, const_literal(false));
194  return result;
195  }
196 
197  void set_equal(const bvt &a, const bvt &b);
198 
199  // if cond holds, a has to be equal to b
200  void cond_implies_equal(literalt cond, const bvt &a, const bvt &b);
201 
202  bvt cond_negate(const bvt &bv, const literalt cond);
203 
204  bvt select(literalt s, const bvt &a, const bvt &b);
205 
206  // computes a[last:first]
207  static bvt extract(const bvt &a, std::size_t first, std::size_t last);
208 
209  // extracts the n most significant bits
210  static bvt extract_msb(const bvt &a, std::size_t n);
211 
212  // extracts the n least significant bits
213  static bvt extract_lsb(const bvt &a, std::size_t n);
214 
215  // put a and b together, where a comes first (lower indices)
216  static bvt concatenate(const bvt &a, const bvt &b);
217 
219  static bvt verilog_bv_normal_bits(const bvt &);
220 
221 protected:
223 
224  void adder(
225  bvt &sum,
226  const bvt &op,
227  literalt carry_in,
229 
230  void adder_no_overflow(
231  bvt &sum,
232  const bvt &op,
233  bool subtract,
234  representationt rep);
235 
236  void adder_no_overflow(bvt &sum, const bvt &op);
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 };
248 
249 #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:779
mp_arith.h
bv_utilst::extract_lsb
static bvt extract_lsb(const bvt &a, std::size_t n)
Definition: bv_utils.cpp:68
bv_utilst::cond_implies_equal
void cond_implies_equal(literalt cond, const bvt &a, const bvt &b)
Definition: bv_utils.cpp:1322
bv_utilst::carry
literalt carry(literalt a, literalt b, literalt c)
Definition: bv_utils.cpp:229
bv_utilst::full_adder
literalt full_adder(const literalt a, const literalt b, const literalt carry_in, literalt &carry_out)
Definition: bv_utils.cpp:138
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:311
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:539
bv_utilst::adder_no_overflow
void adder_no_overflow(bvt &sum, const bvt &op, bool subtract, representationt rep)
Definition: bv_utils.cpp:414
bv_utilst::signed_multiplier
bvt signed_multiplier(const bvt &op0, const bvt &op1)
Definition: bv_utils.cpp:742
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:33
bv_utilst::sign_extension
bvt sign_extension(const bvt &bv, std::size_t new_size)
Definition: bv_utils.h:180
bv_utilst::signed_divider
void signed_divider(const bvt &op0, const bvt &op1, bvt &res, bvt &rem)
Definition: bv_utils.cpp:838
propt::lor
virtual literalt lor(literalt a, literalt b)=0
bv_utilst::prop
propt & prop
Definition: bv_utils.h:222
bv_utilst::incrementer
bvt incrementer(const bvt &op, literalt carry_in)
Definition: bv_utils.cpp:571
bv_utilst::inverted
static bvt inverted(const bvt &op)
Definition: bv_utils.cpp:579
bv_utilst::absolute_value
bvt absolute_value(const bvt &op)
Definition: bv_utils.cpp:773
bv_utilst::zeros
bvt zeros(std::size_t new_size) const
Definition: bv_utils.h:190
bv_utilst::unsigned_multiplier
bvt unsigned_multiplier(const bvt &op0, const bvt &op1)
Definition: bv_utils.cpp:633
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:94
bv_utilst
Definition: bv_utils.h:27
bv_utilst::shift
static bvt shift(const bvt &op, const shiftt shift, std::size_t distance)
Definition: bv_utils.cpp:479
bv_utilst::unsigned_less_than
literalt unsigned_less_than(const bvt &bv0, const bvt &bv1)
Definition: bv_utils.cpp:1270
bv_utilst::unsigned_divider
void unsigned_divider(const bvt &op0, const bvt &op1, bvt &res, bvt &rem)
Definition: bv_utils.cpp:891
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:760
bv_utilst::overflow_sub
literalt overflow_sub(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.cpp:389
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:365
bv_utilst::signed_multiplier_no_overflow
bvt signed_multiplier_no_overflow(const bvt &op0, const bvt &op1)
Definition: bv_utils.cpp:786
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:703
bv_utilst::concatenate
static bvt concatenate(const bvt &a, const bvt &b)
Definition: bv_utils.cpp:78
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:1150
bv_utilst::add_sub
bvt add_sub(const bvt &op0, const bvt &op1, bool subtract)
Definition: bv_utils.cpp:337
bv_utilst::wallace_tree
bvt wallace_tree(const std::vector< bvt > &pps)
Definition: bv_utils.cpp:587
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:822
bv_utilst::build_constant
static bvt build_constant(const mp_integer &i, std::size_t width)
Definition: bv_utils.cpp:13
bv_utilst::rel
literalt rel(const bvt &bv0, irep_idt id, const bvt &bv1, representationt rep)
Definition: bv_utils.cpp:1289
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:531
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:545
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::extension
static bvt extension(const bvt &bv, std::size_t new_size, representationt rep)
Definition: bv_utils.cpp:107
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:40
bv_utilst::signed_less_than
literalt signed_less_than(const bvt &bv0, const bvt &bv1)
Definition: bv_utils.cpp:1282
bv_utilst::shiftt::SHIFT_LRIGHT
@ SHIFT_LRIGHT
bv_utilst::multiplier
bvt multiplier(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.cpp:808
bv_utilst::extract_msb
static bvt extract_msb(const bvt &a, std::size_t n)
Definition: bv_utils.cpp:56
bv_utilst::verilog_bv_normal_bits
static bvt verilog_bv_normal_bits(const bvt &)
Definition: bv_utils.cpp:1360
bv_utilst::adder
void adder(bvt &sum, const bvt &op, literalt carry_in, literalt &carry_out)
Definition: bv_utils.cpp:295
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:326
bv_utilst::equal
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
Definition: bv_utils.cpp:1111
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:1345
bv_utilst::is_one
literalt is_one(const bvt &op)
Definition: bv_utils.cpp:24
bv_utilst::zero_extension
bvt zero_extension(const bvt &bv, std::size_t new_size)
Definition: bv_utils.h:185
bv_utilst::sub
bvt sub(const bvt &op0, const bvt &op1)
Definition: bv_utils.h:65
bv_utilst::is_constant
static bool is_constant(const bvt &bv)
Definition: bv_utils.cpp:1311