array_convt Member List

This is the complete list of members for array_convt, including all inherited members.

add_array_constraints_for_solving() override	array_convt	virtual
add_array_equalities()	array_convt
add_array_equality(unsigned int arr1_id, unsigned int arr2_id, unsigned int arr1_update, unsigned int arr2_update, smt_astt &result, unsigned int start_pos=0)	array_convt
add_initial_ackerman_constraints(const ast_vect &vals, const index_map_containert &idx_map, unsigned int start_point)	array_convt
add_new_indexes()	array_convt
apply_new_selects()	array_convt
array_convt(smt_solver_baset *_ctx)	array_convt
array_equalities	array_convt
array_iface(bool _b, bool inf)	array_iface	inline
array_indexes	array_convt
array_ite(smt_astt cond, const array_ast *true_arr, const array_ast *false_arr, const smt_sort *thesort)	array_convt
array_of_val_containert typedef	array_convt
array_of_val_rect typedef	array_convt
array_of_vals	array_convt
array_relations	array_convt
array_select_containert typedef	array_convt
array_selects	array_convt
array_selectt typedef	array_convt
array_subtypes	array_convt
array_update_containert typedef	array_convt
array_update_vect typedef	array_convt
array_updates	array_convt
array_valuation	array_convt
array_witht typedef	array_convt
ast_vect typedef	array_convt
can_init_infinite_arrays	array_iface
collate_array_values(ast_vect &vals, unsigned int base_array_id, unsigned int array_update_no, const smt_sort *subtype, unsigned int start_point, smt_astt init_val=nullptr, const initial_readert *reader=nullptr)	array_convt
convert_array_assign(const array_ast *src, smt_astt sym)	array_convt
convert_array_of(smt_astt init_val, unsigned long domain_width) override	array_convt	virtual
convert_array_of_wsort(smt_astt init_val, unsigned long domain_width, smt_sortt arr_sort)	array_convt	virtual
ctx	array_convt
default_convert_array_of(smt_astt init_val, unsigned long domain_width, smt_solver_baset *ctx)	array_iface
encode_array_equality(const array_ast *a1, const array_ast *a2)	array_convt
execute_array_ite(ast_vect &dest, const ast_vect &true_vals, const ast_vect &false_vals, const index_map_containert &idx_map, smt_astt cond, unsigned int start_point)	array_convt
execute_array_joining_ite(ast_vect &dest, unsigned int cur_id, const array_ast *true_arr_ast, const array_ast *false_arr_ast, const index_map_containert &idx_map, smt_astt cond, smt_sortt subtype, unsigned int start_point)	array_convt
execute_array_trans(array_update_vect &data, unsigned int arr, unsigned int idx, const smt_sort *subtype, unsigned int start_point)	array_convt
execute_array_update(ast_vect &dest_data, ast_vect &src_data, const index_map_containert &idx_map, const expr2tc &idx, smt_astt val, unsigned int start_point)	array_convt
execute_new_updates()	array_convt
expr_index_map	array_convt
get_array_elem(smt_astt a, uint64_t index, const type2tc &subtype) override	array_convt	virtual
get_array_update(unsigned int id, unsigned int up)	array_convt	inline
idx_record_containert typedef	array_convt
index_map_containert typedef	array_convt
index_map_rect typedef	array_convt
initial_readers	array_convt
initial_readert typedef	array_convt
join_array_indexes()	array_convt
mk_array_symbol(const std::string &name, const smt_sort *ms, smt_sortt subtype) override	array_convt
array_iface::mk_array_symbol(const std::string &name, smt_sortt sort, smt_sortt subtype)=0	array_iface	pure virtual
mk_bounded_array_equality(const array_ast *a1, const array_ast *a2)	array_convt
mk_select(const array_ast *array, const expr2tc &idx, const smt_sort *ressort)	array_convt
mk_store(const array_ast *array, const expr2tc &idx, smt_astt value, const smt_sort *ressort)	array_convt	virtual
mk_unbounded_select(const array_ast *array, const expr2tc &idx, const smt_sort *ressort)	array_convt
mk_unbounded_store(const array_ast *array, const expr2tc &idx, smt_astt value, const smt_sort *ressort)	array_convt
new_array_id()	array_convt
new_ast(smt_sortt _s)	array_convt	inline
new_ast(smt_sortt _s, const std::vector< smt_astt > &_a)	array_convt	inline
num_arrays_history	array_convt
pop_array_ctx() override	array_convt	virtual
push_array_ctx() override	array_convt	virtual
set_initial_reader(smt_astt array, initial_readert reader)	array_convt
supports_bools_in_arrays	array_iface
touched_array_sett typedef	array_convt
touched_arrayt typedef	array_convt
unbounded_array_ite(smt_astt cond, const array_ast *true_arr, const array_ast *false_arr, const smt_sort *thesort)	array_convt
~array_convt()=default	array_convt