Z3
z3_interp.h File Reference

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[])