21 DATA_INVARIANT(operands.size() >= 2,
"cond must have at least two operands");
24 operands.size() % 2 == 0,
"number of cond operands must be even");
33 bv =
prop.new_variables(width);
35 for(
const auto &operand : expr.
operands())
39 cond_literal =
convert(operand);
40 cond_literal=
prop.land(!previous_cond, cond_literal);
42 previous_cond=
prop.lor(previous_cond, cond_literal);
50 prop.l_set_to_true(
prop.limplies(cond_literal, value_literal));
61 for(std::size_t i=expr.
operands().size(); i!=0; i-=2)
65 "since the number of operands is even if i is nonzero it must be "
74 for(std::size_t j = 0; j < bv.size(); j++)
75 bv[j] =
prop.lselect(cond_literal, op[j], bv[j]);
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_cond(const cond_exprt &)
virtual std::size_t boolbv_width(const typet &type) const
this is a parametric version of an if-expression: it returns the value of the first case (using the o...
Base class for all expressions.
std::vector< exprt > operandst
typet & type()
Return the type of the expression.
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
std::vector< literalt > bvt
literalt const_literal(bool value)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.