Definition at line 2929 of file z3++.h.
◆ fixedpoint()
◆ ~fixedpoint()
◆ add_cover()
◆ add_fact()
void add_fact |
( |
func_decl & |
f, |
|
|
unsigned * |
args |
|
) |
| |
|
inline |
◆ add_rule()
void add_rule |
( |
expr & |
rule, |
|
|
symbol const & |
name |
|
) |
| |
|
inline |
◆ assertions()
◆ from_file()
void from_file |
( |
char const * |
s | ) |
|
|
inline |
◆ from_string()
void from_string |
( |
char const * |
s | ) |
|
|
inline |
◆ get_answer()
◆ get_cover_delta()
Definition at line 2950 of file z3++.h.
2953 return expr(
ctx(), r);
◆ get_num_levels()
◆ get_param_descrs()
◆ help()
std::string help |
( |
| ) |
const |
|
inline |
◆ operator Z3_fixedpoint()
operator Z3_fixedpoint |
( |
| ) |
const |
|
inline |
◆ query() [1/2]
◆ query() [2/2]
Definition at line 2940 of file z3++.h.
2941 array<Z3_func_decl> rs(relations);
◆ reason_unknown()
std::string reason_unknown |
( |
| ) |
|
|
inline |
◆ register_relation()
◆ rules()
◆ set()
◆ statistics()
stats statistics |
( |
| ) |
const |
|
inline |
◆ to_string() [1/2]
std::string to_string |
( |
| ) |
|
|
inline |
◆ to_string() [2/2]
Definition at line 2964 of file z3++.h.
2965 array<Z3_ast> qs(queries);
◆ update_rule()
void update_rule |
( |
expr & |
rule, |
|
|
symbol const & |
name |
|
) |
| |
|
inline |
Z3_lbool Z3_API Z3_fixedpoint_query(Z3_context c, Z3_fixedpoint d, Z3_ast query)
Pose a query against the asserted rules.
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.
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....
void Z3_API Z3_fixedpoint_set_params(Z3_context c, Z3_fixedpoint f, Z3_params p)
Set parameters on fixedpoint context.
void Z3_API Z3_fixedpoint_inc_ref(Z3_context c, Z3_fixedpoint d)
Increment the reference counter of the given fixedpoint context.
Z3_string Z3_API Z3_fixedpoint_get_help(Z3_context c, Z3_fixedpoint f)
Return a string describing all fixedpoint available parameters.
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.
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....
Z3_lbool
Lifted Boolean type: false, undefined, true.
Z3_ast Z3_API Z3_fixedpoint_get_answer(Z3_context c, Z3_fixedpoint d)
Retrieve a formula that encodes satisfying answers to the query.
void Z3_API Z3_fixedpoint_dec_ref(Z3_context c, Z3_fixedpoint d)
Decrement the reference counter of the given fixedpoint context.
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.
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...
Z3_fixedpoint Z3_API Z3_mk_fixedpoint(Z3_context c)
Create a new fixedpoint context.
ast_vector_tpl< expr > expr_vector
Z3_ast_vector Z3_API Z3_fixedpoint_get_assertions(Z3_context c, Z3_fixedpoint f)
Retrieve set of background assertions from fixedpoint context.
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.
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.
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.
check_result to_check_result(Z3_lbool l)
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.
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 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...
Z3_error_code check_error() const
Z3_ast_vector Z3_API Z3_fixedpoint_get_rules(Z3_context c, Z3_fixedpoint f)
Retrieve set of rules from fixedpoint context.
Z3_ast Z3_API Z3_fixedpoint_get_cover_delta(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred)
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: