Go to the documentation of this file.
17 const std::vector<exprt> &operands=expr.
operands();
32 operands.size() >= 3,
"case should have at least three operands");
35 operands.size() % 2 == 1,
"number of case operands should be odd");
37 enum { FIRST, COMPARE, VALUE } what=FIRST;
55 compare_bv.size() == op.size(),
56 std::string(
"size of compare operand does not match:\n") +
61 compare_literal=
prop.
land(!previous_compare, compare_literal);
63 previous_compare=
prop.
lor(previous_compare, compare_literal);
70 bv.size() == op.size(),
71 std::string(
"size of value operand does not match:\n") +
#define UNREACHABLE
This should be used to mark dead code.
std::vector< literalt > bvt
virtual literalt new_variable()=0
Base class for all expressions.
virtual literalt lor(literalt a, literalt b)=0
void l_set_to_true(literalt a)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
virtual bvt convert_case(const exprt &expr)
virtual literalt land(literalt a, literalt b)=0
#define Forall_literals(it, bv)
typet & type()
Return the type of the expression.
boolbv_widtht boolbv_width
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,...
virtual literalt limplies(literalt a, literalt b)=0
#define forall_operands(it, expr)
#define PRECONDITION(CONDITION)
literalt const_literal(bool value)
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...
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.