Method get_array_interp_core

src/model/func_interp.cpp:399–449

}

expr_ref func_interp::get_array_interp_core(func_decl * f) const {
    expr_ref r(m());
    if (m_else == nullptr) 
        return r;
    ptr_vector<sort> domain;
    for (sort* s : *f) 
        domain.push_back(s);    

    bool ground = is_ground(m_else);
    for (func_entry * curr : m_entries) {
        ground &= is_ground(curr->get_result());
        for (unsigned i = 0; i < m_arity; ++i) 
            ground &= is_ground(curr->get_arg(i));        
    }
    if (!ground) {
        r = get_interp();
        if (!r) return r;
        sort_ref_vector sorts(m());
        expr_ref_vector vars(m());
        svector<symbol> var_names;
        var_subst sub(m(), false);
        for (unsigned i = 0; i < m_arity; ++i) {
            var_names.push_back(symbol(i));
            sorts.push_back(domain.get(i));
            vars.push_back(m().mk_var(m_arity - i - 1, sorts.back()));
        }
        r = sub(r, vars);
        r = m().mk_lambda(sorts.size(), sorts.data(), var_names.data(), r);        
        return r;
    }

    expr_ref_vector args(m());
    array_util autil(m());
    sort_ref A(autil.mk_array_sort(domain.size(), domain.data(), m_else->get_sort()), m());
    r = autil.mk_const_array(A, m_else);
    for (func_entry * curr : m_entries) {
        expr * res = curr->get_result();

        if (m_else == res) {
            continue;
        }
        args.reset();
        args.push_back(r);        
        for (unsigned i = 0; i < m_arity; ++i) {
            args.push_back(curr->get_arg(i));
        }
        args.push_back(res);
        r = autil.mk_store(args);
    }
    return r;    
}

   
expr * func_interp::get_interp() const {