mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
adding fixedpoint object to C++ API
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
338193548b
commit
509f7409ba
|
@ -2175,6 +2175,50 @@ namespace z3 {
|
|||
};
|
||||
inline std::ostream & operator<<(std::ostream & out, optimize const & s) { out << Z3_optimize_to_string(s.ctx(), s.m_opt); return out; }
|
||||
|
||||
class fixedpoint : public object {
|
||||
Z3_fixedpoint m_fp;
|
||||
public:
|
||||
fixedpoint(context& c):object(c) { m_fp = Z3_mk_fixedpoint(c); Z3_fixedpoint_inc_ref(c, m_fp); }
|
||||
~fixedpoint() { Z3_fixedpoint_dec_ref(ctx(), m_fp); }
|
||||
operator Z3_fixedpoint() const { return m_fp; }
|
||||
void from_string(char const* s) { Z3_fixedpoint_from_string(ctx(), m_fp, s); check_error(); }
|
||||
void from_file(char const* s) { Z3_fixedpoint_from_file(ctx(), m_fp, s); check_error(); }
|
||||
void add_rule(expr& rule, symbol const& name) { Z3_fixedpoint_add_rule(ctx(), m_fp, rule, name); check_error(); }
|
||||
void add_fact(func_decl& f, unsigned * args) { Z3_fixedpoint_add_fact(ctx(), m_fp, f, f.arity(), args); check_error(); }
|
||||
check_result query(expr& q) { Z3_lbool r = Z3_fixedpoint_query(ctx(), m_fp, q); check_error(); to_check_result(r); }
|
||||
check_result query(func_decl_vector& relations) {
|
||||
array<Z3_func_decl> rs(relations);
|
||||
Z3_lbool r = Z3_fixedpoint_query_relations(ctx(), m_fp, rs.size(), rs.ptr());
|
||||
check_error();
|
||||
return to_check_result(r);
|
||||
}
|
||||
expr get_answer() { Z3_ast r = Z3_fixedpoint_get_answer(ctx(), m_fp); check_error(); return expr(ctx(), r); }
|
||||
std::string reason_unknown() { return Z3_fixedpoint_get_reason_unknown(ctx(), m_fp); }
|
||||
void update_rule(expr& rule, symbol const& name) { Z3_fixedpoint_update_rule(ctx(), m_fp, rule, name); check_error(); }
|
||||
unsigned get_num_levels(func_decl& p) { unsigned r = Z3_fixedpoint_get_num_levels(ctx(), m_fp, p); check_error(); return r; }
|
||||
expr get_cover_delta(int level, func_decl& p) {
|
||||
Z3_ast r = Z3_fixedpoint_get_cover_delta(ctx(), m_fp, level, p);
|
||||
check_error();
|
||||
return expr(ctx(), r);
|
||||
}
|
||||
void add_cover(int level, func_decl& p, expr& property) { Z3_fixedpoint_add_cover(ctx(), m_fp, level, p, property); check_error(); }
|
||||
stats statistics() const { Z3_stats r = Z3_fixedpoint_get_statistics(ctx(), m_fp); check_error(); return stats(ctx(), r); }
|
||||
void register_relation(func_decl& p) { Z3_fixedpoint_register_relation(ctx(), m_fp, p); }
|
||||
expr_vector assertions() const { Z3_ast_vector r = Z3_fixedpoint_get_assertions(ctx(), m_fp); check_error(); return expr_vector(ctx(), r); }
|
||||
expr_vector rules() const { Z3_ast_vector r = Z3_fixedpoint_get_rules(ctx(), m_fp); check_error(); return expr_vector(ctx(), r); }
|
||||
void set(params const & p) { Z3_fixedpoint_set_params(ctx(), m_fp, p); check_error(); }
|
||||
std::string help() const { return Z3_fixedpoint_get_help(ctx(), m_fp); }
|
||||
param_descrs get_param_descrs() { return param_descrs(ctx(), Z3_fixedpoint_get_param_descrs(ctx(), m_fp)); }
|
||||
std::string to_string() { return Z3_fixedpoint_to_string(ctx(), m_fp, 0, 0); }
|
||||
std::string to_string(expr_vector const& queries) {
|
||||
array<Z3_ast> qs(queries);
|
||||
return Z3_fixedpoint_to_string(ctx(), m_fp, qs.size(), qs.ptr());
|
||||
}
|
||||
void push() { Z3_fixedpoint_push(ctx(), m_fp); check_error(); }
|
||||
void pop() { Z3_fixedpoint_pop(ctx(), m_fp); check_error(); }
|
||||
};
|
||||
inline std::ostream & operator<<(std::ostream & out, fixedpoint const & f) { return out << Z3_fixedpoint_to_string(f.ctx(), f, 0, 0); }
|
||||
|
||||
inline tactic fail_if(probe const & p) {
|
||||
Z3_tactic r = Z3_tactic_fail_if(p.ctx(), p);
|
||||
p.check_error();
|
||||
|
|
Loading…
Reference in a new issue