19 #ifndef Z3_INTERPOLATION_H_ 20 #define Z3_INTERPOLATION_H_ 122 Z3_ast_vector Z3_API
Z3_get_interpolant(Z3_context c, Z3_ast pf, Z3_ast pat, Z3_params p);
158 Z3_ast_vector *interp,
214 unsigned *num_theory,
274 #endif // __cplusplus Z3_ast Z3_API Z3_mk_interpolant(Z3_context c, Z3_ast a)
Create an AST node marking a formula position for interpolation.
Z3_string Z3_API Z3_interpolation_profile(Z3_context ctx)
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[])
Z3_string * Z3_string_ptr
Z3_lbool Z3_API Z3_compute_interpolant(Z3_context c, Z3_ast pat, Z3_params p, Z3_ast_vector *interp, Z3_model *model)
Z3_lbool
Lifted Boolean type: false, undefined, true.
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[])
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 generat...
Z3_ast_vector Z3_API Z3_get_interpolant(Z3_context c, Z3_ast pf, Z3_ast pat, Z3_params p)
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.
const char * Z3_string
Z3 string type. It is just an alias for const char *.