Z3
z3_interp.h File Reference

Go to the source code of this file.

Functions

Interpolation API
Z3_ast Z3_API Z3_mk_interpolant (Z3_context c, Z3_ast a)
 Create an AST node marking a formula position for interpolation. More...
 
Z3_context Z3_API Z3_mk_interpolation_context (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 (Z3_context c, Z3_ast pf, Z3_ast pat, Z3_params p)
 
Z3_lbool Z3_API Z3_compute_interpolant (Z3_context c, Z3_ast pat, Z3_params p, Z3_ast_vector *interp, Z3_model *model)
 
Z3_string Z3_API Z3_interpolation_profile (Z3_context ctx)
 
int Z3_API Z3_read_interpolation_problem (Z3_context ctx, unsigned *num, Z3_ast *cnsts[], unsigned *parents[], Z3_string filename, Z3_string_ptr error, unsigned *num_theory, Z3_ast *theory[])
 Read an interpolation problem from file. More...
 
int Z3_API Z3_check_interpolant (Z3_context ctx, unsigned num, Z3_ast cnsts[], unsigned parents[], Z3_ast *interps, Z3_string_ptr error, unsigned num_theory, Z3_ast theory[])
 
void Z3_API Z3_write_interpolation_problem (Z3_context ctx, unsigned num, Z3_ast cnsts[], unsigned parents[], Z3_string filename, unsigned num_theory, Z3_ast theory[])