17 const std::vector<exprt> &operands=expr.
operands();
22 bvt bv =
prop.new_variables(width);
25 operands.size() >= 3,
"case should have at least three operands");
28 operands.size() % 2 == 1,
"number of case operands should be odd");
30 enum { FIRST, COMPARE, VALUE } what=FIRST;
35 for(
const auto &operand : expr.
operands())
48 compare_bv.size() == op.size(),
49 std::string(
"size of compare operand does not match:\n") +
50 "compare operand: " + std::to_string(compare_bv.size()) +
51 "\noperand: " + std::to_string(op.size()) +
'\n' + operand.pretty());
53 compare_literal=
bv_utils.equal(compare_bv, op);
54 compare_literal=
prop.land(!previous_compare, compare_literal);
56 previous_compare=
prop.lor(previous_compare, compare_literal);
63 bv.size() == op.size(),
64 std::string(
"size of value operand does not match:\n") +
65 "result size: " + std::to_string(bv.size()) +
66 "\noperand: " + std::to_string(op.size()) +
'\n' + operand.pretty());
72 prop.limplies(compare_literal, value_literal));
virtual const bvt & convert_bv(const exprt &expr, const std::optional< std::size_t > expected_width={})
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...