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(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
29 bv_utils.equal(op0, bv_utils.build_constant(2, op0.size()));
30
33
35
36 return bv_utils.select(eq_2, shift, nondet);
37 }
38
39 return conversion_failed(expr);
40}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
A base class for binary expressions.
Definition std_expr.h:550
exprt & op0()
Definition expr.h:99
exprt & op1()
Definition expr.h:102
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:40
bv_utilst bv_utils
Definition boolbv.h:114
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:84
virtual std::size_t boolbv_width(const typet &type) const
Definition boolbv.h:99
virtual bvt convert_power(const binary_exprt &expr)
bvt select(literalt s, const bvt &a, const bvt &b)
If s is true, selects a otherwise selects b.
Definition bv_utils.cpp:92
static bvt build_constant(const mp_integer &i, std::size_t width)
Definition bv_utils.cpp:11
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
static bvt shift(const bvt &op, const shiftt shift, std::size_t distance)
Definition bv_utils.cpp:477
typet & type()
Return the type of the expression.
Definition expr.h:82
const irep_idt & id() const
Definition irep.h:396
virtual bvt new_variables(std::size_t width)
generates a bitvector of given width with new variables
Definition prop.cpp:20
The type of an expression, extends irept.
Definition type.h:29
std::vector< literalt > bvt
Definition literal.h:201