Go to the documentation of this file.00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019 #ifndef _Z3_INTERPOLATION_H_
00020 #define _Z3_INTERPOLATION_H_
00021
00022 #ifdef __cplusplus
00023 extern "C" {
00024 #endif // __cplusplus
00025
00032
00037
00045 Z3_ast Z3_API Z3_mk_interpolant(__in Z3_context c, __in Z3_ast a);
00046
00047
00063 Z3_context Z3_API Z3_mk_interpolation_context(__in Z3_config cfg);
00064
00130 Z3_ast_vector Z3_API Z3_get_interpolant(__in Z3_context c, __in Z3_ast pf, __in Z3_ast pat, __in Z3_params p);
00131
00132
00133
00134
00135
00136
00137
00138
00139
00140
00141
00142
00143
00144
00145
00146
00147
00148
00149
00150
00151
00152
00153
00154
00155
00156
00157
00158
00159
00160
00161
00162
00163 Z3_lbool Z3_API Z3_compute_interpolant(__in Z3_context c,
00164 __in Z3_ast pat,
00165 __in Z3_params p,
00166 __out Z3_ast_vector *interp,
00167 __out Z3_model *model);
00168
00178 Z3_string Z3_API Z3_interpolation_profile(__in Z3_context ctx);
00179
00216 int Z3_API Z3_read_interpolation_problem(__in Z3_context ctx,
00217 __out unsigned *num,
00218 __out Z3_ast *cnsts[],
00219 __out unsigned *parents[],
00220 __in Z3_string filename,
00221 __out_opt Z3_string_ptr error,
00222 __out unsigned *num_theory,
00223 __out Z3_ast *theory[]);
00224
00225
00226
00246 int Z3_API Z3_check_interpolant(__in Z3_context ctx,
00247 __in unsigned num,
00248 __in_ecount(num) Z3_ast cnsts[],
00249 __in_ecount(num) unsigned parents[],
00250 __in_ecount(num - 1) Z3_ast *interps,
00251 __out_opt Z3_string_ptr error,
00252 __in unsigned num_theory,
00253 __in_ecount(num_theory) Z3_ast theory[]);
00254
00270 void Z3_API Z3_write_interpolation_problem(__in Z3_context ctx,
00271 __in unsigned num,
00272 __in_ecount(num) Z3_ast cnsts[],
00273 __in_ecount(num) unsigned parents[],
00274 __in Z3_string filename,
00275 __in unsigned num_theory,
00276 __in_ecount(num_theory) Z3_ast theory[]);
00277
00280
00281 #ifdef __cplusplus
00282 };
00283 #endif // __cplusplus
00284
00285 #endif