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
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
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
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
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
00945
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
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
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
01051 Z3_OP_LABEL = 0x700,
01052 Z3_OP_LABEL_LIT,
01053
01054
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
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