Method get_map_array_sort

src/ast/rewriter/array_rewriter.cpp:401–407

}

sort_ref array_rewriter::get_map_array_sort(func_decl* f, unsigned num_args, expr* const* args) {
    sort* s0 = args[0]->get_sort();
    unsigned sz = get_array_arity(s0);
    ptr_vector<sort> domain;
    for (unsigned i = 0; i < sz; ++i) domain.push_back(get_array_domain(s0, i));
    return sort_ref(m_util.mk_array_sort(sz, domain.data(), f->get_range()), m());
}

br_status array_rewriter::mk_map_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {