#include <z3++.h>
Public Member Functions | |
fixedpoint (context &c) | |
~fixedpoint () | |
operator Z3_fixedpoint () const | |
void | from_string (char const *s) |
void | 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) |
![]() | |
object (context &c) | |
object (object const &s) | |
context & | ctx () const |
Z3_error_code | check_error () const |
Additional Inherited Members | |
![]() | |
context * | m_ctx |
|
inline |
Definition at line 2848 of file z3++.h.
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().
|
inline |
|
inline |
Definition at line 2853 of file z3++.h.
Referenced by Fixedpoint::fact(), and Fixedpoint::rule().
|
inline |
Definition at line 2874 of file z3++.h.
Referenced by Solver::to_smt2().
|
inline |
|
inline |
|
inline |
Definition at line 2866 of file z3++.h.
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
Definition at line 2856 of file z3++.h.
|
inline |
|
inline |
|
inline |
Definition at line 2875 of file z3++.h.
|
inline |
|
inline |
Definition at line 2872 of file z3++.h.
|
inline |
|
inline |