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 { LEFT, LRIGHT, ARIGHT };
72  bvt shift(const bvt &op, const shiftt shift, std::size_t distance);
73  bvt shift(const bvt &op, const shiftt shift, const bvt &distance);
74 
75  bvt unsigned_multiplier(const bvt &op0, const bvt &op1);
76  bvt signed_multiplier(const bvt &op0, const bvt &op1);
77  bvt multiplier(const bvt &op0, const bvt &op1, representationt rep);
79  const bvt &op0,
80  const bvt &op1,
81  representationt rep);
82 
83  bvt divider(const bvt &op0, const bvt &op1, representationt rep)
84  {
85  bvt res, rem;
86  divider(op0, op1, res, rem, rep);
87  return res;
88  }
89 
90  bvt remainder(const bvt &op0, const bvt &op1, representationt rep)
91  {
92  bvt res, rem;
93  divider(op0, op1, res, rem, rep);
94  return rem;
95  }
96 
97  void divider(
98  const bvt &op0,
99  const bvt &op1,
100  bvt &res,
101  bvt &rem,
102  representationt rep);
103 
104  void signed_divider(
105  const bvt &op0,
106  const bvt &op1,
107  bvt &res,
108  bvt &rem);
109 
110  void unsigned_divider(
111  const bvt &op0,
112  const bvt &op1,
113  bvt &res,
114  bvt &rem);
115 
116  #ifdef COMPACT_EQUAL_CONST
117  typedef std::set<bvt> equal_const_registeredt;
118  equal_const_registeredt equal_const_registered;
119  void equal_const_register(const bvt &var);
120 
121  typedef std::pair<bvt, bvt> var_constant_pairt;
122  typedef std::map<var_constant_pairt, literalt> equal_const_cachet;
123  equal_const_cachet equal_const_cache;
124 
125  literalt equal_const_rec(bvt &var, bvt &constant);
126  literalt equal_const(const bvt &var, const bvt &constant);
127  #endif
128 
129 
130  literalt equal(const bvt &op0, const bvt &op1);
131 
132  static inline literalt sign_bit(const bvt &op)
133  {
134  return op[op.size()-1];
135  }
136 
137  literalt is_zero(const bvt &op)
138  { return !prop.lor(op); }
139 
141  { return prop.lor(op); }
142 
144  {
145  bvt tmp=op;
146  tmp[tmp.size()-1]=!tmp[tmp.size()-1];
147  return is_zero(tmp);
148  }
149 
150  literalt is_one(const bvt &op);
151 
153  { return prop.land(op); }
154 
156  bool or_equal,
157  const bvt &bv0,
158  const bvt &bv1,
159  representationt rep);
160 
161  // id is one of ID_lt, le, gt, ge, equal, notequal
162  literalt rel(
163  const bvt &bv0,
164  irep_idt id,
165  const bvt &bv1,
166  representationt rep);
167 
168  literalt unsigned_less_than(const bvt &bv0, const bvt &bv1);
169  literalt signed_less_than(const bvt &bv0, const bvt &bv1);
170 
171  bool is_constant(const bvt &bv);
172 
173  bvt extension(const bvt &bv, std::size_t new_size, representationt rep);
174 
175  bvt sign_extension(const bvt &bv, std::size_t new_size)
176  {
177  return extension(bv, new_size, representationt::SIGNED);
178  }
179 
180  bvt zero_extension(const bvt &bv, std::size_t new_size)
181  {
182  return extension(bv, new_size, representationt::UNSIGNED);
183  }
184 
185  bvt zeros(std::size_t new_size) const
186  {
187  bvt result;
188  result.resize(new_size, const_literal(false));
189  return result;
190  }
191 
192  void set_equal(const bvt &a, const bvt &b);
193 
194  // if cond holds, a has to be equal to b
195  void cond_implies_equal(literalt cond, const bvt &a, const bvt &b);
196 
197  bvt cond_negate(const bvt &bv, const literalt cond);
198 
199  bvt select(literalt s, const bvt &a, const bvt &b);
200 
201  // computes a[last:first]
202  static bvt extract(const bvt &a, std::size_t first, std::size_t last);
203 
204  // extracts the n most significant bits
205  static bvt extract_msb(const bvt &a, std::size_t n);
206 
207  // extracts the n least significant bits
208  static bvt extract_lsb(const bvt &a, std::size_t n);
209 
210  // put a and b together, where a comes first (lower indices)
211  bvt concatenate(const bvt &a, const bvt &b) const;
212 
214  bvt verilog_bv_normal_bits(const bvt &);
215 
216 protected:
218 
219  void adder(
220  bvt &sum,
221  const bvt &op,
222  literalt carry_in,
224 
225  void adder_no_overflow(
226  bvt &sum,
227  const bvt &op,
228  bool subtract,
229  representationt rep);
230 
231  void adder_no_overflow(bvt &sum, const bvt &op);
232 
234  const bvt &op0, const bvt &op1);
235 
237  const bvt &op0, const bvt &op1);
238 
239  bvt cond_negate_no_overflow(const bvt &bv, const literalt cond);
240 
241  bvt wallace_tree(const std::vector<bvt> &pps);
242 };
243 
244 #endif // CPROVER_SOLVERS_FLATTENING_BV_UTILS_H
bvt wallace_tree(const std::vector< bvt > &pps)
Definition: bv_utils.cpp:569
propt & prop
Definition: bv_utils.h:217
bvt inverted(const bvt &op)
Definition: bv_utils.cpp:561
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:90
bvt multiplier_no_overflow(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.cpp:804
BigInt mp_integer
Definition: mp_arith.h:19
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:132
literalt is_int_min(const bvt &op)
Definition: bv_utils.h:143
bvt cond_negate(const bvt &bv, const literalt cond)
Definition: bv_utils.cpp:741
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:83
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
Definition: bv_utils.cpp:1089
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:1284
literalt is_zero(const bvt &op)
Definition: bv_utils.h:137
bvt unsigned_multiplier_no_overflow(const bvt &op0, const bvt &op1)
Definition: bv_utils.cpp:684
bvt signed_multiplier_no_overflow(const bvt &op0, const bvt &op1)
Definition: bv_utils.cpp:769
virtual literalt land(literalt a, literalt b)=0
literalt is_all_ones(const bvt &op)
Definition: bv_utils.h:152
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:1128
literalt overflow_negate(const bvt &op)
Definition: bv_utils.cpp:527
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:723
literalt rel(const bvt &bv0, irep_idt id, const bvt &bv1, representationt rep)
Definition: bv_utils.cpp:1262
bvt negate(const bvt &op)
Definition: bv_utils.cpp:513
literalt is_not_zero(const bvt &op)
Definition: bv_utils.h:140
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:791
void signed_divider(const bvt &op0, const bvt &op1, bvt &res, bvt &rem)
Definition: bv_utils.cpp:819
bvt absolute_value(const bvt &op)
Definition: bv_utils.cpp:754
bvt unsigned_multiplier(const bvt &op0, const bvt &op1)
Definition: bv_utils.cpp:614
literalt signed_less_than(const bvt &bv0, const bvt &bv1)
Definition: bv_utils.cpp:1255
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:1316
TO_BE_DOCUMENTED.
Definition: prop.h:22
bvt verilog_bv_normal_bits(const bvt &)
Definition: bv_utils.cpp:1331
bvt zero_extension(const bvt &bv, std::size_t new_size)
Definition: bv_utils.h:180
void unsigned_divider(const bvt &op0, const bvt &op1, bvt &res, bvt &rem)
Definition: bv_utils.cpp:873
bvt incrementer(const bvt &op, literalt carry_in)
Definition: bv_utils.cpp:553
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:1243
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:760
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:521
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:1293
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:175
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:197
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:185