Z3
doc/tmp/z3_interp.h
Go to the documentation of this file.
00001 /*++
00002 Copyright (c) 2014 Microsoft Corporation
00003 
00004 Module Name:
00005 
00006     z3_interp.h
00007 
00008 Abstract:
00009 
00010     API for interpolation
00011 
00012 Author:
00013 
00014     Kenneth McMillan (kenmcmil)
00015 
00016 Notes:
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     /* Compute an interpolant for an unsatisfiable conjunction of formulas.
00133 
00134        This takes as an argument an interpolation pattern as in
00135        #Z3_get_interpolant. This is a conjunction, some subformulas of
00136        which are marked with the "interp" operator (see #Z3_mk_interpolant).
00137 
00138        The conjunction is first checked for unsatisfiability. The result
00139        of this check is returned in the out parameter "status". If the result
00140        is unsat, an interpolant is computed from the refutation as in #Z3_get_interpolant
00141        and returned as a vector of formulas. Otherwise the return value is
00142        an empty formula.
00143 
00144        See #Z3_get_interpolant for a discussion of supported theories.
00145 
00146        The advantage of this function over #Z3_get_interpolant is that
00147        it is not necessary to create a suitable SMT solver and generate
00148        a proof. The disadvantage is that it is not possible to use the
00149        solver incrementally.
00150 
00151        Parameters:
00152 
00153        \param c logical context.
00154        \param pat an interpolation pattern
00155        \param p parameters for solver creation
00156        \param status returns the status of the sat check
00157        \param model returns model if satisfiable
00158 
00159        Return value: status of SAT check
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
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines