Z3
doc/tmp/z3_api.h
Go to the documentation of this file.
00001 #ifndef _Z3_API_H_
00002 #define _Z3_API_H_
00003 
00004 #ifdef CAMLIDL
00005   #ifdef MLAPIV3
00006     #define ML3only
00007     #define CorML3
00008   #else
00009     #define ML4only
00010     #define CorML4
00011   #endif
00012 #else
00013   #define Conly
00014   #define CorML3
00015   #define CorML4
00016 #endif
00017 
00018 #ifdef CorML3
00019 DEFINE_TYPE(Z3_symbol);
00020 DEFINE_TYPE(Z3_literals);
00021 DEFINE_TYPE(Z3_theory);
00022 DEFINE_TYPE(Z3_config);
00023 DEFINE_TYPE(Z3_context);
00024 DEFINE_TYPE(Z3_sort);
00025 #define Z3_sort_opt Z3_sort
00026 DEFINE_TYPE(Z3_func_decl);
00027 DEFINE_TYPE(Z3_ast);
00028 #define Z3_ast_opt Z3_ast
00029 DEFINE_TYPE(Z3_app);
00030 DEFINE_TYPE(Z3_pattern);
00031 DEFINE_TYPE(Z3_model);
00032 DEFINE_TYPE(Z3_constructor);
00033 DEFINE_TYPE(Z3_constructor_list);
00034 #endif
00035 #ifdef Conly
00036 DEFINE_TYPE(Z3_params);
00037 DEFINE_TYPE(Z3_param_descrs);
00038 DEFINE_TYPE(Z3_goal);
00039 DEFINE_TYPE(Z3_tactic);
00040 DEFINE_TYPE(Z3_probe);
00041 DEFINE_TYPE(Z3_stats);
00042 DEFINE_TYPE(Z3_solver);
00043 DEFINE_TYPE(Z3_ast_vector);
00044 DEFINE_TYPE(Z3_ast_map);
00045 DEFINE_TYPE(Z3_apply_result);
00046 DEFINE_TYPE(Z3_func_interp);
00047 #define Z3_func_interp_opt Z3_func_interp
00048 DEFINE_TYPE(Z3_func_entry);
00049 DEFINE_TYPE(Z3_fixedpoint);
00050 DEFINE_TYPE(Z3_rcf_num);
00051 DEFINE_VOID(Z3_theory_data);
00052 #endif
00053 
00054 #ifndef __int64
00055 #define __int64 long long
00056 #endif
00057 
00058 #ifndef __uint64
00059 #define __uint64 unsigned long long
00060 #endif
00061 
00067 
00098 #ifdef Conly
00099 
00102 typedef int Z3_bool;
00103 #else
00104 #define Z3_bool boolean
00105 #endif
00106 
00107 #ifdef Conly
00108 
00111 typedef const char * Z3_string;
00112 typedef Z3_string * Z3_string_ptr;
00113 #else
00114 typedef [string] const char * Z3_string;
00115 #define Z3_string_ptr Z3_string *
00116 #endif
00117     
00118 #ifdef Conly
00119 
00122 #define Z3_TRUE  1
00123 
00127 #define Z3_FALSE 0
00128 
00129 #endif
00130 
00135 typedef enum 
00136 {
00137     Z3_L_FALSE = -1,
00138     Z3_L_UNDEF,
00139     Z3_L_TRUE
00140 } Z3_lbool;
00141 
00150 typedef enum 
00151 {
00152     Z3_INT_SYMBOL,
00153     Z3_STRING_SYMBOL 
00154 } Z3_symbol_kind;
00155 
00156 
00171 typedef enum 
00172 {
00173     Z3_PARAMETER_INT,
00174     Z3_PARAMETER_DOUBLE,
00175     Z3_PARAMETER_RATIONAL,
00176     Z3_PARAMETER_SYMBOL,
00177     Z3_PARAMETER_SORT,
00178     Z3_PARAMETER_AST,
00179     Z3_PARAMETER_FUNC_DECL,
00180 } Z3_parameter_kind;
00181 
00186 typedef enum 
00187 {
00188     Z3_UNINTERPRETED_SORT,
00189     Z3_BOOL_SORT,
00190     Z3_INT_SORT,
00191     Z3_REAL_SORT,
00192     Z3_BV_SORT,
00193     Z3_ARRAY_SORT,
00194     Z3_DATATYPE_SORT,
00195     Z3_RELATION_SORT,
00196     Z3_FINITE_DOMAIN_SORT,
00197     Z3_UNKNOWN_SORT = 1000
00198 } Z3_sort_kind;
00199 
00212 typedef enum 
00213 {
00214     Z3_NUMERAL_AST,
00215     Z3_APP_AST,         
00216     Z3_VAR_AST,          
00217     Z3_QUANTIFIER_AST,    
00218     Z3_SORT_AST,
00219     Z3_FUNC_DECL_AST,
00220     Z3_UNKNOWN_AST = 1000 
00221 } Z3_ast_kind;
00222 
00880 typedef enum {
00881     // Basic
00882     Z3_OP_TRUE = 0x100,
00883     Z3_OP_FALSE,
00884     Z3_OP_EQ,
00885     Z3_OP_DISTINCT,
00886     Z3_OP_ITE,
00887     Z3_OP_AND,
00888     Z3_OP_OR,
00889     Z3_OP_IFF,
00890     Z3_OP_XOR,
00891     Z3_OP_NOT,
00892     Z3_OP_IMPLIES,
00893     Z3_OP_OEQ,
00894     Z3_OP_INTERP,
00895 
00896     // Arithmetic
00897     Z3_OP_ANUM = 0x200,
00898     Z3_OP_AGNUM,                
00899     Z3_OP_LE,
00900     Z3_OP_GE,
00901     Z3_OP_LT,
00902     Z3_OP_GT,
00903     Z3_OP_ADD,
00904     Z3_OP_SUB,
00905     Z3_OP_UMINUS,
00906     Z3_OP_MUL,
00907     Z3_OP_DIV,
00908     Z3_OP_IDIV,
00909     Z3_OP_REM,
00910     Z3_OP_MOD,
00911     Z3_OP_TO_REAL,
00912     Z3_OP_TO_INT,
00913     Z3_OP_IS_INT,
00914     Z3_OP_POWER,                
00915 
00916     // Arrays & Sets
00917     Z3_OP_STORE = 0x300,
00918     Z3_OP_SELECT,
00919     Z3_OP_CONST_ARRAY,
00920     Z3_OP_ARRAY_MAP,
00921     Z3_OP_ARRAY_DEFAULT,
00922     Z3_OP_SET_UNION,
00923     Z3_OP_SET_INTERSECT,
00924     Z3_OP_SET_DIFFERENCE,
00925     Z3_OP_SET_COMPLEMENT,
00926     Z3_OP_SET_SUBSET,
00927     Z3_OP_AS_ARRAY,
00928 
00929     // Bit-vectors
00930     Z3_OP_BNUM = 0x400,
00931     Z3_OP_BIT1,
00932     Z3_OP_BIT0,
00933     Z3_OP_BNEG,
00934     Z3_OP_BADD,
00935     Z3_OP_BSUB,
00936     Z3_OP_BMUL,
00937     
00938     Z3_OP_BSDIV,
00939     Z3_OP_BUDIV,
00940     Z3_OP_BSREM,
00941     Z3_OP_BUREM,
00942     Z3_OP_BSMOD,
00943 
00944     // special functions to record the division by 0 cases
00945     // these are internal functions 
00946     Z3_OP_BSDIV0, 
00947     Z3_OP_BUDIV0,
00948     Z3_OP_BSREM0,
00949     Z3_OP_BUREM0,
00950     Z3_OP_BSMOD0,
00951     
00952     Z3_OP_ULEQ,
00953     Z3_OP_SLEQ,
00954     Z3_OP_UGEQ,
00955     Z3_OP_SGEQ,
00956     Z3_OP_ULT,
00957     Z3_OP_SLT,
00958     Z3_OP_UGT,
00959     Z3_OP_SGT,
00960 
00961     Z3_OP_BAND,
00962     Z3_OP_BOR,
00963     Z3_OP_BNOT,
00964     Z3_OP_BXOR,
00965     Z3_OP_BNAND,
00966     Z3_OP_BNOR,
00967     Z3_OP_BXNOR,
00968 
00969     Z3_OP_CONCAT,
00970     Z3_OP_SIGN_EXT,
00971     Z3_OP_ZERO_EXT,
00972     Z3_OP_EXTRACT,
00973     Z3_OP_REPEAT,
00974 
00975     Z3_OP_BREDOR,
00976     Z3_OP_BREDAND,
00977     Z3_OP_BCOMP,
00978 
00979     Z3_OP_BSHL,
00980     Z3_OP_BLSHR,
00981     Z3_OP_BASHR,
00982     Z3_OP_ROTATE_LEFT,
00983     Z3_OP_ROTATE_RIGHT,
00984     Z3_OP_EXT_ROTATE_LEFT,
00985     Z3_OP_EXT_ROTATE_RIGHT,
00986 
00987     Z3_OP_INT2BV,
00988     Z3_OP_BV2INT,
00989     Z3_OP_CARRY,
00990     Z3_OP_XOR3,
00991     
00992     // Proofs
00993     Z3_OP_PR_UNDEF = 0x500,     
00994     Z3_OP_PR_TRUE,
00995     Z3_OP_PR_ASSERTED, 
00996     Z3_OP_PR_GOAL, 
00997     Z3_OP_PR_MODUS_PONENS, 
00998     Z3_OP_PR_REFLEXIVITY, 
00999     Z3_OP_PR_SYMMETRY, 
01000     Z3_OP_PR_TRANSITIVITY, 
01001     Z3_OP_PR_TRANSITIVITY_STAR, 
01002     Z3_OP_PR_MONOTONICITY, 
01003     Z3_OP_PR_QUANT_INTRO,
01004     Z3_OP_PR_DISTRIBUTIVITY, 
01005     Z3_OP_PR_AND_ELIM, 
01006     Z3_OP_PR_NOT_OR_ELIM, 
01007     Z3_OP_PR_REWRITE, 
01008     Z3_OP_PR_REWRITE_STAR, 
01009     Z3_OP_PR_PULL_QUANT, 
01010     Z3_OP_PR_PULL_QUANT_STAR, 
01011     Z3_OP_PR_PUSH_QUANT, 
01012     Z3_OP_PR_ELIM_UNUSED_VARS, 
01013     Z3_OP_PR_DER, 
01014     Z3_OP_PR_QUANT_INST,
01015     Z3_OP_PR_HYPOTHESIS, 
01016     Z3_OP_PR_LEMMA, 
01017     Z3_OP_PR_UNIT_RESOLUTION, 
01018     Z3_OP_PR_IFF_TRUE, 
01019     Z3_OP_PR_IFF_FALSE, 
01020     Z3_OP_PR_COMMUTATIVITY, 
01021     Z3_OP_PR_DEF_AXIOM,
01022     Z3_OP_PR_DEF_INTRO, 
01023     Z3_OP_PR_APPLY_DEF, 
01024     Z3_OP_PR_IFF_OEQ, 
01025     Z3_OP_PR_NNF_POS, 
01026     Z3_OP_PR_NNF_NEG, 
01027     Z3_OP_PR_NNF_STAR, 
01028     Z3_OP_PR_CNF_STAR, 
01029     Z3_OP_PR_SKOLEMIZE,
01030     Z3_OP_PR_MODUS_PONENS_OEQ, 
01031     Z3_OP_PR_TH_LEMMA, 
01032     Z3_OP_PR_HYPER_RESOLVE,
01033 
01034     // Sequences
01035     Z3_OP_RA_STORE = 0x600,
01036     Z3_OP_RA_EMPTY,
01037     Z3_OP_RA_IS_EMPTY,
01038     Z3_OP_RA_JOIN,
01039     Z3_OP_RA_UNION,
01040     Z3_OP_RA_WIDEN,
01041     Z3_OP_RA_PROJECT,
01042     Z3_OP_RA_FILTER,
01043     Z3_OP_RA_NEGATION_FILTER,
01044     Z3_OP_RA_RENAME,
01045     Z3_OP_RA_COMPLEMENT,
01046     Z3_OP_RA_SELECT,
01047     Z3_OP_RA_CLONE,
01048     Z3_OP_FD_LT,
01049 
01050     // Auxiliary
01051     Z3_OP_LABEL = 0x700,
01052     Z3_OP_LABEL_LIT,
01053 
01054     // Datatypes
01055     Z3_OP_DT_CONSTRUCTOR=0x800,
01056     Z3_OP_DT_RECOGNISER,
01057     Z3_OP_DT_ACCESSOR,
01058 
01059     Z3_OP_UNINTERPRETED         
01060 } Z3_decl_kind;
01061 
01076 typedef enum {
01077     Z3_PK_UINT,
01078     Z3_PK_BOOL,
01079     Z3_PK_DOUBLE,
01080     Z3_PK_SYMBOL,
01081     Z3_PK_STRING,
01082     Z3_PK_OTHER,
01083     Z3_PK_INVALID
01084 } Z3_param_kind;
01085 
01086 #ifdef CorML3
01087 
01100 typedef enum {
01101     Z3_NO_FAILURE,
01102     Z3_UNKNOWN,
01103     Z3_TIMEOUT,
01104     Z3_MEMOUT_WATERMARK,     
01105     Z3_CANCELED,      
01106     Z3_NUM_CONFLICTS, 
01107     Z3_THEORY,        
01108     Z3_QUANTIFIERS
01109 } Z3_search_failure;
01110 #endif
01111 
01121 typedef enum {
01122     Z3_PRINT_SMTLIB_FULL,
01123     Z3_PRINT_LOW_LEVEL,
01124     Z3_PRINT_SMTLIB_COMPLIANT,
01125     Z3_PRINT_SMTLIB2_COMPLIANT
01126 } Z3_ast_print_mode;
01127 
01128 
01129 #ifdef CorML4
01130 
01148 typedef enum
01149 {
01150     Z3_OK,            
01151     Z3_SORT_ERROR,    
01152     Z3_IOB,           
01153     Z3_INVALID_ARG,   
01154     Z3_PARSER_ERROR,  
01155     Z3_NO_PARSER,
01156     Z3_INVALID_PATTERN,
01157     Z3_MEMOUT_FAIL,
01158     Z3_FILE_ACCESS_ERROR,
01159     Z3_INTERNAL_FATAL,
01160     Z3_INVALID_USAGE,
01161     Z3_DEC_REF_ERROR,
01162     Z3_EXCEPTION                
01163 } Z3_error_code;
01164 
01165 #endif
01166 
01199 #ifdef Conly
01200 
01203 typedef void Z3_error_handler(Z3_context c, Z3_error_code e);
01204 
01205 #endif
01206 #ifdef ML4only
01207 #include <error_handling.idl>
01208 #endif
01209 
01210 
01211 #ifdef CorML4
01212 
01221 typedef enum 
01222 {
01223     Z3_GOAL_PRECISE,    
01224     Z3_GOAL_UNDER,      
01225     Z3_GOAL_OVER,       
01226     Z3_GOAL_UNDER_OVER  
01227 } Z3_goal_prec;
01228 
01229 #endif
01230 
01233 #ifndef CAMLIDL
01234 #ifdef __cplusplus
01235 extern "C" {
01236 #endif // __cplusplus
01237 #else
01238 [pointer_default(ref)] interface Z3 {
01239 #endif // CAMLIDL
01240     
01241 #ifdef CorML3
01242 
01267     void Z3_API Z3_global_param_set(__in Z3_string param_id, __in Z3_string param_value);
01268 
01269 
01277     void Z3_API Z3_global_param_reset_all(void);
01278     
01291     Z3_bool_opt Z3_API Z3_global_param_get(__in Z3_string param_id, __out_opt Z3_string_ptr param_value);
01292 
01299 
01334     Z3_config Z3_API Z3_mk_config(void);
01335 
01342     void Z3_API Z3_del_config(__in Z3_config c);
01343 
01352     void Z3_API Z3_set_param_value(__in Z3_config c, __in Z3_string param_id, __in Z3_string param_value);
01353     
01355 #endif
01356 
01361 
01384 #ifdef CorML3
01385     Z3_context Z3_API Z3_mk_context(__in Z3_config c);
01386 #endif
01387 #ifdef ML4only
01388 #include <mlx_mk_context_x.idl>
01389 #endif
01390 
01391 #ifdef Conly
01392 
01411     Z3_context Z3_API Z3_mk_context_rc(__in Z3_config c);
01412 #endif
01413     
01414 #ifdef CorML3
01415 
01421     void Z3_API Z3_del_context(__in Z3_context c);
01422 #endif
01423     
01424 #ifdef Conly
01425 
01431     void Z3_API Z3_inc_ref(__in Z3_context c, __in Z3_ast a);
01432 
01439     void Z3_API Z3_dec_ref(__in Z3_context c, __in Z3_ast a);
01440 #endif
01441 
01448     void Z3_API Z3_update_param_value(__in Z3_context c, __in Z3_string param_id, __in Z3_string param_value);
01449 
01450 #ifdef CorML4
01451 
01456     void Z3_API Z3_interrupt(__in Z3_context c);
01457 #endif
01458 
01459 
01462 #ifdef CorML4
01463 
01467     
01477     Z3_params Z3_API Z3_mk_params(__in Z3_context c);
01478     
01479 #ifdef Conly
01480 
01484     void Z3_API Z3_params_inc_ref(__in Z3_context c, __in Z3_params p);
01485 
01490     void Z3_API Z3_params_dec_ref(__in Z3_context c, __in Z3_params p);
01491 #endif
01492 
01497     void Z3_API Z3_params_set_bool(__in Z3_context c, __in Z3_params p, __in Z3_symbol k, __in Z3_bool v);
01498 
01503     void Z3_API Z3_params_set_uint(__in Z3_context c, __in Z3_params p, __in Z3_symbol k, __in unsigned v);
01504 
01509     void Z3_API Z3_params_set_double(__in Z3_context c, __in Z3_params p, __in Z3_symbol k, __in double v);
01510 
01515     void Z3_API Z3_params_set_symbol(__in Z3_context c, __in Z3_params p, __in Z3_symbol k, __in Z3_symbol v);
01516     
01522     Z3_string Z3_API Z3_params_to_string(__in Z3_context c, __in Z3_params p);
01523 
01530     void Z3_API Z3_params_validate(__in Z3_context c, __in Z3_params p, __in Z3_param_descrs d);
01531     
01532 #endif
01533 
01536 #ifdef CorML4
01537 
01541 
01542 #ifdef Conly
01543 
01547     void Z3_API Z3_param_descrs_inc_ref(__in Z3_context c, __in Z3_param_descrs p);
01548 
01553     void Z3_API Z3_param_descrs_dec_ref(__in Z3_context c, __in Z3_param_descrs p);
01554 #endif
01555     
01560     Z3_param_kind Z3_API Z3_param_descrs_get_kind(__in Z3_context c, __in Z3_param_descrs p, __in Z3_symbol n);
01561     
01566     unsigned Z3_API Z3_param_descrs_size(__in Z3_context c, __in Z3_param_descrs p);
01567 
01574     Z3_symbol Z3_API Z3_param_descrs_get_name(__in Z3_context c, __in Z3_param_descrs p, __in unsigned i);
01575 
01581     Z3_string Z3_API Z3_param_descrs_to_string(__in Z3_context c, __in Z3_param_descrs p);
01582 
01584 #endif
01585 
01590 
01591 #ifdef ML4only
01592 #include <mlx_mk_symbol.idl>
01593 #endif
01594 
01610     Z3_symbol Z3_API Z3_mk_int_symbol(__in Z3_context c, __in int i);
01611 
01620     Z3_symbol Z3_API Z3_mk_string_symbol(__in Z3_context c, __in Z3_string s);
01621 
01628 
01629 #ifdef ML4only
01630 #include <mlx_mk_sort.idl>
01631 #endif
01632 
01643     Z3_sort Z3_API Z3_mk_uninterpreted_sort(__in Z3_context c, __in Z3_symbol s);
01644 
01651     Z3_sort Z3_API Z3_mk_bool_sort(__in Z3_context c);
01652     
01663     Z3_sort Z3_API Z3_mk_int_sort(__in Z3_context c);
01664     
01672     Z3_sort Z3_API Z3_mk_real_sort(__in Z3_context c);
01673 
01682     Z3_sort Z3_API Z3_mk_bv_sort(__in Z3_context c, __in unsigned sz);
01683 
01696     Z3_sort Z3_API Z3_mk_finite_domain_sort(__in Z3_context c, __in Z3_symbol name, __in unsigned __int64 size);
01697 
01708     Z3_sort Z3_API Z3_mk_array_sort(__in Z3_context c, __in Z3_sort domain, __in Z3_sort range);
01709 
01729     Z3_sort Z3_API Z3_mk_tuple_sort(__in Z3_context c, 
01730                                         __in Z3_symbol mk_tuple_name, 
01731                                         __in unsigned num_fields, 
01732                                         __in_ecount(num_fields) Z3_symbol const field_names[],
01733                                         __in_ecount(num_fields) Z3_sort const field_sorts[],
01734                                         __out Z3_func_decl * mk_tuple_decl,
01735                                         __out_ecount(num_fields)  Z3_func_decl proj_decl[]);
01736 
01762     Z3_sort Z3_API Z3_mk_enumeration_sort(__in Z3_context c, 
01763                                           __in Z3_symbol name,
01764                                           __in unsigned n,
01765                                           __in_ecount(n)  Z3_symbol  const enum_names[],
01766                                           __out_ecount(n) Z3_func_decl enum_consts[],
01767                                           __out_ecount(n) Z3_func_decl enum_testers[]);
01768 
01789     Z3_sort Z3_API Z3_mk_list_sort(__in Z3_context c,
01790                                    __in Z3_symbol name,
01791                                    __in Z3_sort   elem_sort,
01792                                    __out Z3_func_decl* nil_decl,
01793                                    __out Z3_func_decl* is_nil_decl,
01794                                    __out Z3_func_decl* cons_decl,
01795                                    __out Z3_func_decl* is_cons_decl,
01796                                    __out Z3_func_decl* head_decl,
01797                                    __out Z3_func_decl* tail_decl
01798                                    );
01799 
01800 BEGIN_MLAPI_EXCLUDE
01817     Z3_constructor Z3_API Z3_mk_constructor(__in Z3_context c,
01818                                             __in Z3_symbol name,
01819                                             __in Z3_symbol recognizer,
01820                                             __in unsigned num_fields,
01821                                             __in_ecount(num_fields) Z3_symbol const field_names[],
01822                                             __in_ecount(num_fields) Z3_sort_opt const sorts[],
01823                                             __in_ecount(num_fields) unsigned sort_refs[]
01824                                             );
01825     
01833     void Z3_API Z3_del_constructor(__in Z3_context c, __in Z3_constructor constr);
01834 
01845     Z3_sort Z3_API Z3_mk_datatype(__in Z3_context c,
01846                                   __in Z3_symbol name,
01847                                   __in unsigned num_constructors,
01848                                   __inout_ecount(num_constructors) Z3_constructor constructors[]);
01849 
01850 
01859     Z3_constructor_list Z3_API Z3_mk_constructor_list(__in Z3_context c,
01860                                                       __in unsigned num_constructors,
01861                                                       __in_ecount(num_constructors) Z3_constructor const constructors[]);
01862 
01872     void Z3_API Z3_del_constructor_list(__in Z3_context c, __in Z3_constructor_list clist);
01873                                         
01884     void Z3_API Z3_mk_datatypes(__in Z3_context c,
01885                                 __in unsigned num_sorts,
01886                                 __in_ecount(num_sorts) Z3_symbol const sort_names[],
01887                                 __out_ecount(num_sorts) Z3_sort sorts[],
01888                                 __inout_ecount(num_sorts) Z3_constructor_list constructor_lists[]);
01889 
01901     void Z3_API Z3_query_constructor(__in Z3_context c,
01902                                      __in Z3_constructor constr,
01903                                      __in unsigned num_fields,
01904                                      __out Z3_func_decl* constructor,
01905                                      __out Z3_func_decl* tester,
01906                                      __out_ecount(num_fields) Z3_func_decl accessors[]);
01907 END_MLAPI_EXCLUDE
01908 
01915 
01935     Z3_func_decl Z3_API Z3_mk_func_decl(__in Z3_context c, __in Z3_symbol s,
01936                                         __in unsigned domain_size, __in_ecount(domain_size) Z3_sort const domain[],
01937                                         __in Z3_sort range);
01938 
01939     
01946     Z3_ast Z3_API Z3_mk_app(
01947         __in Z3_context c, 
01948         __in Z3_func_decl d,
01949         __in unsigned num_args, 
01950         __in_ecount(num_args) Z3_ast const args[]);
01951 
01967     Z3_ast Z3_API Z3_mk_const(__in Z3_context c, __in Z3_symbol s, __in Z3_sort ty);
01968 
01980     Z3_func_decl Z3_API Z3_mk_fresh_func_decl(__in Z3_context c, __in Z3_string prefix,
01981                                                    __in unsigned domain_size, __in_ecount(domain_size) Z3_sort const domain[],
01982                                                    __in Z3_sort range);
01983     
01998     Z3_ast Z3_API Z3_mk_fresh_const(__in Z3_context c, __in Z3_string prefix, __in Z3_sort ty);
02009     Z3_ast Z3_API Z3_mk_true(__in Z3_context c);
02010 
02015     Z3_ast Z3_API Z3_mk_false(__in Z3_context c);
02016     
02024     Z3_ast Z3_API Z3_mk_eq(__in Z3_context c, __in Z3_ast l, __in Z3_ast r);
02025     
02040     Z3_ast Z3_API Z3_mk_distinct(__in Z3_context c, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[]);
02041 
02049     Z3_ast Z3_API Z3_mk_not(__in Z3_context c, __in Z3_ast a);
02050         
02060     Z3_ast Z3_API Z3_mk_ite(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2, __in Z3_ast t3);
02061 
02069     Z3_ast Z3_API Z3_mk_iff(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
02070 
02078     Z3_ast Z3_API Z3_mk_implies(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
02079     
02087     Z3_ast Z3_API Z3_mk_xor(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
02088     
02099     Z3_ast Z3_API Z3_mk_and(__in Z3_context c, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[]);
02100     
02111     Z3_ast Z3_API Z3_mk_or(__in Z3_context c, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[]);
02128     Z3_ast Z3_API Z3_mk_add(__in Z3_context c, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[]);
02129     
02141     Z3_ast Z3_API Z3_mk_mul(__in Z3_context c, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[]);
02142     
02153     Z3_ast Z3_API Z3_mk_sub(__in Z3_context c, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[]);
02154 
02162     Z3_ast Z3_API Z3_mk_unary_minus(__in Z3_context c, __in Z3_ast arg);
02163 
02173     Z3_ast Z3_API Z3_mk_div(__in Z3_context c, __in Z3_ast arg1, __in Z3_ast arg2);
02174 
02182     Z3_ast Z3_API Z3_mk_mod(__in Z3_context c, __in Z3_ast arg1, __in Z3_ast arg2);
02183 
02191     Z3_ast Z3_API Z3_mk_rem(__in Z3_context c, __in Z3_ast arg1, __in Z3_ast arg2);
02192 
02199     Z3_ast Z3_API Z3_mk_power(__in Z3_context c, __in Z3_ast arg1, __in Z3_ast arg2);
02200 
02208     Z3_ast Z3_API Z3_mk_lt(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
02209 
02217     Z3_ast Z3_API Z3_mk_le(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
02218 
02226     Z3_ast Z3_API Z3_mk_gt(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
02227 
02235     Z3_ast Z3_API Z3_mk_ge(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
02236 
02254     Z3_ast Z3_API Z3_mk_int2real(__in Z3_context c, __in Z3_ast t1);
02255 
02267     Z3_ast Z3_API Z3_mk_real2int(__in Z3_context c, __in Z3_ast t1);
02268 
02277     Z3_ast Z3_API Z3_mk_is_int(__in Z3_context c, __in Z3_ast t1);
02291     Z3_ast Z3_API Z3_mk_bvnot(__in Z3_context c, __in Z3_ast t1);
02292 
02300     Z3_ast Z3_API Z3_mk_bvredand(__in Z3_context c, __in Z3_ast t1);
02301 
02309     Z3_ast Z3_API Z3_mk_bvredor(__in Z3_context c, __in Z3_ast t1);
02310 
02318     Z3_ast Z3_API Z3_mk_bvand(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
02319 
02327     Z3_ast Z3_API Z3_mk_bvor(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
02328 
02336     Z3_ast Z3_API Z3_mk_bvxor(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
02337 
02345     Z3_ast Z3_API Z3_mk_bvnand(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
02346 
02354     Z3_ast Z3_API Z3_mk_bvnor(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
02355 
02363     Z3_ast Z3_API Z3_mk_bvxnor(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
02364 
02372     Z3_ast Z3_API Z3_mk_bvneg(__in Z3_context c, __in Z3_ast t1);
02373     
02381     Z3_ast Z3_API Z3_mk_bvadd(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
02382 
02390     Z3_ast Z3_API Z3_mk_bvsub(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
02391     
02399     Z3_ast Z3_API Z3_mk_bvmul(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
02400 
02412     Z3_ast Z3_API Z3_mk_bvudiv(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
02413 
02429     Z3_ast Z3_API Z3_mk_bvsdiv(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
02430 
02442     Z3_ast Z3_API Z3_mk_bvurem(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
02443 
02458     Z3_ast Z3_API Z3_mk_bvsrem(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
02459 
02471     Z3_ast Z3_API Z3_mk_bvsmod(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
02472 
02480     Z3_ast Z3_API Z3_mk_bvult(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
02481     
02497     Z3_ast Z3_API Z3_mk_bvslt(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
02498 
02506     Z3_ast Z3_API Z3_mk_bvule(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
02507 
02515     Z3_ast Z3_API Z3_mk_bvsle(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
02516 
02524     Z3_ast Z3_API Z3_mk_bvuge(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
02525 
02533     Z3_ast Z3_API Z3_mk_bvsge(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
02534 
02542     Z3_ast Z3_API Z3_mk_bvugt(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
02543 
02551     Z3_ast Z3_API Z3_mk_bvsgt(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
02552 
02563     Z3_ast Z3_API Z3_mk_concat(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
02564     
02574     Z3_ast Z3_API Z3_mk_extract(__in Z3_context c, __in unsigned high, __in unsigned low, __in Z3_ast t1);
02575 
02585     Z3_ast Z3_API Z3_mk_sign_ext(__in Z3_context c, __in unsigned i, __in Z3_ast t1);
02586 
02596     Z3_ast Z3_API Z3_mk_zero_ext(__in Z3_context c, __in unsigned i, __in Z3_ast t1);
02597 
02605     Z3_ast Z3_API Z3_mk_repeat(__in Z3_context c, __in unsigned i, __in Z3_ast t1);
02606 
02621     Z3_ast Z3_API Z3_mk_bvshl(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
02622 
02637     Z3_ast Z3_API Z3_mk_bvlshr(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
02638 
02654     Z3_ast Z3_API Z3_mk_bvashr(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
02655     
02663     Z3_ast Z3_API Z3_mk_rotate_left(__in Z3_context c, __in unsigned i, __in Z3_ast t1);
02664     
02672     Z3_ast Z3_API Z3_mk_rotate_right(__in Z3_context c, __in unsigned i, __in Z3_ast t1);
02673 
02681     Z3_ast Z3_API Z3_mk_ext_rotate_left(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
02682 
02690     Z3_ast Z3_API Z3_mk_ext_rotate_right(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
02691     
02703     Z3_ast Z3_API Z3_mk_int2bv(__in Z3_context c, __in unsigned n, __in Z3_ast t1);
02704 
02720     Z3_ast Z3_API Z3_mk_bv2int(__in Z3_context c,__in Z3_ast t1, Z3_bool is_signed);
02721 
02730     Z3_ast Z3_API Z3_mk_bvadd_no_overflow(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2, Z3_bool is_signed);
02731 
02740     Z3_ast Z3_API Z3_mk_bvadd_no_underflow(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
02741 
02750     Z3_ast Z3_API Z3_mk_bvsub_no_overflow(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
02751 
02760     Z3_ast Z3_API Z3_mk_bvsub_no_underflow(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2, Z3_bool is_signed);
02761 
02770     Z3_ast Z3_API Z3_mk_bvsdiv_no_overflow(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
02771 
02780     Z3_ast Z3_API Z3_mk_bvneg_no_overflow(__in Z3_context c, __in Z3_ast t1);
02781 
02790     Z3_ast Z3_API Z3_mk_bvmul_no_overflow(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2, Z3_bool is_signed);
02791 
02800     Z3_ast Z3_API Z3_mk_bvmul_no_underflow(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
02821     Z3_ast Z3_API Z3_mk_select(__in Z3_context c, __in Z3_ast a, __in Z3_ast i);
02822     
02839     Z3_ast Z3_API Z3_mk_store(__in Z3_context c, __in Z3_ast a, __in Z3_ast i, __in Z3_ast v);
02840 
02852     Z3_ast Z3_API Z3_mk_const_array(__in Z3_context c, __in Z3_sort domain, __in Z3_ast v);
02853 
02867     Z3_ast Z3_API Z3_mk_map(__in Z3_context c, __in Z3_func_decl f, unsigned n, __in Z3_ast const* args);
02868 
02878     Z3_ast Z3_API Z3_mk_array_default(__in Z3_context c, __in Z3_ast array);
02889     Z3_sort Z3_API Z3_mk_set_sort(__in Z3_context c, __in Z3_sort ty);
02890 
02895     Z3_ast Z3_API Z3_mk_empty_set(__in Z3_context c, __in Z3_sort domain);
02896 
02901     Z3_ast Z3_API Z3_mk_full_set(__in Z3_context c, __in Z3_sort domain);
02902 
02909     Z3_ast Z3_API Z3_mk_set_add(__in Z3_context c, __in Z3_ast set, __in Z3_ast elem);
02910 
02917     Z3_ast Z3_API Z3_mk_set_del(__in Z3_context c, __in Z3_ast set, __in Z3_ast elem);
02918 
02923     Z3_ast Z3_API Z3_mk_set_union(__in Z3_context c, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[]);
02924 
02929     Z3_ast Z3_API Z3_mk_set_intersect(__in Z3_context c, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[]);
02930 
02935     Z3_ast Z3_API Z3_mk_set_difference(__in Z3_context c, __in Z3_ast arg1, __in Z3_ast arg2);
02936 
02941     Z3_ast Z3_API Z3_mk_set_complement(__in Z3_context c, __in Z3_ast arg);
02942 
02949     Z3_ast Z3_API Z3_mk_set_member(__in Z3_context c, __in Z3_ast elem, __in Z3_ast set);
02950 
02955     Z3_ast Z3_API Z3_mk_set_subset(__in Z3_context c, __in Z3_ast arg1, __in Z3_ast arg2);
02962 
02963 #ifdef ML4only
02964 #include <mlx_mk_numeral.idl>
02965 #endif
02966 
02982     Z3_ast Z3_API Z3_mk_numeral(__in Z3_context c, __in Z3_string numeral, __in Z3_sort ty);
02983 
02998     Z3_ast Z3_API Z3_mk_real(__in Z3_context c, __in int num, __in int den);
02999     
03009     Z3_ast Z3_API Z3_mk_int(__in Z3_context c, __in int v, __in Z3_sort ty);
03010     
03011 #ifdef Conly
03012 
03021     Z3_ast Z3_API Z3_mk_unsigned_int(__in Z3_context c, __in unsigned v, __in Z3_sort ty);
03022 #endif
03023 
03033     Z3_ast Z3_API Z3_mk_int64(__in Z3_context c, __in __int64 v, __in Z3_sort ty);
03034 
03035 #ifdef Conly
03036 
03045     Z3_ast Z3_API Z3_mk_unsigned_int64(__in Z3_context c, __in unsigned __int64 v, __in Z3_sort ty);
03046 #endif
03047 
03054 
03074     Z3_pattern Z3_API Z3_mk_pattern(
03075         __in Z3_context c,
03076         __in unsigned num_patterns, __in_ecount(num_patterns) Z3_ast const terms[]);
03077 
03106     Z3_ast Z3_API Z3_mk_bound(__in Z3_context c, __in unsigned index, __in Z3_sort ty);
03107     
03140     Z3_ast Z3_API Z3_mk_forall(__in Z3_context c, __in unsigned weight,
03141                                __in unsigned num_patterns, __in_ecount(num_patterns) Z3_pattern const patterns[],
03142                                __in unsigned num_decls, __in_ecount(num_decls) Z3_sort const sorts[],
03143                                __in_ecount(num_decls) Z3_symbol const decl_names[],
03144                                __in Z3_ast body);
03145 
03155     Z3_ast Z3_API Z3_mk_exists(__in Z3_context c, __in unsigned weight,
03156                                __in unsigned num_patterns, __in_ecount(num_patterns) Z3_pattern const patterns[],
03157                                __in unsigned num_decls, __in_ecount(num_decls) Z3_sort const sorts[],
03158                                __in_ecount(num_decls) Z3_symbol const decl_names[],
03159                                __in Z3_ast body);
03160 
03181     Z3_ast Z3_API Z3_mk_quantifier(
03182         __in Z3_context c, 
03183         __in Z3_bool is_forall, 
03184         __in unsigned weight, 
03185         __in unsigned num_patterns, __in_ecount(num_patterns) Z3_pattern const patterns[], 
03186         __in unsigned num_decls, __in_ecount(num_decls) Z3_sort const sorts[], 
03187         __in_ecount(num_decls) Z3_symbol const decl_names[], 
03188         __in Z3_ast body);
03189 
03190 
03214     Z3_ast Z3_API Z3_mk_quantifier_ex(
03215         __in Z3_context c, 
03216         __in Z3_bool is_forall, 
03217         __in unsigned weight, 
03218         __in Z3_symbol quantifier_id,
03219         __in Z3_symbol skolem_id,
03220         __in unsigned num_patterns, __in_ecount(num_patterns) Z3_pattern const patterns[], 
03221         __in unsigned num_no_patterns, __in_ecount(num_no_patterns) Z3_ast const no_patterns[], 
03222         __in unsigned num_decls, __in_ecount(num_decls) Z3_sort const sorts[], 
03223         __in_ecount(num_decls) Z3_symbol const decl_names[], 
03224         __in Z3_ast body);
03225 
03243     Z3_ast Z3_API Z3_mk_forall_const(
03244         __in Z3_context c, 
03245         unsigned weight,
03246         unsigned num_bound,
03247         __in_ecount(num_bound) Z3_app const bound[],
03248         unsigned num_patterns,
03249         __in_ecount(num_patterns) Z3_pattern const patterns[],
03250         __in Z3_ast body
03251         );
03252 
03272     Z3_ast Z3_API Z3_mk_exists_const(
03273         __in Z3_context c, 
03274         unsigned weight,
03275         unsigned num_bound,
03276         __in_ecount(num_bound) Z3_app const bound[],
03277         unsigned num_patterns,
03278         __in_ecount(num_patterns) Z3_pattern const patterns[],
03279         __in Z3_ast body
03280         );
03281 
03288     Z3_ast Z3_API Z3_mk_quantifier_const(
03289         __in Z3_context c, 
03290         Z3_bool is_forall,
03291         unsigned weight,
03292         unsigned num_bound,  __in_ecount(num_bound) Z3_app const bound[],
03293         unsigned num_patterns, __in_ecount(num_patterns) Z3_pattern const patterns[],
03294         __in Z3_ast body
03295         );
03296 
03297 
03298 
03305     Z3_ast Z3_API Z3_mk_quantifier_const_ex(
03306         __in Z3_context c, 
03307         Z3_bool is_forall,
03308         unsigned weight,
03309         __in Z3_symbol quantifier_id,
03310         __in Z3_symbol skolem_id,
03311         unsigned num_bound,  __in_ecount(num_bound) Z3_app const bound[],
03312         unsigned num_patterns, __in_ecount(num_patterns) Z3_pattern const patterns[],
03313         unsigned num_no_patterns, __in_ecount(num_no_patterns) Z3_ast const no_patterns[],
03314         __in Z3_ast body
03315         );
03316 
03323 
03328 #ifdef ML4only
03329 #include <mlx_symbol_refine.idl>
03330 #endif
03331 
03342     Z3_symbol_kind Z3_API Z3_get_symbol_kind(__in Z3_context c, __in Z3_symbol s);
03343 
03353     int Z3_API Z3_get_symbol_int(__in Z3_context c, __in Z3_symbol s);
03354     
03368     Z3_string Z3_API Z3_get_symbol_string(__in Z3_context c, __in Z3_symbol s);
03369 
03370 
03375 #ifdef ML4only
03376 #include <mlx_sort_refine.idl>
03377 #endif
03378 
03383     Z3_symbol Z3_API Z3_get_sort_name(__in Z3_context c, __in Z3_sort d);
03384 
03390     unsigned Z3_API Z3_get_sort_id(__in Z3_context c, Z3_sort s);
03391 
03401     Z3_ast Z3_API Z3_sort_to_ast(__in Z3_context c, __in Z3_sort s);
03402     
03408     Z3_bool Z3_API Z3_is_eq_sort(__in Z3_context c, __in Z3_sort s1, __in Z3_sort s2);
03409 
03416     Z3_sort_kind Z3_API Z3_get_sort_kind(__in Z3_context c, __in Z3_sort t);
03417 
03418 
03429     unsigned Z3_API Z3_get_bv_sort_size(__in Z3_context c, __in Z3_sort t);
03430 
03437     Z3_bool_opt Z3_API Z3_get_finite_domain_sort_size(__in Z3_context c, __in Z3_sort s, __out_opt unsigned __int64* r);
03438 
03439 
03450     Z3_sort Z3_API Z3_get_array_sort_domain(__in Z3_context c, __in Z3_sort t);
03451 
03462     Z3_sort Z3_API Z3_get_array_sort_range(__in Z3_context c, __in Z3_sort t);
03463 
03464 
03476     Z3_func_decl Z3_API Z3_get_tuple_sort_mk_decl(__in Z3_context c, __in Z3_sort t);
03477     
03488     unsigned Z3_API Z3_get_tuple_sort_num_fields(__in Z3_context c, __in Z3_sort t);
03489 
03502     Z3_func_decl Z3_API Z3_get_tuple_sort_field_decl(__in Z3_context c, __in Z3_sort t, __in unsigned i);
03503 
03514     unsigned Z3_API Z3_get_datatype_sort_num_constructors(
03515         __in Z3_context c, __in Z3_sort t);
03516 
03528     Z3_func_decl Z3_API Z3_get_datatype_sort_constructor(
03529         __in Z3_context c, __in Z3_sort t, unsigned idx);
03530 
03542     Z3_func_decl Z3_API Z3_get_datatype_sort_recognizer(
03543         __in Z3_context c, __in Z3_sort t, unsigned idx);
03544 
03557     Z3_func_decl Z3_API Z3_get_datatype_sort_constructor_accessor(
03558         __in Z3_context c, __in Z3_sort t, unsigned idx_c, unsigned idx_a);
03559 
03560 
03569     unsigned Z3_API Z3_get_relation_arity(__in Z3_context c, __in Z3_sort s);
03570 
03580     Z3_sort Z3_API Z3_get_relation_column(__in Z3_context c, __in Z3_sort s, unsigned col);
03581 
03582 
03592     Z3_ast Z3_API Z3_func_decl_to_ast(__in Z3_context c, __in Z3_func_decl f);
03593 
03599     Z3_bool Z3_API Z3_is_eq_func_decl(__in Z3_context c, __in Z3_func_decl f1, Z3_func_decl f2);
03600 
03606     unsigned Z3_API Z3_get_func_decl_id(__in Z3_context c, Z3_func_decl f);
03607 
03612     Z3_symbol Z3_API Z3_get_decl_name(__in Z3_context c, __in Z3_func_decl d);
03613 
03618     Z3_decl_kind Z3_API Z3_get_decl_kind(__in Z3_context c, __in Z3_func_decl d);
03619 
03626     unsigned Z3_API Z3_get_domain_size(__in Z3_context c, __in Z3_func_decl d);
03627 
03634     unsigned Z3_API Z3_get_arity(__in Z3_context c, __in Z3_func_decl d);
03635 
03645     Z3_sort Z3_API Z3_get_domain(__in Z3_context c, __in Z3_func_decl d, __in unsigned i);
03646 
03647 #ifdef ML4only
03648 #include <mlx_get_domains.idl>
03649 #endif
03650 
03659     Z3_sort Z3_API Z3_get_range(__in Z3_context c, __in Z3_func_decl d);
03660 
03665     unsigned Z3_API Z3_get_decl_num_parameters(__in Z3_context c, __in Z3_func_decl d);
03666 
03675     Z3_parameter_kind Z3_API Z3_get_decl_parameter_kind(__in Z3_context c, __in Z3_func_decl d, unsigned idx);
03676 
03683     int Z3_API Z3_get_decl_int_parameter(__in Z3_context c, __in Z3_func_decl d, unsigned idx);
03684 
03691     double Z3_API Z3_get_decl_double_parameter(__in Z3_context c, __in Z3_func_decl d, unsigned idx);
03692 
03699     Z3_symbol Z3_API Z3_get_decl_symbol_parameter(__in Z3_context c, __in Z3_func_decl d, unsigned idx);
03700 
03707     Z3_sort Z3_API Z3_get_decl_sort_parameter(__in Z3_context c, __in Z3_func_decl d, unsigned idx);
03708 
03715     Z3_ast Z3_API Z3_get_decl_ast_parameter(__in Z3_context c, __in Z3_func_decl d, unsigned idx);
03716 
03723     Z3_func_decl Z3_API Z3_get_decl_func_decl_parameter(__in Z3_context c, __in Z3_func_decl d, unsigned idx);
03724 
03731     Z3_string Z3_API Z3_get_decl_rational_parameter(__in Z3_context c, __in Z3_func_decl d, unsigned idx);
03732 
03742     Z3_ast Z3_API Z3_app_to_ast(__in Z3_context c, __in Z3_app a);
03743 
03748     Z3_func_decl Z3_API Z3_get_app_decl(__in Z3_context c, __in Z3_app a);
03749 
03756     unsigned Z3_API Z3_get_app_num_args(__in Z3_context c, __in Z3_app a);
03757 
03765     Z3_ast Z3_API Z3_get_app_arg(__in Z3_context c, __in Z3_app a, __in unsigned i);
03766 
03767 #ifdef ML4only
03768 #include <mlx_get_app_args.idl>
03769 #endif
03770 
03771 
03776 #ifdef ML4only
03777 #include <mlx_term_refine.idl>
03778 #endif
03779 
03785     Z3_bool Z3_API Z3_is_eq_ast(__in Z3_context c, __in Z3_ast t1, Z3_ast t2);
03786 
03792     unsigned Z3_API Z3_get_ast_id(__in Z3_context c, Z3_ast t);
03793 
03799     unsigned Z3_API Z3_get_ast_hash(__in Z3_context c, __in Z3_ast a);
03800 
03807     Z3_sort Z3_API Z3_get_sort(__in Z3_context c, __in Z3_ast a);
03808 
03813     Z3_bool Z3_API Z3_is_well_sorted(__in Z3_context c, __in Z3_ast t);
03814 
03819     Z3_lbool Z3_API Z3_get_bool_value(__in Z3_context c, __in Z3_ast a);
03820 
03825     Z3_ast_kind Z3_API Z3_get_ast_kind(__in Z3_context c, __in Z3_ast a);
03826 
03829     Z3_bool Z3_API Z3_is_app(__in Z3_context c, __in Z3_ast a);
03830 
03833     Z3_bool Z3_API Z3_is_numeral_ast(__in Z3_context c, __in Z3_ast a);
03834 
03839     Z3_bool Z3_API Z3_is_algebraic_number(__in Z3_context c, __in Z3_ast a);
03840 
03847     Z3_app Z3_API Z3_to_app(__in Z3_context c, __in Z3_ast a);
03848 
03855     Z3_func_decl Z3_API Z3_to_func_decl(__in Z3_context c, __in Z3_ast a);
03856 
03857 
03862 #ifdef ML4only
03863 #include <mlx_numeral_refine.idl>
03864 #endif
03865 
03876     Z3_string Z3_API Z3_get_numeral_string(__in Z3_context c, __in Z3_ast a);
03877 
03885     Z3_string Z3_API Z3_get_numeral_decimal_string(__in Z3_context c, __in Z3_ast a, __in unsigned precision);
03886 
03893     Z3_ast Z3_API Z3_get_numerator(__in Z3_context c, __in Z3_ast a);
03894 
03901     Z3_ast Z3_API Z3_get_denominator(__in Z3_context c, __in Z3_ast a);
03902 
03916     Z3_bool Z3_API Z3_get_numeral_small(__in Z3_context c, __in Z3_ast a, __out __int64* num, __out __int64* den);
03917 
03928     Z3_bool Z3_API Z3_get_numeral_int(__in Z3_context c, __in Z3_ast v, __out int* i);
03929 
03930 #ifdef Conly
03931 
03941     Z3_bool Z3_API Z3_get_numeral_uint(__in Z3_context c, __in Z3_ast v, __out unsigned* u);
03942 #endif
03943 
03944 #ifdef Conly
03945 
03955     Z3_bool Z3_API Z3_get_numeral_uint64(__in Z3_context c, __in Z3_ast v, __out unsigned __int64* u);
03956 #endif
03957 
03968     Z3_bool Z3_API Z3_get_numeral_int64(__in Z3_context c, __in Z3_ast v, __out __int64* i);
03969 
03980     Z3_bool Z3_API Z3_get_numeral_rational_int64(__in Z3_context c, __in Z3_ast v, __out __int64* num, __out __int64* den);
03981     
03990     Z3_ast Z3_API Z3_get_algebraic_number_lower(__in Z3_context c, __in Z3_ast a, __in unsigned precision);
03991 
04000     Z3_ast Z3_API Z3_get_algebraic_number_upper(Z3_context c, Z3_ast a, unsigned precision);
04001 
04002 
04012     Z3_ast Z3_API Z3_pattern_to_ast(__in Z3_context c, __in Z3_pattern p);
04013 
04014 #ifdef ML4only
04015 #include <mlx_get_pattern_terms.idl>
04016 #endif
04017 
04022     unsigned Z3_API Z3_get_pattern_num_terms(__in Z3_context c, __in Z3_pattern p);
04023     
04028     Z3_ast Z3_API Z3_get_pattern(__in Z3_context c, __in Z3_pattern p, __in unsigned idx);
04029 
04030 
04041     unsigned Z3_API Z3_get_index_value(__in Z3_context c, __in Z3_ast a);
04042 
04049     Z3_bool Z3_API Z3_is_quantifier_forall(__in Z3_context c, __in Z3_ast a);
04050 
04057     unsigned Z3_API Z3_get_quantifier_weight(__in Z3_context c, __in Z3_ast a);
04058 
04065     unsigned Z3_API Z3_get_quantifier_num_patterns(__in Z3_context c, __in Z3_ast a);
04066 
04073     Z3_pattern Z3_API Z3_get_quantifier_pattern_ast(__in Z3_context c, __in Z3_ast a, unsigned i);
04074 
04081     unsigned Z3_API Z3_get_quantifier_num_no_patterns(__in Z3_context c, __in Z3_ast a);
04082 
04089     Z3_ast Z3_API Z3_get_quantifier_no_pattern_ast(__in Z3_context c, __in Z3_ast a, unsigned i);
04090 
04097     unsigned Z3_API Z3_get_quantifier_num_bound(__in Z3_context c, __in Z3_ast a);
04098 
04105     Z3_symbol Z3_API Z3_get_quantifier_bound_name(__in Z3_context c, __in Z3_ast a, unsigned i);
04106 
04113     Z3_sort Z3_API Z3_get_quantifier_bound_sort(__in Z3_context c, __in Z3_ast a, unsigned i);
04114 
04121     Z3_ast Z3_API Z3_get_quantifier_body(__in Z3_context c, __in Z3_ast a);
04122 
04123 
04134     Z3_ast Z3_API Z3_simplify(__in Z3_context c, __in Z3_ast a);
04135 
04136 #ifdef CorML4
04137 
04145     Z3_ast Z3_API Z3_simplify_ex(__in Z3_context c, __in Z3_ast a, __in Z3_params p);
04146 
04151     Z3_string Z3_API Z3_simplify_get_help(__in Z3_context c);
04152 
04157     Z3_param_descrs Z3_API Z3_simplify_get_param_descrs(__in Z3_context c);
04158 #endif
04159     
04166 
04174     Z3_ast Z3_API Z3_update_term(__in Z3_context c, __in Z3_ast a, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[]);
04175 
04182     Z3_ast Z3_API Z3_substitute(__in Z3_context c, 
04183                                 __in Z3_ast a, 
04184                                 __in unsigned num_exprs, 
04185                                 __in_ecount(num_exprs) Z3_ast const from[], 
04186                                 __in_ecount(num_exprs) Z3_ast const to[]);
04187 
04193     Z3_ast Z3_API Z3_substitute_vars(__in Z3_context c, 
04194                                      __in Z3_ast a, 
04195                                      __in unsigned num_exprs, 
04196                                      __in_ecount(num_exprs) Z3_ast const to[]);
04197 
04198 #ifdef CorML4
04199 
04205     Z3_ast Z3_API Z3_translate(__in Z3_context source, __in Z3_ast a, __in Z3_context target);
04206 #endif
04207     
04210 #ifdef CorML4
04211 
04215     
04216 #ifdef ML4only
04217 #include <mlx_model.idl>
04218 #endif
04219 #ifdef Conly
04220 
04224     void Z3_API Z3_model_inc_ref(__in Z3_context c, __in Z3_model m);
04225 
04230     void Z3_API Z3_model_dec_ref(__in Z3_context c, __in Z3_model m);
04231 #endif
04232     
04252     Z3_bool_opt Z3_API Z3_model_eval(__in Z3_context c, __in Z3_model m, __in Z3_ast t, __in Z3_bool model_completion, __out_opt Z3_ast * v);
04253 
04267     Z3_ast_opt Z3_API Z3_model_get_const_interp(__in Z3_context c, __in Z3_model m, __in Z3_func_decl a);
04268 
04273     Z3_bool Z3_API Z3_model_has_interp(__in Z3_context c, __in Z3_model m, __in Z3_func_decl a);
04274 
04287     Z3_func_interp_opt Z3_API Z3_model_get_func_interp(__in Z3_context c, __in Z3_model m, __in Z3_func_decl f);
04288 
04295     unsigned Z3_API Z3_model_get_num_consts(__in Z3_context c, __in Z3_model m);
04296 
04306     Z3_func_decl Z3_API Z3_model_get_const_decl(__in Z3_context c, __in Z3_model m, __in unsigned i);
04307     
04315     unsigned Z3_API Z3_model_get_num_funcs(__in Z3_context c, __in Z3_model m);
04316     
04326     Z3_func_decl Z3_API Z3_model_get_func_decl(__in Z3_context c, __in Z3_model m, __in unsigned i);
04327     
04339     unsigned Z3_API Z3_model_get_num_sorts(__in Z3_context c, __in Z3_model m);
04340 
04350     Z3_sort Z3_API Z3_model_get_sort(__in Z3_context c, __in Z3_model m, __in unsigned i);
04351 
04359     Z3_ast_vector Z3_API Z3_model_get_sort_universe(__in Z3_context c, __in Z3_model m, __in Z3_sort s);
04360     
04371     Z3_bool Z3_API Z3_is_as_array(__in Z3_context c, __in Z3_ast a);
04372     
04379     Z3_func_decl Z3_API Z3_get_as_array_func_decl(__in Z3_context c, __in Z3_ast a);
04380 
04381 #ifdef Conly
04382 
04386     void Z3_API Z3_func_interp_inc_ref(__in Z3_context c, __in Z3_func_interp f);
04387 
04392     void Z3_API Z3_func_interp_dec_ref(__in Z3_context c, __in Z3_func_interp f);
04393 #endif
04394 
04403     unsigned Z3_API Z3_func_interp_get_num_entries(__in Z3_context c, __in Z3_func_interp f);
04404 
04414     Z3_func_entry Z3_API Z3_func_interp_get_entry(__in Z3_context c, __in Z3_func_interp f, unsigned i);
04415     
04423     Z3_ast Z3_API Z3_func_interp_get_else(__in Z3_context c, __in Z3_func_interp f);
04424     
04429     unsigned Z3_API Z3_func_interp_get_arity(__in Z3_context c, __in Z3_func_interp f);
04430 
04431 #ifdef Conly
04432 
04436     void Z3_API Z3_func_entry_inc_ref(__in Z3_context c, __in Z3_func_entry e);
04437 
04442     void Z3_API Z3_func_entry_dec_ref(__in Z3_context c, __in Z3_func_entry e);
04443 #endif
04444     
04454     Z3_ast Z3_API Z3_func_entry_get_value(__in Z3_context c, __in Z3_func_entry e);
04455 
04462     unsigned Z3_API Z3_func_entry_get_num_args(__in Z3_context c, __in Z3_func_entry e);
04463     
04472     Z3_ast Z3_API Z3_func_entry_get_arg(__in Z3_context c, __in Z3_func_entry e, __in unsigned i);
04473 
04475 #endif // CorML4
04476 
04481     
04486     Z3_bool Z3_API Z3_open_log(__in Z3_string filename);
04487 
04496     void Z3_API Z3_append_log(__in Z3_string string);
04497 
04502     void Z3_API Z3_close_log(void);
04503 
04511     void Z3_API Z3_toggle_warning_messages(__in Z3_bool enabled);
04512 
04519 
04536     void Z3_API Z3_set_ast_print_mode(__in Z3_context c, __in Z3_ast_print_mode mode);
04537 
04548     Z3_string Z3_API Z3_ast_to_string(__in Z3_context c, __in Z3_ast a);
04549 
04552     Z3_string Z3_API Z3_pattern_to_string(__in Z3_context c, __in Z3_pattern p);
04553 
04556     Z3_string Z3_API Z3_sort_to_string(__in Z3_context c, __in Z3_sort s);
04557     
04560     Z3_string Z3_API Z3_func_decl_to_string(__in Z3_context c, __in Z3_func_decl d);
04561 
04570     Z3_string Z3_API Z3_model_to_string(__in Z3_context c, __in Z3_model m);
04571 
04589     Z3_string Z3_API Z3_benchmark_to_smtlib_string(__in   Z3_context c, 
04590                                                    __in Z3_string name,
04591                                                    __in Z3_string logic,
04592                                                    __in Z3_string status,
04593                                                    __in Z3_string attributes,
04594                                                    __in   unsigned num_assumptions,
04595                                                    __in_ecount(num_assumptions) Z3_ast const assumptions[],
04596                                                    __in   Z3_ast formula);
04597 
04604 
04613     Z3_ast Z3_API Z3_parse_smtlib2_string(__in Z3_context c, 
04614                                           __in Z3_string str,
04615                                           __in unsigned num_sorts,
04616                                           __in_ecount(num_sorts) Z3_symbol const sort_names[],
04617                                           __in_ecount(num_sorts) Z3_sort const sorts[],
04618                                           __in unsigned num_decls,
04619                                           __in_ecount(num_decls) Z3_symbol const decl_names[],
04620                                           __in_ecount(num_decls) Z3_func_decl const decls[]);
04621     
04626     Z3_ast Z3_API Z3_parse_smtlib2_file(__in Z3_context c, 
04627                                         __in Z3_string file_name,
04628                                         __in unsigned num_sorts,
04629                                         __in_ecount(num_sorts) Z3_symbol const sort_names[],
04630                                         __in_ecount(num_sorts) Z3_sort const sorts[],
04631                                         __in unsigned num_decls,
04632                                         __in_ecount(num_decls) Z3_symbol const decl_names[],
04633                                         __in_ecount(num_decls) Z3_func_decl const decls[]);
04634 
04635 #ifdef ML4only
04636 #include <mlx_parse_smtlib.idl>
04637 #endif
04638 
04657     void Z3_API Z3_parse_smtlib_string(__in Z3_context c, 
04658                                        __in Z3_string str,
04659                                        __in unsigned num_sorts,
04660                                        __in_ecount(num_sorts) Z3_symbol const sort_names[],
04661                                        __in_ecount(num_sorts) Z3_sort const sorts[],
04662                                        __in unsigned num_decls,
04663                                        __in_ecount(num_decls) Z3_symbol const decl_names[],
04664                                        __in_ecount(num_decls) Z3_func_decl const decls[]                     
04665                                        );
04666 
04671     void Z3_API Z3_parse_smtlib_file(__in Z3_context c, 
04672                                      __in Z3_string file_name,
04673                                      __in unsigned num_sorts,
04674                                      __in_ecount(num_sorts) Z3_symbol const sort_names[],
04675                                      __in_ecount(num_sorts) Z3_sort const sorts[],
04676                                      __in unsigned num_decls,
04677                                      __in_ecount(num_decls) Z3_symbol const decl_names[],
04678                                      __in_ecount(num_decls) Z3_func_decl const decls[]  
04679                                      );
04680 
04685     unsigned Z3_API Z3_get_smtlib_num_formulas(__in Z3_context c);
04686 
04694     Z3_ast Z3_API Z3_get_smtlib_formula(__in Z3_context c, __in unsigned i);
04695 
04700     unsigned Z3_API Z3_get_smtlib_num_assumptions(__in Z3_context c);
04701 
04709     Z3_ast Z3_API Z3_get_smtlib_assumption(__in Z3_context c, __in unsigned i);
04710 
04715     unsigned Z3_API Z3_get_smtlib_num_decls(__in Z3_context c);
04716 
04724     Z3_func_decl Z3_API Z3_get_smtlib_decl(__in Z3_context c, __in unsigned i);
04725 
04730     unsigned Z3_API Z3_get_smtlib_num_sorts(__in Z3_context c);
04731 
04739     Z3_sort Z3_API Z3_get_smtlib_sort(__in Z3_context c, __in unsigned i);
04740 
04741 BEGIN_MLAPI_EXCLUDE
04747     Z3_string Z3_API Z3_get_smtlib_error(__in Z3_context c);
04748 END_MLAPI_EXCLUDE
04749 
04752 #ifdef CorML4
04753 
04757 
04758 #ifndef SAFE_ERRORS
04759 
04768     Z3_error_code Z3_API Z3_get_error_code(__in Z3_context c);
04769 
04782     void Z3_API Z3_set_error_handler(__in Z3_context c, __in Z3_error_handler h);
04783 #endif
04784     
04789     void Z3_API Z3_set_error(__in Z3_context c, __in Z3_error_code e);
04790 
04791 #ifdef Conly
04792 
04798     Z3_string Z3_API Z3_get_error_msg(__in Z3_error_code err);
04799 #endif
04800     
04801 BEGIN_MLAPI_EXCLUDE
04806     Z3_string Z3_API Z3_get_error_msg_ex(__in Z3_context c, __in Z3_error_code err);
04807 END_MLAPI_EXCLUDE
04808 #ifdef ML4only
04809 #include <mlx_get_error_msg.idl>
04810 #endif
04811 
04812 
04814 #endif
04815 
04820     
04825     void Z3_API Z3_get_version(__out unsigned * major, __out unsigned * minor, __out unsigned * build_number, __out unsigned * revision_number);
04826  
04832     void Z3_API Z3_enable_trace(__in Z3_string tag);
04833 
04839     void Z3_API Z3_disable_trace(__in Z3_string tag);
04840  
04841 #ifdef CorML3
04842 
04851     void Z3_API Z3_reset_memory(void);
04852 #endif
04853     
04856 #ifdef CorML3
04857 
04861     
04862 #ifdef Conly
04863 
04864     //
04865     // callbacks and void* don't work with CAMLIDL.
04866     // 
04867     typedef Z3_bool Z3_reduce_eq_callback_fptr(__in Z3_theory t, __in Z3_ast a, __in Z3_ast b, __out Z3_ast * r);
04868 
04869     typedef Z3_bool Z3_reduce_app_callback_fptr(__in Z3_theory, __in Z3_func_decl, __in unsigned, __in Z3_ast const [], __out Z3_ast *);
04870 
04871     typedef Z3_bool Z3_reduce_distinct_callback_fptr(__in Z3_theory, __in unsigned, __in Z3_ast const [], __out Z3_ast *);
04872 
04873     typedef void Z3_theory_callback_fptr(__in Z3_theory t);
04874     
04875     typedef Z3_bool Z3_theory_final_check_callback_fptr(__in Z3_theory);
04876     
04877     typedef void Z3_theory_ast_callback_fptr(__in Z3_theory, __in Z3_ast);
04878     
04879     typedef void Z3_theory_ast_bool_callback_fptr(__in Z3_theory, __in Z3_ast, __in Z3_bool);
04880     
04881     typedef void Z3_theory_ast_ast_callback_fptr(__in Z3_theory, __in Z3_ast, __in Z3_ast);
04882 
04883 #endif
04884 
04885 #ifdef Conly
04886 
04894     Z3_theory Z3_API Z3_mk_theory(__in Z3_context c, __in Z3_string th_name, __in Z3_theory_data data);
04895 
04901     Z3_theory_data Z3_API Z3_theory_get_ext_data(__in Z3_theory t);
04902 #endif
04903 
04907     Z3_sort Z3_API Z3_theory_mk_sort(__in Z3_context c, __in Z3_theory t, __in Z3_symbol s);
04908     
04912     Z3_ast Z3_API Z3_theory_mk_value(__in Z3_context c, __in Z3_theory t, __in Z3_symbol n, __in Z3_sort s);
04913 
04917     Z3_ast Z3_API Z3_theory_mk_constant(__in Z3_context c, __in Z3_theory t, __in Z3_symbol n, __in Z3_sort s);
04918     
04922     Z3_func_decl Z3_API Z3_theory_mk_func_decl(__in Z3_context c, __in Z3_theory t, __in Z3_symbol n,
04923                                                __in unsigned domain_size, __in_ecount(domain_size) Z3_sort const domain[],
04924                                                __in Z3_sort range);
04925 
04929     Z3_context Z3_API Z3_theory_get_context(__in Z3_theory t);
04930 
04931 
04932 #ifdef Conly
04933 
04943     void Z3_API Z3_set_delete_callback(__in Z3_theory t, __in Z3_theory_callback_fptr f);
04944     
04958     void Z3_API Z3_set_reduce_app_callback(__in Z3_theory t, __in Z3_reduce_app_callback_fptr f);
04959     
04973     void Z3_API Z3_set_reduce_eq_callback(__in Z3_theory t, __in Z3_reduce_eq_callback_fptr f);
04974 
04988     void Z3_API Z3_set_reduce_distinct_callback(__in Z3_theory t, __in Z3_reduce_distinct_callback_fptr f);
04989     
05005     void Z3_API Z3_set_new_app_callback(__in Z3_theory t, __in Z3_theory_ast_callback_fptr f);
05006 
05023     void Z3_API Z3_set_new_elem_callback(__in Z3_theory t, __in Z3_theory_ast_callback_fptr f);
05024 
05032     void Z3_API Z3_set_init_search_callback(__in Z3_theory t, __in Z3_theory_callback_fptr f);
05033         
05043     void Z3_API Z3_set_push_callback(__in Z3_theory t, __in Z3_theory_callback_fptr f);
05044  
05054     void Z3_API Z3_set_pop_callback(__in Z3_theory t, __in Z3_theory_callback_fptr f);
05055 
05063     void Z3_API Z3_set_restart_callback(__in Z3_theory t, __in Z3_theory_callback_fptr f);
05064 
05073     void Z3_API Z3_set_reset_callback(__in Z3_theory t, __in Z3_theory_callback_fptr f);
05074 
05087     void Z3_API Z3_set_final_check_callback(__in Z3_theory t, __in Z3_theory_final_check_callback_fptr f);
05088 
05098     void Z3_API Z3_set_new_eq_callback(__in Z3_theory t, __in Z3_theory_ast_ast_callback_fptr f);
05099 
05109     void Z3_API Z3_set_new_diseq_callback(__in Z3_theory t, __in Z3_theory_ast_ast_callback_fptr f);
05110 
05119     void Z3_API Z3_set_new_assignment_callback(__in Z3_theory t, __in Z3_theory_ast_bool_callback_fptr f);
05120 
05130     void Z3_API Z3_set_new_relevant_callback(__in Z3_theory t, __in Z3_theory_ast_callback_fptr f);
05131 
05132 #endif
05133 
05148     void Z3_API Z3_theory_assert_axiom(__in Z3_theory t, __in Z3_ast ax);
05149 
05157     void Z3_API Z3_theory_assume_eq(__in Z3_theory t, __in Z3_ast lhs, __in Z3_ast rhs);
05158 
05165     void Z3_API Z3_theory_enable_axiom_simplification(__in Z3_theory t, __in Z3_bool flag);
05166 
05170     Z3_ast Z3_API Z3_theory_get_eqc_root(__in Z3_theory t, __in Z3_ast n);
05171     
05186     Z3_ast Z3_API Z3_theory_get_eqc_next(__in Z3_theory t, __in Z3_ast n);
05187 
05191     unsigned Z3_API Z3_theory_get_num_parents(__in Z3_theory t, __in Z3_ast n);
05192     
05197     Z3_ast Z3_API Z3_theory_get_parent(__in Z3_theory t, __in Z3_ast n, __in unsigned i);
05198 
05202     Z3_bool Z3_API Z3_theory_is_value(__in Z3_theory t, __in Z3_ast n);
05203 
05207     Z3_bool Z3_API Z3_theory_is_decl(__in Z3_theory t, __in Z3_func_decl d);
05208     
05214     unsigned Z3_API Z3_theory_get_num_elems(__in Z3_theory t);
05215     
05221     Z3_ast Z3_API Z3_theory_get_elem(__in Z3_theory t, __in unsigned i);
05222 
05228     unsigned Z3_API Z3_theory_get_num_apps(__in Z3_theory t);
05229     
05235     Z3_ast Z3_API Z3_theory_get_app(__in Z3_theory t, __in unsigned i);
05236 
05239 #endif
05240 
05241 #ifdef CorML4
05242 
05246 
05254     Z3_fixedpoint Z3_API Z3_mk_fixedpoint(__in Z3_context c);
05255 
05256 #ifdef Conly
05257 
05261     void Z3_API Z3_fixedpoint_inc_ref(__in Z3_context c,__in Z3_fixedpoint d);
05262 
05267     void Z3_API Z3_fixedpoint_dec_ref(__in Z3_context c,__in Z3_fixedpoint d);
05268 #endif
05269 
05281     void Z3_API Z3_fixedpoint_add_rule(__in Z3_context c,__in Z3_fixedpoint d, __in Z3_ast rule, __in Z3_symbol name);
05282 
05299     void Z3_API Z3_fixedpoint_add_fact(__in Z3_context c,__in Z3_fixedpoint d, 
05300                                        __in Z3_func_decl r, 
05301                                        __in unsigned num_args, __in_ecount(num_args) unsigned args[]);
05302 
05310     void Z3_API Z3_fixedpoint_assert(__in Z3_context c,__in Z3_fixedpoint d, __in Z3_ast axiom);
05311 
05326     Z3_lbool Z3_API Z3_fixedpoint_query(__in Z3_context c,__in Z3_fixedpoint d, __in Z3_ast query);
05327 
05339     Z3_lbool Z3_API Z3_fixedpoint_query_relations(
05340         __in Z3_context c,__in Z3_fixedpoint d, 
05341         __in unsigned num_relations, __in_ecount(num_relations) Z3_func_decl const relations[]);
05342 
05355     Z3_ast Z3_API Z3_fixedpoint_get_answer(__in Z3_context c,__in Z3_fixedpoint d);
05356 
05363     Z3_string Z3_API Z3_fixedpoint_get_reason_unknown(__in Z3_context c,__in Z3_fixedpoint d);
05364 
05370     void Z3_API Z3_fixedpoint_update_rule(__in Z3_context c, __in Z3_fixedpoint d, __in Z3_ast a, __in Z3_symbol name);
05371     
05380     unsigned Z3_API Z3_fixedpoint_get_num_levels(Z3_context c, Z3_fixedpoint d, Z3_func_decl pred);
05381 
05391     Z3_ast Z3_API Z3_fixedpoint_get_cover_delta(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred);
05392 
05404     void Z3_API Z3_fixedpoint_add_cover(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred, Z3_ast property);
05405 
05410     Z3_stats Z3_API Z3_fixedpoint_get_statistics(__in Z3_context c,__in Z3_fixedpoint d);
05411 
05419     void Z3_API Z3_fixedpoint_register_relation(__in Z3_context c,__in Z3_fixedpoint d, __in Z3_func_decl f);
05420 
05429     void Z3_API Z3_fixedpoint_set_predicate_representation(
05430         __in Z3_context c,
05431         __in Z3_fixedpoint d, 
05432         __in Z3_func_decl f, 
05433         __in unsigned num_relations, 
05434         __in_ecount(num_relations) Z3_symbol const relation_kinds[]);
05435                 
05440     Z3_ast_vector Z3_API Z3_fixedpoint_get_rules(
05441         __in Z3_context c,
05442         __in Z3_fixedpoint f);
05443 
05448     Z3_ast_vector Z3_API Z3_fixedpoint_get_assertions(
05449         __in Z3_context c,
05450         __in Z3_fixedpoint f);
05451 
05456     void Z3_API Z3_fixedpoint_set_params(__in Z3_context c, __in Z3_fixedpoint f, __in Z3_params p);
05457 
05462     Z3_string Z3_API Z3_fixedpoint_get_help(__in Z3_context c, __in Z3_fixedpoint f);
05463 
05468     Z3_param_descrs Z3_API Z3_fixedpoint_get_param_descrs(__in Z3_context c, __in Z3_fixedpoint f);
05469 
05478     Z3_string Z3_API Z3_fixedpoint_to_string(
05479         __in Z3_context c, 
05480         __in Z3_fixedpoint f,
05481         __in unsigned num_queries,
05482         __in_ecount(num_queries) Z3_ast queries[]);
05483 
05494     Z3_ast_vector Z3_API Z3_fixedpoint_from_string(
05495         __in Z3_context c, 
05496         __in Z3_fixedpoint f,
05497         __in Z3_string s);
05498 
05509     Z3_ast_vector Z3_API Z3_fixedpoint_from_file(
05510         __in Z3_context c, 
05511         __in Z3_fixedpoint f,
05512         __in Z3_string s);
05513 
05523     void Z3_API Z3_fixedpoint_push(Z3_context c,Z3_fixedpoint d);
05524 
05533     void Z3_API Z3_fixedpoint_pop(Z3_context c,Z3_fixedpoint d);
05534 
05535 #ifdef Conly
05536 
05541     typedef void Z3_fixedpoint_reduce_assign_callback_fptr(
05542         __in void*, __in Z3_func_decl, 
05543         __in unsigned, __in Z3_ast const [], 
05544         __in unsigned, __in Z3_ast const []); 
05545 
05546     typedef void Z3_fixedpoint_reduce_app_callback_fptr(
05547         __in void*, __in Z3_func_decl, 
05548         __in unsigned, __in Z3_ast const [], 
05549         __out Z3_ast*);
05550         
05551 
05555     void Z3_API Z3_fixedpoint_init(__in Z3_context c,__in Z3_fixedpoint d, __in void* state);
05556 
05562     void Z3_API Z3_fixedpoint_set_reduce_assign_callback(
05563         __in Z3_context c,__in Z3_fixedpoint d, __in Z3_fixedpoint_reduce_assign_callback_fptr cb);
05564     
05569     void Z3_API Z3_fixedpoint_set_reduce_app_callback(
05570         __in Z3_context c,__in Z3_fixedpoint d, __in Z3_fixedpoint_reduce_app_callback_fptr cb);
05571         
05572 #endif
05573 #endif
05574 
05575 #ifdef CorML4
05576 
05582     
05590     Z3_ast_vector Z3_API Z3_mk_ast_vector(__in Z3_context c);
05591     
05592 #ifdef Conly
05593 
05597     void Z3_API Z3_ast_vector_inc_ref(__in Z3_context c, __in Z3_ast_vector v);
05598     
05603     void Z3_API Z3_ast_vector_dec_ref(__in Z3_context c, __in Z3_ast_vector v);
05604 #endif
05605     
05610     unsigned Z3_API Z3_ast_vector_size(__in Z3_context c, __in Z3_ast_vector v);
05611 
05618     Z3_ast Z3_API Z3_ast_vector_get(__in Z3_context c, __in Z3_ast_vector v, __in unsigned i);    
05619 
05626     void Z3_API Z3_ast_vector_set(__in Z3_context c, __in Z3_ast_vector v, __in unsigned i, __in Z3_ast a);    
05627 
05632     void Z3_API Z3_ast_vector_resize(__in Z3_context c, __in Z3_ast_vector v, __in unsigned n);
05633 
05638     void Z3_API Z3_ast_vector_push(__in Z3_context c, __in Z3_ast_vector v, __in Z3_ast a);        
05639 
05644     Z3_ast_vector Z3_API Z3_ast_vector_translate(__in Z3_context s, __in Z3_ast_vector v, __in Z3_context t);        
05645 
05650     Z3_string Z3_API Z3_ast_vector_to_string(__in Z3_context c, __in Z3_ast_vector v);
05651 
05658     
05666     Z3_ast_map Z3_API Z3_mk_ast_map(__in Z3_context c);
05667 
05668 #ifdef Conly
05669 
05673     void Z3_API Z3_ast_map_inc_ref(__in Z3_context c, __in Z3_ast_map m);
05674     
05679     void Z3_API Z3_ast_map_dec_ref(__in Z3_context c, __in Z3_ast_map m);
05680 #endif
05681     
05686     Z3_bool Z3_API Z3_ast_map_contains(__in Z3_context c, __in Z3_ast_map m, __in Z3_ast k);
05687 
05694     Z3_ast Z3_API Z3_ast_map_find(__in Z3_context c, __in Z3_ast_map m, __in Z3_ast k);
05695 
05700     void Z3_API Z3_ast_map_insert(__in Z3_context c, __in Z3_ast_map m, __in Z3_ast k, __in Z3_ast v);
05701 
05706     void Z3_API Z3_ast_map_erase(__in Z3_context c, __in Z3_ast_map m, __in Z3_ast k);
05707 
05712     void Z3_API Z3_ast_map_reset(__in Z3_context c, __in Z3_ast_map m);
05713     
05718     unsigned Z3_API Z3_ast_map_size(__in Z3_context c, __in Z3_ast_map m);
05719 
05724     Z3_ast_vector Z3_API Z3_ast_map_keys(__in Z3_context c, __in Z3_ast_map m);
05725 
05730     Z3_string Z3_API Z3_ast_map_to_string(__in Z3_context c, __in Z3_ast_map m);
05731 
05738 
05755     Z3_goal Z3_API Z3_mk_goal(__in Z3_context c, __in Z3_bool models, __in Z3_bool unsat_cores, __in Z3_bool proofs);
05756     
05757 #ifdef Conly
05758 
05762     void Z3_API Z3_goal_inc_ref(__in Z3_context c, __in Z3_goal g);
05763 
05768     void Z3_API Z3_goal_dec_ref(__in Z3_context c, __in Z3_goal g);
05769 #endif
05770 
05777     Z3_goal_prec Z3_API Z3_goal_precision(__in Z3_context c, __in Z3_goal g);
05778 
05783     void Z3_API Z3_goal_assert(__in Z3_context c, __in Z3_goal g, __in Z3_ast a);
05784     
05789     Z3_bool Z3_API Z3_goal_inconsistent(__in Z3_context c, __in Z3_goal g);
05790 
05795     unsigned Z3_API Z3_goal_depth(__in Z3_context c, __in Z3_goal g);
05796 
05801     void Z3_API Z3_goal_reset(__in Z3_context c, __in Z3_goal g);
05802 
05807     unsigned Z3_API Z3_goal_size(__in Z3_context c, __in Z3_goal g);
05808     
05815     Z3_ast Z3_API Z3_goal_formula(__in Z3_context c, __in Z3_goal g, __in unsigned idx);
05816     
05821     unsigned Z3_API Z3_goal_num_exprs(__in Z3_context c, __in Z3_goal g);
05822     
05827     Z3_bool Z3_API Z3_goal_is_decided_sat(__in Z3_context c, __in Z3_goal g);
05828     
05833     Z3_bool Z3_API Z3_goal_is_decided_unsat(__in Z3_context c, __in Z3_goal g);
05834 
05839     Z3_goal Z3_API Z3_goal_translate(__in Z3_context source, __in Z3_goal g, __in Z3_context target);
05840     
05845     Z3_string Z3_API Z3_goal_to_string(__in Z3_context c, __in Z3_goal g);
05846 
05853 
05862     Z3_tactic Z3_API Z3_mk_tactic(__in Z3_context c, __in Z3_string name);
05863 
05864 #ifdef Conly
05865 
05869     void Z3_API Z3_tactic_inc_ref(__in Z3_context c, __in Z3_tactic t);
05870 
05875     void Z3_API Z3_tactic_dec_ref(__in Z3_context c, __in Z3_tactic g);
05876 #endif
05877     
05887     Z3_probe Z3_API Z3_mk_probe(__in Z3_context c, __in Z3_string name);
05888 
05889 #ifdef Conly
05890 
05894     void Z3_API Z3_probe_inc_ref(__in Z3_context c, __in Z3_probe p);
05895 
05900     void Z3_API Z3_probe_dec_ref(__in Z3_context c, __in Z3_probe p);
05901 #endif
05902 
05908     Z3_tactic Z3_API Z3_tactic_and_then(__in Z3_context c, __in Z3_tactic t1, __in Z3_tactic t2);
05909 
05915     Z3_tactic Z3_API Z3_tactic_or_else(__in Z3_context c, __in Z3_tactic t1, __in Z3_tactic t2);
05916 
05921     Z3_tactic Z3_API Z3_tactic_par_or(__in Z3_context c, __in unsigned num, __in_ecount(num) Z3_tactic const ts[]);
05922 
05928     Z3_tactic Z3_API Z3_tactic_par_and_then(__in Z3_context c, __in Z3_tactic t1, __in Z3_tactic t2);
05929     
05935     Z3_tactic Z3_API Z3_tactic_try_for(__in Z3_context c, __in Z3_tactic t, __in unsigned ms);
05936 
05942     Z3_tactic Z3_API Z3_tactic_when(__in Z3_context c, __in Z3_probe p, __in Z3_tactic t);
05943     
05949     Z3_tactic Z3_API Z3_tactic_cond(__in Z3_context c, __in Z3_probe p, __in Z3_tactic t1, __in Z3_tactic t2);
05950     
05956     Z3_tactic Z3_API Z3_tactic_repeat(__in Z3_context c, __in Z3_tactic t, unsigned max);
05957 
05962     Z3_tactic Z3_API Z3_tactic_skip(__in Z3_context c);
05963 
05968     Z3_tactic Z3_API Z3_tactic_fail(__in Z3_context c);
05969 
05974     Z3_tactic Z3_API Z3_tactic_fail_if(__in Z3_context c, __in Z3_probe p);
05975 
05981     Z3_tactic Z3_API Z3_tactic_fail_if_not_decided(__in Z3_context c);
05982 
05987     Z3_tactic Z3_API Z3_tactic_using_params(__in Z3_context c, __in Z3_tactic t, __in Z3_params p);
05988 
05993     Z3_probe Z3_API Z3_probe_const(__in Z3_context x, __in double val);
05994 
06001     Z3_probe Z3_API Z3_probe_lt(__in Z3_context x, __in Z3_probe p1, __in Z3_probe p2);
06002 
06009     Z3_probe Z3_API Z3_probe_gt(__in Z3_context x, __in Z3_probe p1, __in Z3_probe p2);
06010 
06017     Z3_probe Z3_API Z3_probe_le(__in Z3_context x, __in Z3_probe p1, __in Z3_probe p2);
06018 
06025     Z3_probe Z3_API Z3_probe_ge(__in Z3_context x, __in Z3_probe p1, __in Z3_probe p2);
06026 
06033     Z3_probe Z3_API Z3_probe_eq(__in Z3_context x, __in Z3_probe p1, __in Z3_probe p2);
06034 
06041     Z3_probe Z3_API Z3_probe_and(__in Z3_context x, __in Z3_probe p1, __in Z3_probe p2);
06042  
06049     Z3_probe Z3_API Z3_probe_or(__in Z3_context x, __in Z3_probe p1, __in Z3_probe p2);
06050 
06057     Z3_probe Z3_API Z3_probe_not(__in Z3_context x, __in Z3_probe p);
06058 
06063     unsigned Z3_API Z3_get_num_tactics(__in Z3_context c);
06064 
06071     Z3_string Z3_API Z3_get_tactic_name(__in Z3_context c, unsigned i);
06072 
06077     unsigned Z3_API Z3_get_num_probes(__in Z3_context c);
06078 
06085     Z3_string Z3_API Z3_get_probe_name(__in Z3_context c, unsigned i);
06086 
06091     Z3_string Z3_API Z3_tactic_get_help(__in Z3_context c, __in Z3_tactic t);
06092 
06097     Z3_param_descrs Z3_API Z3_tactic_get_param_descrs(__in Z3_context c, __in Z3_tactic t);
06098 
06103     Z3_string Z3_API Z3_tactic_get_descr(__in Z3_context c, __in Z3_string name);
06104     
06109     Z3_string Z3_API Z3_probe_get_descr(__in Z3_context c, __in Z3_string name);
06110 
06116     double Z3_API Z3_probe_apply(__in Z3_context c, __in Z3_probe p, __in Z3_goal g);
06117 
06122     Z3_apply_result Z3_API Z3_tactic_apply(__in Z3_context c, __in Z3_tactic t, __in Z3_goal g);
06123 
06128     Z3_apply_result Z3_API Z3_tactic_apply_ex(Z3_context c, Z3_tactic t, Z3_goal g, Z3_params p);
06129 
06130 #ifdef CorML3
06131 
06135     void Z3_API Z3_apply_result_inc_ref(__in Z3_context c, __in Z3_apply_result r);
06136 
06141     void Z3_API Z3_apply_result_dec_ref(__in Z3_context c, __in Z3_apply_result r);
06142 #endif
06143     
06148     Z3_string Z3_API Z3_apply_result_to_string(__in Z3_context c, __in Z3_apply_result r);
06149     
06154     unsigned Z3_API Z3_apply_result_get_num_subgoals(__in Z3_context c, __in Z3_apply_result r);
06155 
06162     Z3_goal Z3_API Z3_apply_result_get_subgoal(__in Z3_context c, __in Z3_apply_result r, __in unsigned i);
06163     
06169     Z3_model Z3_API Z3_apply_result_convert_model(__in Z3_context c, __in Z3_apply_result r, __in unsigned i, __in Z3_model m);
06170 
06177 
06187     Z3_solver Z3_API Z3_mk_solver(__in Z3_context c);
06188 
06200     Z3_solver Z3_API Z3_mk_simple_solver(__in Z3_context c);
06201 
06210     Z3_solver Z3_API Z3_mk_solver_for_logic(__in Z3_context c, __in Z3_symbol logic);
06211 
06218     Z3_solver Z3_API Z3_mk_solver_from_tactic(__in Z3_context c, __in Z3_tactic t);
06219 
06224     Z3_string Z3_API Z3_solver_get_help(__in Z3_context c, __in Z3_solver s);
06225 
06230     Z3_param_descrs Z3_API Z3_solver_get_param_descrs(__in Z3_context c, __in Z3_solver s);
06231 
06236     void Z3_API Z3_solver_set_params(__in Z3_context c, __in Z3_solver s, __in Z3_params p);
06237     
06238 #ifdef Conly
06239 
06243     void Z3_API Z3_solver_inc_ref(__in Z3_context c, __in Z3_solver s);
06244 
06249     void Z3_API Z3_solver_dec_ref(__in Z3_context c, __in Z3_solver s);
06250 #endif
06251     
06260     void Z3_API Z3_solver_push(__in Z3_context c, __in Z3_solver s);
06261 
06270     void Z3_API Z3_solver_pop(__in Z3_context c, __in Z3_solver s, unsigned n);
06271 
06276     void Z3_API Z3_solver_reset(__in Z3_context c, __in Z3_solver s);
06277     
06285     unsigned Z3_API Z3_solver_get_num_scopes(__in Z3_context c, __in Z3_solver s);
06286     
06294     void Z3_API Z3_solver_assert(__in Z3_context c, __in Z3_solver s, __in Z3_ast a);
06295 
06309     void Z3_API Z3_solver_assert_and_track(__in Z3_context c, __in Z3_solver s, __in Z3_ast a, __in Z3_ast p);
06310     
06315     Z3_ast_vector Z3_API Z3_solver_get_assertions(__in Z3_context c, __in Z3_solver s);
06316     
06332     Z3_lbool Z3_API Z3_solver_check(__in Z3_context c, __in Z3_solver s);
06333 
06344     Z3_lbool Z3_API Z3_solver_check_assumptions(__in Z3_context c, __in Z3_solver s, 
06345                                                 __in unsigned num_assumptions, __in_ecount(num_assumptions) Z3_ast const assumptions[]);
06346 
06354     Z3_model Z3_API Z3_solver_get_model(__in Z3_context c, __in Z3_solver s);
06355 
06364     Z3_ast Z3_API Z3_solver_get_proof(__in Z3_context c, __in Z3_solver s);
06365 
06371     Z3_ast_vector Z3_API Z3_solver_get_unsat_core(__in Z3_context c, __in Z3_solver s);
06372     
06378     Z3_string Z3_API Z3_solver_get_reason_unknown(__in Z3_context c, __in Z3_solver s);
06379     
06386     Z3_stats Z3_API Z3_solver_get_statistics(__in Z3_context c, __in Z3_solver s);
06387     
06392     Z3_string Z3_API Z3_solver_to_string(__in Z3_context c, __in Z3_solver s);
06393 
06400 
06401 #ifdef ML4only
06402 #include <mlx_statistics.idl>
06403 #endif
06404 
06408     Z3_string Z3_API Z3_stats_to_string(__in Z3_context c, __in Z3_stats s);
06409     
06414 #ifdef Conly
06415 
06419     void Z3_API Z3_stats_inc_ref(__in Z3_context c, __in Z3_stats s);
06420 
06425     void Z3_API Z3_stats_dec_ref(__in Z3_context c, __in Z3_stats s);
06426 #endif
06427     
06432     unsigned Z3_API Z3_stats_size(__in Z3_context c, __in Z3_stats s);
06433 
06440     Z3_string Z3_API Z3_stats_get_key(__in Z3_context c, __in Z3_stats s, __in unsigned idx);
06441 
06448     Z3_bool Z3_API Z3_stats_is_uint(__in Z3_context c, __in Z3_stats s, __in unsigned idx);
06449 
06456     Z3_bool Z3_API Z3_stats_is_double(__in Z3_context c, __in Z3_stats s, __in unsigned idx);
06457     
06464     unsigned Z3_API Z3_stats_get_uint_value(__in Z3_context c, __in Z3_stats s, __in unsigned idx);
06465 
06472     double Z3_API Z3_stats_get_double_value(__in Z3_context c, __in Z3_stats s, __in unsigned idx);
06473     
06475 #endif
06476 
06477 
06478 #ifdef CorML3
06479 
06484 
06493     Z3_func_decl Z3_API Z3_mk_injective_function(
06494         __in Z3_context c, 
06495         __in Z3_symbol s, 
06496         unsigned domain_size, __in_ecount(domain_size) Z3_sort const domain[],
06497         __in Z3_sort range
06498         );
06499 
06501 #endif
06502 
06503 
06508 
06509 #ifdef CorML3
06510 
06519     Z3_bool Z3_API Z3_set_logic(__in Z3_context c, __in Z3_string logic);
06520     
06533     void Z3_API Z3_push(__in Z3_context c);
06534     
06549     void Z3_API Z3_pop(__in Z3_context c, __in unsigned num_scopes);
06550 
06562     unsigned Z3_API Z3_get_num_scopes(__in Z3_context c);
06563     
06584     void Z3_API Z3_persist_ast(__in Z3_context c, __in Z3_ast a, __in unsigned num_scopes);
06585 
06601     void Z3_API Z3_assert_cnstr(__in Z3_context c, __in Z3_ast a);
06602     
06625     Z3_lbool Z3_API Z3_check_and_get_model(__in Z3_context c, __out Z3_model * m);
06626     
06637     Z3_lbool Z3_API Z3_check(__in Z3_context c);
06638 
06676     Z3_lbool Z3_API Z3_check_assumptions(
06677         __in Z3_context c, 
06678         __in unsigned num_assumptions, __in_ecount(num_assumptions) Z3_ast const assumptions[], 
06679         __out Z3_model * m, __out Z3_ast* proof, 
06680         __inout unsigned* core_size, __inout_ecount(num_assumptions) Z3_ast core[]
06681         );
06682 #endif
06683 
06684 #ifdef CorML4
06685 
06707     Z3_lbool Z3_API Z3_get_implied_equalities(
06708         __in Z3_context c, 
06709         __in Z3_solver  s, 
06710         __in unsigned num_terms,
06711         __in_ecount(num_terms) Z3_ast const terms[],
06712         __out_ecount(num_terms) unsigned class_ids[]
06713         );
06714 #endif
06715 
06716 #ifdef CorML3
06717 
06730     void Z3_API Z3_del_model(__in Z3_context c, __in Z3_model m);
06731 
06738 
06749     void Z3_API Z3_soft_check_cancel(__in Z3_context c);
06750 
06760     Z3_search_failure Z3_API Z3_get_search_failure(__in Z3_context c);
06761 
06768 
06786     Z3_ast Z3_API Z3_mk_label(__in Z3_context c, __in Z3_symbol s, Z3_bool is_pos, Z3_ast f);
06787 
06800     Z3_literals Z3_API Z3_get_relevant_labels(__in Z3_context c);
06801 
06813     Z3_literals Z3_API Z3_get_relevant_literals(__in Z3_context c);
06814 
06827     Z3_literals Z3_API Z3_get_guessed_literals(__in Z3_context c);
06828 
06837     void Z3_API Z3_del_literals(__in Z3_context c, __in Z3_literals lbls);
06838 
06847     unsigned Z3_API Z3_get_num_literals(__in Z3_context c, __in Z3_literals lbls);
06848 
06855     Z3_symbol Z3_API Z3_get_label_symbol(__in Z3_context c, __in Z3_literals lbls, __in unsigned idx);
06856 
06863     Z3_ast Z3_API Z3_get_literal(__in Z3_context c, __in Z3_literals lbls, __in unsigned idx);
06864 
06875     void Z3_API Z3_disable_literal(__in Z3_context c, __in Z3_literals lbls, __in unsigned idx);
06876 
06883     void Z3_API Z3_block_literals(__in Z3_context c, __in Z3_literals lbls);
06884 
06891 
06902     unsigned Z3_API Z3_get_model_num_constants(__in Z3_context c, __in Z3_model m);
06903 
06915     Z3_func_decl Z3_API Z3_get_model_constant(__in Z3_context c, __in Z3_model m, __in unsigned i);
06916     
06926     unsigned Z3_API Z3_get_model_num_funcs(__in Z3_context c, __in Z3_model m);
06927     
06939     Z3_func_decl Z3_API Z3_get_model_func_decl(__in Z3_context c, __in Z3_model m, __in unsigned i);
06940 
06948     Z3_bool Z3_API Z3_eval_func_decl(__in Z3_context c, __in Z3_model m, __in Z3_func_decl decl, __out Z3_ast* v);
06949 
06964     Z3_bool Z3_API Z3_is_array_value(__in Z3_context c, __in Z3_model m, __in Z3_ast v, __out unsigned* num_entries);
06965 
06976     void Z3_API Z3_get_array_value(__in Z3_context c, 
06977                                    __in Z3_model m,
06978                                    __in Z3_ast v,
06979                                    __in unsigned num_entries,
06980                                    __inout_ecount(num_entries) Z3_ast indices[],
06981                                    __inout_ecount(num_entries) Z3_ast values[],
06982                                    __out Z3_ast* else_value
06983                                    );
06984 
07003     Z3_ast Z3_API Z3_get_model_func_else(__in Z3_context c, __in Z3_model m, __in unsigned i);
07004 
07023     unsigned Z3_API Z3_get_model_func_num_entries(__in Z3_context c, __in Z3_model m, __in unsigned i);
07024     
07048     unsigned Z3_API Z3_get_model_func_entry_num_args(__in Z3_context c,
07049                                                      __in Z3_model m,
07050                                                      __in unsigned i,
07051                                                      __in unsigned j);
07052     
07077     Z3_ast Z3_API Z3_get_model_func_entry_arg(__in Z3_context c,
07078                                                 __in Z3_model m,
07079                                                 __in unsigned i,
07080                                                 __in unsigned j,
07081                                                 __in unsigned k);
07082     
07105     Z3_ast Z3_API Z3_get_model_func_entry_value(__in Z3_context c,
07106                                                   __in Z3_model m,
07107                                                   __in unsigned i,
07108                                                   __in unsigned j);
07109     
07128     Z3_bool Z3_API Z3_eval(__in Z3_context c, __in Z3_model m, __in Z3_ast t, __out Z3_ast * v);
07129 
07139     Z3_bool Z3_API Z3_eval_decl(__in Z3_context c, __in Z3_model m, 
07140                                 __in Z3_func_decl d, 
07141                                 __in unsigned num_args,
07142                                 __in_ecount(num_args) Z3_ast const args[],
07143                                 __out Z3_ast* v);
07144 
07151 
07166     Z3_string Z3_API Z3_context_to_string(__in Z3_context c);
07167 
07182     Z3_string Z3_API Z3_statistics_to_string(__in Z3_context c);
07183 
07196     Z3_ast Z3_API Z3_get_context_assignment(__in Z3_context c);
07197 
07199 #endif
07200 
07201 
07202 #ifndef CAMLIDL
07203 #ifdef __cplusplus
07204 };
07205 #endif // __cplusplus
07206 #else
07207 }
07208 #endif // CAMLIDL
07209 
07212 #endif
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines