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 = 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 }
bv_utilst::shiftt::SHIFT_LEFT
@ SHIFT_LEFT
propt::new_variables
bvt new_variables(std::size_t width)
generates a bitvector of given width with new variables
Definition: prop.cpp:20
typet
The type of an expression, extends irept.
Definition: type.h:29
bvt
std::vector< literalt > bvt
Definition: literal.h:201
binary_exprt
A base class for binary expressions.
Definition: std_expr.h:601
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:96
bv_utilst::shift
bvt shift(const bvt &op, const shiftt shift, std::size_t distance)
Definition: bv_utils.cpp:481
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
boolbvt::boolbv_width
boolbv_widtht boolbv_width
Definition: boolbv.h:95
boolbvt::conversion_failed
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:113
irept::id
const irep_idt & id() const
Definition: irep.h:418
boolbvt::convert_bv
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
Definition: boolbv.cpp:119
bv_utilst::build_constant
bvt build_constant(const mp_integer &i, std::size_t width)
Definition: bv_utils.cpp:15
boolbvt::bv_utils
bv_utilst bv_utils
Definition: boolbv.h:98
literalt
Definition: literal.h:26
boolbv.h
bv_utilst::equal
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
Definition: bv_utils.cpp:1113
boolbvt::convert_power
virtual bvt convert_power(const binary_exprt &expr)
Definition: boolbv_power.cpp:12
binary_exprt::op1
exprt & op1()
Definition: expr.h:105
binary_exprt::op0
exprt & op0()
Definition: expr.h:102
prop_conv_solvert::prop
propt & prop
Definition: prop_conv_solver.h:131