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 
32 
37 
45  Z3_ast Z3_API Z3_mk_interpolant(__in Z3_context c, __in Z3_ast a);
46 
47 
64 
130  Z3_ast_vector Z3_API Z3_get_interpolant(__in Z3_context c, __in Z3_ast pf, __in Z3_ast pat, __in Z3_params p);
131 
132  /* Compute an interpolant for an unsatisfiable conjunction of formulas.
133 
134  This takes as an argument an interpolation pattern as in
135  #Z3_get_interpolant. This is a conjunction, some subformulas of
136  which are marked with the "interp" operator (see #Z3_mk_interpolant).
137 
138  The conjunction is first checked for unsatisfiability. The result
139  of this check is returned in the out parameter "status". If the result
140  is unsat, an interpolant is computed from the refutation as in #Z3_get_interpolant
141  and returned as a vector of formulas. Otherwise the return value is
142  an empty formula.
143 
144  See #Z3_get_interpolant for a discussion of supported theories.
145 
146  The advantage of this function over #Z3_get_interpolant is that
147  it is not necessary to create a suitable SMT solver and generate
148  a proof. The disadvantage is that it is not possible to use the
149  solver incrementally.
150 
151  Parameters:
152 
153  \param c logical context.
154  \param pat an interpolation pattern
155  \param p parameters for solver creation
156  \param status returns the status of the sat check
157  \param model returns model if satisfiable
158 
159  Return value: status of SAT check
160 
161  */
162 
164  __in Z3_ast pat,
165  __in Z3_params p,
166  __out Z3_ast_vector *interp,
167  __out Z3_model *model);
168 
179 
216  int Z3_API Z3_read_interpolation_problem(__in Z3_context ctx,
217  __out unsigned *num,
218  __out Z3_ast *cnsts[],
219  __out unsigned *parents[],
220  __in Z3_string filename,
221  __out_opt Z3_string_ptr error,
222  __out unsigned *num_theory,
223  __out Z3_ast *theory[]);
224 
225 
226 
246  int Z3_API Z3_check_interpolant(__in Z3_context ctx,
247  __in unsigned num,
248  __in_ecount(num) Z3_ast cnsts[],
249  __in_ecount(num) unsigned parents[],
250  __in_ecount(num - 1) Z3_ast *interps,
251  __out_opt Z3_string_ptr error,
252  __in unsigned num_theory,
253  __in_ecount(num_theory) Z3_ast theory[]);
254 
270  void Z3_API Z3_write_interpolation_problem(__in Z3_context ctx,
271  __in unsigned num,
272  __in_ecount(num) Z3_ast cnsts[],
273  __in_ecount(num) unsigned parents[],
274  __in Z3_string filename,
275  __in unsigned num_theory,
276  __in_ecount(num_theory) Z3_ast theory[]);
277 
280 
281 #ifdef __cplusplus
282 };
283 #endif // __cplusplus
284 
285 #endif
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[])
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 generat...
Z3_string * Z3_string_ptr
Definition: z3_api.h:112
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[])
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
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:135
Z3_string Z3_API Z3_interpolation_profile(__in Z3_context ctx)
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)
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.
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.
const char * Z3_string
Z3 string type. It is just an alias for const char *.
Definition: z3_api.h:111