Z3 |

z3_fixedpoint.h
Go to the documentation of this file.
1/*++
2 Copyright (c) 2015 Microsoft Corporation
3
4 Module Name:
5
6 z3_fixedpoint.h
7
8 Abstract:
9
10 Fixedpoint API
11
12 Author:
13
14 Christoph M. Wintersteiger (cwinter) 2015-12-03
15
16 Notes:
17
18--*/
19#pragma once
20
21#ifdef __cplusplus
22 extern "C" {
23#endif // __cplusplus
24
27
37 Z3_fixedpoint Z3_API Z3_mk_fixedpoint(Z3_context c);
38
43 void Z3_API Z3_fixedpoint_inc_ref(Z3_context c, Z3_fixedpoint d);
44
49 void Z3_API Z3_fixedpoint_dec_ref(Z3_context c, Z3_fixedpoint d);
50
62 void Z3_API Z3_fixedpoint_add_rule(Z3_context c, Z3_fixedpoint d, Z3_ast rule, Z3_symbol name);
63
80 void Z3_API Z3_fixedpoint_add_fact(Z3_context c, Z3_fixedpoint d,
81 Z3_func_decl r,
82 unsigned num_args, unsigned args[]);
83
91 void Z3_API Z3_fixedpoint_assert(Z3_context c, Z3_fixedpoint d, Z3_ast axiom);
92
107 Z3_lbool Z3_API Z3_fixedpoint_query(Z3_context c, Z3_fixedpoint d, Z3_ast query);
108
120 Z3_lbool Z3_API Z3_fixedpoint_query_relations(
121 Z3_context c, Z3_fixedpoint d,
122 unsigned num_relations, Z3_func_decl const relations[]);
123
136 Z3_ast Z3_API Z3_fixedpoint_get_answer(Z3_context c, Z3_fixedpoint d);
137
144 Z3_string Z3_API Z3_fixedpoint_get_reason_unknown(Z3_context c, Z3_fixedpoint d);
145
151 void Z3_API Z3_fixedpoint_update_rule(Z3_context c, Z3_fixedpoint d, Z3_ast a, Z3_symbol name);
152
161 unsigned Z3_API Z3_fixedpoint_get_num_levels(Z3_context c, Z3_fixedpoint d, Z3_func_decl pred);
162
172 Z3_ast Z3_API Z3_fixedpoint_get_cover_delta(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred);
173
185 void Z3_API Z3_fixedpoint_add_cover(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred, Z3_ast property);
186
191 Z3_stats Z3_API Z3_fixedpoint_get_statistics(Z3_context c, Z3_fixedpoint d);
192
200 void Z3_API Z3_fixedpoint_register_relation(Z3_context c, Z3_fixedpoint d, Z3_func_decl f);
201
210 void Z3_API Z3_fixedpoint_set_predicate_representation(
211 Z3_context c,
212 Z3_fixedpoint d,
213 Z3_func_decl f,
214 unsigned num_relations,
215 Z3_symbol const relation_kinds[]);
216
221 Z3_ast_vector Z3_API Z3_fixedpoint_get_rules(
222 Z3_context c,
223 Z3_fixedpoint f);
224
229 Z3_ast_vector Z3_API Z3_fixedpoint_get_assertions(
230 Z3_context c,
231 Z3_fixedpoint f);
232
240 void Z3_API Z3_fixedpoint_set_params(Z3_context c, Z3_fixedpoint f, Z3_params p);
241
249 Z3_string Z3_API Z3_fixedpoint_get_help(Z3_context c, Z3_fixedpoint f);
250
258 Z3_param_descrs Z3_API Z3_fixedpoint_get_param_descrs(Z3_context c, Z3_fixedpoint f);
259
271 Z3_string Z3_API Z3_fixedpoint_to_string(
272 Z3_context c,
273 Z3_fixedpoint f,
274 unsigned num_queries,
275 Z3_ast queries[]);
276
290 Z3_ast_vector Z3_API Z3_fixedpoint_from_string(Z3_context c,
291 Z3_fixedpoint f,
292 Z3_string s);
293
307 Z3_ast_vector Z3_API Z3_fixedpoint_from_file(Z3_context c,
308 Z3_fixedpoint f,
309 Z3_string s);
310
313 typedef void Z3_fixedpoint_reduce_assign_callback_fptr(
314 void*, Z3_func_decl,
315 unsigned, Z3_ast const [],
316 unsigned, Z3_ast const []);
317
318 typedef void Z3_fixedpoint_reduce_app_callback_fptr(
319 void*, Z3_func_decl,
320 unsigned, Z3_ast const [],
321 Z3_ast*);
322
323
325 void Z3_API Z3_fixedpoint_init(Z3_context c, Z3_fixedpoint d, void* state);
326
332 void Z3_API Z3_fixedpoint_set_reduce_assign_callback(
333 Z3_context c ,Z3_fixedpoint d, Z3_fixedpoint_reduce_assign_callback_fptr cb);
334
336 void Z3_API Z3_fixedpoint_set_reduce_app_callback(
337 Z3_context c, Z3_fixedpoint d, Z3_fixedpoint_reduce_app_callback_fptr cb);
338
339 typedef void (*Z3_fixedpoint_new_lemma_eh)(void *state, Z3_ast lemma, unsigned level);
340 typedef void (*Z3_fixedpoint_predecessor_eh)(void *state);
341 typedef void (*Z3_fixedpoint_unfold_eh)(void *state);
342
344 void Z3_API Z3_fixedpoint_add_callback(Z3_context ctx, Z3_fixedpoint f, void *state,
345 Z3_fixedpoint_new_lemma_eh new_lemma_eh,
346 Z3_fixedpoint_predecessor_eh predecessor_eh,
347 Z3_fixedpoint_unfold_eh unfold_eh);
348
349 void Z3_API Z3_fixedpoint_add_constraint (Z3_context c, Z3_fixedpoint d, Z3_ast e, unsigned lvl);
350
353
354#ifdef __cplusplus
355}
356#endif // __cplusplus
357
Z3_string
const char * Z3_string
Z3 string type. It is just an alias for const char *.
Definition: z3_api.h:84
Z3_lbool
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:102
Z3_fixedpoint_set_reduce_app_callback
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.
Z3_fixedpoint_add_constraint
void Z3_API Z3_fixedpoint_add_constraint(Z3_context c, Z3_fixedpoint d, Z3_ast e, unsigned lvl)
Z3_fixedpoint_inc_ref
void Z3_API Z3_fixedpoint_inc_ref(Z3_context c, Z3_fixedpoint d)
Increment the reference counter of the given fixedpoint context.
Z3_fixedpoint_add_rule
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:
Z3_fixedpoint_set_predicate_representation
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.
Z3_fixedpoint_predecessor_eh
void(* Z3_fixedpoint_predecessor_eh)(void *state)
Definition: z3_fixedpoint.h:340
Z3_fixedpoint_from_file
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_fixedpoint_set_reduce_assign_callback
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.
Z3_fixedpoint_get_param_descrs
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_fixedpoint_update_rule
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_fixedpoint_from_string
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....
Z3_fixedpoint_get_assertions
Z3_ast_vector Z3_API Z3_fixedpoint_get_assertions(Z3_context c, Z3_fixedpoint f)
Retrieve set of background assertions from fixedpoint context.
Z3_fixedpoint_add_fact
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.
Z3_fixedpoint_reduce_app_callback_fptr
void Z3_fixedpoint_reduce_app_callback_fptr(void *, Z3_func_decl, unsigned, Z3_ast const [], Z3_ast *)
Definition: z3_fixedpoint.h:318
Z3_fixedpoint_dec_ref
void Z3_API Z3_fixedpoint_dec_ref(Z3_context c, Z3_fixedpoint d)
Decrement the reference counter of the given fixedpoint context.
Z3_fixedpoint_query
Z3_lbool Z3_API Z3_fixedpoint_query(Z3_context c, Z3_fixedpoint d, Z3_ast query)
Pose a query against the asserted rules.
Z3_fixedpoint_get_rules
Z3_ast_vector Z3_API Z3_fixedpoint_get_rules(Z3_context c, Z3_fixedpoint f)
Retrieve set of rules from fixedpoint context.
Z3_mk_fixedpoint
Z3_fixedpoint Z3_API Z3_mk_fixedpoint(Z3_context c)
Create a new fixedpoint context.
Z3_fixedpoint_get_num_levels
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.
Z3_fixedpoint_to_string
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_fixedpoint_get_cover_delta
Z3_ast Z3_API Z3_fixedpoint_get_cover_delta(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred)
Z3_fixedpoint_init
void Z3_API Z3_fixedpoint_init(Z3_context c, Z3_fixedpoint d, void *state)
Initialize the context with a user-defined state.
Z3_fixedpoint_get_statistics
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.
Z3_fixedpoint_new_lemma_eh
void(* Z3_fixedpoint_new_lemma_eh)(void *state, Z3_ast lemma, unsigned level)
Definition: z3_fixedpoint.h:339
Z3_fixedpoint_add_callback
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
Z3_fixedpoint_get_reason_unknown
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.
Z3_fixedpoint_get_help
Z3_string Z3_API Z3_fixedpoint_get_help(Z3_context c, Z3_fixedpoint f)
Return a string describing all fixedpoint available parameters.
Z3_fixedpoint_assert
void Z3_API Z3_fixedpoint_assert(Z3_context c, Z3_fixedpoint d, Z3_ast axiom)
Assert a constraint to the fixedpoint context.
Z3_fixedpoint_reduce_assign_callback_fptr
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.
Definition: z3_fixedpoint.h:313
Z3_fixedpoint_set_params
void Z3_API Z3_fixedpoint_set_params(Z3_context c, Z3_fixedpoint f, Z3_params p)
Set parameters on fixedpoint context.
Z3_fixedpoint_get_answer
Z3_ast Z3_API Z3_fixedpoint_get_answer(Z3_context c, Z3_fixedpoint d)
Retrieve a formula that encodes satisfying answers to the query.
Z3_fixedpoint_register_relation
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_add_cover
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_fixedpoint_query_relations
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_fixedpoint_unfold_eh
void(* Z3_fixedpoint_unfold_eh)(void *state)
Definition: z3_fixedpoint.h:341