Go to the source code of this file.
Functions | |
Interpolation API | |
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. More... | |
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 generated as abstract syntax trees in this context using the Z3 C API. More... | |
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 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) |
Z3_string Z3_API | Z3_interpolation_profile (__in Z3_context ctx) |
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. More... | |
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[]) |
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[]) |