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";
30 bv=
prop.new_variables(width);
36 for(
const auto &op : expr.
operands())
40 if(it_bv.size()!=bv.size())
41 throw "constraint_select_one expects matching width";
43 b.push_back(
bv_utils.equal(bv, it_bv));
51 for(
const auto &op : expr.
operands())
59 if(op_bv.size()!=bv.size())
62 for(std::size_t i=0; i<op_bv.size(); i++)
63 bv[i]=
prop.lselect(
prop.new_variable(), bv[i], op_bv[i]);
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...
virtual bvt convert_constraint_select_one(const exprt &expr)
bvt conversion_failed(const exprt &expr)
Print that the expression of x has failed conversion, then return a vector of x's width.
virtual std::size_t boolbv_width(const typet &type) const
Base class for all expressions.
std::vector< exprt > operandst
typet & type()
Return the type of the expression.
const irep_idt & id() const
std::vector< literalt > bvt
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.