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 <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 
23 class bv_utilst
24 {
25 public:
26  explicit bv_utilst(propt &_prop):prop(_prop) { }
27 
28  enum class representationt { SIGNED, UNSIGNED };
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 
138  literalt is_zero(const bvt &op)
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
163  literalt rel(
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 
218 protected:
220 
221  void adder(
222  bvt &sum,
223  const bvt &op,
224  literalt carry_in,
226 
227  void adder_no_overflow(
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
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:777
mp_integer
BigInt mp_integer
Definition: smt_terms.h:12
mp_arith.h
bv_utilst::extract_lsb
static bvt extract_lsb(const bvt &a, std::size_t n)
Definition: bv_utils.cpp:66
bv_utilst::cond_implies_equal
void cond_implies_equal(literalt cond, const bvt &a, const bvt &b)
Definition: bv_utils.cpp:1312
bv_utilst::carry
literalt carry(literalt a, literalt b, literalt c)
Definition: bv_utils.cpp:227
bv_utilst::full_adder
literalt full_adder(const literalt a, const literalt b, const literalt carry_in, literalt &carry_out)
Definition: bv_utils.cpp:136
bv_utilst::inc
bvt inc(const bvt &op)
Definition: bv_utils.h:33
bv_utilst::is_not_zero
literalt is_not_zero(const bvt &op)
Definition: bv_utils.h:141
bv_utilst::carry_out
literalt carry_out(const bvt &op0, const bvt &op1, literalt carry_in)
Definition: bv_utils.cpp:309
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:537
bv_utilst::adder_no_overflow
void adder_no_overflow(bvt &sum, const bvt &op, bool subtract, representationt rep)
Definition: bv_utils.cpp:412
bv_utilst::signed_multiplier
bvt signed_multiplier(const bvt &op0, const bvt &op1)
Definition: bv_utils.cpp:740
bv_utilst::shiftt::SHIFT_ARIGHT
@ SHIFT_ARIGHT
bv_utilst::representationt::UNSIGNED
@ UNSIGNED
bv_utilst::set_equal
void set_equal(const bvt &a, const bvt &b)
Definition: bv_utils.cpp:31
bv_utilst::sign_extension
bvt sign_extension(const bvt &bv, std::size_t new_size)
Definition: bv_utils.h:177
bv_utilst::signed_divider
void signed_divider(const bvt &op0, const bvt &op1, bvt &res, bvt &rem)
Definition: bv_utils.cpp:836
propt::lor
virtual literalt lor(literalt a, literalt b)=0
bv_utilst::prop
propt & prop
Definition: bv_utils.h:219
bv_utilst::incrementer
bvt incrementer(const bvt &op, literalt carry_in)
Definition: bv_utils.cpp:569
bv_utilst::inverted
static bvt inverted(const bvt &op)
Definition: bv_utils.cpp:577
bv_utilst::absolute_value
bvt absolute_value(const bvt &op)
Definition: bv_utils.cpp:771
bv_utilst::zeros
bvt zeros(std::size_t new_size) const
Definition: bv_utils.h:187
bv_utilst::unsigned_multiplier
bvt unsigned_multiplier(const bvt &op0, const bvt &op1)
Definition: bv_utils.cpp:631
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:92
bv_utilst
Definition: bv_utils.h:24
bv_utilst::shift
static bvt shift(const bvt &op, const shiftt shift, std::size_t distance)
Definition: bv_utils.cpp:477
bv_utilst::unsigned_less_than
literalt unsigned_less_than(const bvt &bv0, const bvt &bv1)
Definition: bv_utils.cpp:1260
bv_utilst::unsigned_divider
void unsigned_divider(const bvt &op0, const bvt &op1, bvt &res, bvt &rem)
Definition: bv_utils.cpp:889
bv_utilst::is_int_min
literalt is_int_min(const bvt &op)
Definition: bv_utils.h:144
bv_utilst::add
bvt add(const bvt &op0, const bvt &op1)
Definition: bv_utils.h:61
bv_utilst::representationt::SIGNED
@ SIGNED
bv_utilst::representationt
representationt
Definition: bv_utils.h:28
bv_utilst::cond_negate
bvt cond_negate(const bvt &bv, const literalt cond)
Definition: bv_utils.cpp:758
bv_utilst::overflow_sub
literalt overflow_sub(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.cpp:387
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:363
bv_utilst::signed_multiplier_no_overflow
bvt signed_multiplier_no_overflow(const bvt &op0, const bvt &op1)
Definition: bv_utils.cpp:784
bv_utilst::bv_utilst
bv_utilst(propt &_prop)
Definition: bv_utils.h:26
bv_utilst::unsigned_multiplier_no_overflow
bvt unsigned_multiplier_no_overflow(const bvt &op0, const bvt &op1)
Definition: bv_utils.cpp:701
bv_utilst::concatenate
static bvt concatenate(const bvt &a, const bvt &b)
Definition: bv_utils.cpp:76
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:1142
bv_utilst::add_sub
bvt add_sub(const bvt &op0, const bvt &op1, bool subtract)
Definition: bv_utils.cpp:335
bv_utilst::wallace_tree
bvt wallace_tree(const std::vector< bvt > &pps)
Definition: bv_utils.cpp:585
bv_utilst::remainder
bvt remainder(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.h:91
bv_utilst::multiplier_no_overflow
bvt multiplier_no_overflow(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.cpp:820
bv_utilst::build_constant
static bvt build_constant(const mp_integer &i, std::size_t width)
Definition: bv_utils.cpp:11
bv_utilst::rel
literalt rel(const bvt &bv0, irep_idt id, const bvt &bv1, representationt rep)
Definition: bv_utils.cpp:1279
bv_utilst::shiftt
shiftt
Definition: bv_utils.h:69
propt
TO_BE_DOCUMENTED.
Definition: prop.h:23
bv_utilst::negate
bvt negate(const bvt &op)
Definition: bv_utils.cpp:529
bv_utilst::is_all_ones
literalt is_all_ones(const bvt &op)
Definition: bv_utils.h:153
bv_utilst::overflow_negate
literalt overflow_negate(const bvt &op)
Definition: bv_utils.cpp:543
bv_utilst::shiftt::ROTATE_RIGHT
@ ROTATE_RIGHT
bv_utilst::sign_bit
static literalt sign_bit(const bvt &op)
Definition: bv_utils.h:133
bv_utilst::extension
static bvt extension(const bvt &bv, std::size_t new_size, representationt rep)
Definition: bv_utils.cpp:105
literalt
Definition: literal.h:26
bv_utilst::divider
bvt divider(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.h:84
bv_utilst::extract
static bvt extract(const bvt &a, std::size_t first, std::size_t last)
Definition: bv_utils.cpp:38
bv_utilst::signed_less_than
literalt signed_less_than(const bvt &bv0, const bvt &bv1)
Definition: bv_utils.cpp:1272
bv_utilst::shiftt::SHIFT_LRIGHT
@ SHIFT_LRIGHT
bv_utilst::multiplier
bvt multiplier(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.cpp:806
bv_utilst::extract_msb
static bvt extract_msb(const bvt &a, std::size_t n)
Definition: bv_utils.cpp:54
bv_utilst::verilog_bv_normal_bits
static bvt verilog_bv_normal_bits(const bvt &)
Definition: bv_utils.cpp:1350
bv_utilst::adder
void adder(bvt &sum, const bvt &op, literalt carry_in, literalt &carry_out)
Definition: bv_utils.cpp:293
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:324
bv_utilst::equal
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
Definition: bv_utils.cpp:1103
bv_utilst::is_zero
literalt is_zero(const bvt &op)
Definition: bv_utils.h:138
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:1335
bv_utilst::is_one
literalt is_one(const bvt &op)
Definition: bv_utils.cpp:22
bv_utilst::zero_extension
bvt zero_extension(const bvt &bv, std::size_t new_size)
Definition: bv_utils.h:182
bv_utilst::sub
bvt sub(const bvt &op0, const bvt &op1)
Definition: bv_utils.h:62
bv_utilst::is_constant
static bool is_constant(const bvt &bv)
Definition: bv_utils.cpp:1301