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
bvt wallace_tree(const std::vector< bvt > &pps)
Definition: bv_utils.cpp:588
propt & prop
Definition: bv_utils.h:221
bvt inverted(const bvt &op)
Definition: bv_utils.cpp:580
bvt extension(const bvt &bv, std::size_t new_size, representationt rep)
Definition: bv_utils.cpp:109
bvt remainder(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.h:94
bvt multiplier_no_overflow(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.cpp:823
BigInt mp_integer
Definition: mp_arith.h:22
static bvt extract(const bvt &a, std::size_t first, std::size_t last)
Definition: bv_utils.cpp:42
static literalt sign_bit(const bvt &op)
Definition: bv_utils.h:136
literalt is_int_min(const bvt &op)
Definition: bv_utils.h:147
bvt cond_negate(const bvt &bv, const literalt cond)
Definition: bv_utils.cpp:760
bvt add_sub_no_overflow(const bvt &op0, const bvt &op1, bool subtract, representationt rep)
Definition: bv_utils.cpp:328
bvt divider(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.h:87
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
Definition: bv_utils.cpp:1108
virtual literalt lor(literalt a, literalt b)=0
representationt
Definition: bv_utils.h:31
bvt sub(const bvt &op0, const bvt &op1)
Definition: bv_utils.h:65
void adder(bvt &sum, const bvt &op, literalt carry_in, literalt &carry_out)
Definition: bv_utils.cpp:297
bool is_constant(const bvt &bv)
Definition: bv_utils.cpp:1303
literalt is_zero(const bvt &op)
Definition: bv_utils.h:141
bvt unsigned_multiplier_no_overflow(const bvt &op0, const bvt &op1)
Definition: bv_utils.cpp:703
bvt signed_multiplier_no_overflow(const bvt &op0, const bvt &op1)
Definition: bv_utils.cpp:788
virtual literalt land(literalt a, literalt b)=0
literalt is_all_ones(const bvt &op)
Definition: bv_utils.h:156
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:1147
literalt overflow_negate(const bvt &op)
Definition: bv_utils.cpp:546
void adder_no_overflow(bvt &sum, const bvt &op, bool subtract, representationt rep)
Definition: bv_utils.cpp:416
bvt concatenate(const bvt &a, const bvt &b) const
Definition: bv_utils.cpp:80
bvt signed_multiplier(const bvt &op0, const bvt &op1)
Definition: bv_utils.cpp:742
literalt rel(const bvt &bv0, irep_idt id, const bvt &bv1, representationt rep)
Definition: bv_utils.cpp:1281
bvt negate(const bvt &op)
Definition: bv_utils.cpp:532
literalt is_not_zero(const bvt &op)
Definition: bv_utils.h:144
static bvt extract_msb(const bvt &a, std::size_t n)
Definition: bv_utils.cpp:58
literalt full_adder(const literalt a, const literalt b, const literalt carry_in, literalt &carry_out)
Definition: bv_utils.cpp:140
bvt multiplier(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.cpp:810
void signed_divider(const bvt &op0, const bvt &op1, bvt &res, bvt &rem)
Definition: bv_utils.cpp:838
bvt absolute_value(const bvt &op)
Definition: bv_utils.cpp:773
bvt unsigned_multiplier(const bvt &op0, const bvt &op1)
Definition: bv_utils.cpp:633
literalt signed_less_than(const bvt &bv0, const bvt &bv1)
Definition: bv_utils.cpp:1274
bvt select(literalt s, const bvt &a, const bvt &b)
If s is true, selects a otherwise selects b.
Definition: bv_utils.cpp:96
void set_equal(const bvt &a, const bvt &b)
Definition: bv_utils.cpp:35
literalt verilog_bv_has_x_or_z(const bvt &)
Definition: bv_utils.cpp:1335
TO_BE_DOCUMENTED.
Definition: prop.h:24
bvt verilog_bv_normal_bits(const bvt &)
Definition: bv_utils.cpp:1350
bvt zero_extension(const bvt &bv, std::size_t new_size)
Definition: bv_utils.h:184
void unsigned_divider(const bvt &op0, const bvt &op1, bvt &res, bvt &rem)
Definition: bv_utils.cpp:892
bvt incrementer(const bvt &op, literalt carry_in)
Definition: bv_utils.cpp:572
bvt shift(const bvt &op, const shiftt shift, std::size_t distance)
Definition: bv_utils.cpp:480
literalt unsigned_less_than(const bvt &bv0, const bvt &bv1)
Definition: bv_utils.cpp:1262
literalt const_literal(bool value)
Definition: literal.h:187
bvt add(const bvt &op0, const bvt &op1)
Definition: bv_utils.h:64
literalt is_one(const bvt &op)
Definition: bv_utils.cpp:26
bvt cond_negate_no_overflow(const bvt &bv, const literalt cond)
Definition: bv_utils.cpp:779
static bvt extract_lsb(const bvt &a, std::size_t n)
Definition: bv_utils.cpp:70
bvt inc(const bvt &op)
Definition: bv_utils.h:36
bvt negate_no_overflow(const bvt &op)
Definition: bv_utils.cpp:540
literalt carry_out(const bvt &op0, const bvt &op1, literalt carry_in)
Definition: bv_utils.cpp:313
void cond_implies_equal(literalt cond, const bvt &a, const bvt &b)
Definition: bv_utils.cpp:1312
literalt carry(literalt a, literalt b, literalt c)
Definition: bv_utils.cpp:231
literalt overflow_sub(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.cpp:391
bvt sign_extension(const bvt &bv, std::size_t new_size)
Definition: bv_utils.h:179
literalt overflow_add(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.cpp:367
bvt add_sub(const bvt &op0, const bvt &op1, bool subtract)
Definition: bv_utils.cpp:339
bv_utilst(propt &_prop)
Definition: bv_utils.h:29
std::vector< literalt > bvt
Definition: literal.h:200
bvt build_constant(const mp_integer &i, std::size_t width)
Definition: bv_utils.cpp:15
bvt zeros(std::size_t new_size) const
Definition: bv_utils.h:189