Z3 |

Public Member Functions
fixedpoint Class Reference

`#include <z3++.h>`

Inheritance diagram for fixedpoint:

## Public Member Functions
| fixedpoint (context &c)
| fixedpoint (fixedpoint const &o)
| ~fixedpoint ()
fixedpoint & | operator= (fixedpoint const &o)
| operator Z3_fixedpoint () const
expr_vector | from_string (char const *s)
expr_vector | from_file (char const *s)
void | add_rule (expr &rule, symbol const &name)
void | add_fact (func_decl &f, unsigned *args)
check_result | query (expr &q)
check_result | query (func_decl_vector &relations)
expr | get_answer ()
std::string | reason_unknown ()
void | update_rule (expr &rule, symbol const &name)
unsigned | get_num_levels (func_decl &p)
expr | get_cover_delta (int level, func_decl &p)
void | add_cover (int level, func_decl &p, expr &property)
stats | statistics () const
void | register_relation (func_decl &p)
expr_vector | assertions () const
expr_vector | rules () const
void | set (params const &p)
std::string | help () const
param_descrs | get_param_descrs ()
std::string | to_string ()
std::string | to_string (expr_vector const &queries)
Public Member Functions inherited from object
| object (context &c)
context & | ctx () const
Z3_error_code | check_error () const

## Additional Inherited Members
Protected Attributes inherited from object
context * | m_ctx

## Detailed Description

Definition at line 3118 of file z3++.h.

## Constructor & Destructor Documentation

## ◆ fixedpoint() [1/2]

fixedpoint | ( | context & | c | ) |
| inline

Definition at line 3121 of file z3++.h.

3121:object(c) { m_fp = Z3_mk_fixedpoint(c); Z3_fixedpoint_inc_ref(c, m_fp); }
z3::object::object
object(context &c)
Definition: z3++.h:421
Z3_fixedpoint_inc_ref
void Z3_API Z3_fixedpoint_inc_ref(Z3_context c, Z3_fixedpoint d)
Increment the reference counter of the given fixedpoint context.
Z3_mk_fixedpoint
Z3_fixedpoint Z3_API Z3_mk_fixedpoint(Z3_context c)
Create a new fixedpoint context.

Referenced by Fixedpoint::__deepcopy__(), Fixedpoint::__del__(), Fixedpoint::add_cover(), Fixedpoint::add_rule(), Fixedpoint::assert_exprs(), Fixedpoint::get_answer(), Fixedpoint::get_assertions(), Fixedpoint::get_cover_delta(), Fixedpoint::get_ground_sat_answer(), Fixedpoint::get_num_levels(), Fixedpoint::get_rule_names_along_trace(), Fixedpoint::get_rules(), Fixedpoint::get_rules_along_trace(), Fixedpoint::help(), Fixedpoint::param_descrs(), Fixedpoint::parse_file(), Fixedpoint::parse_string(), Fixedpoint::query(), Fixedpoint::query_from_lvl(), Fixedpoint::reason_unknown(), Fixedpoint::register_relation(), Fixedpoint::set(), Fixedpoint::set_predicate_representation(), Fixedpoint::sexpr(), Fixedpoint::statistics(), Fixedpoint::to_string(), and Fixedpoint::update_rule().

## ◆ fixedpoint() [2/2]

fixedpoint | ( | fixedpoint const & | o | ) |
| inline

Definition at line 3122 of file z3++.h.

3122:object(o), m_fp(o.m_fp) { Z3_fixedpoint_inc_ref(ctx(), m_fp); }
z3::object::ctx
context & ctx() const
Definition: z3++.h:422

Referenced by Fixedpoint::__deepcopy__(), Fixedpoint::__del__(), Fixedpoint::add_cover(), Fixedpoint::add_rule(), Fixedpoint::assert_exprs(), Fixedpoint::get_answer(), Fixedpoint::get_assertions(), Fixedpoint::get_cover_delta(), Fixedpoint::get_ground_sat_answer(), Fixedpoint::get_num_levels(), Fixedpoint::get_rule_names_along_trace(), Fixedpoint::get_rules(), Fixedpoint::get_rules_along_trace(), Fixedpoint::help(), Fixedpoint::param_descrs(), Fixedpoint::parse_file(), Fixedpoint::parse_string(), Fixedpoint::query(), Fixedpoint::query_from_lvl(), Fixedpoint::reason_unknown(), Fixedpoint::register_relation(), Fixedpoint::set(), Fixedpoint::set_predicate_representation(), Fixedpoint::sexpr(), Fixedpoint::statistics(), Fixedpoint::to_string(), and Fixedpoint::update_rule().

## ◆ ~fixedpoint()

~fixedpoint | ( |  | ) |
| inline

Definition at line 3123 of file z3++.h.

3123{ Z3_fixedpoint_dec_ref(ctx(), m_fp); }
Z3_fixedpoint_dec_ref
void Z3_API Z3_fixedpoint_dec_ref(Z3_context c, Z3_fixedpoint d)
Decrement the reference counter of the given fixedpoint context.

## Member Function Documentation

## ◆ add_cover()

void add_cover | ( | int | level,
|  | func_decl & | p,
|  | expr & | property
| ) |  |
| inline

Definition at line 3160 of file z3++.h.

3160{ Z3_fixedpoint_add_cover(ctx(), m_fp, level, p, property); check_error(); }
z3::object::check_error
Z3_error_code check_error() const
Definition: z3++.h:423
Z3_fixedpoint_add_cover
void Z3_API Z3_fixedpoint_add_cover(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred, Z3_ast property)
Add property about the predicate pred. Add a property of predicate pred at level. It gets pushed forw...

## ◆ add_fact()

void add_fact | ( | func_decl & | f,
|  | unsigned * | args
| ) |  |
| inline

Definition at line 3143 of file z3++.h.

3143{ Z3_fixedpoint_add_fact(ctx(), m_fp, f, f.arity(), args); check_error(); }
Z3_fixedpoint_add_fact
void Z3_API Z3_fixedpoint_add_fact(Z3_context c, Z3_fixedpoint d, Z3_func_decl r, unsigned num_args, unsigned args[])
Add a Database fact.

## ◆ add_rule()

void add_rule | ( | expr & | rule,
|  | symbol const & | name
| ) |  |
| inline

Definition at line 3142 of file z3++.h.

3142{ Z3_fixedpoint_add_rule(ctx(), m_fp, rule, name); check_error(); }
Z3_fixedpoint_add_rule
void Z3_API Z3_fixedpoint_add_rule(Z3_context c, Z3_fixedpoint d, Z3_ast rule, Z3_symbol name)
Add a universal Horn clause as a named rule. The horn_rule should be of the form:

Referenced by Fixedpoint::fact(), and Fixedpoint::rule().

## ◆ assertions()

expr_vector assertions | ( |  | ) | const
| inline

Definition at line 3163 of file z3++.h.

3163{ Z3_ast_vector r = Z3_fixedpoint_get_assertions(ctx(), m_fp); check_error(); return expr_vector(ctx(), r); }
z3::expr_vector
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:73
Z3_fixedpoint_get_assertions
Z3_ast_vector Z3_API Z3_fixedpoint_get_assertions(Z3_context c, Z3_fixedpoint f)
Retrieve set of background assertions from fixedpoint context.

Referenced by Solver::to_smt2().

## ◆ from_file()

expr_vector from_file | ( | char const * | s | ) |
| inline

Definition at line 3137 of file z3++.h.

3137 {
3138 Z3_ast_vector r = Z3_fixedpoint_from_file(ctx(), m_fp, s);
3139 check_error();
3140 return expr_vector(ctx(), r);
3141 }
Z3_fixedpoint_from_file
Z3_ast_vector Z3_API Z3_fixedpoint_from_file(Z3_context c, Z3_fixedpoint f, Z3_string s)
Parse an SMT-LIB2 file with fixedpoint rules. Add the rules to the current fixedpoint context....

## ◆ from_string()

expr_vector from_string | ( | char const * | s | ) |
| inline

Definition at line 3132 of file z3++.h.

3132 {
3133 Z3_ast_vector r = Z3_fixedpoint_from_string(ctx(), m_fp, s);
3134 check_error();
3135 return expr_vector(ctx(), r);
3136 }
Z3_fixedpoint_from_string
Z3_ast_vector Z3_API Z3_fixedpoint_from_string(Z3_context c, Z3_fixedpoint f, Z3_string s)
Parse an SMT-LIB2 string with fixedpoint rules. Add the rules to the current fixedpoint context....

## ◆ get_answer()

expr get_answer | ( |  | ) |
| inline

Definition at line 3151 of file z3++.h.

3151{ Z3_ast r = Z3_fixedpoint_get_answer(ctx(), m_fp); check_error(); return expr(ctx(), r); }
Z3_fixedpoint_get_answer
Z3_ast Z3_API Z3_fixedpoint_get_answer(Z3_context c, Z3_fixedpoint d)
Retrieve a formula that encodes satisfying answers to the query.

## ◆ get_cover_delta()

expr get_cover_delta | ( | int | level,
|  | func_decl & | p
| ) |  |
| inline

Definition at line 3155 of file z3++.h.

3155 {
3156 Z3_ast r = Z3_fixedpoint_get_cover_delta(ctx(), m_fp, level, p);
3157 check_error();
3158 return expr(ctx(), r);
3159 }
Z3_fixedpoint_get_cover_delta
Z3_ast Z3_API Z3_fixedpoint_get_cover_delta(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred)

## ◆ get_num_levels()

unsigned get_num_levels | ( | func_decl & | p | ) |
| inline

Definition at line 3154 of file z3++.h.

3154{ unsigned r = Z3_fixedpoint_get_num_levels(ctx(), m_fp, p); check_error(); return r; }
Z3_fixedpoint_get_num_levels
unsigned Z3_API Z3_fixedpoint_get_num_levels(Z3_context c, Z3_fixedpoint d, Z3_func_decl pred)
Query the PDR engine for the maximal levels properties are known about predicate.

## ◆ get_param_descrs()

param_descrs get_param_descrs | ( |  | ) |
| inline

Definition at line 3167 of file z3++.h.

3167{ return param_descrs(ctx(), Z3_fixedpoint_get_param_descrs(ctx(), m_fp)); }
Z3_fixedpoint_get_param_descrs
Z3_param_descrs Z3_API Z3_fixedpoint_get_param_descrs(Z3_context c, Z3_fixedpoint f)
Return the parameter description set for the given fixedpoint object.

## ◆ help()

std::string help | ( |  | ) | const
| inline

Definition at line 3166 of file z3++.h.

3166{ return Z3_fixedpoint_get_help(ctx(), m_fp); }
Z3_fixedpoint_get_help
Z3_string Z3_API Z3_fixedpoint_get_help(Z3_context c, Z3_fixedpoint f)
Return a string describing all fixedpoint available parameters.

## ◆ operator Z3_fixedpoint()

operator Z3_fixedpoint | ( |  | ) | const
| inline

Definition at line 3131 of file z3++.h.

3131{ return m_fp; }

## ◆ operator=()

fixedpoint & operator= | ( | fixedpoint const & | o | ) |
| inline

Definition at line 3124 of file z3++.h.

3124 {
3125 Z3_fixedpoint_inc_ref(o.ctx(), o.m_fp);
3126 Z3_fixedpoint_dec_ref(ctx(), m_fp);
3127 m_fp = o.m_fp;
3128 object::operator=(o);
3129 return *this;
3130 }

## ◆ query() [1/2]

check_result query | ( | expr & | q | ) |
| inline

Definition at line 3144 of file z3++.h.

3144{ Z3_lbool r = Z3_fixedpoint_query(ctx(), m_fp, q); check_error(); return to_check_result(r); }
z3::to_check_result
check_result to_check_result(Z3_lbool l)
Definition: z3++.h:144
Z3_lbool
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:102
Z3_fixedpoint_query
Z3_lbool Z3_API Z3_fixedpoint_query(Z3_context c, Z3_fixedpoint d, Z3_ast query)
Pose a query against the asserted rules.

## ◆ query() [2/2]

check_result query | ( | func_decl_vector & | relations | ) |
| inline

Definition at line 3145 of file z3++.h.

3145 {
3146 array<Z3_func_decl> rs(relations);
3147 Z3_lbool r = Z3_fixedpoint_query_relations(ctx(), m_fp, rs.size(), rs.ptr());
3148 check_error();
3149 return to_check_result(r);
3150 }
Z3_fixedpoint_query_relations
Z3_lbool Z3_API Z3_fixedpoint_query_relations(Z3_context c, Z3_fixedpoint d, unsigned num_relations, Z3_func_decl const relations[])
Pose multiple queries against the asserted rules.

## ◆ reason_unknown()

std::string reason_unknown | ( |  | ) |
| inline

Definition at line 3152 of file z3++.h.

3152{ return Z3_fixedpoint_get_reason_unknown(ctx(), m_fp); }
Z3_fixedpoint_get_reason_unknown
Z3_string Z3_API Z3_fixedpoint_get_reason_unknown(Z3_context c, Z3_fixedpoint d)
Retrieve a string that describes the last status returned by Z3_fixedpoint_query.

## ◆ register_relation()

void register_relation | ( | func_decl & | p | ) |
| inline

Definition at line 3162 of file z3++.h.

3162{ Z3_fixedpoint_register_relation(ctx(), m_fp, p); }
Z3_fixedpoint_register_relation
void Z3_API Z3_fixedpoint_register_relation(Z3_context c, Z3_fixedpoint d, Z3_func_decl f)
Register relation as Fixedpoint defined. Fixedpoint defined relations have least-fixedpoint semantics...

## ◆ rules()

expr_vector rules | ( |  | ) | const
| inline

Definition at line 3164 of file z3++.h.

3164{ Z3_ast_vector r = Z3_fixedpoint_get_rules(ctx(), m_fp); check_error(); return expr_vector(ctx(), r); }
Z3_fixedpoint_get_rules
Z3_ast_vector Z3_API Z3_fixedpoint_get_rules(Z3_context c, Z3_fixedpoint f)
Retrieve set of rules from fixedpoint context.

## ◆ set()

void set | ( | params const & | p | ) |
| inline

Definition at line 3165 of file z3++.h.

3165{ Z3_fixedpoint_set_params(ctx(), m_fp, p); check_error(); }
Z3_fixedpoint_set_params
void Z3_API Z3_fixedpoint_set_params(Z3_context c, Z3_fixedpoint f, Z3_params p)
Set parameters on fixedpoint context.

## ◆ statistics()

stats statistics | ( |  | ) | const
| inline

Definition at line 3161 of file z3++.h.

3161{ Z3_stats r = Z3_fixedpoint_get_statistics(ctx(), m_fp); check_error(); return stats(ctx(), r); }
Z3_fixedpoint_get_statistics
Z3_stats Z3_API Z3_fixedpoint_get_statistics(Z3_context c, Z3_fixedpoint d)
Retrieve statistics information from the last call to Z3_fixedpoint_query.

## ◆ to_string() [1/2]

std::string to_string | ( |  | ) |
| inline

Definition at line 3168 of file z3++.h.

3168{ return Z3_fixedpoint_to_string(ctx(), m_fp, 0, 0); }
Z3_fixedpoint_to_string
Z3_string Z3_API Z3_fixedpoint_to_string(Z3_context c, Z3_fixedpoint f, unsigned num_queries, Z3_ast queries[])
Print the current rules and background axioms as a string.

## ◆ to_string() [2/2]

std::string to_string | ( | expr_vector const & | queries | ) |
| inline

Definition at line 3169 of file z3++.h.

3169 {
3170 array<Z3_ast> qs(queries);
3171 return Z3_fixedpoint_to_string(ctx(), m_fp, qs.size(), qs.ptr());
3172 }

## ◆ update_rule()

void update_rule | ( | expr & | rule,
|  | symbol const & | name
| ) |  |
| inline

Definition at line 3153 of file z3++.h.

3153{ Z3_fixedpoint_update_rule(ctx(), m_fp, rule, name); check_error(); }
Z3_fixedpoint_update_rule
void Z3_API Z3_fixedpoint_update_rule(Z3_context c, Z3_fixedpoint d, Z3_ast a, Z3_symbol name)
Update a named rule. A rule with the same name must have been previously created.