cprover
Loading...
Searching...
No Matches
boolbv_div.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "boolbv.h"
10
12
14{
15 if(expr.type().id()!=ID_unsignedbv &&
16 expr.type().id()!=ID_signedbv &&
17 expr.type().id()!=ID_fixedbv)
18 return conversion_failed(expr);
19
20 std::size_t width=boolbv_width(expr.type());
21
22 if(width==0)
23 return conversion_failed(expr);
24
25 if(expr.op0().type().id()!=expr.type().id() ||
26 expr.op1().type().id()!=expr.type().id())
27 return conversion_failed(expr);
28
29 bvt op0=convert_bv(expr.op0());
30 bvt op1=convert_bv(expr.op1());
31
32 if(op0.size()!=width ||
33 op1.size()!=width)
34 throw "convert_div: unexpected operand width";
35
36 bvt res, rem;
37
38 if(expr.type().id()==ID_fixedbv)
39 {
40 std::size_t fraction_bits=
42
43 bvt zeros;
44 zeros.resize(fraction_bits, const_literal(false));
45
46 // add fraction_bits least-significant bits
47 op0.insert(op0.begin(), zeros.begin(), zeros.end());
48 op1=bv_utils.sign_extension(op1, op1.size()+fraction_bits);
49
51
52 // cut it down again
53 res.resize(width);
54 }
55 else
56 {
60
61 bv_utils.divider(op0, op1, res, rem, rep);
62 }
63
64 return res;
65}
Pre-defined bitvector types.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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
virtual bvt convert_div(const div_exprt &expr)
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
bvt sign_extension(const bvt &bv, std::size_t new_size)
Definition bv_utils.h:177
representationt
Definition bv_utils.h:28
bvt divider(const bvt &op0, const bvt &op1, representationt rep)
Definition bv_utils.h:84
Division.
Definition std_expr.h:1064
typet & type()
Return the type of the expression.
Definition expr.h:82
std::size_t get_fraction_bits() const
const irep_idt & id() const
Definition irep.h:396
std::vector< literalt > bvt
Definition literal.h:201
literalt const_literal(bool value)
Definition literal.h:188