z3_fixedpoint.h File Reference

Go to the source code of this file.

Fixedpoint facilities
typedef void	Z3_fixedpoint_reduce_assign_callback_fptr(void *, Z3_func_decl, unsigned, Z3_ast const [], unsigned, Z3_ast const [])
	The following utilities allows adding user-defined domains. More...
typedef void	Z3_fixedpoint_reduce_app_callback_fptr(void *, Z3_func_decl, unsigned, Z3_ast const [], Z3_ast *)
typedef void(*	Z3_fixedpoint_new_lemma_eh) (void *state, Z3_ast lemma, unsigned level)
typedef void(*	Z3_fixedpoint_predecessor_eh) (void *state)
typedef void(*	Z3_fixedpoint_unfold_eh) (void *state)
Z3_fixedpoint Z3_API	Z3_mk_fixedpoint (Z3_context c)
	Create a new fixedpoint context. More...
void Z3_API	Z3_fixedpoint_inc_ref (Z3_context c, Z3_fixedpoint d)
	Increment the reference counter of the given fixedpoint context. More...
void Z3_API	Z3_fixedpoint_dec_ref (Z3_context c, Z3_fixedpoint d)
	Decrement the reference counter of the given fixedpoint context. More...
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: More...
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. More...
void Z3_API	Z3_fixedpoint_assert (Z3_context c, Z3_fixedpoint d, Z3_ast axiom)
	Assert a constraint to the fixedpoint context. More...
Z3_lbool Z3_API	Z3_fixedpoint_query (Z3_context c, Z3_fixedpoint d, Z3_ast query)
	Pose a query against the asserted rules. More...
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. More...
Z3_ast Z3_API	Z3_fixedpoint_get_answer (Z3_context c, Z3_fixedpoint d)
	Retrieve a formula that encodes satisfying answers to the query. More...
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. More...
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. More...
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. More...
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_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 forward when possible. More...
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. More...
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. For example, the relation is empty if it does not occur in a head or a fact. More...
void Z3_API	Z3_fixedpoint_set_predicate_representation (Z3_context c, Z3_fixedpoint d, Z3_func_decl f, unsigned num_relations, Z3_symbol const relation_kinds[])
	Configure the predicate representation. More...
Z3_ast_vector Z3_API	Z3_fixedpoint_get_rules (Z3_context c, Z3_fixedpoint f)
	Retrieve set of rules from fixedpoint context. More...
Z3_ast_vector Z3_API	Z3_fixedpoint_get_assertions (Z3_context c, Z3_fixedpoint f)
	Retrieve set of background assertions from fixedpoint context. More...
void Z3_API	Z3_fixedpoint_set_params (Z3_context c, Z3_fixedpoint f, Z3_params p)
	Set parameters on fixedpoint context. More...
Z3_string Z3_API	Z3_fixedpoint_get_help (Z3_context c, Z3_fixedpoint f)
	Return a string describing all fixedpoint available parameters. More...
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. More...
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. More...
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. Return the set of queries in the string. More...
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. Return the set of queries in the file. More...
void Z3_API	Z3_fixedpoint_init (Z3_context c, Z3_fixedpoint d, void *state)
	Initialize the context with a user-defined state. More...
void Z3_API	Z3_fixedpoint_set_reduce_assign_callback (Z3_context c, Z3_fixedpoint d, Z3_fixedpoint_reduce_assign_callback_fptr cb)
	Register a callback to destructive updates. More...
void Z3_API	Z3_fixedpoint_set_reduce_app_callback (Z3_context c, Z3_fixedpoint d, Z3_fixedpoint_reduce_app_callback_fptr cb)
	Register a callback for building terms based on the relational operators. More...
void Z3_API	Z3_fixedpoint_add_callback (Z3_context ctx, Z3_fixedpoint f, void *state, Z3_fixedpoint_new_lemma_eh new_lemma_eh, Z3_fixedpoint_predecessor_eh predecessor_eh, Z3_fixedpoint_unfold_eh unfold_eh)
	set export callback for lemmas More...
void Z3_API	Z3_fixedpoint_add_constraint (Z3_context c, Z3_fixedpoint d, Z3_ast e, unsigned lvl)