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

 void Z3_API Z3_solver_import_model_converter(Z3_context c, Z3_solver src, Z3_solver dst) {     Z3_TRY;     LOG_Z3_solver_import_model_converter(c, src, dst);     model_converter_ref mc = to_solver_ref(src)->get_model_converter();     to_solver_ref(dst)->set_model_converter(mc.get());     Z3_CATCH; }

 static Z3_lbool _solver_check(Z3_context c, Z3_solver s, unsigned num_assumptions, Z3_ast const assumptions[]) {     for (unsigned i = 0; i < num_assumptions; i++) {         if (!is_expr(to_ast(assumptions[i]))) {             SET_ERROR_CODE(Z3_INVALID_ARG, "assumption is not an expression");             return Z3_L_UNDEF;         }     }     expr * const * _assumptions = to_exprs(assumptions);     unsigned timeout     = to_solver(s)->m_params.get_uint("timeout", mk_c(c)->get_timeout());     unsigned rlimit      = to_solver(s)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit());     bool     use_ctrl_c  = to_solver(s)->m_params.get_bool("ctrl_c", false);     cancel_eh<reslimit> eh(mk_c(c)->m().limit());     api::context::set_interruptable si(*(mk_c(c)), eh);     lbool result;     {         scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);         scoped_timer timer(timeout, &eh);         scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit);         try {             result = to_solver_ref(s)->check_sat(num_assumptions, _assumptions);         }         catch (z3_exception & ex) {             to_solver_ref(s)->set_reason_unknown(eh);             if (!mk_c(c)->m().canceled()) {                 mk_c(c)->handle_exception(ex);             }             return Z3_L_UNDEF;         }     }     if (result == l_undef) {         to_solver_ref(s)->set_reason_unknown(eh);     }     return static_cast<Z3_lbool>(result); }

 Z3_lbool Z3_API Z3_solver_get_consequences(Z3_context c,                                      Z3_solver s,                                     Z3_ast_vector assumptions,                                     Z3_ast_vector variables,                                     Z3_ast_vector consequences) {     Z3_TRY;     LOG_Z3_solver_get_consequences(c, s, assumptions, variables, consequences);     ast_manager& m = mk_c(c)->m();     RESET_ERROR_CODE();     CHECK_SEARCHING(c);     init_solver(c, s);     expr_ref_vector _assumptions(m), _consequences(m), _variables(m);     ast_ref_vector const& __assumptions = to_ast_vector_ref(assumptions);     for (ast* e : __assumptions) {         if (!is_expr(e)) {             _assumptions.finalize(); _consequences.finalize(); _variables.finalize();             SET_ERROR_CODE(Z3_INVALID_USAGE, "assumption is not an expression");             return Z3_L_UNDEF;         }         _assumptions.push_back(to_expr(e));     }     ast_ref_vector const& __variables = to_ast_vector_ref(variables);     for (ast* a : __variables) {         if (!is_expr(a)) {             _assumptions.finalize(); _consequences.finalize(); _variables.finalize();             SET_ERROR_CODE(Z3_INVALID_USAGE, "variable is not an expression");             return Z3_L_UNDEF;         }         _variables.push_back(to_expr(a));     }     lbool result = l_undef;     unsigned timeout     = to_solver(s)->m_params.get_uint("timeout", mk_c(c)->get_timeout());     unsigned rlimit      = to_solver(s)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit());     bool     use_ctrl_c  = to_solver(s)->m_params.get_bool("ctrl_c", false);     cancel_eh<reslimit> eh(mk_c(c)->m().limit());     api::context::set_interruptable si(*(mk_c(c)), eh);     {         scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);         scoped_timer timer(timeout, &eh);         scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit);         try {             result = to_solver_ref(s)->get_consequences(_assumptions, _variables, _consequences);         }         catch (z3_exception & ex) {             to_solver_ref(s)->set_reason_unknown(eh);             _assumptions.finalize(); _consequences.finalize(); _variables.finalize();             mk_c(c)->handle_exception(ex);             return Z3_L_UNDEF;         }     }     if (result == l_undef) {         to_solver_ref(s)->set_reason_unknown(eh);     }     for (expr* e : _consequences) {         to_ast_vector_ref(consequences).push_back(e);     }     return static_cast<Z3_lbool>(result);      Z3_CATCH_RETURN(Z3_L_UNDEF);         }

 void Z3_API Z3_solver_pop(Z3_context c, Z3_solver s, unsigned n) {     Z3_TRY;     LOG_Z3_solver_pop(c, s, n);     RESET_ERROR_CODE();     init_solver(c, s);     if (n > to_solver_ref(s)->get_scope_level()) {         SET_ERROR_CODE(Z3_IOB, nullptr);         return;     }     if (n > 0)         to_solver_ref(s)->pop(n);     Z3_CATCH; }

 Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s) {     Z3_TRY;     LOG_Z3_solver_get_assertions(c, s);     RESET_ERROR_CODE();     init_solver(c, s);     Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());     mk_c(c)->save_object(v);     unsigned sz = to_solver_ref(s)->get_num_assertions();     for (unsigned i = 0; i < sz; i++) {         v->m_ast_vector.push_back(to_solver_ref(s)->get_assertion(i));     }     RETURN_Z3(of_ast_vector(v));     Z3_CATCH_RETURN(nullptr); }

 void Z3_API Z3_solver_push(Z3_context c, Z3_solver s) {     Z3_TRY;     LOG_Z3_solver_push(c, s);     RESET_ERROR_CODE();     init_solver(c, s);     to_solver_ref(s)->push();     Z3_CATCH; }

 void Z3_API Z3_solver_set_activity(Z3_context c, Z3_solver s, Z3_ast a, double activity) {     Z3_TRY;     LOG_Z3_solver_set_activity(c, s, a, activity);     RESET_ERROR_CODE();     init_solver(c, s);     to_solver_ref(s)->set_activity(to_expr(a), activity);     Z3_CATCH; }

 Z3_string Z3_API Z3_solver_get_reason_unknown(Z3_context c, Z3_solver s) {     Z3_TRY;     LOG_Z3_solver_get_reason_unknown(c, s);     RESET_ERROR_CODE();     init_solver(c, s);     return mk_c(c)->mk_external_string(to_solver_ref(s)->reason_unknown());     Z3_CATCH_RETURN(""); }

 unsigned Z3_API Z3_solver_get_num_scopes(Z3_context c, Z3_solver s) {     Z3_TRY;     LOG_Z3_solver_get_num_scopes(c, s);     RESET_ERROR_CODE();     init_solver(c, s);     return to_solver_ref(s)->get_scope_level();     Z3_CATCH_RETURN(0); }

 void Z3_API Z3_solver_assert(Z3_context c, Z3_solver s, Z3_ast a) {     Z3_TRY;     LOG_Z3_solver_assert(c, s, a);     RESET_ERROR_CODE();     init_solver(c, s);     CHECK_FORMULA(a,);     to_solver_ref(s)->assert_expr(to_expr(a));     Z3_CATCH; }

    void Z3_API Z3_solver_set_params(Z3_context c, Z3_solver s, Z3_params p) {        Z3_TRY;        LOG_Z3_solver_set_params(c, s, p);        RESET_ERROR_CODE();        if (to_solver(s)->m_solver) {            bool old_model = to_solver(s)->m_params.get_bool("model", true);            bool new_model = to_param_ref(p).get_bool("model", true);            if (old_model != new_model)                to_solver_ref(s)->set_produce_models(new_model);            param_descrs r;            to_solver_ref(s)->collect_param_descrs(r);            context_params::collect_solver_param_descrs(r);            to_param_ref(p).validate(r);            to_solver_ref(s)->updt_params(to_param_ref(p));        }        to_solver(s)->m_params.append(to_param_ref(p));        Z3_CATCH;    }

 Z3_string Z3_API Z3_solver_to_dimacs_string(Z3_context c, Z3_solver s) {     Z3_TRY;     LOG_Z3_solver_to_string(c, s);     RESET_ERROR_CODE();     init_solver(c, s);     std::ostringstream buffer;     to_solver_ref(s)->display_dimacs(buffer);     return mk_c(c)->mk_external_string(buffer.str());     Z3_CATCH_RETURN(""); }

 void Z3_API Z3_solver_assert_and_track(Z3_context c, Z3_solver s, Z3_ast a, Z3_ast p) {     Z3_TRY;     LOG_Z3_solver_assert_and_track(c, s, a, p);     RESET_ERROR_CODE();     init_solver(c, s);     CHECK_FORMULA(a,);     CHECK_FORMULA(p,);     to_solver_ref(s)->assert_expr(to_expr(a), to_expr(p));     Z3_CATCH; }

    void solver_from_stream(Z3_context c, Z3_solver s, std::istream& is) {        scoped_ptr<cmd_context> ctx = alloc(cmd_context, false, &(mk_c(c)->m()));        ctx->set_ignore_check(true);        std::stringstream errstrm;        ctx->set_regular_stream(errstrm);        if (!parse_smt2_commands(*ctx.get(), is)) {            ctx = nullptr;            SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str().c_str());            return;        }        bool initialized = to_solver(s)->m_solver.get() != nullptr;        if (!initialized)            init_solver(c, s);        for (expr * e : ctx->assertions()) {            to_solver_ref(s)->assert_expr(e);        }        to_solver_ref(s)->set_model_converter(ctx->get_model_converter());    }

 static void solver_from_dimacs_stream(Z3_context c, Z3_solver s, std::istream& is) {     init_solver(c, s);     ast_manager& m = to_solver_ref(s)->get_manager();     std::stringstream err;     sat::solver solver(to_solver_ref(s)->get_params(), m.limit());     if (!parse_dimacs(is, err, solver)) {         SET_ERROR_CODE(Z3_PARSER_ERROR, err.str().c_str());         return;     }     sat2goal s2g;     ref<sat2goal::mc> mc;     atom2bool_var a2b(m);     for (unsigned v = 0; v < solver.num_vars(); ++v) {         a2b.insert(m.mk_const(symbol(v), m.mk_bool_sort()), v);     }     goal g(m);                 s2g(solver, a2b, to_solver_ref(s)->get_params(), g, mc);     for (unsigned i = 0; i < g.size(); ++i) {         to_solver_ref(s)->assert_expr(g.form(i));     } }

 Z3_stats Z3_API Z3_solver_get_statistics(Z3_context c, Z3_solver s) {     Z3_TRY;     LOG_Z3_solver_get_statistics(c, s);     RESET_ERROR_CODE();     init_solver(c, s);     Z3_stats_ref * st = alloc(Z3_stats_ref);     to_solver_ref(s)->collect_statistics(st->m_stats);     mk_c(c)->save_object(st);     Z3_stats r = of_stats(st);     RETURN_Z3(r);     Z3_CATCH_RETURN(0); }

 Z3_stats Z3_API Z3_solver_get_statistics(Z3_context c, Z3_solver s) {     Z3_TRY;     LOG_Z3_solver_get_statistics(c, s);     RESET_ERROR_CODE();     init_solver(c, s);     Z3_stats_ref * st = alloc(Z3_stats_ref, *mk_c(c));     to_solver_ref(s)->collect_statistics(st->m_stats);     get_memory_statistics(st->m_stats);     get_rlimit_statistics(mk_c(c)->m().limit(), st->m_stats);     mk_c(c)->save_object(st);     Z3_stats r = of_stats(st);     RETURN_Z3(r);     Z3_CATCH_RETURN(nullptr); }

 Z3_ast Z3_API Z3_solver_get_proof(Z3_context c, Z3_solver s) {     Z3_TRY;     LOG_Z3_solver_get_proof(c, s);     RESET_ERROR_CODE();     init_solver(c, s);     proof * p = to_solver_ref(s)->get_proof();     if (!p) {         SET_ERROR_CODE(Z3_INVALID_USAGE, "there is no current proof");         RETURN_Z3(nullptr);     }     mk_c(c)->save_ast_trail(p);     RETURN_Z3(of_ast(p));     Z3_CATCH_RETURN(nullptr); }

 Z3_ast_vector Z3_API Z3_solver_get_trail(Z3_context c, Z3_solver s) {     Z3_TRY;     LOG_Z3_solver_get_trail(c, s);     RESET_ERROR_CODE();     init_solver(c, s);     Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());     mk_c(c)->save_object(v);     expr_ref_vector trail = to_solver_ref(s)->get_trail();     for (expr* f : trail) {         v->m_ast_vector.push_back(f);     }     RETURN_Z3(of_ast_vector(v));     Z3_CATCH_RETURN(nullptr); }

 Z3_lbool Z3_API Z3_get_implied_equalities(Z3_context c,                                            Z3_solver s,                                           unsigned num_terms,                                           Z3_ast const terms[],                                           unsigned class_ids[]) {     Z3_TRY;     LOG_Z3_get_implied_equalities(c, s, num_terms, terms, class_ids);     ast_manager& m = mk_c(c)->m();     RESET_ERROR_CODE();     CHECK_SEARCHING(c);     init_solver(c, s);     lbool result = smt::implied_equalities(m, *to_solver_ref(s), num_terms, to_exprs(terms), class_ids);     return static_cast<Z3_lbool>(result);      Z3_CATCH_RETURN(Z3_L_UNDEF); }

 Z3_ast_vector Z3_API Z3_solver_get_unsat_core(Z3_context c, Z3_solver s) {     Z3_TRY;     LOG_Z3_solver_get_unsat_core(c, s);     RESET_ERROR_CODE();     init_solver(c, s);     ptr_vector<expr> core;     to_solver_ref(s)->get_unsat_core(core);     Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, mk_c(c)->m());     mk_c(c)->save_object(v);     for (unsigned i = 0; i < core.size(); i++) {         v->m_ast_vector.push_back(core[i]);     }     RETURN_Z3(of_ast_vector(v));     Z3_CATCH_RETURN(0); }

 Z3_model Z3_API Z3_solver_get_model(Z3_context c, Z3_solver s) {     Z3_TRY;     LOG_Z3_solver_get_model(c, s);     RESET_ERROR_CODE();     init_solver(c, s);     model_ref _m;     to_solver_ref(s)->get_model(_m);     if (!_m) {         SET_ERROR_CODE(Z3_INVALID_USAGE);         RETURN_Z3(0);     }     Z3_model_ref * m_ref = alloc(Z3_model_ref);      m_ref->m_model = _m;     mk_c(c)->save_object(m_ref);     RETURN_Z3(of_model(m_ref));     Z3_CATCH_RETURN(0); }

 Z3_string Z3_API Z3_solver_get_help(Z3_context c, Z3_solver s) {     Z3_TRY;     LOG_Z3_solver_get_help(c, s);     RESET_ERROR_CODE();     std::ostringstream buffer;     param_descrs descrs;     bool initialized = to_solver(s)->m_solver.get() != nullptr;     if (!initialized)         init_solver(c, s);     to_solver_ref(s)->collect_param_descrs(descrs);     context_params::collect_solver_param_descrs(descrs);     if (!initialized)         to_solver(s)->m_solver = nullptr;     descrs.display(buffer);     return mk_c(c)->mk_external_string(buffer.str());     Z3_CATCH_RETURN(""); }

 Z3_param_descrs Z3_API Z3_solver_get_param_descrs(Z3_context c, Z3_solver s) {     Z3_TRY;     LOG_Z3_solver_get_param_descrs(c, s);     RESET_ERROR_CODE();     Z3_param_descrs_ref * d = alloc(Z3_param_descrs_ref, *mk_c(c));     mk_c(c)->save_object(d);     bool initialized = to_solver(s)->m_solver.get() != nullptr;     if (!initialized)         init_solver(c, s);     to_solver_ref(s)->collect_param_descrs(d->m_descrs);     context_params::collect_solver_param_descrs(d->m_descrs);     if (!initialized)         to_solver(s)->m_solver = nullptr;     Z3_param_descrs r = of_param_descrs(d);     RETURN_Z3(r);     Z3_CATCH_RETURN(nullptr); }

 Z3_ast_vector Z3_API Z3_solver_cube(Z3_context c, Z3_solver s, Z3_ast_vector vs, unsigned cutoff) {     Z3_TRY;     LOG_Z3_solver_cube(c, s, vs, cutoff);     ast_manager& m = mk_c(c)->m();     expr_ref_vector result(m), vars(m);     for (ast* a : to_ast_vector_ref(vs)) {         if (!is_expr(a)) {             SET_ERROR_CODE(Z3_INVALID_USAGE, "cube contains a non-expression");         }         else {             vars.push_back(to_expr(a));         }     }     unsigned timeout     = to_solver(s)->m_params.get_uint("timeout", mk_c(c)->get_timeout());     unsigned rlimit      = to_solver(s)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit());     bool     use_ctrl_c  = to_solver(s)->m_params.get_bool("ctrl_c", false);     cancel_eh<reslimit> eh(mk_c(c)->m().limit());     api::context::set_interruptable si(*(mk_c(c)), eh);     {         scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);         scoped_timer timer(timeout, &eh);         scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit);         try {             result.append(to_solver_ref(s)->cube(vars, cutoff));         }         catch (z3_exception & ex) {             mk_c(c)->handle_exception(ex);             return nullptr;         }     }     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 : result) {         v->m_ast_vector.push_back(e);     }     to_ast_vector_ref(vs).reset();     for (expr* a : vars) {         to_ast_vector_ref(vs).push_back(a);     }     RETURN_Z3(of_ast_vector(v));     Z3_CATCH_RETURN(nullptr); }

 Z3_model Z3_API Z3_solver_get_model(Z3_context c, Z3_solver s) {     Z3_TRY;     LOG_Z3_solver_get_model(c, s);     RESET_ERROR_CODE();     init_solver(c, s);     model_ref _m;     to_solver_ref(s)->get_model(_m);     if (!_m) {         SET_ERROR_CODE(Z3_INVALID_USAGE, "there is no current model");         RETURN_Z3(nullptr);     }     if (_m) {         if (mk_c(c)->params().m_model_compress) _m->compress();     }     Z3_model_ref * m_ref = alloc(Z3_model_ref, *mk_c(c));      m_ref->m_model = _m;     mk_c(c)->save_object(m_ref);     RETURN_Z3(of_model(m_ref));     Z3_CATCH_RETURN(nullptr); }

 void Z3_API Z3_solver_get_levels(Z3_context c, Z3_solver s, Z3_ast_vector literals, unsigned sz, unsigned levels[]) {     Z3_TRY;     LOG_Z3_solver_get_levels(c, s, literals, sz, levels);     RESET_ERROR_CODE();     init_solver(c, s);     if (sz != Z3_ast_vector_size(c, literals)) {         SET_ERROR_CODE(Z3_IOB, nullptr);         return;     }     ptr_vector<expr> _vars;     for (unsigned i = 0; i < sz; ++i) {         expr* e = to_expr(Z3_ast_vector_get(c, literals, i));         mk_c(c)->m().is_not(e, e);         _vars.push_back(e);     }     unsigned_vector _levels(sz);     to_solver_ref(s)->get_levels(_vars, _levels);     for (unsigned i = 0; i < sz; ++i) {         levels[i] = _levels[i];     }     Z3_CATCH; }

 Z3_lbool Z3_API Z3_solver_get_consequences(Z3_context c,                                      Z3_solver s,                                     Z3_ast_vector assumptions,                                     Z3_ast_vector variables,                                     Z3_ast_vector consequences) {     Z3_TRY;     LOG_Z3_solver_get_consequences(c, s, assumptions, variables, consequences);     ast_manager& m = mk_c(c)->m();     RESET_ERROR_CODE();     CHECK_SEARCHING(c);     init_solver(c, s);     expr_ref_vector _assumptions(m), _consequences(m), _variables(m);     ast_ref_vector const& __assumptions = to_ast_vector_ref(assumptions);     unsigned sz = __assumptions.size();     for (unsigned i = 0; i < sz; ++i) {         if (!is_expr(__assumptions[i])) {             SET_ERROR_CODE(Z3_INVALID_USAGE);             return Z3_L_UNDEF;         }         _assumptions.push_back(to_expr(__assumptions[i]));     }     ast_ref_vector const& __variables = to_ast_vector_ref(variables);     sz = __variables.size();     for (unsigned i = 0; i < sz; ++i) {         if (!is_expr(__variables[i])) {             SET_ERROR_CODE(Z3_INVALID_USAGE);             return Z3_L_UNDEF;         }         _variables.push_back(to_expr(__variables[i]));     }     lbool result = to_solver_ref(s)->get_consequences(_assumptions, _variables, _consequences);     for (unsigned i = 0; i < _consequences.size(); ++i) {         to_ast_vector_ref(consequences).push_back(_consequences[i].get());     }     return static_cast<Z3_lbool>(result);      Z3_CATCH_RETURN(Z3_L_UNDEF);         }