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(expr.op0().type().id()!=expr.type().id() ||
23 expr.op1().type().id()!=expr.type().id())
24 return conversion_failed(expr);
25
26 bvt op0=convert_bv(expr.op0());
27 bvt op1=convert_bv(expr.op1());
28
29 if(op0.size()!=width ||
30 op1.size()!=width)
31 throw "convert_div: unexpected operand width";
32
33 bvt res, rem;
34
35 if(expr.type().id()==ID_fixedbv)
36 {
37 std::size_t fraction_bits=
39
40 bvt zeros = bv_utils.zeros(fraction_bits);
41
42 // add fraction_bits least-significant bits
43 op0.insert(op0.begin(), zeros.begin(), zeros.end());
44 op1=bv_utils.sign_extension(op1, op1.size()+fraction_bits);
45
46 bv_utils.divider(op0, op1, res, rem, bv_utilst::representationt::SIGNED);
47
48 // cut it down again
49 res.resize(width);
50 }
51 else
52 {
54 expr.type().id()==ID_signedbv?bv_utilst::representationt::SIGNED:
56
57 bv_utils.divider(op0, op1, res, rem, rep);
58 }
59
60 return res;
61}
Pre-defined bitvector types.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
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
virtual bvt convert_div(const div_exprt &expr)
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
representationt
Definition bv_utils.h:28
Division.
Definition std_expr.h:1157
typet & type()
Return the type of the expression.
Definition expr.h:84
std::size_t get_fraction_bits() const
const irep_idt & id() const
Definition irep.h:388
std::vector< literalt > bvt
Definition literal.h:201