Go to the documentation of this file.
16 if(expr.
id()!=ID_constraint_select_one)
17 throw "expected constraint_select_one expression";
20 throw "constraint_select_one takes at least one operand";
23 throw "constraint_select_one expects matching types";
40 if(it_bv.size()!=bv.size())
41 throw "constraint_select_one expects matching width";
59 if(op_bv.size()!=bv.size())
62 for(std::size_t i=0; i<op_bv.size(); i++)
bvt new_variables(std::size_t width)
generates a bitvector of given width with new variables
std::vector< literalt > bvt
virtual literalt new_variable()=0
Base class for all expressions.
typet & type()
Return the type of the expression.
boolbv_widtht boolbv_width
void conversion_failed(const exprt &expr, bvt &bv)
#define forall_operands(it, expr)
const irep_idt & id() const
std::vector< exprt > operandst
virtual bvt convert_constraint_select_one(const exprt &expr)
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...
virtual bool has_set_to() const
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
virtual literalt lselect(literalt a, literalt b, literalt c)=0
void lcnf(literalt l0, literalt l1)