自学教程：C++ to_sort函数代码示例

    Z3_func_decl Z3_API Z3_mk_injective_function(Z3_context c,                                                  Z3_symbol s,                                                  unsigned domain_size,                                                  Z3_sort const domain[],                                                 Z3_sort range) {        Z3_TRY;        LOG_Z3_mk_injective_function(c, s, domain_size, domain, range);        RESET_ERROR_CODE();         ast_manager & m = mk_c(c)->m();        mk_c(c)->reset_last_result();        sort* range_ = to_sort(range);        func_decl* d = m.mk_func_decl(to_symbol(s), domain_size, to_sorts(domain), range_);        expr_ref_vector args(m);        expr_ref fn(m), body(m);        vector<symbol> names;        for (unsigned i = 0; i < domain_size; ++i) {            unsigned idx = domain_size-i-1;            args.push_back(m.mk_var(idx, to_sort(domain[i])));            names.push_back(symbol(idx));        }        fn = m.mk_app(d, args.size(), args.c_ptr());        for (unsigned i = 0; i < domain_size; ++i) {            expr* arg = args[i].get();            sort* dom = m.get_sort(arg);            func_decl* inv = m.mk_fresh_func_decl(symbol("inv"), to_symbol(s), 1, &range_, dom);            body = m.mk_eq(m.mk_app(inv, fn.get()), arg);            body = m.mk_forall(args.size(), to_sorts(domain), names.c_ptr(), body.get());            mk_c(c)->save_multiple_ast_trail(body.get());            mk_c(c)->assert_cnstr(body.get());        }        mk_c(c)->save_multiple_ast_trail(d);               RETURN_Z3(of_func_decl(d));        Z3_CATCH_RETURN(0);    }

 Z3_sort Z3_API Z3_mk_array_sort(Z3_context c, Z3_sort domain, Z3_sort range) {     Z3_TRY;     LOG_Z3_mk_array_sort(c, domain, range);     RESET_ERROR_CODE();       parameter params[2]  = { parameter(to_sort(domain)), parameter(to_sort(range)) };     sort * ty =  mk_c(c)->m().mk_sort(mk_c(c)->get_array_fid(), ARRAY_SORT, 2, params);     mk_c(c)->save_ast_trail(ty);     RETURN_Z3(of_sort(ty));     Z3_CATCH_RETURN(0); }

sort * bvarray2uf_rewriter_cfg::get_index_sort(sort * s) {    SASSERT(s->get_num_parameters() >= 2);    unsigned total_width = 0;    for (unsigned i = 0; i < s->get_num_parameters() - 1; i++) {        parameter const & p = s->get_parameter(i);        SASSERT(p.is_ast() && is_sort(to_sort(p.get_ast())));        SASSERT(m_bv_util.is_bv_sort(to_sort(p.get_ast())));        total_width += m_bv_util.get_bv_size(to_sort(p.get_ast()));    }    return m_bv_util.mk_sort(total_width);}

void tst_model_retrieval(){              memory::initialize(0);    front_end_params params;    params.m_model = true;    ast_manager m;    m.register_decl_plugins();    family_id array_fid = m.get_family_id(symbol("array"));    array_util au(m);    array_decl_plugin& ad = *static_cast<array_decl_plugin *>(m.get_plugin(array_fid));    // arr_s and select_fn creation copy-pasted from z3.cpp    parameter sparams[2]  = { parameter(to_sort(m.mk_bool_sort())), parameter(to_sort(m.mk_bool_sort())) };    sort_ref arr_s(m.mk_sort(array_fid, ARRAY_SORT, 2, sparams), m);    sort * domain2[2] = {arr_s, m.mk_bool_sort()};    func_decl_ref select_fn(        m.mk_func_decl(array_fid, OP_SELECT, 2, arr_s->get_parameters(), 2, domain2), m);    app_ref a1(m.mk_const(symbol("a1"), arr_s), m);    app_ref a2(m.mk_const(symbol("a2"), arr_s), m);    // (= true (select a1 true))    app_ref fml(m.mk_eq(m.mk_true(),        m.mk_app(select_fn.get(), a1, m.mk_true())), m);    smt::context ctx(m, params);    ctx.assert_expr(fml);    lbool check_result = ctx.check();    std::cout<<((check_result==l_true) ? "satisfiable" :                 (check_result==l_false) ? "unsatisfiable" : "unknown")<<"/n";    ref<model> model;    ctx.get_model(model);    model_v2_pp(std::cout, *model, false);    expr_ref a1_val(model->get_const_interp(a1->get_decl()), m);    app_ref fml2(m.mk_eq(a2, a1_val), m);    ctx.assert_expr(fml2);    std::cout<<"--------------------------/n";    ctx.display(std::cout);    std::cout<<"--------------------------/n";    check_result = ctx.check();    ctx.display(std::cout);    std::cout<<"--------------------------/n";    std::cout<<((check_result==l_true) ? "satisfiable" :                 (check_result==l_false) ? "unsatisfiable" : "unknown")<<"/n";}

 Z3_sort Z3_API Z3_get_array_sort_range(Z3_context c, Z3_sort t) {     Z3_TRY;     LOG_Z3_get_array_sort_range(c, t);     RESET_ERROR_CODE();      CHECK_VALID_AST(t, 0);     if (to_sort(t)->get_family_id() == mk_c(c)->get_array_fid() &&          to_sort(t)->get_decl_kind() == ARRAY_SORT) {         Z3_sort r = reinterpret_cast<Z3_sort>(to_sort(t)->get_parameter(1).get_ast());         RETURN_Z3(r);     }     SET_ERROR_CODE(Z3_INVALID_ARG);     RETURN_Z3(0);     Z3_CATCH_RETURN(0); }

 Z3_ast parse_smtlib2_stream(bool exec, Z3_context c, std::istream& is,                             unsigned num_sorts,                             Z3_symbol const sort_names[],                             Z3_sort const sorts[],                             unsigned num_decls,                             Z3_symbol const decl_names[],                             Z3_func_decl const decls[]) {     Z3_TRY;     cmd_context ctx(&mk_c(c)->fparams(), false, &(mk_c(c)->m()));     ctx.set_ignore_check(true);     if (exec) {         ctx.set_solver(alloc(z3_context_solver, *mk_c(c)));     }     for (unsigned i = 0; i < num_decls; ++i) {        ctx.insert(to_symbol(decl_names[i]), to_func_decl(decls[i]));     }     for (unsigned i = 0; i < num_sorts; ++i) {         psort* ps = ctx.pm().mk_psort_cnst(to_sort(sorts[i]));         ctx.insert(ctx.pm().mk_psort_user_decl(0, to_symbol(sort_names[i]), ps));     }     if (!parse_smt2_commands(ctx, is)) {         SET_ERROR_CODE(Z3_PARSER_ERROR);         return of_ast(mk_c(c)->m().mk_true());     }     ptr_vector<expr>::const_iterator it  = ctx.begin_assertions();     ptr_vector<expr>::const_iterator end = ctx.end_assertions();     unsigned size = static_cast<unsigned>(end - it);     return of_ast(mk_c(c)->mk_and(size, it));     Z3_CATCH_RETURN(0); }

func_decl * float_decl_plugin::mk_float_const_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,                                                   unsigned arity, sort * const * domain, sort * range) {    sort * s;    if (num_parameters == 1 && parameters[0].is_ast() && is_sort(parameters[0].get_ast()) && is_float_sort(to_sort(parameters[0].get_ast()))) {        s = to_sort(parameters[0].get_ast());    }    else if (range != 0 && is_float_sort(range)) {        s = range;    }    else {        m_manager->raise_exception("sort of floating point constant was not specified");    }    SASSERT(is_sort_of(s, m_family_id, FLOAT_SORT));        unsigned ebits = s->get_parameter(0).get_int();    unsigned sbits = s->get_parameter(1).get_int();    scoped_mpf val(m_fm);    if (k == OP_FLOAT_NAN) {        m_fm.mk_nan(ebits, sbits, val);        SASSERT(m_fm.is_nan(val));    }    else if (k == OP_FLOAT_MINUS_INF) {        m_fm.mk_ninf(ebits, sbits, val);    }    else {        SASSERT(k == OP_FLOAT_PLUS_INF);        m_fm.mk_pinf(ebits, sbits, val);    }    return mk_value_decl(val);}

 sort * dl_decl_plugin::mk_relation_sort( unsigned num_parameters, parameter const * parameters) {             bool is_finite = true;     rational r(1);     for (unsigned i = 0; is_finite && i < num_parameters; ++i) {         if (!parameters[i].is_ast() || !is_sort(parameters[i].get_ast())) {             m_manager->raise_exception("expecting sort parameters");             return 0;         }         sort* s = to_sort(parameters[i].get_ast());         sort_size sz1 = s->get_num_elements();         if (sz1.is_finite()) {             r *= rational(sz1.size(),rational::ui64());         }         else {             is_finite = false;         }     }     sort_size sz;     if (is_finite && r.is_uint64()) {         sz = sort_size::mk_finite(r.get_uint64());     }     else {         sz = sort_size::mk_very_big();     }     sort_info info(m_family_id, DL_RELATION_SORT, sz, num_parameters, parameters);     return m_manager->mk_sort(symbol("Table"),info); }

bool fpa_util::contains_floats(ast * a) {    switch (a->get_kind()) {    case AST_APP: {        app * aa = to_app(a);        if (contains_floats(aa->get_decl()))            return true;        else            for (unsigned i = 0; i < aa->get_num_args(); i++)                if (contains_floats(aa->get_arg(i)))                    return true;        break;    }    case AST_VAR:        return contains_floats(to_var(a)->get_sort());        break;    case AST_QUANTIFIER: {        quantifier * q = to_quantifier(a);        for (unsigned i = 0; i < q->get_num_children(); i++)            if (contains_floats(q->get_child(i)))                return true;        for (unsigned i = 0; i < q->get_num_decls(); i++)            if (contains_floats(q->get_decl_sort(i)))                return true;        if (contains_floats(q->get_expr()))            return true;        break;    }    case AST_SORT: {        sort * s = to_sort(a);        if (is_float(s) || is_rm(s))            return true;        else {            for (unsigned i = 0; i < s->get_num_parameters(); i++) {                parameter const & pi = s->get_parameter(i);                if (pi.is_ast() && contains_floats(pi.get_ast()))                    return true;            }        }        break;    }    case AST_FUNC_DECL: {        func_decl * f = to_func_decl(a);        for (unsigned i = 0; i < f->get_arity(); i++)            if (contains_floats(f->get_domain(i)))                return true;        if (contains_floats(f->get_range()))            return true;        for (unsigned i = 0; i < f->get_num_parameters(); i++) {            parameter const & pi = f->get_parameter(i);            if (pi.is_ast() && contains_floats(pi.get_ast()))                return true;        }        break;    }    default:        UNREACHABLE();    }    return false;}

 Z3_ast Z3_API Z3_mk_fpa_zero(Z3_context c, Z3_sort s, Z3_bool negative) {     Z3_TRY;     LOG_Z3_mk_fpa_inf(c, s, negative);     RESET_ERROR_CODE();     CHECK_VALID_AST(s, nullptr);     if (!is_fp_sort(c, s)) {         SET_ERROR_CODE(Z3_INVALID_ARG);         RETURN_Z3(nullptr);     }     api::context * ctx = mk_c(c);     expr * a = negative != 0 ? ctx->fpautil().mk_nzero(to_sort(s)) :                                ctx->fpautil().mk_pzero(to_sort(s));     ctx->save_ast_trail(a);     RETURN_Z3(of_expr(a));     Z3_CATCH_RETURN(nullptr); }

 Z3_ast Z3_API Z3_mk_fpa_to_fp_unsigned(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s) {     Z3_TRY;     LOG_Z3_mk_fpa_to_fp_unsigned(c, rm, t, s);     RESET_ERROR_CODE();     api::context * ctx = mk_c(c);     fpa_util & fu = ctx->fpautil();     if (!fu.is_rm(to_expr(rm)) ||         !ctx->bvutil().is_bv(to_expr(t)) ||         !fu.is_float(to_sort(s))) {         SET_ERROR_CODE(Z3_INVALID_ARG);         return nullptr;     }     expr * a = fu.mk_to_fp_unsigned(to_sort(s), to_expr(rm), to_expr(t));     ctx->save_ast_trail(a);     RETURN_Z3(of_expr(a));     Z3_CATCH_RETURN(nullptr); }

 Z3_bool Z3_API Z3_is_string_sort(Z3_context c, Z3_sort s) {     Z3_TRY;     LOG_Z3_is_string_sort(c, s);     RESET_ERROR_CODE();     bool result = mk_c(c)->sutil().is_string(to_sort(s));     return result?Z3_TRUE:Z3_FALSE;     Z3_CATCH_RETURN(Z3_FALSE); }

 Z3_ast_vector Z3_API Z3_model_get_sort_universe(Z3_context c, Z3_model m, Z3_sort s) {     Z3_TRY;     LOG_Z3_model_get_sort_universe(c, m, s);     RESET_ERROR_CODE();     if (!to_model_ref(m)->has_uninterpreted_sort(to_sort(s))) {         SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);         RETURN_Z3(nullptr);     }     ptr_vector<expr> const & universe = to_model_ref(m)->get_universe(to_sort(s));     Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());     mk_c(c)->save_object(v);     for (expr * e : universe) {         v->m_ast_vector.push_back(e);     }     RETURN_Z3(of_ast_vector(v));     Z3_CATCH_RETURN(nullptr); }

 Z3_ast Z3_API Z3_mk_fpa_to_fp_int_real(Z3_context c, Z3_ast rm, Z3_ast exp, Z3_ast sig, Z3_sort s) {     Z3_TRY;     LOG_Z3_mk_fpa_to_fp_int_real(c, rm, exp, sig, s);     RESET_ERROR_CODE();     api::context * ctx = mk_c(c);     fpa_util & fu = ctx->fpautil();     if (!fu.is_rm(to_expr(rm)) ||         !ctx->autil().is_int(to_expr(exp)) ||         !ctx->autil().is_real(to_expr(sig)) ||         !fu.is_float(to_sort(s))) {         SET_ERROR_CODE(Z3_INVALID_ARG);         return nullptr;     }     expr * a = fu.mk_to_fp(to_sort(s), to_expr(rm), to_expr(exp), to_expr(sig));     ctx->save_ast_trail(a);     RETURN_Z3(of_expr(a));     Z3_CATCH_RETURN(nullptr); }

static sort * get_type(ast_manager & m, family_id datatype_fid, sort * source_datatype, parameter const & p) {    SASSERT(p.is_ast() || p.is_int());    if (p.is_ast()) {        return to_sort(p.get_ast());    }    else {        return get_other_datatype(m, datatype_fid, source_datatype, p.get_int());    }}

 Z3_sort Z3_API Z3_mk_re_sort(Z3_context c, Z3_sort domain) {     Z3_TRY;     LOG_Z3_mk_re_sort(c, domain);     RESET_ERROR_CODE();     sort * ty =  mk_c(c)->sutil().re.mk_re(to_sort(domain));     mk_c(c)->save_ast_trail(ty);     RETURN_Z3(of_sort(ty));     Z3_CATCH_RETURN(0); }

 Z3_ast_vector Z3_API Z3_model_get_sort_universe(Z3_context c, Z3_model m, Z3_sort s) {     Z3_TRY;     LOG_Z3_model_get_sort_universe(c, m, s);     RESET_ERROR_CODE();     if (!to_model_ref(m)->has_uninterpreted_sort(to_sort(s))) {         SET_ERROR_CODE(Z3_INVALID_ARG);         RETURN_Z3(0);     }     ptr_vector<expr> const & universe = to_model_ref(m)->get_universe(to_sort(s));     Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, mk_c(c)->m());     mk_c(c)->save_object(v);     unsigned sz = universe.size();     for (unsigned i = 0; i < sz; i++) {         v->m_ast_vector.push_back(universe[i]);     }     RETURN_Z3(of_ast_vector(v));     Z3_CATCH_RETURN(0); }

 Z3_ast Z3_API Z3_mk_bound(Z3_context c, unsigned index, Z3_sort ty) {     Z3_TRY;     LOG_Z3_mk_bound(c, index, ty);     RESET_ERROR_CODE();     ast* a = mk_c(c)->m().mk_var(index, to_sort(ty));     mk_c(c)->save_ast_trail(a);     RETURN_Z3(of_ast(a));     Z3_CATCH_RETURN(0); }

 Z3_ast Z3_API Z3_mk_fpa_numeral_int(Z3_context c, signed v, Z3_sort ty) {     Z3_TRY;     LOG_Z3_mk_fpa_numeral_int(c, v, ty);     RESET_ERROR_CODE();     if (!is_fp_sort(c, ty)) {         SET_ERROR_CODE(Z3_INVALID_ARG, "fp sort expected");         RETURN_Z3(nullptr);     }     api::context * ctx = mk_c(c);     scoped_mpf tmp(ctx->fpautil().fm());     ctx->fpautil().fm().set(tmp,                             ctx->fpautil().get_ebits(to_sort(ty)),                             ctx->fpautil().get_sbits(to_sort(ty)),                             v);     expr * a = ctx->fpautil().mk_value(tmp);     ctx->save_ast_trail(a);     RETURN_Z3(of_expr(a));     Z3_CATCH_RETURN(nullptr); }

 Z3_ast Z3_API Z3_mk_fpa_numeral_int64_uint64(Z3_context c, Z3_bool sgn, int64_t exp, uint64_t sig, Z3_sort ty) {     Z3_TRY;     LOG_Z3_mk_fpa_numeral_int64_uint64(c, sgn, exp, sig, ty);     RESET_ERROR_CODE();     if (!is_fp_sort(c, ty)) {         SET_ERROR_CODE(Z3_INVALID_ARG);         RETURN_Z3(nullptr);     }     api::context * ctx = mk_c(c);     scoped_mpf tmp(ctx->fpautil().fm());     ctx->fpautil().fm().set(tmp,                             ctx->fpautil().get_ebits(to_sort(ty)),                             ctx->fpautil().get_sbits(to_sort(ty)),                             sgn != 0, exp, sig);     expr * a = ctx->fpautil().mk_value(tmp);     ctx->save_ast_trail(a);     RETURN_Z3(of_expr(a));     Z3_CATCH_RETURN(nullptr); }

 Z3_ast Z3_API Z3_mk_int(Z3_context c, int value, Z3_sort ty) {     Z3_TRY;     LOG_Z3_mk_int(c, value, ty);     RESET_ERROR_CODE();     if (!check_numeral_sort(c, ty)) {         RETURN_Z3(nullptr);     }     ast * a = mk_c(c)->mk_numeral_core(rational(value), to_sort(ty));     RETURN_Z3(of_ast(a));     Z3_CATCH_RETURN(nullptr); }

 Z3_ast Z3_API Z3_mk_fpa_to_fp_bv(Z3_context c, Z3_ast bv, Z3_sort s) {     Z3_TRY;     LOG_Z3_mk_fpa_to_fp_bv(c, bv, s);     RESET_ERROR_CODE();     if (!is_bv(c, bv) || !is_fp_sort(c, s)) {         SET_ERROR_CODE(Z3_INVALID_ARG);         RETURN_Z3(nullptr);     }     api::context * ctx = mk_c(c);     fpa_util & fu = ctx->fpautil();     if (!ctx->bvutil().is_bv(to_expr(bv)) ||         !fu.is_float(to_sort(s))) {         SET_ERROR_CODE(Z3_INVALID_ARG);         return nullptr;     }     expr * a = fu.mk_to_fp(to_sort(s), to_expr(bv));     ctx->save_ast_trail(a);     RETURN_Z3(of_expr(a));     Z3_CATCH_RETURN(nullptr); }

bool is_numeral_sort(Z3_context c, Z3_sort ty) {    if (!ty) return false;    sort * _ty = to_sort(ty);    family_id fid  = _ty->get_family_id();    if (fid != mk_c(c)->get_arith_fid() &&        fid != mk_c(c)->get_bv_fid() &&        fid != mk_c(c)->get_datalog_fid() &&        fid != mk_c(c)->get_fpa_fid()) {        return false;    }    return true;}

 unsigned Z3_API Z3_get_relation_arity(Z3_context c, Z3_sort s) {     Z3_TRY;     LOG_Z3_get_relation_arity(c, s);     RESET_ERROR_CODE();     sort * r = to_sort(s);     if (Z3_get_sort_kind(c, s) != Z3_RELATION_SORT) {         SET_ERROR_CODE(Z3_INVALID_ARG);         return 0;     }     return r->get_num_parameters();     Z3_CATCH_RETURN(0); }

 Z3_ast Z3_API Z3_mk_unsigned_int64(Z3_context c, uint64_t value, Z3_sort ty) {     Z3_TRY;     LOG_Z3_mk_unsigned_int64(c, value, ty);     RESET_ERROR_CODE();     if (!check_numeral_sort(c, ty)) {         RETURN_Z3(nullptr);     }     rational n(value, rational::ui64());     ast * a = mk_c(c)->mk_numeral_core(n, to_sort(ty));     RETURN_Z3(of_ast(a));     Z3_CATCH_RETURN(nullptr); }

 unsigned Z3_API Z3_fpa_get_sbits(Z3_context c, Z3_sort s) {     Z3_TRY;     LOG_Z3_fpa_get_sbits(c, s);     RESET_ERROR_CODE();     CHECK_NON_NULL(s, 0);     CHECK_VALID_AST(s, 0);     if (!is_fp_sort(c, s)) {         SET_ERROR_CODE(Z3_INVALID_ARG);         RETURN_Z3(0);     }     return mk_c(c)->fpautil().get_sbits(to_sort(s));     Z3_CATCH_RETURN(0); }

void decl_collector::visit(ast* n) {    ptr_vector<ast> todo;    todo.push_back(n);    while (!todo.empty()) {        n = todo.back();        todo.pop_back();        if (!m_visited.is_marked(n)) {            m_visited.mark(n, true);                            switch(n->get_kind()) {            case AST_APP: {                app * a = to_app(n);                for (unsigned i = 0; i < a->get_num_args(); ++i) {                    todo.push_back(a->get_arg(i));                }                todo.push_back(a->get_decl());                break;            }                                case AST_QUANTIFIER: {                quantifier * q = to_quantifier(n);                unsigned num_decls = q->get_num_decls();                for (unsigned i = 0; i < num_decls; ++i) {                    todo.push_back(q->get_decl_sort(i));                }                todo.push_back(q->get_expr());                for (unsigned i = 0; i < q->get_num_patterns(); ++i) {                    todo.push_back(q->get_pattern(i));                }                break;            }            case AST_SORT:                 visit_sort(to_sort(n));                break;            case AST_FUNC_DECL: {                func_decl * d = to_func_decl(n);                for (unsigned i = 0; i < d->get_arity(); ++i) {                    todo.push_back(d->get_domain(i));                }                todo.push_back(d->get_range());                visit_func(d);                break;            }            case AST_VAR:                break;            default:                UNREACHABLE();            }        }    }}

void decl_collector::visit(ast* n) {    datatype_util util(m());    m_todo.push_back(n);    while (!m_todo.empty()) {        n = m_todo.back();        m_todo.pop_back();        if (!m_visited.is_marked(n)) {            switch(n->get_kind()) {            case AST_APP: {                app * a = to_app(n);                for (expr* arg : *a) {                    m_todo.push_back(arg);                }                m_todo.push_back(a->get_decl());                break;            }            case AST_QUANTIFIER: {                quantifier * q = to_quantifier(n);                unsigned num_decls = q->get_num_decls();                for (unsigned i = 0; i < num_decls; ++i) {                    m_todo.push_back(q->get_decl_sort(i));                }                m_todo.push_back(q->get_expr());                for (unsigned i = 0; i < q->get_num_patterns(); ++i) {                    m_todo.push_back(q->get_pattern(i));                }                break;            }            case AST_SORT:                 visit_sort(to_sort(n));                break;            case AST_FUNC_DECL: {                func_decl * d = to_func_decl(n);                for (sort* srt : *d) {                    m_todo.push_back(srt);                }                m_todo.push_back(d->get_range());                visit_func(d);                break;            }            case AST_VAR:                break;            default:                UNREACHABLE();            }            m_visited.mark(n, true);        }    }}

 Z3_ast mk_app_array_core(Z3_context c, Z3_sort domain, Z3_ast v) {     RESET_ERROR_CODE();        ast_manager & m = mk_c(c)->m();     expr * _v        = to_expr(v);     sort * _range = m.get_sort(_v);     sort * _domain = to_sort(domain);     parameter params[2]  = { parameter(_domain), parameter(_range) };     sort * a_ty    = mk_c(c)->m().mk_sort(mk_c(c)->get_array_fid(), ARRAY_SORT, 2, params);     parameter param(a_ty);     func_decl * cd   = m.mk_func_decl(mk_c(c)->get_array_fid(), OP_CONST_ARRAY, 1, &param, 1, &_range);     app * r        = m.mk_app(cd, 1, &_v);     mk_c(c)->save_ast_trail(r);     check_sorts(c, r);     return of_ast(r); }