Go to the documentation of this file.
21 if(type.
id()==ID_unsignedbv ||
22 type.
id()==ID_signedbv)
bvt new_variables(std::size_t width)
generates a bitvector of given width with new variables
The type of an expression, extends irept.
std::vector< literalt > bvt
A base class for binary expressions.
bvt select(literalt s, const bvt &a, const bvt &b)
If s is true, selects a otherwise selects b.
bvt shift(const bvt &op, const shiftt shift, std::size_t distance)
typet & type()
Return the type of the expression.
boolbv_widtht boolbv_width
void conversion_failed(const exprt &expr, bvt &bv)
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 build_constant(const mp_integer &i, std::size_t width)
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
virtual bvt convert_power(const binary_exprt &expr)