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

 void Z3_API Z3_fixedpoint_set_reduce_app_callback(     Z3_context c, Z3_fixedpoint d, Z3_fixedpoint_reduce_app_callback_fptr f) {     Z3_TRY;     // no logging     to_fixedpoint_ref(d)->set_reduce_app((reduce_app_callback_fptr)f);            Z3_CATCH; }

 unsigned Z3_API Z3_fixedpoint_get_num_levels(Z3_context c, Z3_fixedpoint d, Z3_func_decl pred) {     Z3_TRY;     LOG_Z3_fixedpoint_get_num_levels(c, d, pred);     RESET_ERROR_CODE();     return to_fixedpoint_ref(d)->get_num_levels(to_func_decl(pred));     Z3_CATCH_RETURN(0) }

 Z3_string Z3_API Z3_fixedpoint_get_reason_unknown(Z3_context c,Z3_fixedpoint d) {     Z3_TRY;     LOG_Z3_fixedpoint_get_reason_unknown(c, d);     RESET_ERROR_CODE();     return mk_c(c)->mk_external_string(to_fixedpoint_ref(d)->get_last_status());     Z3_CATCH_RETURN(""); }

 Z3_ast_vector Z3_API Z3_fixedpoint_get_assertions(     Z3_context c,     Z3_fixedpoint d) {     Z3_TRY;     LOG_Z3_fixedpoint_get_assertions(c, d);     ast_manager& m = mk_c(c)->m();     Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, *mk_c(c), m);     mk_c(c)->save_object(v);     unsigned num_asserts = to_fixedpoint_ref(d)->ctx().get_num_assertions();     for (unsigned i = 0; i < num_asserts; ++i) {         v->m_ast_vector.push_back(to_fixedpoint_ref(d)->ctx().get_assertion(i));     }     RETURN_Z3(of_ast_vector(v));     Z3_CATCH_RETURN(0); }

 void Z3_API Z3_fixedpoint_add_invariant(Z3_context c, Z3_fixedpoint d, Z3_func_decl pred, Z3_ast property) {     Z3_TRY;     LOG_Z3_fixedpoint_add_invariant(c, d, pred, property);     RESET_ERROR_CODE();     to_fixedpoint_ref(d)->ctx ().add_invariant(to_func_decl(pred), to_expr(property));             Z3_CATCH; }

 void Z3_API Z3_fixedpoint_add_cover(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred, Z3_ast property) {     Z3_TRY;     LOG_Z3_fixedpoint_add_cover(c, d, level, pred, property);     RESET_ERROR_CODE();     to_fixedpoint_ref(d)->add_cover(level, to_func_decl(pred), to_expr(property));             Z3_CATCH; }

 void Z3_API Z3_fixedpoint_push(Z3_context c,Z3_fixedpoint d) {     Z3_TRY;     LOG_Z3_fixedpoint_push(c, d);     RESET_ERROR_CODE();     to_fixedpoint_ref(d)->ctx().push();     Z3_CATCH; }

 void Z3_API Z3_fixedpoint_assert(Z3_context c, Z3_fixedpoint d, Z3_ast a) {     Z3_TRY;     LOG_Z3_fixedpoint_assert(c, d, a);     RESET_ERROR_CODE();     CHECK_FORMULA(a,);     to_fixedpoint_ref(d)->ctx().assert_expr(to_expr(a));     Z3_CATCH; }

 void Z3_API Z3_fixedpoint_add_fact(Z3_context c, Z3_fixedpoint d,                                    Z3_func_decl r, unsigned num_args, unsigned args[]) {     Z3_TRY;     LOG_Z3_fixedpoint_add_fact(c, d, r, num_args, args);     RESET_ERROR_CODE();     to_fixedpoint_ref(d)->add_table_fact(to_func_decl(r), num_args, args);     Z3_CATCH; }

 void Z3_API Z3_fixedpoint_update_rule(Z3_context c, Z3_fixedpoint d, Z3_ast a, Z3_symbol name) {     Z3_TRY;     LOG_Z3_fixedpoint_update_rule(c, d, a, name);     RESET_ERROR_CODE();     CHECK_FORMULA(a,);     to_fixedpoint_ref(d)->update_rule(to_expr(a), to_symbol(name));     Z3_CATCH; }

 Z3_ast Z3_API Z3_fixedpoint_get_reachable(Z3_context c, Z3_fixedpoint d, Z3_func_decl pred) {     Z3_TRY;     LOG_Z3_fixedpoint_get_reachable(c, d, pred);     RESET_ERROR_CODE();     expr_ref r = to_fixedpoint_ref(d)->ctx().get_reachable(to_func_decl(pred));     mk_c(c)->save_ast_trail(r);             RETURN_Z3(of_expr(r.get()));     Z3_CATCH_RETURN(nullptr); }

 Z3_ast Z3_API Z3_fixedpoint_get_answer(Z3_context c, Z3_fixedpoint d) {     Z3_TRY;     LOG_Z3_fixedpoint_get_answer(c, d);     RESET_ERROR_CODE();     expr* e = to_fixedpoint_ref(d)->ctx().get_answer_as_formula();     mk_c(c)->save_ast_trail(e);     RETURN_Z3(of_expr(e));     Z3_CATCH_RETURN(0); }

 Z3_ast Z3_API Z3_fixedpoint_get_cover_delta(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred) {     Z3_TRY;     LOG_Z3_fixedpoint_get_cover_delta(c, d, level, pred);     RESET_ERROR_CODE();     expr_ref r = to_fixedpoint_ref(d)->get_cover_delta(level, to_func_decl(pred));     mk_c(c)->save_ast_trail(r);     RETURN_Z3(of_expr(r.get()));     Z3_CATCH_RETURN(0); }

 Z3_param_descrs Z3_API Z3_fixedpoint_get_param_descrs(Z3_context c, Z3_fixedpoint f) {     Z3_TRY;     LOG_Z3_fixedpoint_get_param_descrs(c, f);     RESET_ERROR_CODE();     Z3_param_descrs_ref * d = alloc(Z3_param_descrs_ref);     mk_c(c)->save_object(d);     to_fixedpoint_ref(f)->collect_param_descrs(d->m_descrs);     Z3_param_descrs r = of_param_descrs(d);     RETURN_Z3(r);     Z3_CATCH_RETURN(0); }

 Z3_stats Z3_API Z3_fixedpoint_get_statistics(Z3_context c,Z3_fixedpoint d) {     Z3_TRY;     LOG_Z3_fixedpoint_get_statistics(c, d);     RESET_ERROR_CODE();     Z3_stats_ref * st = alloc(Z3_stats_ref);     to_fixedpoint_ref(d)->ctx().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_string Z3_API Z3_fixedpoint_get_help(Z3_context c, Z3_fixedpoint d) {     Z3_TRY;     LOG_Z3_fixedpoint_get_help(c, d);     RESET_ERROR_CODE();     std::ostringstream buffer;     param_descrs descrs;     to_fixedpoint_ref(d)->collect_param_descrs(descrs);     descrs.display(buffer);     return mk_c(c)->mk_external_string(buffer.str());     Z3_CATCH_RETURN(""); }

 Z3_string Z3_API Z3_fixedpoint_to_string(     Z3_context c,     Z3_fixedpoint d,     unsigned num_queries,     Z3_ast _queries[]) {     Z3_TRY;     expr*const* queries = to_exprs(_queries);     LOG_Z3_fixedpoint_to_string(c, d, num_queries, _queries);     RESET_ERROR_CODE();     return mk_c(c)->mk_external_string(to_fixedpoint_ref(d)->to_string(num_queries, queries));     Z3_CATCH_RETURN(""); }

 Z3_lbool Z3_API Z3_fixedpoint_query(Z3_context c,Z3_fixedpoint d, Z3_ast q) {     Z3_TRY;     LOG_Z3_fixedpoint_query(c, d, q);     RESET_ERROR_CODE();     lbool r = l_undef;     cancel_eh<api::fixedpoint_context> eh(*to_fixedpoint_ref(d));     unsigned timeout = to_fixedpoint(d)->m_params.get_uint(":timeout", UINT_MAX);     api::context::set_interruptable(*(mk_c(c)), eh);             {         scoped_timer timer(timeout, &eh);         try {             r = to_fixedpoint_ref(d)->ctx().query(to_expr(q));         }         catch (z3_exception& ex) {             mk_c(c)->handle_exception(ex);             r = l_undef;         }         to_fixedpoint_ref(d)->ctx().cleanup();     }     return of_lbool(r);     Z3_CATCH_RETURN(Z3_L_UNDEF); }

    void Z3_API Z3_fixedpoint_add_callback(Z3_context c, Z3_fixedpoint d,                                            void *state,                                            Z3_fixedpoint_new_lemma_eh new_lemma_eh,                                            Z3_fixedpoint_predecessor_eh predecessor_eh,                                            Z3_fixedpoint_unfold_eh unfold_eh){        Z3_TRY;            // not logged            to_fixedpoint_ref(d)->ctx().add_callback(state,                                                     reinterpret_cast<datalog::t_new_lemma_eh>(new_lemma_eh),                                                     reinterpret_cast<datalog::t_predecessor_eh>(predecessor_eh),                                                     reinterpret_cast<datalog::t_unfold_eh>(unfold_eh));        Z3_CATCH;    }

 Z3_lbool Z3_API Z3_fixedpoint_query_from_lvl (Z3_context c, Z3_fixedpoint d, Z3_ast q, unsigned lvl) {     Z3_TRY;     LOG_Z3_fixedpoint_query_from_lvl (c, d, q, lvl);     RESET_ERROR_CODE();     lbool r = l_undef;     unsigned timeout = to_fixedpoint(d)->m_params.get_uint("timeout", mk_c(c)->get_timeout());     unsigned rlimit  = to_fixedpoint(d)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit());     {         scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit);         cancel_eh<reslimit> eh(mk_c(c)->m().limit());         api::context::set_interruptable si(*(mk_c(c)), eh);                 scoped_timer timer(timeout, &eh);         try {             r = to_fixedpoint_ref(d)->ctx().query_from_lvl (to_expr(q), lvl);         }         catch (z3_exception& ex) {             mk_c(c)->handle_exception(ex);             r = l_undef;         }         to_fixedpoint_ref(d)->ctx().cleanup();     }     return of_lbool(r);     Z3_CATCH_RETURN(Z3_L_UNDEF); }

 void Z3_API Z3_fixedpoint_set_predicate_representation(     Z3_context c,     Z3_fixedpoint d,     Z3_func_decl f,     unsigned num_relations,     Z3_symbol const relation_kinds[]) {     Z3_TRY;     LOG_Z3_fixedpoint_set_predicate_representation(c, d, f, num_relations, relation_kinds);     svector<symbol> kinds;     for (unsigned i = 0; i < num_relations; ++i) {         kinds.push_back(to_symbol(relation_kinds[i]));     }     to_fixedpoint_ref(d)->ctx().set_predicate_representation(to_func_decl(f), num_relations, kinds.c_ptr());     Z3_CATCH; }

 Z3_lbool Z3_API Z3_fixedpoint_query_relations(     Z3_context c,Z3_fixedpoint d,     unsigned num_relations, Z3_func_decl const relations[]) {     Z3_TRY;     LOG_Z3_fixedpoint_query_relations(c, d, num_relations, relations);     RESET_ERROR_CODE();     lbool r = l_undef;     unsigned timeout = to_fixedpoint(d)->m_params.get_uint("timeout", mk_c(c)->get_timeout());     cancel_eh<reslimit> eh(mk_c(c)->m().limit());     api::context::set_interruptable si(*(mk_c(c)), eh);     {         scoped_timer timer(timeout, &eh);         try {             r = to_fixedpoint_ref(d)->ctx().rel_query(num_relations, to_func_decls(relations));         }         catch (z3_exception& ex) {             mk_c(c)->handle_exception(ex);             r = l_undef;         }         to_fixedpoint_ref(d)->ctx().cleanup();     }     return of_lbool(r);     Z3_CATCH_RETURN(Z3_L_UNDEF); }

 Z3_ast_vector Z3_API Z3_fixedpoint_get_rules_along_trace(     Z3_context c,     Z3_fixedpoint d) {     Z3_TRY;     LOG_Z3_fixedpoint_get_rules_along_trace(c, d);     ast_manager& m = mk_c(c)->m();     Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, *mk_c(c), m);     mk_c(c)->save_object(v);     expr_ref_vector rules(m);     svector<symbol> names;          to_fixedpoint_ref(d)->ctx().get_rules_along_trace_as_formulas(rules, names);     for (unsigned i = 0; i < rules.size(); ++i) {         v->m_ast_vector.push_back(rules[i].get());     }     RETURN_Z3(of_ast_vector(v));     Z3_CATCH_RETURN(nullptr); }

 Z3_symbol Z3_API Z3_fixedpoint_get_rule_names_along_trace(     Z3_context c,     Z3_fixedpoint d) {     Z3_TRY;     LOG_Z3_fixedpoint_get_rule_names_along_trace(c, d);     ast_manager& m = mk_c(c)->m();     Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, *mk_c(c), m);     mk_c(c)->save_object(v);     expr_ref_vector rules(m);     svector<symbol> names;     std::stringstream ss;          to_fixedpoint_ref(d)->ctx().get_rules_along_trace_as_formulas(rules, names);     for (unsigned i = 0; i < names.size(); ++i) {         ss << ";" << names[i].str();     }     RETURN_Z3(of_symbol(symbol(ss.str().substr(1).c_str())));     Z3_CATCH_RETURN(nullptr); }

 Z3_ast_vector Z3_API Z3_fixedpoint_simplify_rules(     Z3_context c,     Z3_fixedpoint d,     unsigned num_rules,     Z3_ast _rules[],     unsigned num_outputs,     Z3_func_decl _outputs[]) {     Z3_TRY;     LOG_Z3_fixedpoint_simplify_rules(c, d, num_rules, _rules, num_outputs, _outputs);     RESET_ERROR_CODE();             expr** rules = (expr**)_rules;     func_decl** outputs = (func_decl**)_outputs;     ast_manager& m = mk_c(c)->m();             expr_ref_vector result(m);     to_fixedpoint_ref(d)->simplify_rules(num_rules, rules, num_outputs, outputs, result);             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 < result.size(); ++i) {         v->m_ast_vector.push_back(result[i].get());     }     RETURN_Z3(of_ast_vector(v));     Z3_CATCH_RETURN(0) }

 void Z3_API Z3_fixedpoint_init(Z3_context c,Z3_fixedpoint d, void* state) {     Z3_TRY;     // not logged     to_fixedpoint_ref(d)->set_state(state);     Z3_CATCH; }

 void Z3_API Z3_fixedpoint_register_relation(Z3_context c,Z3_fixedpoint d, Z3_func_decl f) {     Z3_TRY;     LOG_Z3_fixedpoint_register_relation(c, d, f);     to_fixedpoint_ref(d)->ctx().register_predicate(to_func_decl(f), true);     Z3_CATCH; }

 void Z3_API Z3_fixedpoint_add_constraint (Z3_context c, Z3_fixedpoint d, Z3_ast e, unsigned lvl){     to_fixedpoint_ref(d)->ctx().add_constraint(to_expr(e), lvl); }