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_if(const if_exprt &expr)
virtual std::size_t boolbv_width(const typet &type) const
bvt select(literalt s, const bvt &a, const bvt &b)
If s is true, selects a otherwise selects b.
typet & type()
Return the type of the expression.
The trinary if-then-else operator.
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
std::vector< literalt > bvt