15 const std::vector<exprt> &operands=expr.
operands();
30 throw "case takes at least three operands";
32 if((operands.size()%2)!=1)
33 throw "number of case operands must be odd";
35 enum { FIRST, COMPARE,
VALUE } what=FIRST;
52 if(compare_bv.size()!=op.size())
54 std::cerr <<
"compare operand: " << compare_bv.size()
55 <<
"\noperand: " << op.size() <<
'\n' 59 throw "size of compare operand does not match";
63 compare_literal=
prop.
land(!previous_compare, compare_literal);
65 previous_compare=
prop.
lor(previous_compare, compare_literal);
71 if(bv.size()!=op.size())
73 std::cerr <<
"result size: " << bv.size()
74 <<
"\noperand: " << op.size() <<
'\n' 78 throw "size of value operand does not match";
virtual bvt convert_case(const exprt &expr)
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
boolbv_widtht boolbv_width
virtual literalt lor(literalt a, literalt b)=0
virtual literalt limplies(literalt a, literalt b)=0
void l_set_to_true(literalt a)
virtual literalt land(literalt a, literalt b)=0
virtual literalt new_variable()=0
#define Forall_literals(it, bv)
virtual const bvt & convert_bv(const exprt &expr)
void conversion_failed(const exprt &expr, bvt &bv)
#define forall_operands(it, expr)
literalt const_literal(bool value)
Base class for all expressions.
std::vector< literalt > bvt