fixedpoint Class Reference

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

Constructor & Destructor Documentation

fixedpoint() [1/2]

fixedpoint ( context &  c )

inline

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

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

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

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

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

inlineoverride

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

{ Z3_fixedpoint_dec_ref(ctx(), m_fp); }

Member Function Documentation

add_cover()

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

inline

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

{ Z3_fixedpoint_add_cover(ctx(), m_fp, level, p, property); check_error();  }

add_fact()

void add_fact ( func_decl &  f, unsigned *  args  )

inline

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

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

add_rule()

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

inline

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

{ Z3_fixedpoint_add_rule(ctx(), m_fp, rule, name); check_error(); }

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

assertions()

expr_vector assertions ( ) const

inline

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

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

Referenced by Solver::to_smt2().

from_file()

expr_vector from_file ( char const *  s )

inline

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

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

from_string()

expr_vector from_string ( char const *  s )

inline

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

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

get_answer()

expr get_answer ( )

inline

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

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

get_cover_delta()

expr get_cover_delta ( int  level, func_decl &  p  )

inline

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

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

get_num_levels()

unsigned get_num_levels ( func_decl &  p )

inline

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

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

get_param_descrs()

param_descrs get_param_descrs ( )

inline

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

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

help()

std::string help ( ) const

inline

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

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

operator Z3_fixedpoint()

operator Z3_fixedpoint ( ) const

inline

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

{ return m_fp; }

operator=()

fixedpoint& operator= ( fixedpoint const &  o )

inline

Definition at line 3408 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;
        }

query() [1/2]

check_result query ( expr &  q )

inline

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

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

query() [2/2]

check_result query ( func_decl_vector &  relations )

inline

Definition at line 3429 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);
        }

reason_unknown()

std::string reason_unknown ( )

inline

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

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

register_relation()

void register_relation ( func_decl &  p )

inline

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

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

rules()

expr_vector rules ( ) const

inline

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

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

set()

void set ( params const &  p )

inline

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

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

statistics()

stats statistics ( ) const

inline

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

{ Z3_stats r = Z3_fixedpoint_get_statistics(ctx(), m_fp); check_error(); return stats(ctx(), r); }

to_string() [1/2]

std::string to_string ( )

inline

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

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

to_string() [2/2]

std::string to_string ( expr_vector const &  queries )

inline

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

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

update_rule()

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

inline

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

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