cprover
Loading...
Searching...
No Matches
boolbv_mult.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "boolbv.h"
10
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 {
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}
Pre-defined bitvector types.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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_mult(const mult_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
bvt signed_multiplier(const bvt &op0, const bvt &op1)
Definition bv_utils.cpp:740
bvt sign_extension(const bvt &bv, std::size_t new_size)
Definition bv_utils.h:177
representationt
Definition bv_utils.h:28
bvt multiplier(const bvt &op0, const bvt &op1, representationt rep)
Definition bv_utils.cpp:806
Base class for all expressions.
Definition expr.h:54
std::vector< exprt > operandst
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:82
operandst & operands()
Definition expr.h:92
std::size_t get_fraction_bits() const
const irep_idt & id() const
Definition irep.h:396
Binary multiplication Associativity is not specified.
Definition std_expr.h:1019
exprt & op0()
Definition std_expr.h:844
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