9#ifndef CPROVER_SOLVERS_FLATTENING_LITERAL_VECTOR_EXPR_H
10#define CPROVER_SOLVERS_FLATTENING_LITERAL_VECTOR_EXPR_H
30 result.reserve(sub.size());
31 for(
auto &literal_irep : sub)
45 sub.reserve(
bv.size());
46 for(
auto &literal :
bv)
47 sub.emplace_back(
irept{std::to_string(literal.get())});
54 return base.
id() == ID_literal_vector;
Base class for all expressions.
static void check(const exprt &, const validation_modet)
Check that the expression is well-formed (shallow checks only, i.e., subexpressions and its type are ...
There are a large number of kinds of tree structured or tree-like data in CPROVER.
const irept & find(const irep_idt &name) const
const irep_idt & id() const
irept & add(const irep_idt &name)
literal_vector_exprt(const bvt &__bv, typet __type)
nullary_exprt(const irep_idt &_id, typet _type)
The type of an expression, extends irept.
std::vector< literalt > bvt
const literal_vector_exprt & to_literal_vector_expr(const exprt &expr)
Cast a generic exprt to a literal_vector_exprt.
bool can_cast_expr< literal_vector_exprt >(const exprt &base)
#define PRECONDITION(CONDITION)
API to expression classes.
signed long long int unsafe_string2signedlonglong(const std::string &str, int base)