cprover
boolbv_power.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #include "boolbv.h"
11 
13 {
14  const typet &type=ns.follow(expr.type());
15 
16  std::size_t width=boolbv_width(type);
17 
18  if(width==0)
19  return conversion_failed(expr);
20 
21  if(type.id()==ID_unsignedbv ||
22  type.id()==ID_signedbv)
23  {
24  // Let's do the special case 2**x
25  bvt op0=convert_bv(expr.op0());
26  bvt op1=convert_bv(expr.op1());
27 
28  literalt eq_2=
29  bv_utils.equal(op0, bv_utils.build_constant(2, op0.size()));
30 
31  bvt one=bv_utils.build_constant(1, width);
33 
34  bvt nondet=prop.new_variables(width);
35 
36  return bv_utils.select(eq_2, shift, nondet);
37  }
38 
39  return conversion_failed(expr);
40 }
The type of an expression.
Definition: type.h:22
bv_utilst bv_utils
Definition: boolbv.h:93
exprt & op0()
Definition: expr.h:72
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
Definition: bv_utils.cpp:1108
bvt new_variables(std::size_t width)
generates a bitvector of given width with new variables
Definition: prop.cpp:39
boolbv_widtht boolbv_width
Definition: boolbv.h:90
typet & type()
Definition: expr.h:56
const irep_idt & id() const
Definition: irep.h:189
A generic base class for binary expressions.
Definition: std_expr.h:649
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:116
exprt & op1()
Definition: expr.h:75
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:108
const namespacet & ns
const typet & follow(const typet &) const
Definition: namespace.cpp:55
bvt select(literalt s, const bvt &a, const bvt &b)
If s is true, selects a otherwise selects b.
Definition: bv_utils.cpp:96
bvt shift(const bvt &op, const shiftt shift, std::size_t distance)
Definition: bv_utils.cpp:480
std::vector< literalt > bvt
Definition: literal.h:200
bvt build_constant(const mp_integer &i, std::size_t width)
Definition: bv_utils.cpp:15
virtual bvt convert_power(const binary_exprt &expr)