Z3
Public Member Functions
fixedpoint Class Reference
+ Inheritance diagram for fixedpoint:

Public Member Functions

 fixedpoint (context &c)
 
 fixedpoint (fixedpoint const &o)
 
 ~fixedpoint ()
 
fixedpointoperator= (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)
 
contextctx () const
 
Z3_error_code check_error () const
 

Additional Inherited Members

- Protected Attributes inherited from object
contextm_ctx
 

Detailed Description

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

Constructor & Destructor Documentation

fixedpoint ( context c)
inline

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

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

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

3355 :object(o), m_fp(o.m_fp) { Z3_fixedpoint_inc_ref(ctx(), m_fp); }
void Z3_API Z3_fixedpoint_inc_ref(Z3_context c, Z3_fixedpoint d)
Increment the reference counter of the given fixedpoint context.
context & ctx() const
Definition: z3++.h:473
object(context &c)
Definition: z3++.h:472
~fixedpoint ( )
inline

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

3356 { Z3_fixedpoint_dec_ref(ctx(), m_fp); }
context & ctx() const
Definition: z3++.h:473
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

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

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

3393 { Z3_fixedpoint_add_cover(ctx(), m_fp, level, p, property); check_error(); }
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
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...
void add_fact ( func_decl f,
unsigned *  args 
)
inline

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

3376 { Z3_fixedpoint_add_fact(ctx(), m_fp, f, f.arity(), args); check_error(); }
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
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.
void add_rule ( expr rule,
symbol const &  name 
)
inline

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

3375 { Z3_fixedpoint_add_rule(ctx(), m_fp, rule, name); check_error(); }
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: ...
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
expr_vector assertions ( ) const
inline

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

3396 { Z3_ast_vector r = Z3_fixedpoint_get_assertions(ctx(), m_fp); check_error(); return expr_vector(ctx(), r); }
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
Z3_ast_vector Z3_API Z3_fixedpoint_get_assertions(Z3_context c, Z3_fixedpoint f)
Retrieve set of background assertions from fixedpoint context.
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:76
expr_vector from_file ( char const *  s)
inline

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

3370  {
3371  Z3_ast_vector r = Z3_fixedpoint_from_file(ctx(), m_fp, s);
3372  check_error();
3373  return expr_vector(ctx(), r);
3374  }
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
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...
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:76
expr_vector from_string ( char const *  s)
inline

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

3365  {
3366  Z3_ast_vector r = Z3_fixedpoint_from_string(ctx(), m_fp, s);
3367  check_error();
3368  return expr_vector(ctx(), r);
3369  }
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...
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:76
expr get_answer ( )
inline

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

3384 { Z3_ast r = Z3_fixedpoint_get_answer(ctx(), m_fp); check_error(); return expr(ctx(), r); }
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
Z3_ast Z3_API Z3_fixedpoint_get_answer(Z3_context c, Z3_fixedpoint d)
Retrieve a formula that encodes satisfying answers to the query.
expr get_cover_delta ( int  level,
func_decl p 
)
inline

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

3388  {
3389  Z3_ast r = Z3_fixedpoint_get_cover_delta(ctx(), m_fp, level, p);
3390  check_error();
3391  return expr(ctx(), r);
3392  }
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
Z3_ast Z3_API Z3_fixedpoint_get_cover_delta(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred)
unsigned get_num_levels ( func_decl p)
inline

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

3387 { unsigned r = Z3_fixedpoint_get_num_levels(ctx(), m_fp, p); check_error(); return r; }
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
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. ...
param_descrs get_param_descrs ( )
inline

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

3400 { return param_descrs(ctx(), Z3_fixedpoint_get_param_descrs(ctx(), m_fp)); }
context & ctx() const
Definition: z3++.h:473
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.
std::string help ( ) const
inline

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

3399 { return Z3_fixedpoint_get_help(ctx(), m_fp); }
context & ctx() const
Definition: z3++.h:473
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 ( ) const
inline

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

3364 { return m_fp; }
fixedpoint& operator= ( fixedpoint const &  o)
inline

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

3357  {
3358  Z3_fixedpoint_inc_ref(o.ctx(), o.m_fp);
3359  Z3_fixedpoint_dec_ref(ctx(), m_fp);
3360  m_fp = o.m_fp;
3361  object::operator=(o);
3362  return *this;
3363  }
void Z3_API Z3_fixedpoint_inc_ref(Z3_context c, Z3_fixedpoint d)
Increment the reference counter of the given fixedpoint context.
context & ctx() const
Definition: z3++.h:473
void Z3_API Z3_fixedpoint_dec_ref(Z3_context c, Z3_fixedpoint d)
Decrement the reference counter of the given fixedpoint context.
check_result query ( expr q)
inline

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

3377 { Z3_lbool r = Z3_fixedpoint_query(ctx(), m_fp, q); check_error(); return to_check_result(r); }
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:60
check_result to_check_result(Z3_lbool l)
Definition: z3++.h:147
Z3_lbool Z3_API Z3_fixedpoint_query(Z3_context c, Z3_fixedpoint d, Z3_ast query)
Pose a query against the asserted rules.
check_result query ( func_decl_vector relations)
inline

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

3378  {
3379  array<Z3_func_decl> rs(relations);
3380  Z3_lbool r = Z3_fixedpoint_query_relations(ctx(), m_fp, rs.size(), rs.ptr());
3381  check_error();
3382  return to_check_result(r);
3383  }
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:60
check_result to_check_result(Z3_lbool l)
Definition: z3++.h:147
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.
std::string reason_unknown ( )
inline

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

3385 { return Z3_fixedpoint_get_reason_unknown(ctx(), m_fp); }
context & ctx() const
Definition: z3++.h:473
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. ...
void register_relation ( func_decl p)
inline

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

3395 { Z3_fixedpoint_register_relation(ctx(), m_fp, p); }
context & ctx() const
Definition: z3++.h:473
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...
expr_vector rules ( ) const
inline

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

3397 { Z3_ast_vector r = Z3_fixedpoint_get_rules(ctx(), m_fp); check_error(); return expr_vector(ctx(), r); }
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
Z3_ast_vector Z3_API Z3_fixedpoint_get_rules(Z3_context c, Z3_fixedpoint f)
Retrieve set of rules from fixedpoint context.
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:76
void set ( params const &  p)
inline

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

3398 { Z3_fixedpoint_set_params(ctx(), m_fp, p); check_error(); }
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
void Z3_API Z3_fixedpoint_set_params(Z3_context c, Z3_fixedpoint f, Z3_params p)
Set parameters on fixedpoint context.
stats statistics ( ) const
inline

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

3394 { Z3_stats r = Z3_fixedpoint_get_statistics(ctx(), m_fp); check_error(); return stats(ctx(), r); }
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.
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
std::string to_string ( )
inline

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

3401 { return Z3_fixedpoint_to_string(ctx(), m_fp, 0, 0); }
context & ctx() const
Definition: z3++.h:473
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.
std::string to_string ( expr_vector const &  queries)
inline

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

3402  {
3403  array<Z3_ast> qs(queries);
3404  return Z3_fixedpoint_to_string(ctx(), m_fp, qs.size(), qs.ptr());
3405  }
context & ctx() const
Definition: z3++.h:473
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.
void update_rule ( expr rule,
symbol const &  name 
)
inline

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

3386 { Z3_fixedpoint_update_rule(ctx(), m_fp, rule, name); check_error(); }
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
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. ...