cprover
boolbv_mult.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "boolbv.h"
10 
11 #include <util/std_types.h>
12 
14 {
15  std::size_t width=boolbv_width(expr.type());
16 
17  if(width==0)
18  return conversion_failed(expr);
19 
20  bvt bv;
21  bv.resize(width);
22 
23  const exprt::operandst &operands=expr.operands();
24  DATA_INVARIANT(!operands.empty(), "multiplication must have operands");
25 
26  const exprt &op0=expr.op0();
27 
29  op0.type() == expr.type(),
30  "multiplication operands should have same type as expression");
31 
32  if(expr.type().id()==ID_fixedbv)
33  {
34  bv = convert_bv(op0, width);
35 
36  std::size_t fraction_bits=
38 
39  for(exprt::operandst::const_iterator it=operands.begin()+1;
40  it!=operands.end(); it++)
41  {
43  it->type() == expr.type(),
44  "multiplication operands should have same type as expression");
45 
46  // do a sign extension by fraction_bits bits
47  bv=bv_utils.sign_extension(bv, bv.size()+fraction_bits);
48 
49  bvt op = convert_bv(*it, width);
50 
51  op=bv_utils.sign_extension(op, bv.size());
52 
53  bv=bv_utils.signed_multiplier(bv, op);
54 
55  // cut it down again
56  bv.erase(bv.begin(), bv.begin()+fraction_bits);
57  }
58 
59  return bv;
60  }
61  else if(expr.type().id()==ID_unsignedbv ||
62  expr.type().id()==ID_signedbv)
63  {
65  expr.type().id()==ID_signedbv?bv_utilst::representationt::SIGNED:
67 
68  bv = convert_bv(op0, width);
69 
70  for(exprt::operandst::const_iterator it=operands.begin()+1;
71  it!=operands.end(); it++)
72  {
74  it->type() == expr.type(),
75  "multiplication operands should have same type as expression");
76 
77  const bvt &op = convert_bv(*it, width);
78 
79  bv = bv_utils.multiplier(bv, op, rep);
80  }
81 
82  return bv;
83  }
84 
85  return conversion_failed(expr);
86 }
bvt
std::vector< literalt > bvt
Definition: literal.h:201
bv_utilst::signed_multiplier
bvt signed_multiplier(const bvt &op0, const bvt &op1)
Definition: bv_utils.cpp:744
bv_utilst::representationt::UNSIGNED
@ UNSIGNED
bv_utilst::sign_extension
bvt sign_extension(const bvt &bv, std::size_t new_size)
Definition: bv_utils.h:179
exprt
Base class for all expressions.
Definition: expr.h:53
boolbvt::convert_mult
virtual bvt convert_mult(const mult_exprt &expr)
Definition: boolbv_mult.cpp:13
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
to_fixedbv_type
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
Definition: std_types.h:1362
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
std_types.h
Pre-defined types.
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:986
irept::id
const irep_idt & id() const
Definition: irep.h:418
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
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
fixedbv_typet::get_fraction_bits
std::size_t get_fraction_bits() const
Definition: std_types.h:1324
boolbvt::bv_utils
bv_utilst bv_utils
Definition: boolbv.h:98
bv_utilst::multiplier
bvt multiplier(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.cpp:810
boolbv.h
exprt::operands
operandst & operands()
Definition: expr.h:95
multi_ary_exprt::op0
exprt & op0()
Definition: std_expr.h:811