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 
46 
47 
64 
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  Z3_ast pat,
165  Z3_params p,
166  Z3_ast_vector *interp,
167  Z3_model *model);
168 
179 
217  unsigned *num,
218  Z3_ast *cnsts[],
219  unsigned *parents[],
220  Z3_string filename,
221  Z3_string_ptr error,
222  unsigned *num_theory,
223  Z3_ast *theory[]);
224 
225 
226 
246  int Z3_API Z3_check_interpolant(Z3_context ctx,
247  unsigned num,
248  Z3_ast cnsts[],
249  unsigned parents[],
250  Z3_ast *interps,
251  Z3_string_ptr error,
252  unsigned num_theory,
253  Z3_ast theory[]);
254 
271  unsigned num,
272  Z3_ast cnsts[],
273  unsigned parents[],
274  Z3_string filename,
275  unsigned num_theory,
276  Z3_ast theory[]);
277 
280 
281 #ifdef __cplusplus
282 };
283 #endif // __cplusplus
284 
285 #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:120
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:143
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:119