cprover
Loading...
Searching...
No Matches
boolbv_power.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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(type.id()==ID_unsignedbv ||
19 type.id()==ID_signedbv)
20 {
21 // Let's do the special case 2**x
22 bvt op0=convert_bv(expr.op0());
23 bvt op1=convert_bv(expr.op1());
24
25 literalt eq_2=
26 bv_utils.equal(op0, bv_utils.build_constant(2, op0.size()));
27
28 bvt one=bv_utils.build_constant(1, width);
29 bvt shift=bv_utils.shift(one, bv_utilst::shiftt::SHIFT_LEFT, op1);
30
31 bvt nondet=prop.new_variables(width);
32
33 return bv_utils.select(eq_2, shift, nondet);
34 }
35
36 return conversion_failed(expr);
37}
A base class for binary expressions.
Definition std_expr.h:638
exprt & op0()
Definition expr.h:133
exprt & op1()
Definition expr.h:136
virtual const bvt & convert_bv(const exprt &expr, const std::optional< std::size_t > expected_width={})
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
Definition boolbv.cpp:39
bv_utilst bv_utils
Definition boolbv.h:118
bvt conversion_failed(const exprt &expr)
Print that the expression of x has failed conversion, then return a vector of x's width.
Definition boolbv.cpp:94
virtual std::size_t boolbv_width(const typet &type) const
Definition boolbv.h:103
virtual bvt convert_power(const binary_exprt &expr)
typet & type()
Return the type of the expression.
Definition expr.h:84
const irep_idt & id() const
Definition irep.h:388
The type of an expression, extends irept.
Definition type.h:29
std::vector< literalt > bvt
Definition literal.h:201