17 const std::vector<exprt> &operands=expr.
operands();
28 operands.size() >= 3,
"case should have at least three operands");
31 operands.size() % 2 == 1,
"number of case operands should be odd");
52 std::string(
"size of compare operand does not match:\n") +
53 "compare operand: " + std::to_string(
compare_bv.size()) +
54 "\noperand: " + std::to_string(op.size()) +
'\n' + it->pretty());
66 bv.size() == op.size(),
67 std::string(
"size of value operand does not match:\n") +
68 "result size: " + std::to_string(bv.size()) +
69 "\noperand: " + std::to_string(op.size()) +
'\n' + it->pretty());
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
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 conversion_failed(const exprt &expr)
Print that the expression of x has failed conversion, then return a vector of x's width.
virtual std::size_t boolbv_width(const typet &type) const
virtual bvt convert_case(const exprt &expr)
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
Base class for all expressions.
typet & type()
Return the type of the expression.
const irep_idt & id() const
void l_set_to_true(literalt a)
virtual literalt land(literalt a, literalt b)=0
virtual literalt limplies(literalt a, literalt b)=0
virtual bvt new_variables(std::size_t width)
generates a bitvector of given width with new variables
virtual literalt lor(literalt a, literalt b)=0
#define forall_operands(it, expr)
std::vector< literalt > bvt
literalt const_literal(bool value)
#define UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)