Go to the documentation of this file.
25 DATA_INVARIANT(operands.size() >= 2,
"cond must have at least two operands");
28 operands.size() % 2 == 0,
"number of cond operands must be even");
45 cond_literal=
prop.
land(!previous_cond, cond_literal);
47 previous_cond=
prop.
lor(previous_cond, cond_literal);
64 for(std::size_t i=expr.
operands().size(); i!=0; i-=2)
68 "since the number of operands is even if i is nonzero it must be "
77 for(std::size_t j = 0; j < bv.size(); j++)
virtual bvt convert_cond(const cond_exprt &)
std::size_t size() const
Amount of nodes this expression tree contains.
std::vector< literalt > bvt
virtual literalt new_variable()=0
Base class for all expressions.
virtual literalt lor(literalt a, literalt b)=0
void l_set_to_true(literalt a)
virtual literalt land(literalt a, literalt b)=0
#define Forall_literals(it, bv)
typet & type()
Return the type of the expression.
boolbv_widtht boolbv_width
void conversion_failed(const exprt &expr, bvt &bv)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
virtual literalt limplies(literalt a, literalt b)=0
#define forall_operands(it, expr)
literalt const_literal(bool value)
std::vector< exprt > operandst
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...
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
this is a parametric version of an if-expression: it returns the value of the first case (using the o...
virtual bool has_set_to() const
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
virtual literalt lselect(literalt a, literalt b, literalt c)=0