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