cprover
Loading...
Searching...
No Matches
boolbv_mod.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 #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
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
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
41 expr.type().id()==ID_signedbv?bv_utilst::representationt::SIGNED:
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}
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_mod(const mod_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
representationt
Definition bv_utils.h:28
bvt divider(const bvt &op0, const bvt &op1, representationt rep)
Definition bv_utils.h:84
typet & type()
Return the type of the expression.
Definition expr.h:82
const irep_idt & id() const
Definition irep.h:396
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition std_expr.h:1135
std::vector< literalt > bvt
Definition literal.h:201
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:510