|
Z3
|
|
|
Z3
|
|
00001 00002 /*++ 00003 Copyright (c) 2015 Microsoft Corporation 00004 00005 --*/ 00006 00007 #ifndef Z3_API_H_ 00008 #define Z3_API_H_ 00009 00010 #ifdef CAMLIDL 00011 #ifdef MLAPIV3 00012 #define ML3only 00013 #define CorML3 00014 #else 00015 #define ML4only 00016 #define CorML4 00017 #endif 00018 #else 00019 #define Conly 00020 #define CorML3 00021 #define CorML4 00022 #endif 00023 00024 #ifdef CorML3 00025 DEFINE_TYPE(Z3_symbol); 00026 DEFINE_TYPE(Z3_literals); 00027 DEFINE_TYPE(Z3_theory); 00028 DEFINE_TYPE(Z3_config); 00029 DEFINE_TYPE(Z3_context); 00030 DEFINE_TYPE(Z3_sort); 00031 #define Z3_sort_opt Z3_sort 00032 DEFINE_TYPE(Z3_func_decl); 00033 DEFINE_TYPE(Z3_ast); 00034 #define Z3_ast_opt Z3_ast 00035 DEFINE_TYPE(Z3_app); 00036 DEFINE_TYPE(Z3_pattern); 00037 DEFINE_TYPE(Z3_model); 00038 DEFINE_TYPE(Z3_constructor); 00039 DEFINE_TYPE(Z3_constructor_list); 00040 #endif 00041 #ifdef Conly 00042 DEFINE_TYPE(Z3_params); 00043 DEFINE_TYPE(Z3_param_descrs); 00044 DEFINE_TYPE(Z3_goal); 00045 DEFINE_TYPE(Z3_tactic); 00046 DEFINE_TYPE(Z3_probe); 00047 DEFINE_TYPE(Z3_stats); 00048 DEFINE_TYPE(Z3_solver); 00049 DEFINE_TYPE(Z3_ast_vector); 00050 DEFINE_TYPE(Z3_ast_map); 00051 DEFINE_TYPE(Z3_apply_result); 00052 DEFINE_TYPE(Z3_func_interp); 00053 #define Z3_func_interp_opt Z3_func_interp 00054 DEFINE_TYPE(Z3_func_entry); 00055 DEFINE_TYPE(Z3_fixedpoint); 00056 DEFINE_TYPE(Z3_optimize); 00057 DEFINE_TYPE(Z3_rcf_num); 00058 DEFINE_VOID(Z3_theory_data); 00059 #endif 00060 00061 #ifndef __int64 00062 #define __int64 long long 00063 #endif 00064 00065 #ifndef __uint64 00066 #define __uint64 unsigned long long 00067 #endif 00068 00074 00106 #ifdef Conly 00107 00110 typedef int Z3_bool; 00111 #else 00112 #define Z3_bool boolean 00113 #endif 00114 00115 #ifdef Conly 00116 00119 typedef const char * Z3_string; 00120 typedef Z3_string * Z3_string_ptr; 00121 #else 00122 typedef [string] const char * Z3_string; 00123 #define Z3_string_ptr Z3_string * 00124 #endif 00125 00126 #ifdef Conly 00127 00130 #define Z3_TRUE 1 00131 00135 #define Z3_FALSE 0 00136 00137 #endif 00138 00143 typedef enum 00144 { 00145 Z3_L_FALSE = -1, 00146 Z3_L_UNDEF, 00147 Z3_L_TRUE 00148 } Z3_lbool; 00149 00158 typedef enum 00159 { 00160 Z3_INT_SYMBOL, 00161 Z3_STRING_SYMBOL 00162 } Z3_symbol_kind; 00163 00164 00179 typedef enum 00180 { 00181 Z3_PARAMETER_INT, 00182 Z3_PARAMETER_DOUBLE, 00183 Z3_PARAMETER_RATIONAL, 00184 Z3_PARAMETER_SYMBOL, 00185 Z3_PARAMETER_SORT, 00186 Z3_PARAMETER_AST, 00187 Z3_PARAMETER_FUNC_DECL, 00188 } Z3_parameter_kind; 00189 00194 typedef enum 00195 { 00196 Z3_UNINTERPRETED_SORT, 00197 Z3_BOOL_SORT, 00198 Z3_INT_SORT, 00199 Z3_REAL_SORT, 00200 Z3_BV_SORT, 00201 Z3_ARRAY_SORT, 00202 Z3_DATATYPE_SORT, 00203 Z3_RELATION_SORT, 00204 Z3_FINITE_DOMAIN_SORT, 00205 Z3_FLOATING_POINT_SORT, 00206 Z3_ROUNDING_MODE_SORT, 00207 Z3_UNKNOWN_SORT = 1000 00208 } Z3_sort_kind; 00209 00222 typedef enum 00223 { 00224 Z3_NUMERAL_AST, 00225 Z3_APP_AST, 00226 Z3_VAR_AST, 00227 Z3_QUANTIFIER_AST, 00228 Z3_SORT_AST, 00229 Z3_FUNC_DECL_AST, 00230 Z3_UNKNOWN_AST = 1000 00231 } Z3_ast_kind; 00232 00988 typedef enum { 00989 // Basic 00990 Z3_OP_TRUE = 0x100, 00991 Z3_OP_FALSE, 00992 Z3_OP_EQ, 00993 Z3_OP_DISTINCT, 00994 Z3_OP_ITE, 00995 Z3_OP_AND, 00996 Z3_OP_OR, 00997 Z3_OP_IFF, 00998 Z3_OP_XOR, 00999 Z3_OP_NOT, 01000 Z3_OP_IMPLIES, 01001 Z3_OP_OEQ, 01002 Z3_OP_INTERP, 01003 01004 // Arithmetic 01005 Z3_OP_ANUM = 0x200, 01006 Z3_OP_AGNUM, 01007 Z3_OP_LE, 01008 Z3_OP_GE, 01009 Z3_OP_LT, 01010 Z3_OP_GT, 01011 Z3_OP_ADD, 01012 Z3_OP_SUB, 01013 Z3_OP_UMINUS, 01014 Z3_OP_MUL, 01015 Z3_OP_DIV, 01016 Z3_OP_IDIV, 01017 Z3_OP_REM, 01018 Z3_OP_MOD, 01019 Z3_OP_TO_REAL, 01020 Z3_OP_TO_INT, 01021 Z3_OP_IS_INT, 01022 Z3_OP_POWER, 01023 01024 // Arrays & Sets 01025 Z3_OP_STORE = 0x300, 01026 Z3_OP_SELECT, 01027 Z3_OP_CONST_ARRAY, 01028 Z3_OP_ARRAY_MAP, 01029 Z3_OP_ARRAY_DEFAULT, 01030 Z3_OP_SET_UNION, 01031 Z3_OP_SET_INTERSECT, 01032 Z3_OP_SET_DIFFERENCE, 01033 Z3_OP_SET_COMPLEMENT, 01034 Z3_OP_SET_SUBSET, 01035 Z3_OP_AS_ARRAY, 01036 01037 // Bit-vectors 01038 Z3_OP_BNUM = 0x400, 01039 Z3_OP_BIT1, 01040 Z3_OP_BIT0, 01041 Z3_OP_BNEG, 01042 Z3_OP_BADD, 01043 Z3_OP_BSUB, 01044 Z3_OP_BMUL, 01045 01046 Z3_OP_BSDIV, 01047 Z3_OP_BUDIV, 01048 Z3_OP_BSREM, 01049 Z3_OP_BUREM, 01050 Z3_OP_BSMOD, 01051 01052 // special functions to record the division by 0 cases 01053 // these are internal functions 01054 Z3_OP_BSDIV0, 01055 Z3_OP_BUDIV0, 01056 Z3_OP_BSREM0, 01057 Z3_OP_BUREM0, 01058 Z3_OP_BSMOD0, 01059 01060 Z3_OP_ULEQ, 01061 Z3_OP_SLEQ, 01062 Z3_OP_UGEQ, 01063 Z3_OP_SGEQ, 01064 Z3_OP_ULT, 01065 Z3_OP_SLT, 01066 Z3_OP_UGT, 01067 Z3_OP_SGT, 01068 01069 Z3_OP_BAND, 01070 Z3_OP_BOR, 01071 Z3_OP_BNOT, 01072 Z3_OP_BXOR, 01073 Z3_OP_BNAND, 01074 Z3_OP_BNOR, 01075 Z3_OP_BXNOR, 01076 01077 Z3_OP_CONCAT, 01078 Z3_OP_SIGN_EXT, 01079 Z3_OP_ZERO_EXT, 01080 Z3_OP_EXTRACT, 01081 Z3_OP_REPEAT, 01082 01083 Z3_OP_BREDOR, 01084 Z3_OP_BREDAND, 01085 Z3_OP_BCOMP, 01086 01087 Z3_OP_BSHL, 01088 Z3_OP_BLSHR, 01089 Z3_OP_BASHR, 01090 Z3_OP_ROTATE_LEFT, 01091 Z3_OP_ROTATE_RIGHT, 01092 Z3_OP_EXT_ROTATE_LEFT, 01093 Z3_OP_EXT_ROTATE_RIGHT, 01094 01095 Z3_OP_INT2BV, 01096 Z3_OP_BV2INT, 01097 Z3_OP_CARRY, 01098 Z3_OP_XOR3, 01099 01100 // Proofs 01101 Z3_OP_PR_UNDEF = 0x500, 01102 Z3_OP_PR_TRUE, 01103 Z3_OP_PR_ASSERTED, 01104 Z3_OP_PR_GOAL, 01105 Z3_OP_PR_MODUS_PONENS, 01106 Z3_OP_PR_REFLEXIVITY, 01107 Z3_OP_PR_SYMMETRY, 01108 Z3_OP_PR_TRANSITIVITY, 01109 Z3_OP_PR_TRANSITIVITY_STAR, 01110 Z3_OP_PR_MONOTONICITY, 01111 Z3_OP_PR_QUANT_INTRO, 01112 Z3_OP_PR_DISTRIBUTIVITY, 01113 Z3_OP_PR_AND_ELIM, 01114 Z3_OP_PR_NOT_OR_ELIM, 01115 Z3_OP_PR_REWRITE, 01116 Z3_OP_PR_REWRITE_STAR, 01117 Z3_OP_PR_PULL_QUANT, 01118 Z3_OP_PR_PULL_QUANT_STAR, 01119 Z3_OP_PR_PUSH_QUANT, 01120 Z3_OP_PR_ELIM_UNUSED_VARS, 01121 Z3_OP_PR_DER, 01122 Z3_OP_PR_QUANT_INST, 01123 Z3_OP_PR_HYPOTHESIS, 01124 Z3_OP_PR_LEMMA, 01125 Z3_OP_PR_UNIT_RESOLUTION, 01126 Z3_OP_PR_IFF_TRUE, 01127 Z3_OP_PR_IFF_FALSE, 01128 Z3_OP_PR_COMMUTATIVITY, 01129 Z3_OP_PR_DEF_AXIOM, 01130 Z3_OP_PR_DEF_INTRO, 01131 Z3_OP_PR_APPLY_DEF, 01132 Z3_OP_PR_IFF_OEQ, 01133 Z3_OP_PR_NNF_POS, 01134 Z3_OP_PR_NNF_NEG, 01135 Z3_OP_PR_NNF_STAR, 01136 Z3_OP_PR_CNF_STAR, 01137 Z3_OP_PR_SKOLEMIZE, 01138 Z3_OP_PR_MODUS_PONENS_OEQ, 01139 Z3_OP_PR_TH_LEMMA, 01140 Z3_OP_PR_HYPER_RESOLVE, 01141 01142 // Sequences 01143 Z3_OP_RA_STORE = 0x600, 01144 Z3_OP_RA_EMPTY, 01145 Z3_OP_RA_IS_EMPTY, 01146 Z3_OP_RA_JOIN, 01147 Z3_OP_RA_UNION, 01148 Z3_OP_RA_WIDEN, 01149 Z3_OP_RA_PROJECT, 01150 Z3_OP_RA_FILTER, 01151 Z3_OP_RA_NEGATION_FILTER, 01152 Z3_OP_RA_RENAME, 01153 Z3_OP_RA_COMPLEMENT, 01154 Z3_OP_RA_SELECT, 01155 Z3_OP_RA_CLONE, 01156 Z3_OP_FD_LT, 01157 01158 // Auxiliary 01159 Z3_OP_LABEL = 0x700, 01160 Z3_OP_LABEL_LIT, 01161 01162 // Datatypes 01163 Z3_OP_DT_CONSTRUCTOR=0x800, 01164 Z3_OP_DT_RECOGNISER, 01165 Z3_OP_DT_ACCESSOR, 01166 Z3_OP_DT_UPDATE_FIELD, 01167 01168 // Pseudo Booleans 01169 Z3_OP_PB_AT_MOST=0x900, 01170 Z3_OP_PB_LE, 01171 Z3_OP_PB_GE, 01172 01173 // Floating-Point Arithmetic 01174 Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN, 01175 Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY, 01176 Z3_OP_FPA_RM_TOWARD_POSITIVE, 01177 Z3_OP_FPA_RM_TOWARD_NEGATIVE, 01178 Z3_OP_FPA_RM_TOWARD_ZERO, 01179 01180 Z3_OP_FPA_NUM, 01181 Z3_OP_FPA_PLUS_INF, 01182 Z3_OP_FPA_MINUS_INF, 01183 Z3_OP_FPA_NAN, 01184 Z3_OP_FPA_PLUS_ZERO, 01185 Z3_OP_FPA_MINUS_ZERO, 01186 01187 Z3_OP_FPA_ADD, 01188 Z3_OP_FPA_SUB, 01189 Z3_OP_FPA_NEG, 01190 Z3_OP_FPA_MUL, 01191 Z3_OP_FPA_DIV, 01192 Z3_OP_FPA_REM, 01193 Z3_OP_FPA_ABS, 01194 Z3_OP_FPA_MIN, 01195 Z3_OP_FPA_MAX, 01196 Z3_OP_FPA_FMA, 01197 Z3_OP_FPA_SQRT, 01198 Z3_OP_FPA_ROUND_TO_INTEGRAL, 01199 01200 Z3_OP_FPA_EQ, 01201 Z3_OP_FPA_LT, 01202 Z3_OP_FPA_GT, 01203 Z3_OP_FPA_LE, 01204 Z3_OP_FPA_GE, 01205 Z3_OP_FPA_IS_NAN, 01206 Z3_OP_FPA_IS_INF, 01207 Z3_OP_FPA_IS_ZERO, 01208 Z3_OP_FPA_IS_NORMAL, 01209 Z3_OP_FPA_IS_SUBNORMAL, 01210 Z3_OP_FPA_IS_NEGATIVE, 01211 Z3_OP_FPA_IS_POSITIVE, 01212 01213 Z3_OP_FPA_FP, 01214 Z3_OP_FPA_TO_FP, 01215 Z3_OP_FPA_TO_FP_UNSIGNED, 01216 Z3_OP_FPA_TO_UBV, 01217 Z3_OP_FPA_TO_SBV, 01218 Z3_OP_FPA_TO_REAL, 01219 01220 Z3_OP_FPA_TO_IEEE_BV, 01221 01222 Z3_OP_UNINTERPRETED 01223 } Z3_decl_kind; 01224 01239 typedef enum { 01240 Z3_PK_UINT, 01241 Z3_PK_BOOL, 01242 Z3_PK_DOUBLE, 01243 Z3_PK_SYMBOL, 01244 Z3_PK_STRING, 01245 Z3_PK_OTHER, 01246 Z3_PK_INVALID 01247 } Z3_param_kind; 01248 01249 #ifdef CorML3 01250 01263 typedef enum { 01264 Z3_NO_FAILURE, 01265 Z3_UNKNOWN, 01266 Z3_TIMEOUT, 01267 Z3_MEMOUT_WATERMARK, 01268 Z3_CANCELED, 01269 Z3_NUM_CONFLICTS, 01270 Z3_THEORY, 01271 Z3_QUANTIFIERS 01272 } Z3_search_failure; 01273 #endif 01274 01284 typedef enum { 01285 Z3_PRINT_SMTLIB_FULL, 01286 Z3_PRINT_LOW_LEVEL, 01287 Z3_PRINT_SMTLIB_COMPLIANT, 01288 Z3_PRINT_SMTLIB2_COMPLIANT 01289 } Z3_ast_print_mode; 01290 01291 01292 #ifdef CorML4 01293 01311 typedef enum 01312 { 01313 Z3_OK, 01314 Z3_SORT_ERROR, 01315 Z3_IOB, 01316 Z3_INVALID_ARG, 01317 Z3_PARSER_ERROR, 01318 Z3_NO_PARSER, 01319 Z3_INVALID_PATTERN, 01320 Z3_MEMOUT_FAIL, 01321 Z3_FILE_ACCESS_ERROR, 01322 Z3_INTERNAL_FATAL, 01323 Z3_INVALID_USAGE, 01324 Z3_DEC_REF_ERROR, 01325 Z3_EXCEPTION 01326 } Z3_error_code; 01327 01328 #endif 01329 01363 #ifdef Conly 01364 01367 typedef void Z3_error_handler(Z3_context c, Z3_error_code e); 01368 01369 #endif 01370 #ifdef ML4only 01371 #include <error_handling.idl> 01372 #endif 01373 01374 01375 #ifdef CorML4 01376 01385 typedef enum 01386 { 01387 Z3_GOAL_PRECISE, 01388 Z3_GOAL_UNDER, 01389 Z3_GOAL_OVER, 01390 Z3_GOAL_UNDER_OVER 01391 } Z3_goal_prec; 01392 01393 #endif 01394 01397 #ifndef CAMLIDL 01398 #ifdef __cplusplus 01399 extern "C" { 01400 #endif // __cplusplus 01401 #else 01402 [pointer_default(ref)] interface Z3 { 01403 #endif // CAMLIDL 01404 01405 #ifdef CorML3 01406 01431 void Z3_API Z3_global_param_set(Z3_string param_id, Z3_string param_value); 01432 01433 01441 void Z3_API Z3_global_param_reset_all(void); 01442 01455 Z3_bool_opt Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value); 01456 01463 01498 Z3_config Z3_API Z3_mk_config(void); 01499 01506 void Z3_API Z3_del_config(Z3_config c); 01507 01516 void Z3_API Z3_set_param_value(Z3_config c, Z3_string param_id, Z3_string param_value); 01517 01519 #endif 01520 01525 01548 #ifdef CorML3 01549 Z3_context Z3_API Z3_mk_context(Z3_config c); 01550 #endif 01551 #ifdef ML4only 01552 #include <mlx_mk_context_x.idl> 01553 #endif 01554 01555 #ifdef Conly 01556 01575 Z3_context Z3_API Z3_mk_context_rc(Z3_config c); 01576 #endif 01577 01578 #ifdef CorML3 01579 01585 void Z3_API Z3_del_context(Z3_context c); 01586 #endif 01587 01588 #ifdef Conly 01589 01595 void Z3_API Z3_inc_ref(Z3_context c, Z3_ast a); 01596 01603 void Z3_API Z3_dec_ref(Z3_context c, Z3_ast a); 01604 #endif 01605 01612 void Z3_API Z3_update_param_value(Z3_context c, Z3_string param_id, Z3_string param_value); 01613 01614 #ifdef CorML4 01615 01620 void Z3_API Z3_interrupt(Z3_context c); 01621 #endif 01622 01623 01626 #ifdef CorML4 01627 01631 01641 Z3_params Z3_API Z3_mk_params(Z3_context c); 01642 01643 #ifdef Conly 01644 01648 void Z3_API Z3_params_inc_ref(Z3_context c, Z3_params p); 01649 01654 void Z3_API Z3_params_dec_ref(Z3_context c, Z3_params p); 01655 #endif 01656 01661 void Z3_API Z3_params_set_bool(Z3_context c, Z3_params p, Z3_symbol k, Z3_bool v); 01662 01667 void Z3_API Z3_params_set_uint(Z3_context c, Z3_params p, Z3_symbol k, unsigned v); 01668 01673 void Z3_API Z3_params_set_double(Z3_context c, Z3_params p, Z3_symbol k, double v); 01674 01679 void Z3_API Z3_params_set_symbol(Z3_context c, Z3_params p, Z3_symbol k, Z3_symbol v); 01680 01686 Z3_string Z3_API Z3_params_to_string(Z3_context c, Z3_params p); 01687 01694 void Z3_API Z3_params_validate(Z3_context c, Z3_params p, Z3_param_descrs d); 01695 01696 #endif 01697 01700 #ifdef CorML4 01701 01705 01706 #ifdef Conly 01707 01711 void Z3_API Z3_param_descrs_inc_ref(Z3_context c, Z3_param_descrs p); 01712 01717 void Z3_API Z3_param_descrs_dec_ref(Z3_context c, Z3_param_descrs p); 01718 #endif 01719 01724 Z3_param_kind Z3_API Z3_param_descrs_get_kind(Z3_context c, Z3_param_descrs p, Z3_symbol n); 01725 01730 unsigned Z3_API Z3_param_descrs_size(Z3_context c, Z3_param_descrs p); 01731 01738 Z3_symbol Z3_API Z3_param_descrs_get_name(Z3_context c, Z3_param_descrs p, unsigned i); 01739 01745 Z3_string Z3_API Z3_param_descrs_to_string(Z3_context c, Z3_param_descrs p); 01746 01748 #endif 01749 01754 01755 #ifdef ML4only 01756 #include <mlx_mk_symbol.idl> 01757 #endif 01758 01774 Z3_symbol Z3_API Z3_mk_int_symbol(Z3_context c, int i); 01775 01784 Z3_symbol Z3_API Z3_mk_string_symbol(Z3_context c, Z3_string s); 01785 01792 01793 #ifdef ML4only 01794 #include <mlx_mk_sort.idl> 01795 #endif 01796 01807 Z3_sort Z3_API Z3_mk_uninterpreted_sort(Z3_context c, Z3_symbol s); 01808 01815 Z3_sort Z3_API Z3_mk_bool_sort(Z3_context c); 01816 01827 Z3_sort Z3_API Z3_mk_int_sort(Z3_context c); 01828 01835 Z3_sort Z3_API Z3_mk_real_sort(Z3_context c); 01836 01845 Z3_sort Z3_API Z3_mk_bv_sort(Z3_context c, unsigned sz); 01846 01859 Z3_sort Z3_API Z3_mk_finite_domain_sort(Z3_context c, Z3_symbol name, unsigned __int64 size); 01860 01871 Z3_sort Z3_API Z3_mk_array_sort(Z3_context c, Z3_sort domain, Z3_sort range); 01872 01892 Z3_sort Z3_API Z3_mk_tuple_sort(Z3_context c, 01893 Z3_symbol mk_tuple_name, 01894 unsigned num_fields, 01895 Z3_symbol const field_names[], 01896 Z3_sort const field_sorts[], 01897 Z3_func_decl * mk_tuple_decl, 01898 Z3_func_decl proj_decl[]); 01899 01925 Z3_sort Z3_API Z3_mk_enumeration_sort(Z3_context c, 01926 Z3_symbol name, 01927 unsigned n, 01928 Z3_symbol const enum_names[], 01929 Z3_func_decl enum_consts[], 01930 Z3_func_decl enum_testers[]); 01931 01952 Z3_sort Z3_API Z3_mk_list_sort(Z3_context c, 01953 Z3_symbol name, 01954 Z3_sort elem_sort, 01955 Z3_func_decl* nil_decl, 01956 Z3_func_decl* is_nil_decl, 01957 Z3_func_decl* cons_decl, 01958 Z3_func_decl* is_cons_decl, 01959 Z3_func_decl* head_decl, 01960 Z3_func_decl* tail_decl 01961 ); 01962 01963 BEGIN_MLAPI_EXCLUDE 01980 Z3_constructor Z3_API Z3_mk_constructor(Z3_context c, 01981 Z3_symbol name, 01982 Z3_symbol recognizer, 01983 unsigned num_fields, 01984 Z3_symbol const field_names[], 01985 Z3_sort_opt const sorts[], 01986 unsigned sort_refs[] 01987 ); 01988 01996 void Z3_API Z3_del_constructor(Z3_context c, Z3_constructor constr); 01997 02008 Z3_sort Z3_API Z3_mk_datatype(Z3_context c, 02009 Z3_symbol name, 02010 unsigned num_constructors, 02011 Z3_constructor constructors[]); 02012 02013 02022 Z3_constructor_list Z3_API Z3_mk_constructor_list(Z3_context c, 02023 unsigned num_constructors, 02024 Z3_constructor const constructors[]); 02025 02035 void Z3_API Z3_del_constructor_list(Z3_context c, Z3_constructor_list clist); 02036 02047 void Z3_API Z3_mk_datatypes(Z3_context c, 02048 unsigned num_sorts, 02049 Z3_symbol const sort_names[], 02050 Z3_sort sorts[], 02051 Z3_constructor_list constructor_lists[]); 02052 02064 void Z3_API Z3_query_constructor(Z3_context c, 02065 Z3_constructor constr, 02066 unsigned num_fields, 02067 Z3_func_decl* constructor, 02068 Z3_func_decl* tester, 02069 Z3_func_decl accessors[]); 02070 END_MLAPI_EXCLUDE 02071 02078 02098 Z3_func_decl Z3_API Z3_mk_func_decl(Z3_context c, Z3_symbol s, 02099 unsigned domain_size, Z3_sort const domain[], 02100 Z3_sort range); 02101 02102 02109 Z3_ast Z3_API Z3_mk_app( 02110 Z3_context c, 02111 Z3_func_decl d, 02112 unsigned num_args, 02113 Z3_ast const args[]); 02114 02130 Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty); 02131 02143 Z3_func_decl Z3_API Z3_mk_fresh_func_decl(Z3_context c, Z3_string prefix, 02144 unsigned domain_size, Z3_sort const domain[], 02145 Z3_sort range); 02146 02161 Z3_ast Z3_API Z3_mk_fresh_const(Z3_context c, Z3_string prefix, Z3_sort ty); 02172 Z3_ast Z3_API Z3_mk_true(Z3_context c); 02173 02178 Z3_ast Z3_API Z3_mk_false(Z3_context c); 02179 02187 Z3_ast Z3_API Z3_mk_eq(Z3_context c, Z3_ast l, Z3_ast r); 02188 02203 Z3_ast Z3_API Z3_mk_distinct(Z3_context c, unsigned num_args, Z3_ast const args[]); 02204 02212 Z3_ast Z3_API Z3_mk_not(Z3_context c, Z3_ast a); 02213 02223 Z3_ast Z3_API Z3_mk_ite(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3); 02224 02232 Z3_ast Z3_API Z3_mk_iff(Z3_context c, Z3_ast t1, Z3_ast t2); 02233 02241 Z3_ast Z3_API Z3_mk_implies(Z3_context c, Z3_ast t1, Z3_ast t2); 02242 02250 Z3_ast Z3_API Z3_mk_xor(Z3_context c, Z3_ast t1, Z3_ast t2); 02251 02262 Z3_ast Z3_API Z3_mk_and(Z3_context c, unsigned num_args, Z3_ast const args[]); 02263 02274 Z3_ast Z3_API Z3_mk_or(Z3_context c, unsigned num_args, Z3_ast const args[]); 02291 Z3_ast Z3_API Z3_mk_add(Z3_context c, unsigned num_args, Z3_ast const args[]); 02292 02304 Z3_ast Z3_API Z3_mk_mul(Z3_context c, unsigned num_args, Z3_ast const args[]); 02305 02316 Z3_ast Z3_API Z3_mk_sub(Z3_context c, unsigned num_args, Z3_ast const args[]); 02317 02325 Z3_ast Z3_API Z3_mk_unary_minus(Z3_context c, Z3_ast arg); 02326 02336 Z3_ast Z3_API Z3_mk_div(Z3_context c, Z3_ast arg1, Z3_ast arg2); 02337 02345 Z3_ast Z3_API Z3_mk_mod(Z3_context c, Z3_ast arg1, Z3_ast arg2); 02346 02354 Z3_ast Z3_API Z3_mk_rem(Z3_context c, Z3_ast arg1, Z3_ast arg2); 02355 02362 Z3_ast Z3_API Z3_mk_power(Z3_context c, Z3_ast arg1, Z3_ast arg2); 02363 02371 Z3_ast Z3_API Z3_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2); 02372 02380 Z3_ast Z3_API Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2); 02381 02389 Z3_ast Z3_API Z3_mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2); 02390 02398 Z3_ast Z3_API Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2); 02399 02417 Z3_ast Z3_API Z3_mk_int2real(Z3_context c, Z3_ast t1); 02418 02430 Z3_ast Z3_API Z3_mk_real2int(Z3_context c, Z3_ast t1); 02431 02440 Z3_ast Z3_API Z3_mk_is_int(Z3_context c, Z3_ast t1); 02454 Z3_ast Z3_API Z3_mk_bvnot(Z3_context c, Z3_ast t1); 02455 02463 Z3_ast Z3_API Z3_mk_bvredand(Z3_context c, Z3_ast t1); 02464 02472 Z3_ast Z3_API Z3_mk_bvredor(Z3_context c, Z3_ast t1); 02473 02481 Z3_ast Z3_API Z3_mk_bvand(Z3_context c, Z3_ast t1, Z3_ast t2); 02482 02490 Z3_ast Z3_API Z3_mk_bvor(Z3_context c, Z3_ast t1, Z3_ast t2); 02491 02499 Z3_ast Z3_API Z3_mk_bvxor(Z3_context c, Z3_ast t1, Z3_ast t2); 02500 02508 Z3_ast Z3_API Z3_mk_bvnand(Z3_context c, Z3_ast t1, Z3_ast t2); 02509 02517 Z3_ast Z3_API Z3_mk_bvnor(Z3_context c, Z3_ast t1, Z3_ast t2); 02518 02526 Z3_ast Z3_API Z3_mk_bvxnor(Z3_context c, Z3_ast t1, Z3_ast t2); 02527 02535 Z3_ast Z3_API Z3_mk_bvneg(Z3_context c, Z3_ast t1); 02536 02544 Z3_ast Z3_API Z3_mk_bvadd(Z3_context c, Z3_ast t1, Z3_ast t2); 02545 02553 Z3_ast Z3_API Z3_mk_bvsub(Z3_context c, Z3_ast t1, Z3_ast t2); 02554 02562 Z3_ast Z3_API Z3_mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2); 02563 02575 Z3_ast Z3_API Z3_mk_bvudiv(Z3_context c, Z3_ast t1, Z3_ast t2); 02576 02592 Z3_ast Z3_API Z3_mk_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2); 02593 02605 Z3_ast Z3_API Z3_mk_bvurem(Z3_context c, Z3_ast t1, Z3_ast t2); 02606 02621 Z3_ast Z3_API Z3_mk_bvsrem(Z3_context c, Z3_ast t1, Z3_ast t2); 02622 02634 Z3_ast Z3_API Z3_mk_bvsmod(Z3_context c, Z3_ast t1, Z3_ast t2); 02635 02643 Z3_ast Z3_API Z3_mk_bvult(Z3_context c, Z3_ast t1, Z3_ast t2); 02644 02660 Z3_ast Z3_API Z3_mk_bvslt(Z3_context c, Z3_ast t1, Z3_ast t2); 02661 02669 Z3_ast Z3_API Z3_mk_bvule(Z3_context c, Z3_ast t1, Z3_ast t2); 02670 02678 Z3_ast Z3_API Z3_mk_bvsle(Z3_context c, Z3_ast t1, Z3_ast t2); 02679 02687 Z3_ast Z3_API Z3_mk_bvuge(Z3_context c, Z3_ast t1, Z3_ast t2); 02688 02696 Z3_ast Z3_API Z3_mk_bvsge(Z3_context c, Z3_ast t1, Z3_ast t2); 02697 02705 Z3_ast Z3_API Z3_mk_bvugt(Z3_context c, Z3_ast t1, Z3_ast t2); 02706 02714 Z3_ast Z3_API Z3_mk_bvsgt(Z3_context c, Z3_ast t1, Z3_ast t2); 02715 02726 Z3_ast Z3_API Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2); 02727 02737 Z3_ast Z3_API Z3_mk_extract(Z3_context c, unsigned high, unsigned low, Z3_ast t1); 02738 02748 Z3_ast Z3_API Z3_mk_sign_ext(Z3_context c, unsigned i, Z3_ast t1); 02749 02759 Z3_ast Z3_API Z3_mk_zero_ext(Z3_context c, unsigned i, Z3_ast t1); 02760 02768 Z3_ast Z3_API Z3_mk_repeat(Z3_context c, unsigned i, Z3_ast t1); 02769 02784 Z3_ast Z3_API Z3_mk_bvshl(Z3_context c, Z3_ast t1, Z3_ast t2); 02785 02800 Z3_ast Z3_API Z3_mk_bvlshr(Z3_context c, Z3_ast t1, Z3_ast t2); 02801 02817 Z3_ast Z3_API Z3_mk_bvashr(Z3_context c, Z3_ast t1, Z3_ast t2); 02818 02826 Z3_ast Z3_API Z3_mk_rotate_left(Z3_context c, unsigned i, Z3_ast t1); 02827 02835 Z3_ast Z3_API Z3_mk_rotate_right(Z3_context c, unsigned i, Z3_ast t1); 02836 02844 Z3_ast Z3_API Z3_mk_ext_rotate_left(Z3_context c, Z3_ast t1, Z3_ast t2); 02845 02853 Z3_ast Z3_API Z3_mk_ext_rotate_right(Z3_context c, Z3_ast t1, Z3_ast t2); 02854 02866 Z3_ast Z3_API Z3_mk_int2bv(Z3_context c, unsigned n, Z3_ast t1); 02867 02883 Z3_ast Z3_API Z3_mk_bv2int(Z3_context c,Z3_ast t1, Z3_bool is_signed); 02884 02893 Z3_ast Z3_API Z3_mk_bvadd_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_bool is_signed); 02894 02903 Z3_ast Z3_API Z3_mk_bvadd_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2); 02904 02913 Z3_ast Z3_API Z3_mk_bvsub_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2); 02914 02923 Z3_ast Z3_API Z3_mk_bvsub_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_bool is_signed); 02924 02933 Z3_ast Z3_API Z3_mk_bvsdiv_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2); 02934 02943 Z3_ast Z3_API Z3_mk_bvneg_no_overflow(Z3_context c, Z3_ast t1); 02944 02953 Z3_ast Z3_API Z3_mk_bvmul_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_bool is_signed); 02954 02963 Z3_ast Z3_API Z3_mk_bvmul_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2); 02984 Z3_ast Z3_API Z3_mk_select(Z3_context c, Z3_ast a, Z3_ast i); 02985 03002 Z3_ast Z3_API Z3_mk_store(Z3_context c, Z3_ast a, Z3_ast i, Z3_ast v); 03003 03015 Z3_ast Z3_API Z3_mk_const_array(Z3_context c, Z3_sort domain, Z3_ast v); 03016 03030 Z3_ast Z3_API Z3_mk_map(Z3_context c, Z3_func_decl f, unsigned n, Z3_ast const* args); 03031 03041 Z3_ast Z3_API Z3_mk_array_default(Z3_context c, Z3_ast array); 03052 Z3_sort Z3_API Z3_mk_set_sort(Z3_context c, Z3_sort ty); 03053 03058 Z3_ast Z3_API Z3_mk_empty_set(Z3_context c, Z3_sort domain); 03059 03064 Z3_ast Z3_API Z3_mk_full_set(Z3_context c, Z3_sort domain); 03065 03072 Z3_ast Z3_API Z3_mk_set_add(Z3_context c, Z3_ast set, Z3_ast elem); 03073 03080 Z3_ast Z3_API Z3_mk_set_del(Z3_context c, Z3_ast set, Z3_ast elem); 03081 03086 Z3_ast Z3_API Z3_mk_set_union(Z3_context c, unsigned num_args, Z3_ast const args[]); 03087 03092 Z3_ast Z3_API Z3_mk_set_intersect(Z3_context c, unsigned num_args, Z3_ast const args[]); 03093 03098 Z3_ast Z3_API Z3_mk_set_difference(Z3_context c, Z3_ast arg1, Z3_ast arg2); 03099 03104 Z3_ast Z3_API Z3_mk_set_complement(Z3_context c, Z3_ast arg); 03105 03112 Z3_ast Z3_API Z3_mk_set_member(Z3_context c, Z3_ast elem, Z3_ast set); 03113 03118 Z3_ast Z3_API Z3_mk_set_subset(Z3_context c, Z3_ast arg1, Z3_ast arg2); 03125 03126 #ifdef ML4only 03127 #include <mlx_mk_numeral.idl> 03128 #endif 03129 03145 Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty); 03146 03161 Z3_ast Z3_API Z3_mk_real(Z3_context c, int num, int den); 03162 03172 Z3_ast Z3_API Z3_mk_int(Z3_context c, int v, Z3_sort ty); 03173 03174 #ifdef Conly 03175 03184 Z3_ast Z3_API Z3_mk_unsigned_int(Z3_context c, unsigned v, Z3_sort ty); 03185 #endif 03186 03196 Z3_ast Z3_API Z3_mk_int64(Z3_context c, __int64 v, Z3_sort ty); 03197 03198 #ifdef Conly 03199 03208 Z3_ast Z3_API Z3_mk_unsigned_int64(Z3_context c, unsigned __int64 v, Z3_sort ty); 03209 #endif 03210 03217 03237 Z3_pattern Z3_API Z3_mk_pattern( 03238 Z3_context c, 03239 unsigned num_patterns, Z3_ast const terms[]); 03240 03269 Z3_ast Z3_API Z3_mk_bound(Z3_context c, unsigned index, Z3_sort ty); 03270 03303 Z3_ast Z3_API Z3_mk_forall(Z3_context c, unsigned weight, 03304 unsigned num_patterns, Z3_pattern const patterns[], 03305 unsigned num_decls, Z3_sort const sorts[], 03306 Z3_symbol const decl_names[], 03307 Z3_ast body); 03308 03318 Z3_ast Z3_API Z3_mk_exists(Z3_context c, unsigned weight, 03319 unsigned num_patterns, Z3_pattern const patterns[], 03320 unsigned num_decls, Z3_sort const sorts[], 03321 Z3_symbol const decl_names[], 03322 Z3_ast body); 03323 03344 Z3_ast Z3_API Z3_mk_quantifier( 03345 Z3_context c, 03346 Z3_bool is_forall, 03347 unsigned weight, 03348 unsigned num_patterns, Z3_pattern const patterns[], 03349 unsigned num_decls, Z3_sort const sorts[], 03350 Z3_symbol const decl_names[], 03351 Z3_ast body); 03352 03353 03377 Z3_ast Z3_API Z3_mk_quantifier_ex( 03378 Z3_context c, 03379 Z3_bool is_forall, 03380 unsigned weight, 03381 Z3_symbol quantifier_id, 03382 Z3_symbol skolem_id, 03383 unsigned num_patterns, Z3_pattern const patterns[], 03384 unsigned num_no_patterns, Z3_ast const no_patterns[], 03385 unsigned num_decls, Z3_sort const sorts[], 03386 Z3_symbol const decl_names[], 03387 Z3_ast body); 03388 03406 Z3_ast Z3_API Z3_mk_forall_const( 03407 Z3_context c, 03408 unsigned weight, 03409 unsigned num_bound, 03410 Z3_app const bound[], 03411 unsigned num_patterns, 03412 Z3_pattern const patterns[], 03413 Z3_ast body 03414 ); 03415 03435 Z3_ast Z3_API Z3_mk_exists_const( 03436 Z3_context c, 03437 unsigned weight, 03438 unsigned num_bound, 03439 Z3_app const bound[], 03440 unsigned num_patterns, 03441 Z3_pattern const patterns[], 03442 Z3_ast body 03443 ); 03444 03451 Z3_ast Z3_API Z3_mk_quantifier_const( 03452 Z3_context c, 03453 Z3_bool is_forall, 03454 unsigned weight, 03455 unsigned num_bound, Z3_app const bound[], 03456 unsigned num_patterns, Z3_pattern const patterns[], 03457 Z3_ast body 03458 ); 03459 03460 03461 03468 Z3_ast Z3_API Z3_mk_quantifier_const_ex( 03469 Z3_context c, 03470 Z3_bool is_forall, 03471 unsigned weight, 03472 Z3_symbol quantifier_id, 03473 Z3_symbol skolem_id, 03474 unsigned num_bound, Z3_app const bound[], 03475 unsigned num_patterns, Z3_pattern const patterns[], 03476 unsigned num_no_patterns, Z3_ast const no_patterns[], 03477 Z3_ast body 03478 ); 03479 03486 03491 #ifdef ML4only 03492 #include <mlx_symbol_refine.idl> 03493 #endif 03494 03505 Z3_symbol_kind Z3_API Z3_get_symbol_kind(Z3_context c, Z3_symbol s); 03506 03516 int Z3_API Z3_get_symbol_int(Z3_context c, Z3_symbol s); 03517 03531 Z3_string Z3_API Z3_get_symbol_string(Z3_context c, Z3_symbol s); 03532 03533 03538 #ifdef ML4only 03539 #include <mlx_sort_refine.idl> 03540 #endif 03541 03546 Z3_symbol Z3_API Z3_get_sort_name(Z3_context c, Z3_sort d); 03547 03553 unsigned Z3_API Z3_get_sort_id(Z3_context c, Z3_sort s); 03554 03564 Z3_ast Z3_API Z3_sort_to_ast(Z3_context c, Z3_sort s); 03565 03571 Z3_bool Z3_API Z3_is_eq_sort(Z3_context c, Z3_sort s1, Z3_sort s2); 03572 03579 Z3_sort_kind Z3_API Z3_get_sort_kind(Z3_context c, Z3_sort t); 03580 03581 03592 unsigned Z3_API Z3_get_bv_sort_size(Z3_context c, Z3_sort t); 03593 03600 Z3_bool_opt Z3_API Z3_get_finite_domain_sort_size(Z3_context c, Z3_sort s, unsigned __int64* r); 03601 03602 03613 Z3_sort Z3_API Z3_get_array_sort_domain(Z3_context c, Z3_sort t); 03614 03625 Z3_sort Z3_API Z3_get_array_sort_range(Z3_context c, Z3_sort t); 03626 03627 03639 Z3_func_decl Z3_API Z3_get_tuple_sort_mk_decl(Z3_context c, Z3_sort t); 03640 03651 unsigned Z3_API Z3_get_tuple_sort_num_fields(Z3_context c, Z3_sort t); 03652 03665 Z3_func_decl Z3_API Z3_get_tuple_sort_field_decl(Z3_context c, Z3_sort t, unsigned i); 03666 03677 unsigned Z3_API Z3_get_datatype_sort_num_constructors( 03678 Z3_context c, Z3_sort t); 03679 03691 Z3_func_decl Z3_API Z3_get_datatype_sort_constructor( 03692 Z3_context c, Z3_sort t, unsigned idx); 03693 03705 Z3_func_decl Z3_API Z3_get_datatype_sort_recognizer( 03706 Z3_context c, Z3_sort t, unsigned idx); 03707 03720 Z3_func_decl Z3_API Z3_get_datatype_sort_constructor_accessor( 03721 Z3_context c, Z3_sort t, unsigned idx_c, unsigned idx_a); 03722 03741 Z3_ast Z3_API Z3_datatype_update_field( 03742 Z3_context c, Z3_func_decl field_access, 03743 Z3_ast t, Z3_ast value); 03744 03753 unsigned Z3_API Z3_get_relation_arity(Z3_context c, Z3_sort s); 03754 03764 Z3_sort Z3_API Z3_get_relation_column(Z3_context c, Z3_sort s, unsigned col); 03765 03766 03774 Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args, 03775 Z3_ast const args[], unsigned k); 03776 03784 Z3_ast Z3_API Z3_mk_pble(Z3_context c, unsigned num_args, 03785 Z3_ast const args[], int coeffs[], 03786 int k); 03787 03797 Z3_ast Z3_API Z3_func_decl_to_ast(Z3_context c, Z3_func_decl f); 03798 03804 Z3_bool Z3_API Z3_is_eq_func_decl(Z3_context c, Z3_func_decl f1, Z3_func_decl f2); 03805 03811 unsigned Z3_API Z3_get_func_decl_id(Z3_context c, Z3_func_decl f); 03812 03817 Z3_symbol Z3_API Z3_get_decl_name(Z3_context c, Z3_func_decl d); 03818 03823 Z3_decl_kind Z3_API Z3_get_decl_kind(Z3_context c, Z3_func_decl d); 03824 03831 unsigned Z3_API Z3_get_domain_size(Z3_context c, Z3_func_decl d); 03832 03839 unsigned Z3_API Z3_get_arity(Z3_context c, Z3_func_decl d); 03840 03850 Z3_sort Z3_API Z3_get_domain(Z3_context c, Z3_func_decl d, unsigned i); 03851 03852 #ifdef ML4only 03853 #include <mlx_get_domains.idl> 03854 #endif 03855 03864 Z3_sort Z3_API Z3_get_range(Z3_context c, Z3_func_decl d); 03865 03870 unsigned Z3_API Z3_get_decl_num_parameters(Z3_context c, Z3_func_decl d); 03871 03880 Z3_parameter_kind Z3_API Z3_get_decl_parameter_kind(Z3_context c, Z3_func_decl d, unsigned idx); 03881 03888 int Z3_API Z3_get_decl_int_parameter(Z3_context c, Z3_func_decl d, unsigned idx); 03889 03896 double Z3_API Z3_get_decl_double_parameter(Z3_context c, Z3_func_decl d, unsigned idx); 03897 03904 Z3_symbol Z3_API Z3_get_decl_symbol_parameter(Z3_context c, Z3_func_decl d, unsigned idx); 03905 03912 Z3_sort Z3_API Z3_get_decl_sort_parameter(Z3_context c, Z3_func_decl d, unsigned idx); 03913 03920 Z3_ast Z3_API Z3_get_decl_ast_parameter(Z3_context c, Z3_func_decl d, unsigned idx); 03921 03928 Z3_func_decl Z3_API Z3_get_decl_func_decl_parameter(Z3_context c, Z3_func_decl d, unsigned idx); 03929 03936 Z3_string Z3_API Z3_get_decl_rational_parameter(Z3_context c, Z3_func_decl d, unsigned idx); 03937 03947 Z3_ast Z3_API Z3_app_to_ast(Z3_context c, Z3_app a); 03948 03953 Z3_func_decl Z3_API Z3_get_app_decl(Z3_context c, Z3_app a); 03954 03961 unsigned Z3_API Z3_get_app_num_args(Z3_context c, Z3_app a); 03962 03970 Z3_ast Z3_API Z3_get_app_arg(Z3_context c, Z3_app a, unsigned i); 03971 03972 #ifdef ML4only 03973 #include <mlx_get_app_args.idl> 03974 #endif 03975 03976 03981 #ifdef ML4only 03982 #include <mlx_term_refine.idl> 03983 #endif 03984 03990 Z3_bool Z3_API Z3_is_eq_ast(Z3_context c, Z3_ast t1, Z3_ast t2); 03991 04003 unsigned Z3_API Z3_get_ast_id(Z3_context c, Z3_ast t); 04004 04012 unsigned Z3_API Z3_get_ast_hash(Z3_context c, Z3_ast a); 04013 04020 Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a); 04021 04026 Z3_bool Z3_API Z3_is_well_sorted(Z3_context c, Z3_ast t); 04027 04032 Z3_lbool Z3_API Z3_get_bool_value(Z3_context c, Z3_ast a); 04033 04038 Z3_ast_kind Z3_API Z3_get_ast_kind(Z3_context c, Z3_ast a); 04039 04042 Z3_bool Z3_API Z3_is_app(Z3_context c, Z3_ast a); 04043 04046 Z3_bool Z3_API Z3_is_numeral_ast(Z3_context c, Z3_ast a); 04047 04052 Z3_bool Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a); 04053 04060 Z3_app Z3_API Z3_to_app(Z3_context c, Z3_ast a); 04061 04068 Z3_func_decl Z3_API Z3_to_func_decl(Z3_context c, Z3_ast a); 04069 04070 04075 #ifdef ML4only 04076 #include <mlx_numeral_refine.idl> 04077 #endif 04078 04089 Z3_string Z3_API Z3_get_numeral_string(Z3_context c, Z3_ast a); 04090 04098 Z3_string Z3_API Z3_get_numeral_decimal_string(Z3_context c, Z3_ast a, unsigned precision); 04099 04106 Z3_ast Z3_API Z3_get_numerator(Z3_context c, Z3_ast a); 04107 04114 Z3_ast Z3_API Z3_get_denominator(Z3_context c, Z3_ast a); 04115 04129 Z3_bool Z3_API Z3_get_numeral_small(Z3_context c, Z3_ast a, __int64* num, __int64* den); 04130 04141 Z3_bool Z3_API Z3_get_numeral_int(Z3_context c, Z3_ast v, int* i); 04142 04143 #ifdef Conly 04144 04154 Z3_bool Z3_API Z3_get_numeral_uint(Z3_context c, Z3_ast v, unsigned* u); 04155 #endif 04156 04157 #ifdef Conly 04158 04168 Z3_bool Z3_API Z3_get_numeral_uint64(Z3_context c, Z3_ast v, unsigned __int64* u); 04169 #endif 04170 04181 Z3_bool Z3_API Z3_get_numeral_int64(Z3_context c, Z3_ast v, __int64* i); 04182 04193 Z3_bool Z3_API Z3_get_numeral_rational_int64(Z3_context c, Z3_ast v, __int64* num, __int64* den); 04194 04203 Z3_ast Z3_API Z3_get_algebraic_number_lower(Z3_context c, Z3_ast a, unsigned precision); 04204 04213 Z3_ast Z3_API Z3_get_algebraic_number_upper(Z3_context c, Z3_ast a, unsigned precision); 04214 04215 04225 Z3_ast Z3_API Z3_pattern_to_ast(Z3_context c, Z3_pattern p); 04226 04227 #ifdef ML4only 04228 #include <mlx_get_pattern_terms.idl> 04229 #endif 04230 04235 unsigned Z3_API Z3_get_pattern_num_terms(Z3_context c, Z3_pattern p); 04236 04241 Z3_ast Z3_API Z3_get_pattern(Z3_context c, Z3_pattern p, unsigned idx); 04242 04243 04254 unsigned Z3_API Z3_get_index_value(Z3_context c, Z3_ast a); 04255 04262 Z3_bool Z3_API Z3_is_quantifier_forall(Z3_context c, Z3_ast a); 04263 04270 unsigned Z3_API Z3_get_quantifier_weight(Z3_context c, Z3_ast a); 04271 04278 unsigned Z3_API Z3_get_quantifier_num_patterns(Z3_context c, Z3_ast a); 04279 04286 Z3_pattern Z3_API Z3_get_quantifier_pattern_ast(Z3_context c, Z3_ast a, unsigned i); 04287 04294 unsigned Z3_API Z3_get_quantifier_num_no_patterns(Z3_context c, Z3_ast a); 04295 04302 Z3_ast Z3_API Z3_get_quantifier_no_pattern_ast(Z3_context c, Z3_ast a, unsigned i); 04303 04310 unsigned Z3_API Z3_get_quantifier_num_bound(Z3_context c, Z3_ast a); 04311 04318 Z3_symbol Z3_API Z3_get_quantifier_bound_name(Z3_context c, Z3_ast a, unsigned i); 04319 04326 Z3_sort Z3_API Z3_get_quantifier_bound_sort(Z3_context c, Z3_ast a, unsigned i); 04327 04334 Z3_ast Z3_API Z3_get_quantifier_body(Z3_context c, Z3_ast a); 04335 04336 04347 Z3_ast Z3_API Z3_simplify(Z3_context c, Z3_ast a); 04348 04349 #ifdef CorML4 04350 04358 Z3_ast Z3_API Z3_simplify_ex(Z3_context c, Z3_ast a, Z3_params p); 04359 04364 Z3_string Z3_API Z3_simplify_get_help(Z3_context c); 04365 04370 Z3_param_descrs Z3_API Z3_simplify_get_param_descrs(Z3_context c); 04371 #endif 04372 04379 04387 Z3_ast Z3_API Z3_update_term(Z3_context c, Z3_ast a, unsigned num_args, Z3_ast const args[]); 04388 04395 Z3_ast Z3_API Z3_substitute(Z3_context c, 04396 Z3_ast a, 04397 unsigned num_exprs, 04398 Z3_ast const from[], 04399 Z3_ast const to[]); 04400 04406 Z3_ast Z3_API Z3_substitute_vars(Z3_context c, 04407 Z3_ast a, 04408 unsigned num_exprs, 04409 Z3_ast const to[]); 04410 04411 #ifdef CorML4 04412 04418 Z3_ast Z3_API Z3_translate(Z3_context source, Z3_ast a, Z3_context target); 04419 #endif 04420 04423 #ifdef CorML4 04424 04428 04429 #ifdef ML4only 04430 #include <mlx_model.idl> 04431 #endif 04432 #ifdef Conly 04433 04437 void Z3_API Z3_model_inc_ref(Z3_context c, Z3_model m); 04438 04443 void Z3_API Z3_model_dec_ref(Z3_context c, Z3_model m); 04444 #endif 04445 04465 Z3_bool_opt Z3_API Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, Z3_bool model_completion, Z3_ast * v); 04466 04480 Z3_ast_opt Z3_API Z3_model_get_const_interp(Z3_context c, Z3_model m, Z3_func_decl a); 04481 04486 Z3_bool Z3_API Z3_model_has_interp(Z3_context c, Z3_model m, Z3_func_decl a); 04487 04500 Z3_func_interp_opt Z3_API Z3_model_get_func_interp(Z3_context c, Z3_model m, Z3_func_decl f); 04501 04508 unsigned Z3_API Z3_model_get_num_consts(Z3_context c, Z3_model m); 04509 04519 Z3_func_decl Z3_API Z3_model_get_const_decl(Z3_context c, Z3_model m, unsigned i); 04520 04528 unsigned Z3_API Z3_model_get_num_funcs(Z3_context c, Z3_model m); 04529 04539 Z3_func_decl Z3_API Z3_model_get_func_decl(Z3_context c, Z3_model m, unsigned i); 04540 04552 unsigned Z3_API Z3_model_get_num_sorts(Z3_context c, Z3_model m); 04553 04563 Z3_sort Z3_API Z3_model_get_sort(Z3_context c, Z3_model m, unsigned i); 04564 04572 Z3_ast_vector Z3_API Z3_model_get_sort_universe(Z3_context c, Z3_model m, Z3_sort s); 04573 04584 Z3_bool Z3_API Z3_is_as_array(Z3_context c, Z3_ast a); 04585 04592 Z3_func_decl Z3_API Z3_get_as_array_func_decl(Z3_context c, Z3_ast a); 04593 04594 #ifdef Conly 04595 04599 void Z3_API Z3_func_interp_inc_ref(Z3_context c, Z3_func_interp f); 04600 04605 void Z3_API Z3_func_interp_dec_ref(Z3_context c, Z3_func_interp f); 04606 #endif 04607 04616 unsigned Z3_API Z3_func_interp_get_num_entries(Z3_context c, Z3_func_interp f); 04617 04627 Z3_func_entry Z3_API Z3_func_interp_get_entry(Z3_context c, Z3_func_interp f, unsigned i); 04628 04636 Z3_ast Z3_API Z3_func_interp_get_else(Z3_context c, Z3_func_interp f); 04637 04642 unsigned Z3_API Z3_func_interp_get_arity(Z3_context c, Z3_func_interp f); 04643 04644 #ifdef Conly 04645 04649 void Z3_API Z3_func_entry_inc_ref(Z3_context c, Z3_func_entry e); 04650 04655 void Z3_API Z3_func_entry_dec_ref(Z3_context c, Z3_func_entry e); 04656 #endif 04657 04667 Z3_ast Z3_API Z3_func_entry_get_value(Z3_context c, Z3_func_entry e); 04668 04675 unsigned Z3_API Z3_func_entry_get_num_args(Z3_context c, Z3_func_entry e); 04676 04685 Z3_ast Z3_API Z3_func_entry_get_arg(Z3_context c, Z3_func_entry e, unsigned i); 04686 04688 #endif // CorML4 04689 04694 04699 Z3_bool Z3_API Z3_open_log(Z3_string filename); 04700 04709 void Z3_API Z3_append_log(Z3_string string); 04710 04715 void Z3_API Z3_close_log(void); 04716 04724 void Z3_API Z3_toggle_warning_messages(Z3_bool enabled); 04725 04732 04749 void Z3_API Z3_set_ast_print_mode(Z3_context c, Z3_ast_print_mode mode); 04750 04761 Z3_string Z3_API Z3_ast_to_string(Z3_context c, Z3_ast a); 04762 04765 Z3_string Z3_API Z3_pattern_to_string(Z3_context c, Z3_pattern p); 04766 04769 Z3_string Z3_API Z3_sort_to_string(Z3_context c, Z3_sort s); 04770 04773 Z3_string Z3_API Z3_func_decl_to_string(Z3_context c, Z3_func_decl d); 04774 04783 Z3_string Z3_API Z3_model_to_string(Z3_context c, Z3_model m); 04784 04802 Z3_string Z3_API Z3_benchmark_to_smtlib_string(Z3_context c, 04803 Z3_string name, 04804 Z3_string logic, 04805 Z3_string status, 04806 Z3_string attributes, 04807 unsigned num_assumptions, 04808 Z3_ast const assumptions[], 04809 Z3_ast formula); 04810 04817 04826 Z3_ast Z3_API Z3_parse_smtlib2_string(Z3_context c, 04827 Z3_string str, 04828 unsigned num_sorts, 04829 Z3_symbol const sort_names[], 04830 Z3_sort const sorts[], 04831 unsigned num_decls, 04832 Z3_symbol const decl_names[], 04833 Z3_func_decl const decls[]); 04834 04839 Z3_ast Z3_API Z3_parse_smtlib2_file(Z3_context c, 04840 Z3_string file_name, 04841 unsigned num_sorts, 04842 Z3_symbol const sort_names[], 04843 Z3_sort const sorts[], 04844 unsigned num_decls, 04845 Z3_symbol const decl_names[], 04846 Z3_func_decl const decls[]); 04847 04848 #ifdef ML4only 04849 #include <mlx_parse_smtlib.idl> 04850 #endif 04851 04870 void Z3_API Z3_parse_smtlib_string(Z3_context c, 04871 Z3_string str, 04872 unsigned num_sorts, 04873 Z3_symbol const sort_names[], 04874 Z3_sort const sorts[], 04875 unsigned num_decls, 04876 Z3_symbol const decl_names[], 04877 Z3_func_decl const decls[] 04878 ); 04879 04884 void Z3_API Z3_parse_smtlib_file(Z3_context c, 04885 Z3_string file_name, 04886 unsigned num_sorts, 04887 Z3_symbol const sort_names[], 04888 Z3_sort const sorts[], 04889 unsigned num_decls, 04890 Z3_symbol const decl_names[], 04891 Z3_func_decl const decls[] 04892 ); 04893 04898 unsigned Z3_API Z3_get_smtlib_num_formulas(Z3_context c); 04899 04907 Z3_ast Z3_API Z3_get_smtlib_formula(Z3_context c, unsigned i); 04908 04913 unsigned Z3_API Z3_get_smtlib_num_assumptions(Z3_context c); 04914 04922 Z3_ast Z3_API Z3_get_smtlib_assumption(Z3_context c, unsigned i); 04923 04928 unsigned Z3_API Z3_get_smtlib_num_decls(Z3_context c); 04929 04937 Z3_func_decl Z3_API Z3_get_smtlib_decl(Z3_context c, unsigned i); 04938 04943 unsigned Z3_API Z3_get_smtlib_num_sorts(Z3_context c); 04944 04952 Z3_sort Z3_API Z3_get_smtlib_sort(Z3_context c, unsigned i); 04953 04954 BEGIN_MLAPI_EXCLUDE 04960 Z3_string Z3_API Z3_get_smtlib_error(Z3_context c); 04961 END_MLAPI_EXCLUDE 04962 04965 #ifdef CorML4 04966 04970 04971 #ifndef SAFE_ERRORS 04972 04981 Z3_error_code Z3_API Z3_get_error_code(Z3_context c); 04982 04995 void Z3_API Z3_set_error_handler(Z3_context c, Z3_error_handler h); 04996 #endif 04997 05002 void Z3_API Z3_set_error(Z3_context c, Z3_error_code e); 05003 05004 #ifdef Conly 05005 05011 Z3_string Z3_API Z3_get_error_msg(Z3_error_code err); 05012 #endif 05013 05014 BEGIN_MLAPI_EXCLUDE 05019 Z3_string Z3_API Z3_get_error_msg_ex(Z3_context c, Z3_error_code err); 05020 END_MLAPI_EXCLUDE 05021 #ifdef ML4only 05022 #include <mlx_get_error_msg.idl> 05023 #endif 05024 05025 05027 #endif 05028 05033 05038 void Z3_API Z3_get_version(unsigned * major, unsigned * minor, unsigned * build_number, unsigned * revision_number); 05039 05045 void Z3_API Z3_enable_trace(Z3_string tag); 05046 05052 void Z3_API Z3_disable_trace(Z3_string tag); 05053 05054 #ifdef CorML3 05055 05064 void Z3_API Z3_reset_memory(void); 05065 #endif 05066 05067 #ifdef CorML3 05068 05075 void Z3_API Z3_finalize_memory(void); 05076 #endif 05077 05080 #ifdef CorML3 05081 05085 05086 #ifdef Conly 05087 05088 // 05089 // callbacks and void* don't work with CAMLIDL. 05090 // 05091 typedef Z3_bool Z3_reduce_eq_callback_fptr(Z3_theory t, Z3_ast a, Z3_ast b, Z3_ast * r); 05092 05093 typedef Z3_bool Z3_reduce_app_callback_fptr(Z3_theory, Z3_func_decl, unsigned, Z3_ast const [], Z3_ast *); 05094 05095 typedef Z3_bool Z3_reduce_distinct_callback_fptr(Z3_theory, unsigned, Z3_ast const [], Z3_ast *); 05096 05097 typedef void Z3_theory_callback_fptr(Z3_theory t); 05098 05099 typedef Z3_bool Z3_theory_final_check_callback_fptr(Z3_theory); 05100 05101 typedef void Z3_theory_ast_callback_fptr(Z3_theory, Z3_ast); 05102 05103 typedef void Z3_theory_ast_bool_callback_fptr(Z3_theory, Z3_ast, Z3_bool); 05104 05105 typedef void Z3_theory_ast_ast_callback_fptr(Z3_theory, Z3_ast, Z3_ast); 05106 05107 #endif 05108 05109 #ifdef Conly 05110 05118 Z3_theory Z3_API Z3_mk_theory(Z3_context c, Z3_string th_name, Z3_theory_data data); 05119 05125 Z3_theory_data Z3_API Z3_theory_get_ext_data(Z3_theory t); 05126 #endif 05127 05131 Z3_sort Z3_API Z3_theory_mk_sort(Z3_context c, Z3_theory t, Z3_symbol s); 05132 05136 Z3_ast Z3_API Z3_theory_mk_value(Z3_context c, Z3_theory t, Z3_symbol n, Z3_sort s); 05137 05141 Z3_ast Z3_API Z3_theory_mk_constant(Z3_context c, Z3_theory t, Z3_symbol n, Z3_sort s); 05142 05146 Z3_func_decl Z3_API Z3_theory_mk_func_decl(Z3_context c, Z3_theory t, Z3_symbol n, 05147 unsigned domain_size, Z3_sort const domain[], 05148 Z3_sort range); 05149 05153 Z3_context Z3_API Z3_theory_get_context(Z3_theory t); 05154 05155 05156 #ifdef Conly 05157 05167 void Z3_API Z3_set_delete_callback(Z3_theory t, Z3_theory_callback_fptr f); 05168 05182 void Z3_API Z3_set_reduce_app_callback(Z3_theory t, Z3_reduce_app_callback_fptr f); 05183 05197 void Z3_API Z3_set_reduce_eq_callback(Z3_theory t, Z3_reduce_eq_callback_fptr f); 05198 05212 void Z3_API Z3_set_reduce_distinct_callback(Z3_theory t, Z3_reduce_distinct_callback_fptr f); 05213 05229 void Z3_API Z3_set_new_app_callback(Z3_theory t, Z3_theory_ast_callback_fptr f); 05230 05247 void Z3_API Z3_set_new_elem_callback(Z3_theory t, Z3_theory_ast_callback_fptr f); 05248 05256 void Z3_API Z3_set_init_search_callback(Z3_theory t, Z3_theory_callback_fptr f); 05257 05267 void Z3_API Z3_set_push_callback(Z3_theory t, Z3_theory_callback_fptr f); 05268 05278 void Z3_API Z3_set_pop_callback(Z3_theory t, Z3_theory_callback_fptr f); 05279 05287 void Z3_API Z3_set_restart_callback(Z3_theory t, Z3_theory_callback_fptr f); 05288 05297 void Z3_API Z3_set_reset_callback(Z3_theory t, Z3_theory_callback_fptr f); 05298 05311 void Z3_API Z3_set_final_check_callback(Z3_theory t, Z3_theory_final_check_callback_fptr f); 05312 05322 void Z3_API Z3_set_new_eq_callback(Z3_theory t, Z3_theory_ast_ast_callback_fptr f); 05323 05333 void Z3_API Z3_set_new_diseq_callback(Z3_theory t, Z3_theory_ast_ast_callback_fptr f); 05334 05343 void Z3_API Z3_set_new_assignment_callback(Z3_theory t, Z3_theory_ast_bool_callback_fptr f); 05344 05354 void Z3_API Z3_set_new_relevant_callback(Z3_theory t, Z3_theory_ast_callback_fptr f); 05355 05356 #endif 05357 05372 void Z3_API Z3_theory_assert_axiom(Z3_theory t, Z3_ast ax); 05373 05381 void Z3_API Z3_theory_assume_eq(Z3_theory t, Z3_ast lhs, Z3_ast rhs); 05382 05389 void Z3_API Z3_theory_enable_axiom_simplification(Z3_theory t, Z3_bool flag); 05390 05394 Z3_ast Z3_API Z3_theory_get_eqc_root(Z3_theory t, Z3_ast n); 05395 05410 Z3_ast Z3_API Z3_theory_get_eqc_next(Z3_theory t, Z3_ast n); 05411 05415 unsigned Z3_API Z3_theory_get_num_parents(Z3_theory t, Z3_ast n); 05416 05421 Z3_ast Z3_API Z3_theory_get_parent(Z3_theory t, Z3_ast n, unsigned i); 05422 05426 Z3_bool Z3_API Z3_theory_is_value(Z3_theory t, Z3_ast n); 05427 05431 Z3_bool Z3_API Z3_theory_is_decl(Z3_theory t, Z3_func_decl d); 05432 05438 unsigned Z3_API Z3_theory_get_num_elems(Z3_theory t); 05439 05445 Z3_ast Z3_API Z3_theory_get_elem(Z3_theory t, unsigned i); 05446 05452 unsigned Z3_API Z3_theory_get_num_apps(Z3_theory t); 05453 05459 Z3_ast Z3_API Z3_theory_get_app(Z3_theory t, unsigned i); 05460 05463 #endif 05464 05465 #ifdef CorML4 05466 05470 05478 Z3_fixedpoint Z3_API Z3_mk_fixedpoint(Z3_context c); 05479 05480 #ifdef Conly 05481 05485 void Z3_API Z3_fixedpoint_inc_ref(Z3_context c,Z3_fixedpoint d); 05486 05491 void Z3_API Z3_fixedpoint_dec_ref(Z3_context c,Z3_fixedpoint d); 05492 #endif 05493 05505 void Z3_API Z3_fixedpoint_add_rule(Z3_context c,Z3_fixedpoint d, Z3_ast rule, Z3_symbol name); 05506 05523 void Z3_API Z3_fixedpoint_add_fact(Z3_context c,Z3_fixedpoint d, 05524 Z3_func_decl r, 05525 unsigned num_args, unsigned args[]); 05526 05534 void Z3_API Z3_fixedpoint_assert(Z3_context c,Z3_fixedpoint d, Z3_ast axiom); 05535 05550 Z3_lbool Z3_API Z3_fixedpoint_query(Z3_context c,Z3_fixedpoint d, Z3_ast query); 05551 05563 Z3_lbool Z3_API Z3_fixedpoint_query_relations( 05564 Z3_context c,Z3_fixedpoint d, 05565 unsigned num_relations, Z3_func_decl const relations[]); 05566 05579 Z3_ast Z3_API Z3_fixedpoint_get_answer(Z3_context c,Z3_fixedpoint d); 05580 05587 Z3_string Z3_API Z3_fixedpoint_get_reason_unknown(Z3_context c,Z3_fixedpoint d); 05588 05594 void Z3_API Z3_fixedpoint_update_rule(Z3_context c, Z3_fixedpoint d, Z3_ast a, Z3_symbol name); 05595 05604 unsigned Z3_API Z3_fixedpoint_get_num_levels(Z3_context c, Z3_fixedpoint d, Z3_func_decl pred); 05605 05615 Z3_ast Z3_API Z3_fixedpoint_get_cover_delta(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred); 05616 05628 void Z3_API Z3_fixedpoint_add_cover(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred, Z3_ast property); 05629 05634 Z3_stats Z3_API Z3_fixedpoint_get_statistics(Z3_context c,Z3_fixedpoint d); 05635 05643 void Z3_API Z3_fixedpoint_register_relation(Z3_context c,Z3_fixedpoint d, Z3_func_decl f); 05644 05653 void Z3_API Z3_fixedpoint_set_predicate_representation( 05654 Z3_context c, 05655 Z3_fixedpoint d, 05656 Z3_func_decl f, 05657 unsigned num_relations, 05658 Z3_symbol const relation_kinds[]); 05659 05664 Z3_ast_vector Z3_API Z3_fixedpoint_get_rules( 05665 Z3_context c, 05666 Z3_fixedpoint f); 05667 05672 Z3_ast_vector Z3_API Z3_fixedpoint_get_assertions( 05673 Z3_context c, 05674 Z3_fixedpoint f); 05675 05680 void Z3_API Z3_fixedpoint_set_params(Z3_context c, Z3_fixedpoint f, Z3_params p); 05681 05686 Z3_string Z3_API Z3_fixedpoint_get_help(Z3_context c, Z3_fixedpoint f); 05687 05692 Z3_param_descrs Z3_API Z3_fixedpoint_get_param_descrs(Z3_context c, Z3_fixedpoint f); 05693 05702 Z3_string Z3_API Z3_fixedpoint_to_string( 05703 Z3_context c, 05704 Z3_fixedpoint f, 05705 unsigned num_queries, 05706 Z3_ast queries[]); 05707 05718 Z3_ast_vector Z3_API Z3_fixedpoint_from_string( 05719 Z3_context c, 05720 Z3_fixedpoint f, 05721 Z3_string s); 05722 05733 Z3_ast_vector Z3_API Z3_fixedpoint_from_file( 05734 Z3_context c, 05735 Z3_fixedpoint f, 05736 Z3_string s); 05737 05747 void Z3_API Z3_fixedpoint_push(Z3_context c,Z3_fixedpoint d); 05748 05757 void Z3_API Z3_fixedpoint_pop(Z3_context c,Z3_fixedpoint d); 05758 05759 #ifdef Conly 05760 05765 typedef void Z3_fixedpoint_reduce_assign_callback_fptr( 05766 void*, Z3_func_decl, 05767 unsigned, Z3_ast const [], 05768 unsigned, Z3_ast const []); 05769 05770 typedef void Z3_fixedpoint_reduce_app_callback_fptr( 05771 void*, Z3_func_decl, 05772 unsigned, Z3_ast const [], 05773 Z3_ast*); 05774 05775 05779 void Z3_API Z3_fixedpoint_init(Z3_context c,Z3_fixedpoint d, void* state); 05780 05786 void Z3_API Z3_fixedpoint_set_reduce_assign_callback( 05787 Z3_context c,Z3_fixedpoint d, Z3_fixedpoint_reduce_assign_callback_fptr cb); 05788 05793 void Z3_API Z3_fixedpoint_set_reduce_app_callback( 05794 Z3_context c,Z3_fixedpoint d, Z3_fixedpoint_reduce_app_callback_fptr cb); 05795 05796 #endif 05797 #endif 05798 05799 05800 05801 #ifdef CorML4 05802 05806 05814 Z3_optimize Z3_API Z3_mk_optimize(Z3_context c); 05815 05816 #ifdef Conly 05817 05821 void Z3_API Z3_optimize_inc_ref(Z3_context c,Z3_optimize d); 05822 05827 void Z3_API Z3_optimize_dec_ref(Z3_context c,Z3_optimize d); 05828 #endif 05829 05834 void Z3_API Z3_optimize_assert(Z3_context c, Z3_optimize o, Z3_ast a); 05835 05836 05846 unsigned Z3_API Z3_optimize_assert_soft(Z3_context c, Z3_optimize o, Z3_ast a, Z3_string weight, Z3_symbol id); 05847 05848 05855 unsigned Z3_API Z3_optimize_maximize(Z3_context c, Z3_optimize o, Z3_ast t); 05856 05864 unsigned Z3_API Z3_optimize_minimize(Z3_context c, Z3_optimize o, Z3_ast t); 05865 05866 05876 void Z3_API Z3_optimize_push(Z3_context c,Z3_optimize d); 05877 05886 void Z3_API Z3_optimize_pop(Z3_context c,Z3_optimize d); 05887 05894 Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o); 05895 05896 05903 Z3_string Z3_API Z3_optimize_get_reason_unknown(Z3_context c,Z3_optimize d); 05904 05913 Z3_model Z3_API Z3_optimize_get_model(Z3_context c, Z3_optimize o); 05914 05923 void Z3_API Z3_optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p); 05924 05932 Z3_param_descrs Z3_API Z3_optimize_get_param_descrs(Z3_context c, Z3_optimize o); 05933 05942 Z3_ast Z3_API Z3_optimize_get_lower(Z3_context c, Z3_optimize o, unsigned idx); 05943 05952 Z3_ast Z3_API Z3_optimize_get_upper(Z3_context c, Z3_optimize o, unsigned idx); 05953 05960 Z3_string Z3_API Z3_optimize_to_string( 05961 Z3_context c, 05962 Z3_optimize o); 05963 05964 05969 Z3_string Z3_API Z3_optimize_get_help(Z3_context c, Z3_optimize t); 05970 05975 Z3_stats Z3_API Z3_optimize_get_statistics(Z3_context c,Z3_optimize d); 05976 05977 05978 #endif 05979 05980 #ifdef CorML4 05981 05987 05995 Z3_ast_vector Z3_API Z3_mk_ast_vector(Z3_context c); 05996 05997 #ifdef Conly 05998 06002 void Z3_API Z3_ast_vector_inc_ref(Z3_context c, Z3_ast_vector v); 06003 06008 void Z3_API Z3_ast_vector_dec_ref(Z3_context c, Z3_ast_vector v); 06009 #endif 06010 06015 unsigned Z3_API Z3_ast_vector_size(Z3_context c, Z3_ast_vector v); 06016 06023 Z3_ast Z3_API Z3_ast_vector_get(Z3_context c, Z3_ast_vector v, unsigned i); 06024 06031 void Z3_API Z3_ast_vector_set(Z3_context c, Z3_ast_vector v, unsigned i, Z3_ast a); 06032 06037 void Z3_API Z3_ast_vector_resize(Z3_context c, Z3_ast_vector v, unsigned n); 06038 06043 void Z3_API Z3_ast_vector_push(Z3_context c, Z3_ast_vector v, Z3_ast a); 06044 06049 Z3_ast_vector Z3_API Z3_ast_vector_translate(Z3_context s, Z3_ast_vector v, Z3_context t); 06050 06055 Z3_string Z3_API Z3_ast_vector_to_string(Z3_context c, Z3_ast_vector v); 06056 06063 06071 Z3_ast_map Z3_API Z3_mk_ast_map(Z3_context c); 06072 06073 #ifdef Conly 06074 06078 void Z3_API Z3_ast_map_inc_ref(Z3_context c, Z3_ast_map m); 06079 06084 void Z3_API Z3_ast_map_dec_ref(Z3_context c, Z3_ast_map m); 06085 #endif 06086 06091 Z3_bool Z3_API Z3_ast_map_contains(Z3_context c, Z3_ast_map m, Z3_ast k); 06092 06099 Z3_ast Z3_API Z3_ast_map_find(Z3_context c, Z3_ast_map m, Z3_ast k); 06100 06105 void Z3_API Z3_ast_map_insert(Z3_context c, Z3_ast_map m, Z3_ast k, Z3_ast v); 06106 06111 void Z3_API Z3_ast_map_erase(Z3_context c, Z3_ast_map m, Z3_ast k); 06112 06117 void Z3_API Z3_ast_map_reset(Z3_context c, Z3_ast_map m); 06118 06123 unsigned Z3_API Z3_ast_map_size(Z3_context c, Z3_ast_map m); 06124 06129 Z3_ast_vector Z3_API Z3_ast_map_keys(Z3_context c, Z3_ast_map m); 06130 06135 Z3_string Z3_API Z3_ast_map_to_string(Z3_context c, Z3_ast_map m); 06136 06143 06160 Z3_goal Z3_API Z3_mk_goal(Z3_context c, Z3_bool models, Z3_bool unsat_cores, Z3_bool proofs); 06161 06162 #ifdef Conly 06163 06167 void Z3_API Z3_goal_inc_ref(Z3_context c, Z3_goal g); 06168 06173 void Z3_API Z3_goal_dec_ref(Z3_context c, Z3_goal g); 06174 #endif 06175 06182 Z3_goal_prec Z3_API Z3_goal_precision(Z3_context c, Z3_goal g); 06183 06188 void Z3_API Z3_goal_assert(Z3_context c, Z3_goal g, Z3_ast a); 06189 06194 Z3_bool Z3_API Z3_goal_inconsistent(Z3_context c, Z3_goal g); 06195 06200 unsigned Z3_API Z3_goal_depth(Z3_context c, Z3_goal g); 06201 06206 void Z3_API Z3_goal_reset(Z3_context c, Z3_goal g); 06207 06212 unsigned Z3_API Z3_goal_size(Z3_context c, Z3_goal g); 06213 06220 Z3_ast Z3_API Z3_goal_formula(Z3_context c, Z3_goal g, unsigned idx); 06221 06226 unsigned Z3_API Z3_goal_num_exprs(Z3_context c, Z3_goal g); 06227 06232 Z3_bool Z3_API Z3_goal_is_decided_sat(Z3_context c, Z3_goal g); 06233 06238 Z3_bool Z3_API Z3_goal_is_decided_unsat(Z3_context c, Z3_goal g); 06239 06244 Z3_goal Z3_API Z3_goal_translate(Z3_context source, Z3_goal g, Z3_context target); 06245 06250 Z3_string Z3_API Z3_goal_to_string(Z3_context c, Z3_goal g); 06251 06258 06267 Z3_tactic Z3_API Z3_mk_tactic(Z3_context c, Z3_string name); 06268 06269 #ifdef Conly 06270 06274 void Z3_API Z3_tactic_inc_ref(Z3_context c, Z3_tactic t); 06275 06280 void Z3_API Z3_tactic_dec_ref(Z3_context c, Z3_tactic g); 06281 #endif 06282 06292 Z3_probe Z3_API Z3_mk_probe(Z3_context c, Z3_string name); 06293 06294 #ifdef Conly 06295 06299 void Z3_API Z3_probe_inc_ref(Z3_context c, Z3_probe p); 06300 06305 void Z3_API Z3_probe_dec_ref(Z3_context c, Z3_probe p); 06306 #endif 06307 06313 Z3_tactic Z3_API Z3_tactic_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2); 06314 06320 Z3_tactic Z3_API Z3_tactic_or_else(Z3_context c, Z3_tactic t1, Z3_tactic t2); 06321 06326 Z3_tactic Z3_API Z3_tactic_par_or(Z3_context c, unsigned num, Z3_tactic const ts[]); 06327 06333 Z3_tactic Z3_API Z3_tactic_par_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2); 06334 06340 Z3_tactic Z3_API Z3_tactic_try_for(Z3_context c, Z3_tactic t, unsigned ms); 06341 06347 Z3_tactic Z3_API Z3_tactic_when(Z3_context c, Z3_probe p, Z3_tactic t); 06348 06354 Z3_tactic Z3_API Z3_tactic_cond(Z3_context c, Z3_probe p, Z3_tactic t1, Z3_tactic t2); 06355 06361 Z3_tactic Z3_API Z3_tactic_repeat(Z3_context c, Z3_tactic t, unsigned max); 06362 06367 Z3_tactic Z3_API Z3_tactic_skip(Z3_context c); 06368 06373 Z3_tactic Z3_API Z3_tactic_fail(Z3_context c); 06374 06379 Z3_tactic Z3_API Z3_tactic_fail_if(Z3_context c, Z3_probe p); 06380 06386 Z3_tactic Z3_API Z3_tactic_fail_if_not_decided(Z3_context c); 06387 06392 Z3_tactic Z3_API Z3_tactic_using_params(Z3_context c, Z3_tactic t, Z3_params p); 06393 06398 Z3_probe Z3_API Z3_probe_const(Z3_context x, double val); 06399 06406 Z3_probe Z3_API Z3_probe_lt(Z3_context x, Z3_probe p1, Z3_probe p2); 06407 06414 Z3_probe Z3_API Z3_probe_gt(Z3_context x, Z3_probe p1, Z3_probe p2); 06415 06422 Z3_probe Z3_API Z3_probe_le(Z3_context x, Z3_probe p1, Z3_probe p2); 06423 06430 Z3_probe Z3_API Z3_probe_ge(Z3_context x, Z3_probe p1, Z3_probe p2); 06431 06438 Z3_probe Z3_API Z3_probe_eq(Z3_context x, Z3_probe p1, Z3_probe p2); 06439 06446 Z3_probe Z3_API Z3_probe_and(Z3_context x, Z3_probe p1, Z3_probe p2); 06447 06454 Z3_probe Z3_API Z3_probe_or(Z3_context x, Z3_probe p1, Z3_probe p2); 06455 06462 Z3_probe Z3_API Z3_probe_not(Z3_context x, Z3_probe p); 06463 06468 unsigned Z3_API Z3_get_num_tactics(Z3_context c); 06469 06476 Z3_string Z3_API Z3_get_tactic_name(Z3_context c, unsigned i); 06477 06482 unsigned Z3_API Z3_get_num_probes(Z3_context c); 06483 06490 Z3_string Z3_API Z3_get_probe_name(Z3_context c, unsigned i); 06491 06496 Z3_string Z3_API Z3_tactic_get_help(Z3_context c, Z3_tactic t); 06497 06502 Z3_param_descrs Z3_API Z3_tactic_get_param_descrs(Z3_context c, Z3_tactic t); 06503 06508 Z3_string Z3_API Z3_tactic_get_descr(Z3_context c, Z3_string name); 06509 06514 Z3_string Z3_API Z3_probe_get_descr(Z3_context c, Z3_string name); 06515 06521 double Z3_API Z3_probe_apply(Z3_context c, Z3_probe p, Z3_goal g); 06522 06527 Z3_apply_result Z3_API Z3_tactic_apply(Z3_context c, Z3_tactic t, Z3_goal g); 06528 06533 Z3_apply_result Z3_API Z3_tactic_apply_ex(Z3_context c, Z3_tactic t, Z3_goal g, Z3_params p); 06534 06535 #ifdef CorML3 06536 06540 void Z3_API Z3_apply_result_inc_ref(Z3_context c, Z3_apply_result r); 06541 06546 void Z3_API Z3_apply_result_dec_ref(Z3_context c, Z3_apply_result r); 06547 #endif 06548 06553 Z3_string Z3_API Z3_apply_result_to_string(Z3_context c, Z3_apply_result r); 06554 06559 unsigned Z3_API Z3_apply_result_get_num_subgoals(Z3_context c, Z3_apply_result r); 06560 06567 Z3_goal Z3_API Z3_apply_result_get_subgoal(Z3_context c, Z3_apply_result r, unsigned i); 06568 06574 Z3_model Z3_API Z3_apply_result_convert_model(Z3_context c, Z3_apply_result r, unsigned i, Z3_model m); 06575 06582 06592 Z3_solver Z3_API Z3_mk_solver(Z3_context c); 06593 06605 Z3_solver Z3_API Z3_mk_simple_solver(Z3_context c); 06606 06615 Z3_solver Z3_API Z3_mk_solver_for_logic(Z3_context c, Z3_symbol logic); 06616 06623 Z3_solver Z3_API Z3_mk_solver_from_tactic(Z3_context c, Z3_tactic t); 06624 06629 Z3_string Z3_API Z3_solver_get_help(Z3_context c, Z3_solver s); 06630 06635 Z3_param_descrs Z3_API Z3_solver_get_param_descrs(Z3_context c, Z3_solver s); 06636 06641 void Z3_API Z3_solver_set_params(Z3_context c, Z3_solver s, Z3_params p); 06642 06643 #ifdef Conly 06644 06648 void Z3_API Z3_solver_inc_ref(Z3_context c, Z3_solver s); 06649 06654 void Z3_API Z3_solver_dec_ref(Z3_context c, Z3_solver s); 06655 #endif 06656 06665 void Z3_API Z3_solver_push(Z3_context c, Z3_solver s); 06666 06675 void Z3_API Z3_solver_pop(Z3_context c, Z3_solver s, unsigned n); 06676 06681 void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s); 06682 06690 unsigned Z3_API Z3_solver_get_num_scopes(Z3_context c, Z3_solver s); 06691 06699 void Z3_API Z3_solver_assert(Z3_context c, Z3_solver s, Z3_ast a); 06700 06714 void Z3_API Z3_solver_assert_and_track(Z3_context c, Z3_solver s, Z3_ast a, Z3_ast p); 06715 06720 Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s); 06721 06737 Z3_lbool Z3_API Z3_solver_check(Z3_context c, Z3_solver s); 06738 06749 Z3_lbool Z3_API Z3_solver_check_assumptions(Z3_context c, Z3_solver s, 06750 unsigned num_assumptions, Z3_ast const assumptions[]); 06751 06759 Z3_model Z3_API Z3_solver_get_model(Z3_context c, Z3_solver s); 06760 06769 Z3_ast Z3_API Z3_solver_get_proof(Z3_context c, Z3_solver s); 06770 06776 Z3_ast_vector Z3_API Z3_solver_get_unsat_core(Z3_context c, Z3_solver s); 06777 06783 Z3_string Z3_API Z3_solver_get_reason_unknown(Z3_context c, Z3_solver s); 06784 06791 Z3_stats Z3_API Z3_solver_get_statistics(Z3_context c, Z3_solver s); 06792 06797 Z3_string Z3_API Z3_solver_to_string(Z3_context c, Z3_solver s); 06798 06805 06806 #ifdef ML4only 06807 #include <mlx_statistics.idl> 06808 #endif 06809 06813 Z3_string Z3_API Z3_stats_to_string(Z3_context c, Z3_stats s); 06814 06819 #ifdef Conly 06820 06824 void Z3_API Z3_stats_inc_ref(Z3_context c, Z3_stats s); 06825 06830 void Z3_API Z3_stats_dec_ref(Z3_context c, Z3_stats s); 06831 #endif 06832 06837 unsigned Z3_API Z3_stats_size(Z3_context c, Z3_stats s); 06838 06845 Z3_string Z3_API Z3_stats_get_key(Z3_context c, Z3_stats s, unsigned idx); 06846 06853 Z3_bool Z3_API Z3_stats_is_uint(Z3_context c, Z3_stats s, unsigned idx); 06854 06861 Z3_bool Z3_API Z3_stats_is_double(Z3_context c, Z3_stats s, unsigned idx); 06862 06869 unsigned Z3_API Z3_stats_get_uint_value(Z3_context c, Z3_stats s, unsigned idx); 06870 06877 double Z3_API Z3_stats_get_double_value(Z3_context c, Z3_stats s, unsigned idx); 06878 06880 #endif 06881 06882 06883 #ifdef CorML3 06884 06889 06898 Z3_func_decl Z3_API Z3_mk_injective_function( 06899 Z3_context c, 06900 Z3_symbol s, 06901 unsigned domain_size, Z3_sort const domain[], 06902 Z3_sort range 06903 ); 06904 06906 #endif 06907 06908 06913 06914 #ifdef CorML3 06915 06924 Z3_bool Z3_API Z3_set_logic(Z3_context c, Z3_string logic); 06925 06938 void Z3_API Z3_push(Z3_context c); 06939 06954 void Z3_API Z3_pop(Z3_context c, unsigned num_scopes); 06955 06967 unsigned Z3_API Z3_get_num_scopes(Z3_context c); 06968 06989 void Z3_API Z3_persist_ast(Z3_context c, Z3_ast a, unsigned num_scopes); 06990 07006 void Z3_API Z3_assert_cnstr(Z3_context c, Z3_ast a); 07007 07030 Z3_lbool Z3_API Z3_check_and_get_model(Z3_context c, Z3_model * m); 07031 07042 Z3_lbool Z3_API Z3_check(Z3_context c); 07043 07081 Z3_lbool Z3_API Z3_check_assumptions( 07082 Z3_context c, 07083 unsigned num_assumptions, Z3_ast const assumptions[], 07084 Z3_model * m, Z3_ast* proof, 07085 unsigned* core_size, Z3_ast core[] 07086 ); 07087 #endif 07088 07089 #ifdef CorML4 07090 07112 Z3_lbool Z3_API Z3_get_implied_equalities( 07113 Z3_context c, 07114 Z3_solver s, 07115 unsigned num_terms, 07116 Z3_ast const terms[], 07117 unsigned class_ids[] 07118 ); 07119 #endif 07120 07121 #ifdef CorML3 07122 07135 void Z3_API Z3_del_model(Z3_context c, Z3_model m); 07136 07143 07154 void Z3_API Z3_soft_check_cancel(Z3_context c); 07155 07165 Z3_search_failure Z3_API Z3_get_search_failure(Z3_context c); 07166 07173 07191 Z3_ast Z3_API Z3_mk_label(Z3_context c, Z3_symbol s, Z3_bool is_pos, Z3_ast f); 07192 07205 Z3_literals Z3_API Z3_get_relevant_labels(Z3_context c); 07206 07218 Z3_literals Z3_API Z3_get_relevant_literals(Z3_context c); 07219 07232 Z3_literals Z3_API Z3_get_guessed_literals(Z3_context c); 07233 07242 void Z3_API Z3_del_literals(Z3_context c, Z3_literals lbls); 07243 07252 unsigned Z3_API Z3_get_num_literals(Z3_context c, Z3_literals lbls); 07253 07260 Z3_symbol Z3_API Z3_get_label_symbol(Z3_context c, Z3_literals lbls, unsigned idx); 07261 07268 Z3_ast Z3_API Z3_get_literal(Z3_context c, Z3_literals lbls, unsigned idx); 07269 07280 void Z3_API Z3_disable_literal(Z3_context c, Z3_literals lbls, unsigned idx); 07281 07288 void Z3_API Z3_block_literals(Z3_context c, Z3_literals lbls); 07289 07296 07307 unsigned Z3_API Z3_get_model_num_constants(Z3_context c, Z3_model m); 07308 07320 Z3_func_decl Z3_API Z3_get_model_constant(Z3_context c, Z3_model m, unsigned i); 07321 07331 unsigned Z3_API Z3_get_model_num_funcs(Z3_context c, Z3_model m); 07332 07344 Z3_func_decl Z3_API Z3_get_model_func_decl(Z3_context c, Z3_model m, unsigned i); 07345 07353 Z3_bool Z3_API Z3_eval_func_decl(Z3_context c, Z3_model m, Z3_func_decl decl, Z3_ast* v); 07354 07369 Z3_bool Z3_API Z3_is_array_value(Z3_context c, Z3_model m, Z3_ast v, unsigned* num_entries); 07370 07381 void Z3_API Z3_get_array_value(Z3_context c, 07382 Z3_model m, 07383 Z3_ast v, 07384 unsigned num_entries, 07385 Z3_ast indices[], 07386 Z3_ast values[], 07387 Z3_ast* else_value 07388 ); 07389 07408 Z3_ast Z3_API Z3_get_model_func_else(Z3_context c, Z3_model m, unsigned i); 07409 07428 unsigned Z3_API Z3_get_model_func_num_entries(Z3_context c, Z3_model m, unsigned i); 07429 07453 unsigned Z3_API Z3_get_model_func_entry_num_args(Z3_context c, 07454 Z3_model m, 07455 unsigned i, 07456 unsigned j); 07457 07482 Z3_ast Z3_API Z3_get_model_func_entry_arg(Z3_context c, 07483 Z3_model m, 07484 unsigned i, 07485 unsigned j, 07486 unsigned k); 07487 07510 Z3_ast Z3_API Z3_get_model_func_entry_value(Z3_context c, 07511 Z3_model m, 07512 unsigned i, 07513 unsigned j); 07514 07533 Z3_bool Z3_API Z3_eval(Z3_context c, Z3_model m, Z3_ast t, Z3_ast * v); 07534 07544 Z3_bool Z3_API Z3_eval_decl(Z3_context c, Z3_model m, 07545 Z3_func_decl d, 07546 unsigned num_args, 07547 Z3_ast const args[], 07548 Z3_ast* v); 07549 07556 07571 Z3_string Z3_API Z3_context_to_string(Z3_context c); 07572 07587 Z3_string Z3_API Z3_statistics_to_string(Z3_context c); 07588 07601 Z3_ast Z3_API Z3_get_context_assignment(Z3_context c); 07602 07604 #endif 07605 07606 07607 #ifndef CAMLIDL 07608 #ifdef __cplusplus 07609 }; 07610 #endif // __cplusplus 07611 #else 07612 } 07613 #endif // CAMLIDL 07614 07617 #endif
1.7.6.1