19 if(expr.
id()!=ID_index)
20 throw "expected index expression";
23 throw "index takes two operands";
32 if(array_op_type.
id()==ID_array)
51 for(std::size_t i=0; i<width; i++)
58 if(array.
id()==ID_symbol)
71 throw "failed to convert array size";
84 #define UNIFORM_ARRAY_HACK 85 #ifdef UNIFORM_ARRAY_HACK 86 bool is_uniform =
false;
88 if(array.
id()==ID_array_of)
92 else if(array.
id()==ID_constant || array.
id()==ID_array)
94 bool found_exception =
false;
97 if(*it != array.
op0())
99 found_exception =
true;
110 static int uniform_array_counter;
112 std::string identifier=
113 "__CPROVER_internal_uniform_array_"+
114 std::to_string(uniform_array_counter++);
126 if(lower_bound.lhs().is_nil() ||
128 throw "number conversion failed (2)";
130 and_exprt range_condition(lower_bound, upper_bound);
141 #define ACTUAL_ARRAY_HACK 142 #ifdef ACTUAL_ARRAY_HACK 145 if((array.
id()==ID_constant || array.
id()==ID_array) &&
148 #ifdef CONSTANT_ARRAY_HACK 153 static int actual_array_counter;
155 std::string identifier=
156 "__CPROVER_internal_actual_array_"+
157 std::to_string(actual_array_counter++);
165 index_equality.
lhs()=index;
170 #ifdef COMPACT_EQUAL_CONST 175 exprt::operandst::const_iterator it = array.
operands().begin();
182 throw "number conversion failed (1)";
184 assert(it != array.
operands().end());
186 value_equality.
rhs()=*it++;
208 if(array_size*width!=array_bv.size())
209 throw "unexpected array size";
219 for(std::size_t i=0; i<width; i++)
225 index_equality.
lhs()=index;
227 #ifdef COMPACT_EQUAL_CONST 232 equal_bv.resize(width);
239 throw "number conversion failed (1)";
243 for(std::size_t j=0; j<width; j++)
258 #ifdef COMPACT_EQUAL_CONST 264 assert(array_size>0);
274 for(std::size_t j=0; j<width; j++)
333 for(std::size_t i=0; i<width; i++)
339 for(std::size_t i=0; i<width; i++)
map_entryt & get_map_entry(const irep_idt &identifier, const typet &type)
The type of an expression.
const typet & follow(const typet &src) const
A generic base class for relations, i.e., binary predicates.
virtual literalt convert(const exprt &expr) override
exprt simplify_expr(const exprt &src, const namespacet &ns)
boolbv_widtht boolbv_width
bool is_unbounded_array(const typet &type) const override
#define forall_expr(it, expr)
virtual literalt limplies(literalt a, literalt b)=0
void l_set_to_true(literalt a)
virtual literalt land(literalt a, literalt b)=0
const irep_idt & id() const
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
virtual literalt new_variable()=0
virtual const bvt & convert_bv(const exprt &expr)
API to expression classes.
void conversion_failed(const exprt &expr, bvt &bv)
const exprt & size() const
virtual literalt lequal(literalt a, literalt b)=0
virtual literalt equality(const exprt &e1, const exprt &e2)
void record_array_index(const index_exprt &expr)
Base class for all expressions.
virtual bvt convert_index(const exprt &array, const mp_integer &index)
index operator with constant index
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
virtual bool has_set_to() const
Expression to hold a symbol (variable)
virtual literalt lselect(literalt a, literalt b, literalt c)=0
std::size_t integer2size_t(const mp_integer &n)
const typet & subtype() const
std::vector< literalt > bvt