cprover
boolbv_mod.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
12
bvt
boolbvt::convert_mod
(
const
mod_exprt
&expr)
13
{
14
#if 0
15
// TODO
16
if
(expr.
type
().
id
()==ID_floatbv)
17
{
18
}
19
#endif
20
21
if
(expr.
type
().
id
()!=ID_unsignedbv &&
22
expr.
type
().
id
()!=ID_signedbv)
23
return
conversion_failed
(expr);
24
25
std::size_t width=
boolbv_width
(expr.
type
());
26
27
if
(width==0)
28
return
conversion_failed
(expr);
29
30
DATA_INVARIANT
(
31
expr.
op0
().
type
().
id
() == expr.
type
().
id
(),
32
"type of the first operand of a modulo operation shall equal the "
33
"expression type"
);
34
35
DATA_INVARIANT
(
36
expr.
op1
().
type
().
id
() == expr.
type
().
id
(),
37
"type of the second operand of a modulo operation shall equal the "
38
"expression type"
);
39
40
bv_utilst::representationt
rep=
41
expr.
type
().
id
()==ID_signedbv?
bv_utilst::representationt::SIGNED
:
42
bv_utilst::representationt::UNSIGNED
;
43
44
const
bvt
&op0 =
convert_bv
(expr.
op0
(), width);
45
const
bvt
&op1 =
convert_bv
(expr.
op1
(), width);
46
47
bvt
res, rem;
48
49
bv_utils
.
divider
(op0, op1, res, rem, rep);
50
51
return
rem;
52
}
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition:
invariant.h:485
bvt
std::vector< literalt > bvt
Definition:
literal.h:200
bv_utilst::representationt::UNSIGNED
boolbvt::convert_mod
virtual bvt convert_mod(const mod_exprt &expr)
Definition:
boolbv_mod.cpp:12
exprt::op0
exprt & op0()
Definition:
expr.h:84
exprt::type
typet & type()
Return the type of the expression.
Definition:
expr.h:68
boolbvt::boolbv_width
boolbv_widtht boolbv_width
Definition:
boolbv.h:92
boolbvt::conversion_failed
void conversion_failed(const exprt &expr, bvt &bv)
Definition:
boolbv.h:110
bv_utilst::representationt::SIGNED
bv_utilst::representationt
representationt
Definition:
bv_utils.h:31
exprt::op1
exprt & op1()
Definition:
expr.h:87
irept::id
const irep_idt & id() const
Definition:
irep.h:259
boolbvt::convert_bv
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Definition:
boolbv.cpp:112
boolbvt::bv_utils
bv_utilst bv_utils
Definition:
boolbv.h:95
bv_utilst::divider
bvt divider(const bvt &op0, const bvt &op1, representationt rep)
Definition:
bv_utils.h:87
boolbv.h
mod_exprt
Modulo.
Definition:
std_expr.h:1287
solvers
flattening
boolbv_mod.cpp
Generated by
1.8.16