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 }
bvt
std::vector< literalt > bvt
Definition: literal.h:201
bv_utilst::representationt::UNSIGNED
@ UNSIGNED
boolbvt::convert_mod
virtual bvt convert_mod(const mod_exprt &expr)
Definition: boolbv_mod.cpp:12
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
boolbvt::boolbv_width
boolbv_widtht boolbv_width
Definition: boolbv.h:95
boolbvt::conversion_failed
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:113
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:511
bv_utilst::representationt::SIGNED
@ SIGNED
bv_utilst::representationt
representationt
Definition: bv_utils.h:31
irept::id
const irep_idt & id() const
Definition: irep.h:418
boolbvt::convert_bv
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:119
boolbvt::bv_utils
bv_utilst bv_utils
Definition: boolbv.h:98
bv_utilst::divider
bvt divider(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.h:87
boolbv.h
binary_exprt::op1
exprt & op1()
Definition: expr.h:105
binary_exprt::op0
exprt & op0()
Definition: expr.h:102
mod_exprt
Modulo.
Definition: std_expr.h:1100