26 throw "cond takes at least two operands";
28 if((operands.size()%2)!=0)
29 throw "number of cond operands must be even";
46 cond_literal=
prop.
land(!previous_cond, cond_literal);
48 previous_cond=
prop.
lor(previous_cond, cond_literal);
55 bv.size() == op.size(),
56 std::string(
"size of value operand does not match:\n") +
71 for(std::size_t i=expr.
operands().size(); i!=0; i-=2)
81 if(bv.size()!=op.size())
82 throw "unexpected operand size in convert_cond";
84 for(std::size_t i=0; i<bv.size(); i++)
literalt convert(const exprt &expr) override
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)
virtual bvt convert_cond(const exprt &expr)
std::vector< exprt > operandst
literalt const_literal(bool value)
Base class for all expressions.
virtual bool has_set_to() const
std::string to_string(const string_constraintt &expr)
Used for debug printing.
virtual literalt lselect(literalt a, literalt b, literalt c)=0
#define DATA_INVARIANT(CONDITION, REASON)
std::vector< literalt > bvt