Go to the documentation of this file.
24 DATA_INVARIANT(!operands.empty(),
"multiplication must have operands");
30 "multiplication operands should have same type as expression");
32 if(expr.
type().
id()==ID_fixedbv)
36 std::size_t fraction_bits=
39 for(exprt::operandst::const_iterator it=operands.begin()+1;
40 it!=operands.end(); it++)
43 it->type() == expr.
type(),
44 "multiplication operands should have same type as expression");
56 bv.erase(bv.begin(), bv.begin()+fraction_bits);
61 else if(expr.
type().
id()==ID_unsignedbv ||
62 expr.
type().
id()==ID_signedbv)
70 for(exprt::operandst::const_iterator it=operands.begin()+1;
71 it!=operands.end(); it++)
74 it->type() == expr.
type(),
75 "multiplication operands should have same type as expression");
std::vector< literalt > bvt
bvt signed_multiplier(const bvt &op0, const bvt &op1)
bvt sign_extension(const bvt &bv, std::size_t new_size)
Base class for all expressions.
virtual bvt convert_mult(const mult_exprt &expr)
typet & type()
Return the type of the expression.
boolbv_widtht boolbv_width
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
void conversion_failed(const exprt &expr, bvt &bv)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Binary multiplication Associativity is not specified.
const irep_idt & id() const
std::vector< exprt > operandst
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...
std::size_t get_fraction_bits() const
bvt multiplier(const bvt &op0, const bvt &op1, representationt rep)