Z3
z3_interp.h
Go to the documentation of this file.
1 /*++
2 Copyright (c) 2014 Microsoft Corporation
3 
4 Module Name:
5 
6  z3_interp.h
7 
8 Abstract:
9 
10  API for interpolation
11 
12 Author:
13 
14  Kenneth McMillan (kenmcmil)
15 
16 Notes:
17 
18 --*/
19 #ifndef Z3_INTERPOLATION_H_
20 #define Z3_INTERPOLATION_H_
21 
22 #ifdef __cplusplus
23 extern "C" {
24 #endif // __cplusplus
25 
28 
37  Z3_ast Z3_API Z3_mk_interpolant(Z3_context c, Z3_ast a);
38 
39 
55  Z3_context Z3_API Z3_mk_interpolation_context(Z3_config cfg);
56 
122  Z3_ast_vector Z3_API Z3_get_interpolant(Z3_context c, Z3_ast pf, Z3_ast pat, Z3_params p);
123 
124  /* Compute an interpolant for an unsatisfiable conjunction of formulas.
125 
126  This takes as an argument an interpolation pattern as in
127  #Z3_get_interpolant. This is a conjunction, some subformulas of
128  which are marked with the "interp" operator (see #Z3_mk_interpolant).
129 
130  The conjunction is first checked for unsatisfiability. The result
131  of this check is returned in the out parameter "status". If the result
132  is unsat, an interpolant is computed from the refutation as in #Z3_get_interpolant
133  and returned as a vector of formulas. Otherwise the return value is
134  an empty formula.
135 
136  See #Z3_get_interpolant for a discussion of supported theories.
137 
138  The advantage of this function over #Z3_get_interpolant is that
139  it is not necessary to create a suitable SMT solver and generate
140  a proof. The disadvantage is that it is not possible to use the
141  solver incrementally.
142 
143  Parameters:
144 
145  \param c logical context.
146  \param pat an interpolation pattern
147  \param p parameters for solver creation
148  \param status returns the status of the sat check
149  \param model returns model if satisfiable
150 
151  Return value: status of SAT check
152 
153  */
154 
155  Z3_lbool Z3_API Z3_compute_interpolant(Z3_context c,
156  Z3_ast pat,
157  Z3_params p,
158  Z3_ast_vector *interp,
159  Z3_model *model);
160 
170  Z3_string Z3_API Z3_interpolation_profile(Z3_context ctx);
171 
208  int Z3_API Z3_read_interpolation_problem(Z3_context ctx,
209  unsigned *num,
210  Z3_ast *cnsts[],
211  unsigned *parents[],
212  Z3_string filename,
213  Z3_string_ptr error,
214  unsigned *num_theory,
215  Z3_ast *theory[]);
216 
217 
218 
238  int Z3_API Z3_check_interpolant(Z3_context ctx,
239  unsigned num,
240  Z3_ast cnsts[],
241  unsigned parents[],
242  Z3_ast *interps,
243  Z3_string_ptr error,
244  unsigned num_theory,
245  Z3_ast theory[]);
246 
262  void Z3_API Z3_write_interpolation_problem(Z3_context ctx,
263  unsigned num,
264  Z3_ast cnsts[],
265  unsigned parents[],
266  Z3_string filename,
267  unsigned num_theory,
268  Z3_ast theory[]);
271 
272 #ifdef __cplusplus
273 }
274 #endif // __cplusplus
275 
276 #endif
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
Definition: z3_api.h:90
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.
Definition: z3_api.h:105
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 *.
Definition: z3_api.h:89