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 
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 & op1()
Definition: expr.h:102
exprt & op0()
Definition: expr.h:99
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)
Definition: boolbv_mod.cpp:12
bv_utilst bv_utils
Definition: boolbv.h:112
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:97
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:407
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