19 #ifndef _Z3_INTERPOLATION_H_
20 #define _Z3_INTERPOLATION_H_
219 __out
unsigned *parents[],
222 __out
unsigned *num_theory,
248 __in_ecount(num)
Z3_ast cnsts[],
249 __in_ecount(num)
unsigned parents[],
250 __in_ecount(num - 1)
Z3_ast *interps,
252 __in
unsigned num_theory,
253 __in_ecount(num_theory)
Z3_ast theory[]);
272 __in_ecount(num)
Z3_ast cnsts[],
273 __in_ecount(num)
unsigned parents[],
275 __in
unsigned num_theory,
276 __in_ecount(num_theory)
Z3_ast theory[]);
283 #endif // __cplusplus
int Z3_API Z3_check_interpolant(__in Z3_context ctx, __in unsigned num, __in_ecount(num) Z3_ast cnsts[], __in_ecount(num) unsigned parents[], __in_ecount(num-1) Z3_ast *interps, __out Z3_string_ptr error, __in unsigned num_theory, __in_ecount(num_theory) Z3_ast theory[])
Z3_context Z3_API Z3_mk_interpolation_context(__in Z3_config cfg)
This function generates a Z3 context suitable for generation of interpolants. Formulas can be generat...
Z3_string * Z3_string_ptr
void Z3_API Z3_write_interpolation_problem(__in Z3_context ctx, __in unsigned num, __in_ecount(num) Z3_ast cnsts[], __in_ecount(num) unsigned parents[], __in Z3_string filename, __in unsigned num_theory, __in_ecount(num_theory) Z3_ast theory[])
Z3_ast_vector Z3_API Z3_get_interpolant(__in Z3_context c, __in Z3_ast pf, __in Z3_ast pat, __in Z3_params p)
Z3_lbool
Lifted Boolean type: false, undefined, true.
Z3_string Z3_API Z3_interpolation_profile(__in Z3_context ctx)
Z3_lbool Z3_API Z3_compute_interpolant(__in Z3_context c, __in Z3_ast pat, __in Z3_params p, __out Z3_ast_vector *interp, __out Z3_model *model)
int Z3_API Z3_read_interpolation_problem(__in Z3_context ctx, __out unsigned *num, __out Z3_ast *cnsts[], __out unsigned *parents[], __in Z3_string filename, __out Z3_string_ptr error, __out unsigned *num_theory, __out Z3_ast *theory[])
Read an interpolation problem from file.
Z3_ast Z3_API Z3_mk_interpolant(__in Z3_context c, __in Z3_ast a)
Create an AST node marking a formula position for interpolation.
const char * Z3_string
Z3 string type. It is just an alias for const char *.