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 
30  if(expr.op0().type().id()!=expr.type().id() ||
31  expr.op1().type().id()!=expr.type().id())
32  throw "mod got mixed-type operands";
33 
35  expr.type().id()==ID_signedbv?bv_utilst::representationt::SIGNED:
37 
38  const bvt &op0=convert_bv(expr.op0());
39  const bvt &op1=convert_bv(expr.op1());
40 
41  if(op0.size()!=width ||
42  op1.size()!=width)
43  throw "convert_mod: unexpected operand width";
44 
45  bvt res, rem;
46 
47  bv_utils.divider(op0, op1, res, rem, rep);
48 
49  return rem;
50 }
bv_utilst bv_utils
Definition: boolbv.h:93
exprt & op0()
Definition: expr.h:72
bvt divider(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.h:87
boolbv_widtht boolbv_width
Definition: boolbv.h:90
representationt
Definition: bv_utils.h:31
typet & type()
Definition: expr.h:56
const irep_idt & id() const
Definition: irep.h:259
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:116
exprt & op1()
Definition: expr.h:75
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:108
virtual bvt convert_mod(const mod_exprt &expr)
Definition: boolbv_mod.cpp:12
std::vector< literalt > bvt
Definition: literal.h:200
binary modulo
Definition: std_expr.h:1133