Inheritance diagram for fixedpoint:

Public Member Functions
	fixedpoint (context &c)

	fixedpoint (fixedpoint const &o)

	~fixedpoint () override

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)

virtual	~object ()=default

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 3579 of file z3++.h.

Constructor & Destructor Documentation

fixedpoint ( context & c )

inline

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

3582 :object(c) { m_fp = Z3_mk_fixedpoint(c); Z3_fixedpoint_inc_ref(c, m_fp); }

Z3_mk_fixedpoint

Z3_fixedpoint Z3_API Z3_mk_fixedpoint(Z3_context c)

Create a new fixedpoint context.

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::object::object

object(context &c)

Definition: z3++.h:538

fixedpoint ( fixedpoint const & o )

inline

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

3583 :object(o), m_fp(o.m_fp) { Z3_fixedpoint_inc_ref(ctx(), m_fp); }

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::object::ctx

context & ctx() const

Definition: z3++.h:540

z3::object::object

object(context &c)

Definition: z3++.h:538

~fixedpoint ( )

inlineoverride

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

3584 { Z3_fixedpoint_dec_ref(ctx(), m_fp); }

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

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

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

inline

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

3621 { 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:541

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

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...

void add_fact	(	func_decl &	f,
		unsigned *	args
	)

inline

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

3604 { Z3_fixedpoint_add_fact(ctx(), m_fp, f, f.arity(), args); check_error(); }

z3::object::check_error

Z3_error_code check_error() const

Definition: z3++.h:541

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

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.

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

inline

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

3603 { 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: ...

z3::object::check_error

Z3_error_code check_error() const

Definition: z3++.h:541

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

expr_vector assertions ( ) const

inline

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

3624 { Z3_ast_vector r = Z3_fixedpoint_get_assertions(ctx(), m_fp); check_error(); return expr_vector(ctx(), r); }

z3::object::check_error

Z3_error_code check_error() const

Definition: z3++.h:541

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

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.

z3::expr_vector

ast_vector_tpl< expr > expr_vector

Definition: z3++.h:77

expr_vector from_file ( char const * s )

inline

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

                                              { 
             Z3_ast_vector r = Z3_fixedpoint_from_file(ctx(), m_fp, s); 
             check_error(); 
             return expr_vector(ctx(), r);
         }

expr_vector from_string ( char const * s )

inline

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

                                                { 
             Z3_ast_vector r = Z3_fixedpoint_from_string(ctx(), m_fp, s); 
             check_error(); 
             return expr_vector(ctx(), r);
         }

expr get_answer ( )

inline

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

3612 { Z3_ast r = Z3_fixedpoint_get_answer(ctx(), m_fp); check_error(); return expr(ctx(), r); }

z3::object::check_error

Z3_error_code check_error() const

Definition: z3++.h:541

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

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.

expr get_cover_delta	(	int	level,
		func_decl &	p
	)

inline

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

                                                       {
             Z3_ast r = Z3_fixedpoint_get_cover_delta(ctx(), m_fp, level, p);
             check_error();
             return expr(ctx(), r);
         }

unsigned get_num_levels ( func_decl & p )

inline

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

3615 { unsigned r = Z3_fixedpoint_get_num_levels(ctx(), m_fp, p); check_error(); return r; }

z3::object::check_error

Z3_error_code check_error() const

Definition: z3++.h:541

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

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. ...

param_descrs get_param_descrs ( )

inline

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

3628 { return param_descrs(ctx(), Z3_fixedpoint_get_param_descrs(ctx(), m_fp)); }

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

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.

std::string help ( ) const

inline

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

3627 { return Z3_fixedpoint_get_help(ctx(), m_fp); }

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

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 ( ) const

inline

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

3592 { return m_fp; }

fixedpoint& operator= ( fixedpoint const & o )

inline

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

                                                      {
             Z3_fixedpoint_inc_ref(o.ctx(), o.m_fp);
             Z3_fixedpoint_dec_ref(ctx(), m_fp);
             m_fp = o.m_fp;
             object::operator=(o);
             return *this;
         }

check_result query ( expr & q )

inline

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

3605 { Z3_lbool r = Z3_fixedpoint_query(ctx(), m_fp, q); check_error(); return to_check_result(r); }

z3::object::check_error

Z3_error_code check_error() const

Definition: z3++.h:541

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

Z3_lbool

Lifted Boolean type: false, undefined, true.

Definition: z3_api.h:57

z3::to_check_result

check_result to_check_result(Z3_lbool l)

Definition: z3++.h:178

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.

check_result query ( func_decl_vector & relations )

inline

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

                                                         {
             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);
         }

std::string reason_unknown ( )

inline

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

3613 { return Z3_fixedpoint_get_reason_unknown(ctx(), m_fp); }

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

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. ...

void register_relation ( func_decl & p )

inline

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

3623 { Z3_fixedpoint_register_relation(ctx(), m_fp, p); }

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

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...

expr_vector rules ( ) const

inline

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

3625 { Z3_ast_vector r = Z3_fixedpoint_get_rules(ctx(), m_fp); check_error(); return expr_vector(ctx(), r); }

z3::object::check_error

Z3_error_code check_error() const

Definition: z3++.h:541

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

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.

z3::expr_vector

ast_vector_tpl< expr > expr_vector

Definition: z3++.h:77

void set ( params const & p )

inline

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

3626 { Z3_fixedpoint_set_params(ctx(), m_fp, p); check_error(); }

z3::object::check_error

Z3_error_code check_error() const

Definition: z3++.h:541

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

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.

stats statistics ( ) const

inline

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

3622 { 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.

z3::object::check_error

Z3_error_code check_error() const

Definition: z3++.h:541

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

std::string to_string ( )

inline

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

3629 { return Z3_fixedpoint_to_string(ctx(), m_fp, 0, 0); }

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

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.

std::string to_string ( expr_vector const & queries )

inline

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

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

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

inline

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

3614 { Z3_fixedpoint_update_rule(ctx(), m_fp, rule, name); check_error(); }

z3::object::check_error

Z3_error_code check_error() const

Definition: z3++.h:541

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

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. ...

Public Member Functions

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

Member Function Documentation