Go to the documentation of this file.
36 if(bvtype==bvtypet::IS_UNKNOWN &&
37 (type.
id()==ID_vector || type.
id()==ID_complex))
45 "bitvector representation of type needs to have at least one bit");
48 width % sub_width == 0,
49 "total bitvector width needs to be a multiple of the component bitvector "
54 for(std::size_t sub_idx = 0; sub_idx < width; sub_idx += sub_width)
58 const auto sub_it = std::next(op_bv.begin(), sub_idx);
59 std::copy_n(sub_it, sub_width, std::back_inserter(tmp_op));
64 tmp_op = float_utils.
negate(tmp_op);
70 tmp_op.size() == sub_width,
71 "bitvector after negation shall have same bit width");
73 std::copy(tmp_op.begin(), tmp_op.end(), std::back_inserter(bv));
78 else if(bvtype==bvtypet::IS_FIXED && op_bvtype==bvtypet::IS_FIXED)
82 else if(bvtype==bvtypet::IS_FLOAT && op_bvtype==bvtypet::IS_FLOAT)
85 return float_utils.
negate(op_bv);
87 else if((op_bvtype==bvtypet::IS_SIGNED || op_bvtype==bvtypet::IS_UNSIGNED) &&
88 (bvtype==bvtypet::IS_SIGNED || bvtype==bvtypet::IS_UNSIGNED))
const typet & subtype() const
The type of an expression, extends irept.
std::vector< literalt > bvt
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
bvtypet get_bvtype(const typet &type)
Base class for all expressions.
typet & type()
Return the type of the expression.
virtual std::size_t boolbv_width(const typet &type) const
Pre-defined bitvector types.
The unary minus expression.
const irep_idt & id() const
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...
bvt negate(const bvt &op)
virtual bvt convert_unary_minus(const unary_minus_exprt &expr)
bvt conversion_failed(const exprt &expr)
Print that the expression of x has failed conversion, then return a vector of x's width.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.