diff --git a/Makefile.in b/Makefile.in index fd4366d13..f53afdee7 100644 --- a/Makefile.in +++ b/Makefile.in @@ -338,6 +338,9 @@ install: $(BIN_DIR)/$(Z3) $(BIN_DIR)/lib$(Z3).@SO_EXT@ $(BIN_DIR)/lib$(Z3).a @cp lib/z3.h $(PREFIX)/include @cp lib/z3_v1.h $(PREFIX)/include @cp lib/z3_macros.h $(PREFIX)/include + @cp lib/z3_internal.h $(PREFIX)/include + @cp lib/z3_internal_types.h $(PREFIX)/include + @cp lib/z3_poly.h $(PREFIX)/include @cp c++/z3++.h $(PREFIX)/include uninstall: @@ -349,6 +352,9 @@ uninstall: @rm -f $(PREFIX)/include/z3_v1.h @rm -f $(PREFIX)/include/z3_macros.h @rm -f $(PREFIX)/include/z3++.h + @rm -f $(PREFIX)/include/z3_internal.h + @rm -f $(PREFIX)/include/z3_internal_types.h + @rm -f $(PREFIX)/include/z3_poly.h install-z3py: $(BIN_DIR)/lib$(Z3).@SO_EXT@ @if test $(HAS_PYTHON) -eq 0; then echo "Python is not available in your system."; exit 1; fi @@ -360,6 +366,7 @@ install-z3py: $(BIN_DIR)/lib$(Z3).@SO_EXT@ @cp python/z3consts.pyc $(PYTHON_PACKAGE_DIR) @cp python/z3tactics.pyc $(PYTHON_PACKAGE_DIR) @cp python/z3printer.pyc $(PYTHON_PACKAGE_DIR) + @cp python/z3poly.pyc $(PYTHON_PACKAGE_DIR) @cp $(BIN_DIR)/lib$(Z3).@SO_EXT@ $(PYTHON_PACKAGE_DIR) @if python python/z3test.py; then echo "Z3Py was successfully installed."; else echo "Failed to execute Z3Py regressions..."; exit 1; fi @@ -372,4 +379,5 @@ uninstall-z3py: @rm -f $(PYTHON_PACKAGE_DIR)/z3consts.pyc @rm -f $(PYTHON_PACKAGE_DIR)/z3tactics.pyc @rm -f $(PYTHON_PACKAGE_DIR)/z3printer.pyc + @rm -f $(PYTHON_PACKAGE_DIR)/z3poly.pyc @rm -f $(PYTHON_PACKAGE_DIR)/$(BIN_DIR)/lib$(Z3).@SO_EXT@ diff --git a/Microsoft.Z3/Native.cs b/Microsoft.Z3/Native.cs index b54cf510f..d959fd254 100644 --- a/Microsoft.Z3/Native.cs +++ b/Microsoft.Z3/Native.cs @@ -8,6 +8,7 @@ using System.Runtime.InteropServices; namespace Microsoft.Z3 { + using Z3_monomial = System.IntPtr; using Z3_config = System.IntPtr; using Z3_context = System.IntPtr; using Z3_ast = System.IntPtr; @@ -34,6 +35,8 @@ namespace Microsoft.Z3 using Z3_func_entry = System.IntPtr; using Z3_fixedpoint = System.IntPtr; using Z3_param_descrs = System.IntPtr; + using Z3_polynomial_manager = System.IntPtr; + using Z3_polynomial = System.IntPtr; public class Native { @@ -1492,6 +1495,24 @@ namespace Microsoft.Z3 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)] public extern static Z3_ast Z3_get_context_assignment(Z3_context a0); + [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)] + public extern static Z3_polynomial_manager Z3_mk_polynomial_manager(Z3_context a0); + + [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)] + public extern static void Z3_del_polynomial_manager(Z3_context a0, Z3_polynomial_manager a1); + + [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)] + public extern static Z3_polynomial Z3_mk_zero_polynomial(Z3_context a0, Z3_polynomial_manager a1); + + [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)] + public extern static void Z3_polynomial_inc_ref(Z3_context a0, Z3_polynomial_manager a1, Z3_polynomial a2); + + [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)] + public extern static void Z3_polynomial_dec_ref(Z3_context a0, Z3_polynomial_manager a1, Z3_polynomial a2); + + [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)] + public extern static IntPtr Z3_polynomial_to_string(Z3_context a0, Z3_polynomial_manager a1, Z3_polynomial a2); + } public static void Z3_set_error_handler(Z3_context a0, Z3_error_handler a1) { @@ -5215,6 +5236,51 @@ namespace Microsoft.Z3 return r; } + public static Z3_polynomial_manager Z3_mk_polynomial_manager(Z3_context a0) { + Z3_polynomial_manager r = LIB.Z3_mk_polynomial_manager(a0); + Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0); + if (err != Z3_error_code.Z3_OK) + throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err))); + return r; + } + + public static void Z3_del_polynomial_manager(Z3_context a0, Z3_polynomial_manager a1) { + LIB.Z3_del_polynomial_manager(a0, a1); + Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0); + if (err != Z3_error_code.Z3_OK) + throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err))); + } + + public static Z3_polynomial Z3_mk_zero_polynomial(Z3_context a0, Z3_polynomial_manager a1) { + Z3_polynomial r = LIB.Z3_mk_zero_polynomial(a0, a1); + Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0); + if (err != Z3_error_code.Z3_OK) + throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err))); + return r; + } + + public static void Z3_polynomial_inc_ref(Z3_context a0, Z3_polynomial_manager a1, Z3_polynomial a2) { + LIB.Z3_polynomial_inc_ref(a0, a1, a2); + Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0); + if (err != Z3_error_code.Z3_OK) + throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err))); + } + + public static void Z3_polynomial_dec_ref(Z3_context a0, Z3_polynomial_manager a1, Z3_polynomial a2) { + LIB.Z3_polynomial_dec_ref(a0, a1, a2); + Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0); + if (err != Z3_error_code.Z3_OK) + throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err))); + } + + public static string Z3_polynomial_to_string(Z3_context a0, Z3_polynomial_manager a1, Z3_polynomial a2) { + IntPtr r = LIB.Z3_polynomial_to_string(a0, a1, a2); + Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0); + if (err != Z3_error_code.Z3_OK) + throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err))); + return Marshal.PtrToStringAnsi(r); + } + } } diff --git a/dll/z3.def b/dll/z3.def index efa434da3..ddbc9404b 100644 --- a/dll/z3.def +++ b/dll/z3.def @@ -1,522 +1,528 @@ LIBRARY "Z3" EXPORTS - Z3_mk_config @1 - Z3_del_config @2 - Z3_set_param_value @3 - Z3_mk_context @4 - Z3_mk_context_rc @5 - Z3_del_context @6 - Z3_inc_ref @7 - Z3_dec_ref @8 - Z3_update_param_value @9 - Z3_get_param_value @10 - Z3_interrupt @11 - Z3_mk_params @12 - Z3_params_inc_ref @13 - Z3_params_dec_ref @14 - Z3_params_set_bool @15 - Z3_params_set_uint @16 - Z3_params_set_double @17 - Z3_params_set_symbol @18 - Z3_params_to_string @19 - Z3_params_validate @20 - Z3_param_descrs_inc_ref @21 - Z3_param_descrs_dec_ref @22 - Z3_param_descrs_get_kind @23 - Z3_param_descrs_size @24 - Z3_param_descrs_get_name @25 - Z3_param_descrs_to_string @26 - Z3_mk_int_symbol @27 - Z3_mk_string_symbol @28 - Z3_mk_uninterpreted_sort @29 - Z3_mk_bool_sort @30 - Z3_mk_int_sort @31 - Z3_mk_real_sort @32 - Z3_mk_bv_sort @33 - Z3_mk_finite_domain_sort @34 - Z3_mk_array_sort @35 - Z3_mk_tuple_sort @36 - Z3_mk_enumeration_sort @37 - Z3_mk_list_sort @38 - Z3_mk_constructor @39 - Z3_del_constructor @40 - Z3_mk_datatype @41 - Z3_mk_constructor_list @42 - Z3_del_constructor_list @43 - Z3_mk_datatypes @44 - Z3_query_constructor @45 - Z3_mk_func_decl @46 - Z3_mk_app @47 - Z3_mk_const @48 - Z3_mk_fresh_func_decl @49 - Z3_mk_fresh_const @50 - Z3_mk_true @51 - Z3_mk_false @52 - Z3_mk_eq @53 - Z3_mk_distinct @54 - Z3_mk_not @55 - Z3_mk_ite @56 - Z3_mk_iff @57 - Z3_mk_implies @58 - Z3_mk_xor @59 - Z3_mk_and @60 - Z3_mk_or @61 - Z3_mk_add @62 - Z3_mk_mul @63 - Z3_mk_sub @64 - Z3_mk_unary_minus @65 - Z3_mk_div @66 - Z3_mk_mod @67 - Z3_mk_rem @68 - Z3_mk_power @69 - Z3_mk_lt @70 - Z3_mk_le @71 - Z3_mk_gt @72 - Z3_mk_ge @73 - Z3_mk_int2real @74 - Z3_mk_real2int @75 - Z3_mk_is_int @76 - Z3_mk_bvnot @77 - Z3_mk_bvredand @78 - Z3_mk_bvredor @79 - Z3_mk_bvand @80 - Z3_mk_bvor @81 - Z3_mk_bvxor @82 - Z3_mk_bvnand @83 - Z3_mk_bvnor @84 - Z3_mk_bvxnor @85 - Z3_mk_bvneg @86 - Z3_mk_bvadd @87 - Z3_mk_bvsub @88 - Z3_mk_bvmul @89 - Z3_mk_bvudiv @90 - Z3_mk_bvsdiv @91 - Z3_mk_bvurem @92 - Z3_mk_bvsrem @93 - Z3_mk_bvsmod @94 - Z3_mk_bvult @95 - Z3_mk_bvslt @96 - Z3_mk_bvule @97 - Z3_mk_bvsle @98 - Z3_mk_bvuge @99 - Z3_mk_bvsge @100 - Z3_mk_bvugt @101 - Z3_mk_bvsgt @102 - Z3_mk_concat @103 - Z3_mk_extract @104 - Z3_mk_sign_ext @105 - Z3_mk_zero_ext @106 - Z3_mk_repeat @107 - Z3_mk_bvshl @108 - Z3_mk_bvlshr @109 - Z3_mk_bvashr @110 - Z3_mk_rotate_left @111 - Z3_mk_rotate_right @112 - Z3_mk_ext_rotate_left @113 - Z3_mk_ext_rotate_right @114 - Z3_mk_int2bv @115 - Z3_mk_bv2int @116 - Z3_mk_bvadd_no_overflow @117 - Z3_mk_bvadd_no_underflow @118 - Z3_mk_bvsub_no_overflow @119 - Z3_mk_bvsub_no_underflow @120 - Z3_mk_bvsdiv_no_overflow @121 - Z3_mk_bvneg_no_overflow @122 - Z3_mk_bvmul_no_overflow @123 - Z3_mk_bvmul_no_underflow @124 - Z3_mk_select @125 - Z3_mk_store @126 - Z3_mk_const_array @127 - Z3_mk_map @128 - Z3_mk_array_default @129 - Z3_mk_set_sort @130 - Z3_mk_empty_set @131 - Z3_mk_full_set @132 - Z3_mk_set_add @133 - Z3_mk_set_del @134 - Z3_mk_set_union @135 - Z3_mk_set_intersect @136 - Z3_mk_set_difference @137 - Z3_mk_set_complement @138 - Z3_mk_set_member @139 - Z3_mk_set_subset @140 - Z3_mk_numeral @141 - Z3_mk_real @142 - Z3_mk_int @143 - Z3_mk_unsigned_int @144 - Z3_mk_int64 @145 - Z3_mk_unsigned_int64 @146 - Z3_mk_pattern @147 - Z3_mk_bound @148 - Z3_mk_forall @149 - Z3_mk_exists @150 - Z3_mk_quantifier @151 - Z3_mk_quantifier_ex @152 - Z3_mk_forall_const @153 - Z3_mk_exists_const @154 - Z3_mk_quantifier_const @155 - Z3_mk_quantifier_const_ex @156 - Z3_get_symbol_kind @157 - Z3_get_symbol_int @158 - Z3_get_symbol_string @159 - Z3_get_sort_name @160 - Z3_get_sort_id @161 - Z3_sort_to_ast @162 - Z3_is_eq_sort @163 - Z3_get_sort_kind @164 - Z3_get_bv_sort_size @165 - Z3_get_finite_domain_sort_size @166 - Z3_get_array_sort_domain @167 - Z3_get_array_sort_range @168 - Z3_get_tuple_sort_mk_decl @169 - Z3_get_tuple_sort_num_fields @170 - Z3_get_tuple_sort_field_decl @171 - Z3_get_datatype_sort_num_constructors @172 - Z3_get_datatype_sort_constructor @173 - Z3_get_datatype_sort_recognizer @174 - Z3_get_datatype_sort_constructor_accessor @175 - Z3_get_relation_arity @176 - Z3_get_relation_column @177 - Z3_func_decl_to_ast @178 - Z3_is_eq_func_decl @179 - Z3_get_func_decl_id @180 - Z3_get_decl_name @181 - Z3_get_decl_kind @182 - Z3_get_domain_size @183 - Z3_get_arity @184 - Z3_get_domain @185 - Z3_get_range @186 - Z3_get_decl_num_parameters @187 - Z3_get_decl_parameter_kind @188 - Z3_get_decl_int_parameter @189 - Z3_get_decl_double_parameter @190 - Z3_get_decl_symbol_parameter @191 - Z3_get_decl_sort_parameter @192 - Z3_get_decl_ast_parameter @193 - Z3_get_decl_func_decl_parameter @194 - Z3_get_decl_rational_parameter @195 - Z3_app_to_ast @196 - Z3_get_app_decl @197 - Z3_get_app_num_args @198 - Z3_get_app_arg @199 - Z3_is_eq_ast @200 - Z3_get_ast_id @201 - Z3_get_ast_hash @202 - Z3_get_sort @203 - Z3_is_well_sorted @204 - Z3_get_bool_value @205 - Z3_get_ast_kind @206 - Z3_is_app @207 - Z3_is_numeral_ast @208 - Z3_is_algebraic_number @209 - Z3_to_app @210 - Z3_to_func_decl @211 - Z3_get_numeral_string @212 - Z3_get_numeral_decimal_string @213 - Z3_get_numerator @214 - Z3_get_denominator @215 - Z3_get_numeral_small @216 - Z3_get_numeral_int @217 - Z3_get_numeral_uint @218 - Z3_get_numeral_uint64 @219 - Z3_get_numeral_int64 @220 - Z3_get_numeral_rational_int64 @221 - Z3_get_algebraic_number_lower @222 - Z3_get_algebraic_number_upper @223 - Z3_pattern_to_ast @224 - Z3_get_pattern_num_terms @225 - Z3_get_pattern @226 - Z3_get_index_value @227 - Z3_is_quantifier_forall @228 - Z3_get_quantifier_weight @229 - Z3_get_quantifier_num_patterns @230 - Z3_get_quantifier_pattern_ast @231 - Z3_get_quantifier_num_no_patterns @232 - Z3_get_quantifier_no_pattern_ast @233 - Z3_get_quantifier_num_bound @234 - Z3_get_quantifier_bound_name @235 - Z3_get_quantifier_bound_sort @236 - Z3_get_quantifier_body @237 - Z3_simplify @238 - Z3_simplify_ex @239 - Z3_simplify_get_help @240 - Z3_simplify_get_param_descrs @241 - Z3_update_term @242 - Z3_substitute @243 - Z3_substitute_vars @244 - Z3_translate @245 - Z3_model_inc_ref @246 - Z3_model_dec_ref @247 - Z3_model_eval @248 - Z3_model_get_const_interp @249 - Z3_model_get_func_interp @250 - Z3_model_get_num_consts @251 - Z3_model_get_const_decl @252 - Z3_model_get_num_funcs @253 - Z3_model_get_func_decl @254 - Z3_model_get_num_sorts @255 - Z3_model_get_sort @256 - Z3_model_get_sort_universe @257 - Z3_is_as_array @258 - Z3_get_as_array_func_decl @259 - Z3_func_interp_inc_ref @260 - Z3_func_interp_dec_ref @261 - Z3_func_interp_get_num_entries @262 - Z3_func_interp_get_entry @263 - Z3_func_interp_get_else @264 - Z3_func_interp_get_arity @265 - Z3_func_entry_inc_ref @266 - Z3_func_entry_dec_ref @267 - Z3_func_entry_get_value @268 - Z3_func_entry_get_num_args @269 - Z3_func_entry_get_arg @270 - Z3_open_log @271 - Z3_append_log @272 - Z3_close_log @273 - Z3_toggle_warning_messages @274 - Z3_set_ast_print_mode @275 - Z3_ast_to_string @276 - Z3_pattern_to_string @277 - Z3_sort_to_string @278 - Z3_func_decl_to_string @279 - Z3_model_to_string @280 - Z3_benchmark_to_smtlib_string @281 - Z3_parse_smtlib2_string @282 - Z3_parse_smtlib2_file @283 - Z3_parse_smtlib_string @284 - Z3_parse_smtlib_file @285 - Z3_get_smtlib_num_formulas @286 - Z3_get_smtlib_formula @287 - Z3_get_smtlib_num_assumptions @288 - Z3_get_smtlib_assumption @289 - Z3_get_smtlib_num_decls @290 - Z3_get_smtlib_decl @291 - Z3_get_smtlib_num_sorts @292 - Z3_get_smtlib_sort @293 - Z3_get_smtlib_error @294 - Z3_parse_z3_string @295 - Z3_parse_z3_file @296 - Z3_get_error_code @297 - Z3_set_error_handler @298 - Z3_set_error @299 - Z3_get_error_msg @300 - Z3_get_error_msg_ex @301 - Z3_get_version @302 - Z3_reset_memory @303 - Z3_mk_theory @304 - Z3_theory_get_ext_data @305 - Z3_theory_mk_sort @306 - Z3_theory_mk_value @307 - Z3_theory_mk_constant @308 - Z3_theory_mk_func_decl @309 - Z3_theory_get_context @310 - Z3_set_delete_callback @311 - Z3_set_reduce_app_callback @312 - Z3_set_reduce_eq_callback @313 - Z3_set_reduce_distinct_callback @314 - Z3_set_new_app_callback @315 - Z3_set_new_elem_callback @316 - Z3_set_init_search_callback @317 - Z3_set_push_callback @318 - Z3_set_pop_callback @319 - Z3_set_restart_callback @320 - Z3_set_reset_callback @321 - Z3_set_final_check_callback @322 - Z3_set_new_eq_callback @323 - Z3_set_new_diseq_callback @324 - Z3_set_new_assignment_callback @325 - Z3_set_new_relevant_callback @326 - Z3_theory_assert_axiom @327 - Z3_theory_assume_eq @328 - Z3_theory_enable_axiom_simplification @329 - Z3_theory_get_eqc_root @330 - Z3_theory_get_eqc_next @331 - Z3_theory_get_num_parents @332 - Z3_theory_get_parent @333 - Z3_theory_is_value @334 - Z3_theory_is_decl @335 - Z3_theory_get_num_elems @336 - Z3_theory_get_elem @337 - Z3_theory_get_num_apps @338 - Z3_theory_get_app @339 - Z3_mk_fixedpoint @340 - Z3_fixedpoint_inc_ref @341 - Z3_fixedpoint_dec_ref @342 - Z3_fixedpoint_add_rule @343 - Z3_fixedpoint_add_fact @344 - Z3_fixedpoint_assert @345 - Z3_fixedpoint_query @346 - Z3_fixedpoint_query_relations @347 - Z3_fixedpoint_get_answer @348 - Z3_fixedpoint_get_reason_unknown @349 - Z3_fixedpoint_update_rule @350 - Z3_fixedpoint_get_num_levels @351 - Z3_fixedpoint_get_cover_delta @352 - Z3_fixedpoint_add_cover @353 - Z3_fixedpoint_get_statistics @354 - Z3_fixedpoint_register_relation @355 - Z3_fixedpoint_set_predicate_representation @356 - Z3_fixedpoint_simplify_rules @357 - Z3_fixedpoint_set_params @358 - Z3_fixedpoint_get_help @359 - Z3_fixedpoint_get_param_descrs @360 - Z3_fixedpoint_to_string @361 - Z3_fixedpoint_push @362 - Z3_fixedpoint_pop @363 - Z3_fixedpoint_init @364 - Z3_fixedpoint_set_reduce_assign_callback @365 - Z3_fixedpoint_set_reduce_app_callback @366 - Z3_mk_ast_vector @367 - Z3_ast_vector_inc_ref @368 - Z3_ast_vector_dec_ref @369 - Z3_ast_vector_size @370 - Z3_ast_vector_get @371 - Z3_ast_vector_set @372 - Z3_ast_vector_resize @373 - Z3_ast_vector_push @374 - Z3_ast_vector_translate @375 - Z3_ast_vector_to_string @376 - Z3_mk_ast_map @377 - Z3_ast_map_inc_ref @378 - Z3_ast_map_dec_ref @379 - Z3_ast_map_contains @380 - Z3_ast_map_find @381 - Z3_ast_map_insert @382 - Z3_ast_map_erase @383 - Z3_ast_map_reset @384 - Z3_ast_map_size @385 - Z3_ast_map_keys @386 - Z3_ast_map_to_string @387 - Z3_mk_goal @388 - Z3_goal_inc_ref @389 - Z3_goal_dec_ref @390 - Z3_goal_precision @391 - Z3_goal_assert @392 - Z3_goal_inconsistent @393 - Z3_goal_depth @394 - Z3_goal_reset @395 - Z3_goal_size @396 - Z3_goal_formula @397 - Z3_goal_num_exprs @398 - Z3_goal_is_decided_sat @399 - Z3_goal_is_decided_unsat @400 - Z3_goal_translate @401 - Z3_goal_to_string @402 - Z3_mk_tactic @403 - Z3_tactic_inc_ref @404 - Z3_tactic_dec_ref @405 - Z3_mk_probe @406 - Z3_probe_inc_ref @407 - Z3_probe_dec_ref @408 - Z3_tactic_and_then @409 - Z3_tactic_or_else @410 - Z3_tactic_par_or @411 - Z3_tactic_par_and_then @412 - Z3_tactic_try_for @413 - Z3_tactic_when @414 - Z3_tactic_cond @415 - Z3_tactic_repeat @416 - Z3_tactic_skip @417 - Z3_tactic_fail @418 - Z3_tactic_fail_if @419 - Z3_tactic_fail_if_not_decided @420 - Z3_tactic_using_params @421 - Z3_probe_const @422 - Z3_probe_lt @423 - Z3_probe_gt @424 - Z3_probe_le @425 - Z3_probe_ge @426 - Z3_probe_eq @427 - Z3_probe_and @428 - Z3_probe_or @429 - Z3_probe_not @430 - Z3_get_num_tactics @431 - Z3_get_tactic_name @432 - Z3_get_num_probes @433 - Z3_get_probe_name @434 - Z3_tactic_get_help @435 - Z3_tactic_get_param_descrs @436 - Z3_tactic_get_descr @437 - Z3_probe_get_descr @438 - Z3_probe_apply @439 - Z3_tactic_apply @440 - Z3_tactic_apply_ex @441 - Z3_apply_result_inc_ref @442 - Z3_apply_result_dec_ref @443 - Z3_apply_result_to_string @444 - Z3_apply_result_get_num_subgoals @445 - Z3_apply_result_get_subgoal @446 - Z3_apply_result_convert_model @447 - Z3_mk_solver @448 - Z3_mk_simple_solver @449 - Z3_mk_solver_for_logic @450 - Z3_mk_solver_from_tactic @451 - Z3_solver_get_help @452 - Z3_solver_get_param_descrs @453 - Z3_solver_set_params @454 - Z3_solver_inc_ref @455 - Z3_solver_dec_ref @456 - Z3_solver_push @457 - Z3_solver_pop @458 - Z3_solver_reset @459 - Z3_solver_get_num_scopes @460 - Z3_solver_assert @461 - Z3_solver_get_assertions @462 - Z3_solver_check @463 - Z3_solver_check_assumptions @464 - Z3_solver_get_model @465 - Z3_solver_get_proof @466 - Z3_solver_get_unsat_core @467 - Z3_solver_get_reason_unknown @468 - Z3_solver_get_statistics @469 - Z3_solver_to_string @470 - Z3_stats_to_string @471 - Z3_stats_inc_ref @472 - Z3_stats_dec_ref @473 - Z3_stats_size @474 - Z3_stats_get_key @475 - Z3_stats_is_uint @476 - Z3_stats_is_double @477 - Z3_stats_get_uint_value @478 - Z3_stats_get_double_value @479 - Z3_mk_injective_function @480 - Z3_set_logic @481 - Z3_push @482 - Z3_pop @483 - Z3_get_num_scopes @484 - Z3_persist_ast @485 - Z3_assert_cnstr @486 - Z3_check_and_get_model @487 - Z3_check @488 - Z3_check_assumptions @489 - Z3_get_implied_equalities @490 - Z3_del_model @491 - Z3_soft_check_cancel @492 - Z3_get_search_failure @493 - Z3_mk_label @494 - Z3_get_relevant_labels @495 - Z3_get_relevant_literals @496 - Z3_get_guessed_literals @497 - Z3_del_literals @498 - Z3_get_num_literals @499 - Z3_get_label_symbol @500 - Z3_get_literal @501 - Z3_disable_literal @502 - Z3_block_literals @503 - Z3_get_model_num_constants @504 - Z3_get_model_constant @505 - Z3_get_model_num_funcs @506 - Z3_get_model_func_decl @507 - Z3_eval_func_decl @508 - Z3_is_array_value @509 - Z3_get_array_value @510 - Z3_get_model_func_else @511 - Z3_get_model_func_num_entries @512 - Z3_get_model_func_entry_num_args @513 - Z3_get_model_func_entry_arg @514 - Z3_get_model_func_entry_value @515 - Z3_eval @516 - Z3_eval_decl @517 - Z3_context_to_string @518 - Z3_statistics_to_string @519 - Z3_get_context_assignment @520 + Z3_mk_config @3 + Z3_del_config @4 + Z3_set_param_value @5 + Z3_mk_context @6 + Z3_mk_context_rc @7 + Z3_del_context @8 + Z3_inc_ref @9 + Z3_dec_ref @10 + Z3_update_param_value @11 + Z3_get_param_value @12 + Z3_interrupt @13 + Z3_mk_params @14 + Z3_params_inc_ref @15 + Z3_params_dec_ref @16 + Z3_params_set_bool @17 + Z3_params_set_uint @18 + Z3_params_set_double @19 + Z3_params_set_symbol @20 + Z3_params_to_string @21 + Z3_params_validate @22 + Z3_param_descrs_inc_ref @23 + Z3_param_descrs_dec_ref @24 + Z3_param_descrs_get_kind @25 + Z3_param_descrs_size @26 + Z3_param_descrs_get_name @27 + Z3_param_descrs_to_string @28 + Z3_mk_int_symbol @29 + Z3_mk_string_symbol @30 + Z3_mk_uninterpreted_sort @31 + Z3_mk_bool_sort @32 + Z3_mk_int_sort @33 + Z3_mk_real_sort @34 + Z3_mk_bv_sort @35 + Z3_mk_finite_domain_sort @36 + Z3_mk_array_sort @37 + Z3_mk_tuple_sort @38 + Z3_mk_enumeration_sort @39 + Z3_mk_list_sort @40 + Z3_mk_constructor @41 + Z3_del_constructor @42 + Z3_mk_datatype @43 + Z3_mk_constructor_list @44 + Z3_del_constructor_list @45 + Z3_mk_datatypes @46 + Z3_query_constructor @47 + Z3_mk_func_decl @48 + Z3_mk_app @49 + Z3_mk_const @50 + Z3_mk_fresh_func_decl @51 + Z3_mk_fresh_const @52 + Z3_mk_true @53 + Z3_mk_false @54 + Z3_mk_eq @55 + Z3_mk_distinct @56 + Z3_mk_not @57 + Z3_mk_ite @58 + Z3_mk_iff @59 + Z3_mk_implies @60 + Z3_mk_xor @61 + Z3_mk_and @62 + Z3_mk_or @63 + Z3_mk_add @64 + Z3_mk_mul @65 + Z3_mk_sub @66 + Z3_mk_unary_minus @67 + Z3_mk_div @68 + Z3_mk_mod @69 + Z3_mk_rem @70 + Z3_mk_power @71 + Z3_mk_lt @72 + Z3_mk_le @73 + Z3_mk_gt @74 + Z3_mk_ge @75 + Z3_mk_int2real @76 + Z3_mk_real2int @77 + Z3_mk_is_int @78 + Z3_mk_bvnot @79 + Z3_mk_bvredand @80 + Z3_mk_bvredor @81 + Z3_mk_bvand @82 + Z3_mk_bvor @83 + Z3_mk_bvxor @84 + Z3_mk_bvnand @85 + Z3_mk_bvnor @86 + Z3_mk_bvxnor @87 + Z3_mk_bvneg @88 + Z3_mk_bvadd @89 + Z3_mk_bvsub @90 + Z3_mk_bvmul @91 + Z3_mk_bvudiv @92 + Z3_mk_bvsdiv @93 + Z3_mk_bvurem @94 + Z3_mk_bvsrem @95 + Z3_mk_bvsmod @96 + Z3_mk_bvult @97 + Z3_mk_bvslt @98 + Z3_mk_bvule @99 + Z3_mk_bvsle @100 + Z3_mk_bvuge @101 + Z3_mk_bvsge @102 + Z3_mk_bvugt @103 + Z3_mk_bvsgt @104 + Z3_mk_concat @105 + Z3_mk_extract @106 + Z3_mk_sign_ext @107 + Z3_mk_zero_ext @108 + Z3_mk_repeat @109 + Z3_mk_bvshl @110 + Z3_mk_bvlshr @111 + Z3_mk_bvashr @112 + Z3_mk_rotate_left @113 + Z3_mk_rotate_right @114 + Z3_mk_ext_rotate_left @115 + Z3_mk_ext_rotate_right @116 + Z3_mk_int2bv @117 + Z3_mk_bv2int @118 + Z3_mk_bvadd_no_overflow @119 + Z3_mk_bvadd_no_underflow @120 + Z3_mk_bvsub_no_overflow @121 + Z3_mk_bvsub_no_underflow @122 + Z3_mk_bvsdiv_no_overflow @123 + Z3_mk_bvneg_no_overflow @124 + Z3_mk_bvmul_no_overflow @125 + Z3_mk_bvmul_no_underflow @126 + Z3_mk_select @127 + Z3_mk_store @128 + Z3_mk_const_array @129 + Z3_mk_map @130 + Z3_mk_array_default @131 + Z3_mk_set_sort @132 + Z3_mk_empty_set @133 + Z3_mk_full_set @134 + Z3_mk_set_add @135 + Z3_mk_set_del @136 + Z3_mk_set_union @137 + Z3_mk_set_intersect @138 + Z3_mk_set_difference @139 + Z3_mk_set_complement @140 + Z3_mk_set_member @141 + Z3_mk_set_subset @142 + Z3_mk_numeral @143 + Z3_mk_real @144 + Z3_mk_int @145 + Z3_mk_unsigned_int @146 + Z3_mk_int64 @147 + Z3_mk_unsigned_int64 @148 + Z3_mk_pattern @149 + Z3_mk_bound @150 + Z3_mk_forall @151 + Z3_mk_exists @152 + Z3_mk_quantifier @153 + Z3_mk_quantifier_ex @154 + Z3_mk_forall_const @155 + Z3_mk_exists_const @156 + Z3_mk_quantifier_const @157 + Z3_mk_quantifier_const_ex @158 + Z3_get_symbol_kind @159 + Z3_get_symbol_int @160 + Z3_get_symbol_string @161 + Z3_get_sort_name @162 + Z3_get_sort_id @163 + Z3_sort_to_ast @164 + Z3_is_eq_sort @165 + Z3_get_sort_kind @166 + Z3_get_bv_sort_size @167 + Z3_get_finite_domain_sort_size @168 + Z3_get_array_sort_domain @169 + Z3_get_array_sort_range @170 + Z3_get_tuple_sort_mk_decl @171 + Z3_get_tuple_sort_num_fields @172 + Z3_get_tuple_sort_field_decl @173 + Z3_get_datatype_sort_num_constructors @174 + Z3_get_datatype_sort_constructor @175 + Z3_get_datatype_sort_recognizer @176 + Z3_get_datatype_sort_constructor_accessor @177 + Z3_get_relation_arity @178 + Z3_get_relation_column @179 + Z3_func_decl_to_ast @180 + Z3_is_eq_func_decl @181 + Z3_get_func_decl_id @182 + Z3_get_decl_name @183 + Z3_get_decl_kind @184 + Z3_get_domain_size @185 + Z3_get_arity @186 + Z3_get_domain @187 + Z3_get_range @188 + Z3_get_decl_num_parameters @189 + Z3_get_decl_parameter_kind @190 + Z3_get_decl_int_parameter @191 + Z3_get_decl_double_parameter @192 + Z3_get_decl_symbol_parameter @193 + Z3_get_decl_sort_parameter @194 + Z3_get_decl_ast_parameter @195 + Z3_get_decl_func_decl_parameter @196 + Z3_get_decl_rational_parameter @197 + Z3_app_to_ast @198 + Z3_get_app_decl @199 + Z3_get_app_num_args @200 + Z3_get_app_arg @201 + Z3_is_eq_ast @202 + Z3_get_ast_id @203 + Z3_get_ast_hash @204 + Z3_get_sort @205 + Z3_is_well_sorted @206 + Z3_get_bool_value @207 + Z3_get_ast_kind @208 + Z3_is_app @209 + Z3_is_numeral_ast @210 + Z3_is_algebraic_number @211 + Z3_to_app @212 + Z3_to_func_decl @213 + Z3_get_numeral_string @214 + Z3_get_numeral_decimal_string @215 + Z3_get_numerator @216 + Z3_get_denominator @217 + Z3_get_numeral_small @218 + Z3_get_numeral_int @219 + Z3_get_numeral_uint @220 + Z3_get_numeral_uint64 @221 + Z3_get_numeral_int64 @222 + Z3_get_numeral_rational_int64 @223 + Z3_get_algebraic_number_lower @224 + Z3_get_algebraic_number_upper @225 + Z3_pattern_to_ast @226 + Z3_get_pattern_num_terms @227 + Z3_get_pattern @228 + Z3_get_index_value @229 + Z3_is_quantifier_forall @230 + Z3_get_quantifier_weight @231 + Z3_get_quantifier_num_patterns @232 + Z3_get_quantifier_pattern_ast @233 + Z3_get_quantifier_num_no_patterns @234 + Z3_get_quantifier_no_pattern_ast @235 + Z3_get_quantifier_num_bound @236 + Z3_get_quantifier_bound_name @237 + Z3_get_quantifier_bound_sort @238 + Z3_get_quantifier_body @239 + Z3_simplify @240 + Z3_simplify_ex @241 + Z3_simplify_get_help @242 + Z3_simplify_get_param_descrs @243 + Z3_update_term @244 + Z3_substitute @245 + Z3_substitute_vars @246 + Z3_translate @247 + Z3_model_inc_ref @248 + Z3_model_dec_ref @249 + Z3_model_eval @250 + Z3_model_get_const_interp @251 + Z3_model_get_func_interp @252 + Z3_model_get_num_consts @253 + Z3_model_get_const_decl @254 + Z3_model_get_num_funcs @255 + Z3_model_get_func_decl @256 + Z3_model_get_num_sorts @257 + Z3_model_get_sort @258 + Z3_model_get_sort_universe @259 + Z3_is_as_array @260 + Z3_get_as_array_func_decl @261 + Z3_func_interp_inc_ref @262 + Z3_func_interp_dec_ref @263 + Z3_func_interp_get_num_entries @264 + Z3_func_interp_get_entry @265 + Z3_func_interp_get_else @266 + Z3_func_interp_get_arity @267 + Z3_func_entry_inc_ref @268 + Z3_func_entry_dec_ref @269 + Z3_func_entry_get_value @270 + Z3_func_entry_get_num_args @271 + Z3_func_entry_get_arg @272 + Z3_open_log @273 + Z3_append_log @274 + Z3_close_log @275 + Z3_toggle_warning_messages @276 + Z3_set_ast_print_mode @277 + Z3_ast_to_string @278 + Z3_pattern_to_string @279 + Z3_sort_to_string @280 + Z3_func_decl_to_string @281 + Z3_model_to_string @282 + Z3_benchmark_to_smtlib_string @283 + Z3_parse_smtlib2_string @284 + Z3_parse_smtlib2_file @285 + Z3_parse_smtlib_string @286 + Z3_parse_smtlib_file @287 + Z3_get_smtlib_num_formulas @288 + Z3_get_smtlib_formula @289 + Z3_get_smtlib_num_assumptions @290 + Z3_get_smtlib_assumption @291 + Z3_get_smtlib_num_decls @292 + Z3_get_smtlib_decl @293 + Z3_get_smtlib_num_sorts @294 + Z3_get_smtlib_sort @295 + Z3_get_smtlib_error @296 + Z3_parse_z3_string @297 + Z3_parse_z3_file @298 + Z3_get_error_code @299 + Z3_set_error_handler @300 + Z3_set_error @301 + Z3_get_error_msg @302 + Z3_get_error_msg_ex @303 + Z3_get_version @304 + Z3_reset_memory @305 + Z3_mk_theory @306 + Z3_theory_get_ext_data @307 + Z3_theory_mk_sort @308 + Z3_theory_mk_value @309 + Z3_theory_mk_constant @310 + Z3_theory_mk_func_decl @311 + Z3_theory_get_context @312 + Z3_set_delete_callback @313 + Z3_set_reduce_app_callback @314 + Z3_set_reduce_eq_callback @315 + Z3_set_reduce_distinct_callback @316 + Z3_set_new_app_callback @317 + Z3_set_new_elem_callback @318 + Z3_set_init_search_callback @319 + Z3_set_push_callback @320 + Z3_set_pop_callback @321 + Z3_set_restart_callback @322 + Z3_set_reset_callback @323 + Z3_set_final_check_callback @324 + Z3_set_new_eq_callback @325 + Z3_set_new_diseq_callback @326 + Z3_set_new_assignment_callback @327 + Z3_set_new_relevant_callback @328 + Z3_theory_assert_axiom @329 + Z3_theory_assume_eq @330 + Z3_theory_enable_axiom_simplification @331 + Z3_theory_get_eqc_root @332 + Z3_theory_get_eqc_next @333 + Z3_theory_get_num_parents @334 + Z3_theory_get_parent @335 + Z3_theory_is_value @336 + Z3_theory_is_decl @337 + Z3_theory_get_num_elems @338 + Z3_theory_get_elem @339 + Z3_theory_get_num_apps @340 + Z3_theory_get_app @341 + Z3_mk_fixedpoint @342 + Z3_fixedpoint_inc_ref @343 + Z3_fixedpoint_dec_ref @344 + Z3_fixedpoint_add_rule @345 + Z3_fixedpoint_add_fact @346 + Z3_fixedpoint_assert @347 + Z3_fixedpoint_query @348 + Z3_fixedpoint_query_relations @349 + Z3_fixedpoint_get_answer @350 + Z3_fixedpoint_get_reason_unknown @351 + Z3_fixedpoint_update_rule @352 + Z3_fixedpoint_get_num_levels @353 + Z3_fixedpoint_get_cover_delta @354 + Z3_fixedpoint_add_cover @355 + Z3_fixedpoint_get_statistics @356 + Z3_fixedpoint_register_relation @357 + Z3_fixedpoint_set_predicate_representation @358 + Z3_fixedpoint_simplify_rules @359 + Z3_fixedpoint_set_params @360 + Z3_fixedpoint_get_help @361 + Z3_fixedpoint_get_param_descrs @362 + Z3_fixedpoint_to_string @363 + Z3_fixedpoint_push @364 + Z3_fixedpoint_pop @365 + Z3_fixedpoint_init @366 + Z3_fixedpoint_set_reduce_assign_callback @367 + Z3_fixedpoint_set_reduce_app_callback @368 + Z3_mk_ast_vector @369 + Z3_ast_vector_inc_ref @370 + Z3_ast_vector_dec_ref @371 + Z3_ast_vector_size @372 + Z3_ast_vector_get @373 + Z3_ast_vector_set @374 + Z3_ast_vector_resize @375 + Z3_ast_vector_push @376 + Z3_ast_vector_translate @377 + Z3_ast_vector_to_string @378 + Z3_mk_ast_map @379 + Z3_ast_map_inc_ref @380 + Z3_ast_map_dec_ref @381 + Z3_ast_map_contains @382 + Z3_ast_map_find @383 + Z3_ast_map_insert @384 + Z3_ast_map_erase @385 + Z3_ast_map_reset @386 + Z3_ast_map_size @387 + Z3_ast_map_keys @388 + Z3_ast_map_to_string @389 + Z3_mk_goal @390 + Z3_goal_inc_ref @391 + Z3_goal_dec_ref @392 + Z3_goal_precision @393 + Z3_goal_assert @394 + Z3_goal_inconsistent @395 + Z3_goal_depth @396 + Z3_goal_reset @397 + Z3_goal_size @398 + Z3_goal_formula @399 + Z3_goal_num_exprs @400 + Z3_goal_is_decided_sat @401 + Z3_goal_is_decided_unsat @402 + Z3_goal_translate @403 + Z3_goal_to_string @404 + Z3_mk_tactic @405 + Z3_tactic_inc_ref @406 + Z3_tactic_dec_ref @407 + Z3_mk_probe @408 + Z3_probe_inc_ref @409 + Z3_probe_dec_ref @410 + Z3_tactic_and_then @411 + Z3_tactic_or_else @412 + Z3_tactic_par_or @413 + Z3_tactic_par_and_then @414 + Z3_tactic_try_for @415 + Z3_tactic_when @416 + Z3_tactic_cond @417 + Z3_tactic_repeat @418 + Z3_tactic_skip @419 + Z3_tactic_fail @420 + Z3_tactic_fail_if @421 + Z3_tactic_fail_if_not_decided @422 + Z3_tactic_using_params @423 + Z3_probe_const @424 + Z3_probe_lt @425 + Z3_probe_gt @426 + Z3_probe_le @427 + Z3_probe_ge @428 + Z3_probe_eq @429 + Z3_probe_and @430 + Z3_probe_or @431 + Z3_probe_not @432 + Z3_get_num_tactics @433 + Z3_get_tactic_name @434 + Z3_get_num_probes @435 + Z3_get_probe_name @436 + Z3_tactic_get_help @437 + Z3_tactic_get_param_descrs @438 + Z3_tactic_get_descr @439 + Z3_probe_get_descr @440 + Z3_probe_apply @441 + Z3_tactic_apply @442 + Z3_tactic_apply_ex @443 + Z3_apply_result_inc_ref @444 + Z3_apply_result_dec_ref @445 + Z3_apply_result_to_string @446 + Z3_apply_result_get_num_subgoals @447 + Z3_apply_result_get_subgoal @448 + Z3_apply_result_convert_model @449 + Z3_mk_solver @450 + Z3_mk_simple_solver @451 + Z3_mk_solver_for_logic @452 + Z3_mk_solver_from_tactic @453 + Z3_solver_get_help @454 + Z3_solver_get_param_descrs @455 + Z3_solver_set_params @456 + Z3_solver_inc_ref @457 + Z3_solver_dec_ref @458 + Z3_solver_push @459 + Z3_solver_pop @460 + Z3_solver_reset @461 + Z3_solver_get_num_scopes @462 + Z3_solver_assert @463 + Z3_solver_get_assertions @464 + Z3_solver_check @465 + Z3_solver_check_assumptions @466 + Z3_solver_get_model @467 + Z3_solver_get_proof @468 + Z3_solver_get_unsat_core @469 + Z3_solver_get_reason_unknown @470 + Z3_solver_get_statistics @471 + Z3_solver_to_string @472 + Z3_stats_to_string @473 + Z3_stats_inc_ref @474 + Z3_stats_dec_ref @475 + Z3_stats_size @476 + Z3_stats_get_key @477 + Z3_stats_is_uint @478 + Z3_stats_is_double @479 + Z3_stats_get_uint_value @480 + Z3_stats_get_double_value @481 + Z3_mk_injective_function @482 + Z3_set_logic @483 + Z3_push @484 + Z3_pop @485 + Z3_get_num_scopes @486 + Z3_persist_ast @487 + Z3_assert_cnstr @488 + Z3_check_and_get_model @489 + Z3_check @490 + Z3_check_assumptions @491 + Z3_get_implied_equalities @492 + Z3_del_model @493 + Z3_soft_check_cancel @494 + Z3_get_search_failure @495 + Z3_mk_label @496 + Z3_get_relevant_labels @497 + Z3_get_relevant_literals @498 + Z3_get_guessed_literals @499 + Z3_del_literals @500 + Z3_get_num_literals @501 + Z3_get_label_symbol @502 + Z3_get_literal @503 + Z3_disable_literal @504 + Z3_block_literals @505 + Z3_get_model_num_constants @506 + Z3_get_model_constant @507 + Z3_get_model_num_funcs @508 + Z3_get_model_func_decl @509 + Z3_eval_func_decl @510 + Z3_is_array_value @511 + Z3_get_array_value @512 + Z3_get_model_func_else @513 + Z3_get_model_func_num_entries @514 + Z3_get_model_func_entry_num_args @515 + Z3_get_model_func_entry_arg @516 + Z3_get_model_func_entry_value @517 + Z3_eval @518 + Z3_eval_decl @519 + Z3_context_to_string @520 + Z3_statistics_to_string @521 + Z3_get_context_assignment @522 + Z3_mk_polynomial_manager @1 + Z3_del_polynomial_manager @2 + Z3_mk_zero_polynomial @3 + Z3_polynomial_inc_ref @4 + Z3_polynomial_dec_ref @5 + Z3_polynomial_to_string @6 diff --git a/dll/z3_dbg.def b/dll/z3_dbg.def index 1de8e7e31..00091abd3 100644 --- a/dll/z3_dbg.def +++ b/dll/z3_dbg.def @@ -1,522 +1,528 @@ LIBRARY "Z3_DBG" EXPORTS - Z3_mk_config @1 - Z3_del_config @2 - Z3_set_param_value @3 - Z3_mk_context @4 - Z3_mk_context_rc @5 - Z3_del_context @6 - Z3_inc_ref @7 - Z3_dec_ref @8 - Z3_update_param_value @9 - Z3_get_param_value @10 - Z3_interrupt @11 - Z3_mk_params @12 - Z3_params_inc_ref @13 - Z3_params_dec_ref @14 - Z3_params_set_bool @15 - Z3_params_set_uint @16 - Z3_params_set_double @17 - Z3_params_set_symbol @18 - Z3_params_to_string @19 - Z3_params_validate @20 - Z3_param_descrs_inc_ref @21 - Z3_param_descrs_dec_ref @22 - Z3_param_descrs_get_kind @23 - Z3_param_descrs_size @24 - Z3_param_descrs_get_name @25 - Z3_param_descrs_to_string @26 - Z3_mk_int_symbol @27 - Z3_mk_string_symbol @28 - Z3_mk_uninterpreted_sort @29 - Z3_mk_bool_sort @30 - Z3_mk_int_sort @31 - Z3_mk_real_sort @32 - Z3_mk_bv_sort @33 - Z3_mk_finite_domain_sort @34 - Z3_mk_array_sort @35 - Z3_mk_tuple_sort @36 - Z3_mk_enumeration_sort @37 - Z3_mk_list_sort @38 - Z3_mk_constructor @39 - Z3_del_constructor @40 - Z3_mk_datatype @41 - Z3_mk_constructor_list @42 - Z3_del_constructor_list @43 - Z3_mk_datatypes @44 - Z3_query_constructor @45 - Z3_mk_func_decl @46 - Z3_mk_app @47 - Z3_mk_const @48 - Z3_mk_fresh_func_decl @49 - Z3_mk_fresh_const @50 - Z3_mk_true @51 - Z3_mk_false @52 - Z3_mk_eq @53 - Z3_mk_distinct @54 - Z3_mk_not @55 - Z3_mk_ite @56 - Z3_mk_iff @57 - Z3_mk_implies @58 - Z3_mk_xor @59 - Z3_mk_and @60 - Z3_mk_or @61 - Z3_mk_add @62 - Z3_mk_mul @63 - Z3_mk_sub @64 - Z3_mk_unary_minus @65 - Z3_mk_div @66 - Z3_mk_mod @67 - Z3_mk_rem @68 - Z3_mk_power @69 - Z3_mk_lt @70 - Z3_mk_le @71 - Z3_mk_gt @72 - Z3_mk_ge @73 - Z3_mk_int2real @74 - Z3_mk_real2int @75 - Z3_mk_is_int @76 - Z3_mk_bvnot @77 - Z3_mk_bvredand @78 - Z3_mk_bvredor @79 - Z3_mk_bvand @80 - Z3_mk_bvor @81 - Z3_mk_bvxor @82 - Z3_mk_bvnand @83 - Z3_mk_bvnor @84 - Z3_mk_bvxnor @85 - Z3_mk_bvneg @86 - Z3_mk_bvadd @87 - Z3_mk_bvsub @88 - Z3_mk_bvmul @89 - Z3_mk_bvudiv @90 - Z3_mk_bvsdiv @91 - Z3_mk_bvurem @92 - Z3_mk_bvsrem @93 - Z3_mk_bvsmod @94 - Z3_mk_bvult @95 - Z3_mk_bvslt @96 - Z3_mk_bvule @97 - Z3_mk_bvsle @98 - Z3_mk_bvuge @99 - Z3_mk_bvsge @100 - Z3_mk_bvugt @101 - Z3_mk_bvsgt @102 - Z3_mk_concat @103 - Z3_mk_extract @104 - Z3_mk_sign_ext @105 - Z3_mk_zero_ext @106 - Z3_mk_repeat @107 - Z3_mk_bvshl @108 - Z3_mk_bvlshr @109 - Z3_mk_bvashr @110 - Z3_mk_rotate_left @111 - Z3_mk_rotate_right @112 - Z3_mk_ext_rotate_left @113 - Z3_mk_ext_rotate_right @114 - Z3_mk_int2bv @115 - Z3_mk_bv2int @116 - Z3_mk_bvadd_no_overflow @117 - Z3_mk_bvadd_no_underflow @118 - Z3_mk_bvsub_no_overflow @119 - Z3_mk_bvsub_no_underflow @120 - Z3_mk_bvsdiv_no_overflow @121 - Z3_mk_bvneg_no_overflow @122 - Z3_mk_bvmul_no_overflow @123 - Z3_mk_bvmul_no_underflow @124 - Z3_mk_select @125 - Z3_mk_store @126 - Z3_mk_const_array @127 - Z3_mk_map @128 - Z3_mk_array_default @129 - Z3_mk_set_sort @130 - Z3_mk_empty_set @131 - Z3_mk_full_set @132 - Z3_mk_set_add @133 - Z3_mk_set_del @134 - Z3_mk_set_union @135 - Z3_mk_set_intersect @136 - Z3_mk_set_difference @137 - Z3_mk_set_complement @138 - Z3_mk_set_member @139 - Z3_mk_set_subset @140 - Z3_mk_numeral @141 - Z3_mk_real @142 - Z3_mk_int @143 - Z3_mk_unsigned_int @144 - Z3_mk_int64 @145 - Z3_mk_unsigned_int64 @146 - Z3_mk_pattern @147 - Z3_mk_bound @148 - Z3_mk_forall @149 - Z3_mk_exists @150 - Z3_mk_quantifier @151 - Z3_mk_quantifier_ex @152 - Z3_mk_forall_const @153 - Z3_mk_exists_const @154 - Z3_mk_quantifier_const @155 - Z3_mk_quantifier_const_ex @156 - Z3_get_symbol_kind @157 - Z3_get_symbol_int @158 - Z3_get_symbol_string @159 - Z3_get_sort_name @160 - Z3_get_sort_id @161 - Z3_sort_to_ast @162 - Z3_is_eq_sort @163 - Z3_get_sort_kind @164 - Z3_get_bv_sort_size @165 - Z3_get_finite_domain_sort_size @166 - Z3_get_array_sort_domain @167 - Z3_get_array_sort_range @168 - Z3_get_tuple_sort_mk_decl @169 - Z3_get_tuple_sort_num_fields @170 - Z3_get_tuple_sort_field_decl @171 - Z3_get_datatype_sort_num_constructors @172 - Z3_get_datatype_sort_constructor @173 - Z3_get_datatype_sort_recognizer @174 - Z3_get_datatype_sort_constructor_accessor @175 - Z3_get_relation_arity @176 - Z3_get_relation_column @177 - Z3_func_decl_to_ast @178 - Z3_is_eq_func_decl @179 - Z3_get_func_decl_id @180 - Z3_get_decl_name @181 - Z3_get_decl_kind @182 - Z3_get_domain_size @183 - Z3_get_arity @184 - Z3_get_domain @185 - Z3_get_range @186 - Z3_get_decl_num_parameters @187 - Z3_get_decl_parameter_kind @188 - Z3_get_decl_int_parameter @189 - Z3_get_decl_double_parameter @190 - Z3_get_decl_symbol_parameter @191 - Z3_get_decl_sort_parameter @192 - Z3_get_decl_ast_parameter @193 - Z3_get_decl_func_decl_parameter @194 - Z3_get_decl_rational_parameter @195 - Z3_app_to_ast @196 - Z3_get_app_decl @197 - Z3_get_app_num_args @198 - Z3_get_app_arg @199 - Z3_is_eq_ast @200 - Z3_get_ast_id @201 - Z3_get_ast_hash @202 - Z3_get_sort @203 - Z3_is_well_sorted @204 - Z3_get_bool_value @205 - Z3_get_ast_kind @206 - Z3_is_app @207 - Z3_is_numeral_ast @208 - Z3_is_algebraic_number @209 - Z3_to_app @210 - Z3_to_func_decl @211 - Z3_get_numeral_string @212 - Z3_get_numeral_decimal_string @213 - Z3_get_numerator @214 - Z3_get_denominator @215 - Z3_get_numeral_small @216 - Z3_get_numeral_int @217 - Z3_get_numeral_uint @218 - Z3_get_numeral_uint64 @219 - Z3_get_numeral_int64 @220 - Z3_get_numeral_rational_int64 @221 - Z3_get_algebraic_number_lower @222 - Z3_get_algebraic_number_upper @223 - Z3_pattern_to_ast @224 - Z3_get_pattern_num_terms @225 - Z3_get_pattern @226 - Z3_get_index_value @227 - Z3_is_quantifier_forall @228 - Z3_get_quantifier_weight @229 - Z3_get_quantifier_num_patterns @230 - Z3_get_quantifier_pattern_ast @231 - Z3_get_quantifier_num_no_patterns @232 - Z3_get_quantifier_no_pattern_ast @233 - Z3_get_quantifier_num_bound @234 - Z3_get_quantifier_bound_name @235 - Z3_get_quantifier_bound_sort @236 - Z3_get_quantifier_body @237 - Z3_simplify @238 - Z3_simplify_ex @239 - Z3_simplify_get_help @240 - Z3_simplify_get_param_descrs @241 - Z3_update_term @242 - Z3_substitute @243 - Z3_substitute_vars @244 - Z3_translate @245 - Z3_model_inc_ref @246 - Z3_model_dec_ref @247 - Z3_model_eval @248 - Z3_model_get_const_interp @249 - Z3_model_get_func_interp @250 - Z3_model_get_num_consts @251 - Z3_model_get_const_decl @252 - Z3_model_get_num_funcs @253 - Z3_model_get_func_decl @254 - Z3_model_get_num_sorts @255 - Z3_model_get_sort @256 - Z3_model_get_sort_universe @257 - Z3_is_as_array @258 - Z3_get_as_array_func_decl @259 - Z3_func_interp_inc_ref @260 - Z3_func_interp_dec_ref @261 - Z3_func_interp_get_num_entries @262 - Z3_func_interp_get_entry @263 - Z3_func_interp_get_else @264 - Z3_func_interp_get_arity @265 - Z3_func_entry_inc_ref @266 - Z3_func_entry_dec_ref @267 - Z3_func_entry_get_value @268 - Z3_func_entry_get_num_args @269 - Z3_func_entry_get_arg @270 - Z3_open_log @271 - Z3_append_log @272 - Z3_close_log @273 - Z3_toggle_warning_messages @274 - Z3_set_ast_print_mode @275 - Z3_ast_to_string @276 - Z3_pattern_to_string @277 - Z3_sort_to_string @278 - Z3_func_decl_to_string @279 - Z3_model_to_string @280 - Z3_benchmark_to_smtlib_string @281 - Z3_parse_smtlib2_string @282 - Z3_parse_smtlib2_file @283 - Z3_parse_smtlib_string @284 - Z3_parse_smtlib_file @285 - Z3_get_smtlib_num_formulas @286 - Z3_get_smtlib_formula @287 - Z3_get_smtlib_num_assumptions @288 - Z3_get_smtlib_assumption @289 - Z3_get_smtlib_num_decls @290 - Z3_get_smtlib_decl @291 - Z3_get_smtlib_num_sorts @292 - Z3_get_smtlib_sort @293 - Z3_get_smtlib_error @294 - Z3_parse_z3_string @295 - Z3_parse_z3_file @296 - Z3_get_error_code @297 - Z3_set_error_handler @298 - Z3_set_error @299 - Z3_get_error_msg @300 - Z3_get_error_msg_ex @301 - Z3_get_version @302 - Z3_reset_memory @303 - Z3_mk_theory @304 - Z3_theory_get_ext_data @305 - Z3_theory_mk_sort @306 - Z3_theory_mk_value @307 - Z3_theory_mk_constant @308 - Z3_theory_mk_func_decl @309 - Z3_theory_get_context @310 - Z3_set_delete_callback @311 - Z3_set_reduce_app_callback @312 - Z3_set_reduce_eq_callback @313 - Z3_set_reduce_distinct_callback @314 - Z3_set_new_app_callback @315 - Z3_set_new_elem_callback @316 - Z3_set_init_search_callback @317 - Z3_set_push_callback @318 - Z3_set_pop_callback @319 - Z3_set_restart_callback @320 - Z3_set_reset_callback @321 - Z3_set_final_check_callback @322 - Z3_set_new_eq_callback @323 - Z3_set_new_diseq_callback @324 - Z3_set_new_assignment_callback @325 - Z3_set_new_relevant_callback @326 - Z3_theory_assert_axiom @327 - Z3_theory_assume_eq @328 - Z3_theory_enable_axiom_simplification @329 - Z3_theory_get_eqc_root @330 - Z3_theory_get_eqc_next @331 - Z3_theory_get_num_parents @332 - Z3_theory_get_parent @333 - Z3_theory_is_value @334 - Z3_theory_is_decl @335 - Z3_theory_get_num_elems @336 - Z3_theory_get_elem @337 - Z3_theory_get_num_apps @338 - Z3_theory_get_app @339 - Z3_mk_fixedpoint @340 - Z3_fixedpoint_inc_ref @341 - Z3_fixedpoint_dec_ref @342 - Z3_fixedpoint_add_rule @343 - Z3_fixedpoint_add_fact @344 - Z3_fixedpoint_assert @345 - Z3_fixedpoint_query @346 - Z3_fixedpoint_query_relations @347 - Z3_fixedpoint_get_answer @348 - Z3_fixedpoint_get_reason_unknown @349 - Z3_fixedpoint_update_rule @350 - Z3_fixedpoint_get_num_levels @351 - Z3_fixedpoint_get_cover_delta @352 - Z3_fixedpoint_add_cover @353 - Z3_fixedpoint_get_statistics @354 - Z3_fixedpoint_register_relation @355 - Z3_fixedpoint_set_predicate_representation @356 - Z3_fixedpoint_simplify_rules @357 - Z3_fixedpoint_set_params @358 - Z3_fixedpoint_get_help @359 - Z3_fixedpoint_get_param_descrs @360 - Z3_fixedpoint_to_string @361 - Z3_fixedpoint_push @362 - Z3_fixedpoint_pop @363 - Z3_fixedpoint_init @364 - Z3_fixedpoint_set_reduce_assign_callback @365 - Z3_fixedpoint_set_reduce_app_callback @366 - Z3_mk_ast_vector @367 - Z3_ast_vector_inc_ref @368 - Z3_ast_vector_dec_ref @369 - Z3_ast_vector_size @370 - Z3_ast_vector_get @371 - Z3_ast_vector_set @372 - Z3_ast_vector_resize @373 - Z3_ast_vector_push @374 - Z3_ast_vector_translate @375 - Z3_ast_vector_to_string @376 - Z3_mk_ast_map @377 - Z3_ast_map_inc_ref @378 - Z3_ast_map_dec_ref @379 - Z3_ast_map_contains @380 - Z3_ast_map_find @381 - Z3_ast_map_insert @382 - Z3_ast_map_erase @383 - Z3_ast_map_reset @384 - Z3_ast_map_size @385 - Z3_ast_map_keys @386 - Z3_ast_map_to_string @387 - Z3_mk_goal @388 - Z3_goal_inc_ref @389 - Z3_goal_dec_ref @390 - Z3_goal_precision @391 - Z3_goal_assert @392 - Z3_goal_inconsistent @393 - Z3_goal_depth @394 - Z3_goal_reset @395 - Z3_goal_size @396 - Z3_goal_formula @397 - Z3_goal_num_exprs @398 - Z3_goal_is_decided_sat @399 - Z3_goal_is_decided_unsat @400 - Z3_goal_translate @401 - Z3_goal_to_string @402 - Z3_mk_tactic @403 - Z3_tactic_inc_ref @404 - Z3_tactic_dec_ref @405 - Z3_mk_probe @406 - Z3_probe_inc_ref @407 - Z3_probe_dec_ref @408 - Z3_tactic_and_then @409 - Z3_tactic_or_else @410 - Z3_tactic_par_or @411 - Z3_tactic_par_and_then @412 - Z3_tactic_try_for @413 - Z3_tactic_when @414 - Z3_tactic_cond @415 - Z3_tactic_repeat @416 - Z3_tactic_skip @417 - Z3_tactic_fail @418 - Z3_tactic_fail_if @419 - Z3_tactic_fail_if_not_decided @420 - Z3_tactic_using_params @421 - Z3_probe_const @422 - Z3_probe_lt @423 - Z3_probe_gt @424 - Z3_probe_le @425 - Z3_probe_ge @426 - Z3_probe_eq @427 - Z3_probe_and @428 - Z3_probe_or @429 - Z3_probe_not @430 - Z3_get_num_tactics @431 - Z3_get_tactic_name @432 - Z3_get_num_probes @433 - Z3_get_probe_name @434 - Z3_tactic_get_help @435 - Z3_tactic_get_param_descrs @436 - Z3_tactic_get_descr @437 - Z3_probe_get_descr @438 - Z3_probe_apply @439 - Z3_tactic_apply @440 - Z3_tactic_apply_ex @441 - Z3_apply_result_inc_ref @442 - Z3_apply_result_dec_ref @443 - Z3_apply_result_to_string @444 - Z3_apply_result_get_num_subgoals @445 - Z3_apply_result_get_subgoal @446 - Z3_apply_result_convert_model @447 - Z3_mk_solver @448 - Z3_mk_simple_solver @449 - Z3_mk_solver_for_logic @450 - Z3_mk_solver_from_tactic @451 - Z3_solver_get_help @452 - Z3_solver_get_param_descrs @453 - Z3_solver_set_params @454 - Z3_solver_inc_ref @455 - Z3_solver_dec_ref @456 - Z3_solver_push @457 - Z3_solver_pop @458 - Z3_solver_reset @459 - Z3_solver_get_num_scopes @460 - Z3_solver_assert @461 - Z3_solver_get_assertions @462 - Z3_solver_check @463 - Z3_solver_check_assumptions @464 - Z3_solver_get_model @465 - Z3_solver_get_proof @466 - Z3_solver_get_unsat_core @467 - Z3_solver_get_reason_unknown @468 - Z3_solver_get_statistics @469 - Z3_solver_to_string @470 - Z3_stats_to_string @471 - Z3_stats_inc_ref @472 - Z3_stats_dec_ref @473 - Z3_stats_size @474 - Z3_stats_get_key @475 - Z3_stats_is_uint @476 - Z3_stats_is_double @477 - Z3_stats_get_uint_value @478 - Z3_stats_get_double_value @479 - Z3_mk_injective_function @480 - Z3_set_logic @481 - Z3_push @482 - Z3_pop @483 - Z3_get_num_scopes @484 - Z3_persist_ast @485 - Z3_assert_cnstr @486 - Z3_check_and_get_model @487 - Z3_check @488 - Z3_check_assumptions @489 - Z3_get_implied_equalities @490 - Z3_del_model @491 - Z3_soft_check_cancel @492 - Z3_get_search_failure @493 - Z3_mk_label @494 - Z3_get_relevant_labels @495 - Z3_get_relevant_literals @496 - Z3_get_guessed_literals @497 - Z3_del_literals @498 - Z3_get_num_literals @499 - Z3_get_label_symbol @500 - Z3_get_literal @501 - Z3_disable_literal @502 - Z3_block_literals @503 - Z3_get_model_num_constants @504 - Z3_get_model_constant @505 - Z3_get_model_num_funcs @506 - Z3_get_model_func_decl @507 - Z3_eval_func_decl @508 - Z3_is_array_value @509 - Z3_get_array_value @510 - Z3_get_model_func_else @511 - Z3_get_model_func_num_entries @512 - Z3_get_model_func_entry_num_args @513 - Z3_get_model_func_entry_arg @514 - Z3_get_model_func_entry_value @515 - Z3_eval @516 - Z3_eval_decl @517 - Z3_context_to_string @518 - Z3_statistics_to_string @519 - Z3_get_context_assignment @520 + Z3_mk_config @3 + Z3_del_config @4 + Z3_set_param_value @5 + Z3_mk_context @6 + Z3_mk_context_rc @7 + Z3_del_context @8 + Z3_inc_ref @9 + Z3_dec_ref @10 + Z3_update_param_value @11 + Z3_get_param_value @12 + Z3_interrupt @13 + Z3_mk_params @14 + Z3_params_inc_ref @15 + Z3_params_dec_ref @16 + Z3_params_set_bool @17 + Z3_params_set_uint @18 + Z3_params_set_double @19 + Z3_params_set_symbol @20 + Z3_params_to_string @21 + Z3_params_validate @22 + Z3_param_descrs_inc_ref @23 + Z3_param_descrs_dec_ref @24 + Z3_param_descrs_get_kind @25 + Z3_param_descrs_size @26 + Z3_param_descrs_get_name @27 + Z3_param_descrs_to_string @28 + Z3_mk_int_symbol @29 + Z3_mk_string_symbol @30 + Z3_mk_uninterpreted_sort @31 + Z3_mk_bool_sort @32 + Z3_mk_int_sort @33 + Z3_mk_real_sort @34 + Z3_mk_bv_sort @35 + Z3_mk_finite_domain_sort @36 + Z3_mk_array_sort @37 + Z3_mk_tuple_sort @38 + Z3_mk_enumeration_sort @39 + Z3_mk_list_sort @40 + Z3_mk_constructor @41 + Z3_del_constructor @42 + Z3_mk_datatype @43 + Z3_mk_constructor_list @44 + Z3_del_constructor_list @45 + Z3_mk_datatypes @46 + Z3_query_constructor @47 + Z3_mk_func_decl @48 + Z3_mk_app @49 + Z3_mk_const @50 + Z3_mk_fresh_func_decl @51 + Z3_mk_fresh_const @52 + Z3_mk_true @53 + Z3_mk_false @54 + Z3_mk_eq @55 + Z3_mk_distinct @56 + Z3_mk_not @57 + Z3_mk_ite @58 + Z3_mk_iff @59 + Z3_mk_implies @60 + Z3_mk_xor @61 + Z3_mk_and @62 + Z3_mk_or @63 + Z3_mk_add @64 + Z3_mk_mul @65 + Z3_mk_sub @66 + Z3_mk_unary_minus @67 + Z3_mk_div @68 + Z3_mk_mod @69 + Z3_mk_rem @70 + Z3_mk_power @71 + Z3_mk_lt @72 + Z3_mk_le @73 + Z3_mk_gt @74 + Z3_mk_ge @75 + Z3_mk_int2real @76 + Z3_mk_real2int @77 + Z3_mk_is_int @78 + Z3_mk_bvnot @79 + Z3_mk_bvredand @80 + Z3_mk_bvredor @81 + Z3_mk_bvand @82 + Z3_mk_bvor @83 + Z3_mk_bvxor @84 + Z3_mk_bvnand @85 + Z3_mk_bvnor @86 + Z3_mk_bvxnor @87 + Z3_mk_bvneg @88 + Z3_mk_bvadd @89 + Z3_mk_bvsub @90 + Z3_mk_bvmul @91 + Z3_mk_bvudiv @92 + Z3_mk_bvsdiv @93 + Z3_mk_bvurem @94 + Z3_mk_bvsrem @95 + Z3_mk_bvsmod @96 + Z3_mk_bvult @97 + Z3_mk_bvslt @98 + Z3_mk_bvule @99 + Z3_mk_bvsle @100 + Z3_mk_bvuge @101 + Z3_mk_bvsge @102 + Z3_mk_bvugt @103 + Z3_mk_bvsgt @104 + Z3_mk_concat @105 + Z3_mk_extract @106 + Z3_mk_sign_ext @107 + Z3_mk_zero_ext @108 + Z3_mk_repeat @109 + Z3_mk_bvshl @110 + Z3_mk_bvlshr @111 + Z3_mk_bvashr @112 + Z3_mk_rotate_left @113 + Z3_mk_rotate_right @114 + Z3_mk_ext_rotate_left @115 + Z3_mk_ext_rotate_right @116 + Z3_mk_int2bv @117 + Z3_mk_bv2int @118 + Z3_mk_bvadd_no_overflow @119 + Z3_mk_bvadd_no_underflow @120 + Z3_mk_bvsub_no_overflow @121 + Z3_mk_bvsub_no_underflow @122 + Z3_mk_bvsdiv_no_overflow @123 + Z3_mk_bvneg_no_overflow @124 + Z3_mk_bvmul_no_overflow @125 + Z3_mk_bvmul_no_underflow @126 + Z3_mk_select @127 + Z3_mk_store @128 + Z3_mk_const_array @129 + Z3_mk_map @130 + Z3_mk_array_default @131 + Z3_mk_set_sort @132 + Z3_mk_empty_set @133 + Z3_mk_full_set @134 + Z3_mk_set_add @135 + Z3_mk_set_del @136 + Z3_mk_set_union @137 + Z3_mk_set_intersect @138 + Z3_mk_set_difference @139 + Z3_mk_set_complement @140 + Z3_mk_set_member @141 + Z3_mk_set_subset @142 + Z3_mk_numeral @143 + Z3_mk_real @144 + Z3_mk_int @145 + Z3_mk_unsigned_int @146 + Z3_mk_int64 @147 + Z3_mk_unsigned_int64 @148 + Z3_mk_pattern @149 + Z3_mk_bound @150 + Z3_mk_forall @151 + Z3_mk_exists @152 + Z3_mk_quantifier @153 + Z3_mk_quantifier_ex @154 + Z3_mk_forall_const @155 + Z3_mk_exists_const @156 + Z3_mk_quantifier_const @157 + Z3_mk_quantifier_const_ex @158 + Z3_get_symbol_kind @159 + Z3_get_symbol_int @160 + Z3_get_symbol_string @161 + Z3_get_sort_name @162 + Z3_get_sort_id @163 + Z3_sort_to_ast @164 + Z3_is_eq_sort @165 + Z3_get_sort_kind @166 + Z3_get_bv_sort_size @167 + Z3_get_finite_domain_sort_size @168 + Z3_get_array_sort_domain @169 + Z3_get_array_sort_range @170 + Z3_get_tuple_sort_mk_decl @171 + Z3_get_tuple_sort_num_fields @172 + Z3_get_tuple_sort_field_decl @173 + Z3_get_datatype_sort_num_constructors @174 + Z3_get_datatype_sort_constructor @175 + Z3_get_datatype_sort_recognizer @176 + Z3_get_datatype_sort_constructor_accessor @177 + Z3_get_relation_arity @178 + Z3_get_relation_column @179 + Z3_func_decl_to_ast @180 + Z3_is_eq_func_decl @181 + Z3_get_func_decl_id @182 + Z3_get_decl_name @183 + Z3_get_decl_kind @184 + Z3_get_domain_size @185 + Z3_get_arity @186 + Z3_get_domain @187 + Z3_get_range @188 + Z3_get_decl_num_parameters @189 + Z3_get_decl_parameter_kind @190 + Z3_get_decl_int_parameter @191 + Z3_get_decl_double_parameter @192 + Z3_get_decl_symbol_parameter @193 + Z3_get_decl_sort_parameter @194 + Z3_get_decl_ast_parameter @195 + Z3_get_decl_func_decl_parameter @196 + Z3_get_decl_rational_parameter @197 + Z3_app_to_ast @198 + Z3_get_app_decl @199 + Z3_get_app_num_args @200 + Z3_get_app_arg @201 + Z3_is_eq_ast @202 + Z3_get_ast_id @203 + Z3_get_ast_hash @204 + Z3_get_sort @205 + Z3_is_well_sorted @206 + Z3_get_bool_value @207 + Z3_get_ast_kind @208 + Z3_is_app @209 + Z3_is_numeral_ast @210 + Z3_is_algebraic_number @211 + Z3_to_app @212 + Z3_to_func_decl @213 + Z3_get_numeral_string @214 + Z3_get_numeral_decimal_string @215 + Z3_get_numerator @216 + Z3_get_denominator @217 + Z3_get_numeral_small @218 + Z3_get_numeral_int @219 + Z3_get_numeral_uint @220 + Z3_get_numeral_uint64 @221 + Z3_get_numeral_int64 @222 + Z3_get_numeral_rational_int64 @223 + Z3_get_algebraic_number_lower @224 + Z3_get_algebraic_number_upper @225 + Z3_pattern_to_ast @226 + Z3_get_pattern_num_terms @227 + Z3_get_pattern @228 + Z3_get_index_value @229 + Z3_is_quantifier_forall @230 + Z3_get_quantifier_weight @231 + Z3_get_quantifier_num_patterns @232 + Z3_get_quantifier_pattern_ast @233 + Z3_get_quantifier_num_no_patterns @234 + Z3_get_quantifier_no_pattern_ast @235 + Z3_get_quantifier_num_bound @236 + Z3_get_quantifier_bound_name @237 + Z3_get_quantifier_bound_sort @238 + Z3_get_quantifier_body @239 + Z3_simplify @240 + Z3_simplify_ex @241 + Z3_simplify_get_help @242 + Z3_simplify_get_param_descrs @243 + Z3_update_term @244 + Z3_substitute @245 + Z3_substitute_vars @246 + Z3_translate @247 + Z3_model_inc_ref @248 + Z3_model_dec_ref @249 + Z3_model_eval @250 + Z3_model_get_const_interp @251 + Z3_model_get_func_interp @252 + Z3_model_get_num_consts @253 + Z3_model_get_const_decl @254 + Z3_model_get_num_funcs @255 + Z3_model_get_func_decl @256 + Z3_model_get_num_sorts @257 + Z3_model_get_sort @258 + Z3_model_get_sort_universe @259 + Z3_is_as_array @260 + Z3_get_as_array_func_decl @261 + Z3_func_interp_inc_ref @262 + Z3_func_interp_dec_ref @263 + Z3_func_interp_get_num_entries @264 + Z3_func_interp_get_entry @265 + Z3_func_interp_get_else @266 + Z3_func_interp_get_arity @267 + Z3_func_entry_inc_ref @268 + Z3_func_entry_dec_ref @269 + Z3_func_entry_get_value @270 + Z3_func_entry_get_num_args @271 + Z3_func_entry_get_arg @272 + Z3_open_log @273 + Z3_append_log @274 + Z3_close_log @275 + Z3_toggle_warning_messages @276 + Z3_set_ast_print_mode @277 + Z3_ast_to_string @278 + Z3_pattern_to_string @279 + Z3_sort_to_string @280 + Z3_func_decl_to_string @281 + Z3_model_to_string @282 + Z3_benchmark_to_smtlib_string @283 + Z3_parse_smtlib2_string @284 + Z3_parse_smtlib2_file @285 + Z3_parse_smtlib_string @286 + Z3_parse_smtlib_file @287 + Z3_get_smtlib_num_formulas @288 + Z3_get_smtlib_formula @289 + Z3_get_smtlib_num_assumptions @290 + Z3_get_smtlib_assumption @291 + Z3_get_smtlib_num_decls @292 + Z3_get_smtlib_decl @293 + Z3_get_smtlib_num_sorts @294 + Z3_get_smtlib_sort @295 + Z3_get_smtlib_error @296 + Z3_parse_z3_string @297 + Z3_parse_z3_file @298 + Z3_get_error_code @299 + Z3_set_error_handler @300 + Z3_set_error @301 + Z3_get_error_msg @302 + Z3_get_error_msg_ex @303 + Z3_get_version @304 + Z3_reset_memory @305 + Z3_mk_theory @306 + Z3_theory_get_ext_data @307 + Z3_theory_mk_sort @308 + Z3_theory_mk_value @309 + Z3_theory_mk_constant @310 + Z3_theory_mk_func_decl @311 + Z3_theory_get_context @312 + Z3_set_delete_callback @313 + Z3_set_reduce_app_callback @314 + Z3_set_reduce_eq_callback @315 + Z3_set_reduce_distinct_callback @316 + Z3_set_new_app_callback @317 + Z3_set_new_elem_callback @318 + Z3_set_init_search_callback @319 + Z3_set_push_callback @320 + Z3_set_pop_callback @321 + Z3_set_restart_callback @322 + Z3_set_reset_callback @323 + Z3_set_final_check_callback @324 + Z3_set_new_eq_callback @325 + Z3_set_new_diseq_callback @326 + Z3_set_new_assignment_callback @327 + Z3_set_new_relevant_callback @328 + Z3_theory_assert_axiom @329 + Z3_theory_assume_eq @330 + Z3_theory_enable_axiom_simplification @331 + Z3_theory_get_eqc_root @332 + Z3_theory_get_eqc_next @333 + Z3_theory_get_num_parents @334 + Z3_theory_get_parent @335 + Z3_theory_is_value @336 + Z3_theory_is_decl @337 + Z3_theory_get_num_elems @338 + Z3_theory_get_elem @339 + Z3_theory_get_num_apps @340 + Z3_theory_get_app @341 + Z3_mk_fixedpoint @342 + Z3_fixedpoint_inc_ref @343 + Z3_fixedpoint_dec_ref @344 + Z3_fixedpoint_add_rule @345 + Z3_fixedpoint_add_fact @346 + Z3_fixedpoint_assert @347 + Z3_fixedpoint_query @348 + Z3_fixedpoint_query_relations @349 + Z3_fixedpoint_get_answer @350 + Z3_fixedpoint_get_reason_unknown @351 + Z3_fixedpoint_update_rule @352 + Z3_fixedpoint_get_num_levels @353 + Z3_fixedpoint_get_cover_delta @354 + Z3_fixedpoint_add_cover @355 + Z3_fixedpoint_get_statistics @356 + Z3_fixedpoint_register_relation @357 + Z3_fixedpoint_set_predicate_representation @358 + Z3_fixedpoint_simplify_rules @359 + Z3_fixedpoint_set_params @360 + Z3_fixedpoint_get_help @361 + Z3_fixedpoint_get_param_descrs @362 + Z3_fixedpoint_to_string @363 + Z3_fixedpoint_push @364 + Z3_fixedpoint_pop @365 + Z3_fixedpoint_init @366 + Z3_fixedpoint_set_reduce_assign_callback @367 + Z3_fixedpoint_set_reduce_app_callback @368 + Z3_mk_ast_vector @369 + Z3_ast_vector_inc_ref @370 + Z3_ast_vector_dec_ref @371 + Z3_ast_vector_size @372 + Z3_ast_vector_get @373 + Z3_ast_vector_set @374 + Z3_ast_vector_resize @375 + Z3_ast_vector_push @376 + Z3_ast_vector_translate @377 + Z3_ast_vector_to_string @378 + Z3_mk_ast_map @379 + Z3_ast_map_inc_ref @380 + Z3_ast_map_dec_ref @381 + Z3_ast_map_contains @382 + Z3_ast_map_find @383 + Z3_ast_map_insert @384 + Z3_ast_map_erase @385 + Z3_ast_map_reset @386 + Z3_ast_map_size @387 + Z3_ast_map_keys @388 + Z3_ast_map_to_string @389 + Z3_mk_goal @390 + Z3_goal_inc_ref @391 + Z3_goal_dec_ref @392 + Z3_goal_precision @393 + Z3_goal_assert @394 + Z3_goal_inconsistent @395 + Z3_goal_depth @396 + Z3_goal_reset @397 + Z3_goal_size @398 + Z3_goal_formula @399 + Z3_goal_num_exprs @400 + Z3_goal_is_decided_sat @401 + Z3_goal_is_decided_unsat @402 + Z3_goal_translate @403 + Z3_goal_to_string @404 + Z3_mk_tactic @405 + Z3_tactic_inc_ref @406 + Z3_tactic_dec_ref @407 + Z3_mk_probe @408 + Z3_probe_inc_ref @409 + Z3_probe_dec_ref @410 + Z3_tactic_and_then @411 + Z3_tactic_or_else @412 + Z3_tactic_par_or @413 + Z3_tactic_par_and_then @414 + Z3_tactic_try_for @415 + Z3_tactic_when @416 + Z3_tactic_cond @417 + Z3_tactic_repeat @418 + Z3_tactic_skip @419 + Z3_tactic_fail @420 + Z3_tactic_fail_if @421 + Z3_tactic_fail_if_not_decided @422 + Z3_tactic_using_params @423 + Z3_probe_const @424 + Z3_probe_lt @425 + Z3_probe_gt @426 + Z3_probe_le @427 + Z3_probe_ge @428 + Z3_probe_eq @429 + Z3_probe_and @430 + Z3_probe_or @431 + Z3_probe_not @432 + Z3_get_num_tactics @433 + Z3_get_tactic_name @434 + Z3_get_num_probes @435 + Z3_get_probe_name @436 + Z3_tactic_get_help @437 + Z3_tactic_get_param_descrs @438 + Z3_tactic_get_descr @439 + Z3_probe_get_descr @440 + Z3_probe_apply @441 + Z3_tactic_apply @442 + Z3_tactic_apply_ex @443 + Z3_apply_result_inc_ref @444 + Z3_apply_result_dec_ref @445 + Z3_apply_result_to_string @446 + Z3_apply_result_get_num_subgoals @447 + Z3_apply_result_get_subgoal @448 + Z3_apply_result_convert_model @449 + Z3_mk_solver @450 + Z3_mk_simple_solver @451 + Z3_mk_solver_for_logic @452 + Z3_mk_solver_from_tactic @453 + Z3_solver_get_help @454 + Z3_solver_get_param_descrs @455 + Z3_solver_set_params @456 + Z3_solver_inc_ref @457 + Z3_solver_dec_ref @458 + Z3_solver_push @459 + Z3_solver_pop @460 + Z3_solver_reset @461 + Z3_solver_get_num_scopes @462 + Z3_solver_assert @463 + Z3_solver_get_assertions @464 + Z3_solver_check @465 + Z3_solver_check_assumptions @466 + Z3_solver_get_model @467 + Z3_solver_get_proof @468 + Z3_solver_get_unsat_core @469 + Z3_solver_get_reason_unknown @470 + Z3_solver_get_statistics @471 + Z3_solver_to_string @472 + Z3_stats_to_string @473 + Z3_stats_inc_ref @474 + Z3_stats_dec_ref @475 + Z3_stats_size @476 + Z3_stats_get_key @477 + Z3_stats_is_uint @478 + Z3_stats_is_double @479 + Z3_stats_get_uint_value @480 + Z3_stats_get_double_value @481 + Z3_mk_injective_function @482 + Z3_set_logic @483 + Z3_push @484 + Z3_pop @485 + Z3_get_num_scopes @486 + Z3_persist_ast @487 + Z3_assert_cnstr @488 + Z3_check_and_get_model @489 + Z3_check @490 + Z3_check_assumptions @491 + Z3_get_implied_equalities @492 + Z3_del_model @493 + Z3_soft_check_cancel @494 + Z3_get_search_failure @495 + Z3_mk_label @496 + Z3_get_relevant_labels @497 + Z3_get_relevant_literals @498 + Z3_get_guessed_literals @499 + Z3_del_literals @500 + Z3_get_num_literals @501 + Z3_get_label_symbol @502 + Z3_get_literal @503 + Z3_disable_literal @504 + Z3_block_literals @505 + Z3_get_model_num_constants @506 + Z3_get_model_constant @507 + Z3_get_model_num_funcs @508 + Z3_get_model_func_decl @509 + Z3_eval_func_decl @510 + Z3_is_array_value @511 + Z3_get_array_value @512 + Z3_get_model_func_else @513 + Z3_get_model_func_num_entries @514 + Z3_get_model_func_entry_num_args @515 + Z3_get_model_func_entry_arg @516 + Z3_get_model_func_entry_value @517 + Z3_eval @518 + Z3_eval_decl @519 + Z3_context_to_string @520 + Z3_statistics_to_string @521 + Z3_get_context_assignment @522 + Z3_mk_polynomial_manager @1 + Z3_del_polynomial_manager @2 + Z3_mk_zero_polynomial @3 + Z3_polynomial_inc_ref @4 + Z3_polynomial_dec_ref @5 + Z3_polynomial_to_string @6 diff --git a/lib/api_ast.cpp b/lib/api_ast.cpp index 425ec26a5..925e69e1f 100644 --- a/lib/api_ast.cpp +++ b/lib/api_ast.cpp @@ -16,7 +16,7 @@ Revision History: --*/ #include -#include"z3.h" +#include"z3_internal.h" #include"api_log_macros.h" #include"api_context.h" #include"api_util.h" diff --git a/lib/api_commands.cpp b/lib/api_commands.cpp index 4b6cd61c5..d36799ec7 100644 --- a/lib/api_commands.cpp +++ b/lib/api_commands.cpp @@ -1,5 +1,6 @@ // Automatically generated file, generator: update_api.py #include"z3.h" +#include"z3_internal.h" #include"z3_replayer.h" void Z3_replacer_error_handler(Z3_context ctx, Z3_error_code c) { printf("[REPLAYER ERROR HANDLER]: %s\n", Z3_get_error_msg_ex(ctx, c)); } void exec_Z3_mk_config(z3_replayer & in) { @@ -3003,6 +3004,40 @@ void exec_Z3_get_context_assignment(z3_replayer & in) { reinterpret_cast(in.get_obj(0))); in.store_result(result); } +void exec_Z3_mk_polynomial_manager(z3_replayer & in) { + Z3_polynomial_manager result = Z3_mk_polynomial_manager( + reinterpret_cast(in.get_obj(0))); + in.store_result(result); +} +void exec_Z3_del_polynomial_manager(z3_replayer & in) { + Z3_del_polynomial_manager( + reinterpret_cast(in.get_obj(0)), + reinterpret_cast(in.get_obj(1))); +} +void exec_Z3_mk_zero_polynomial(z3_replayer & in) { + Z3_polynomial result = Z3_mk_zero_polynomial( + reinterpret_cast(in.get_obj(0)), + reinterpret_cast(in.get_obj(1))); + in.store_result(result); +} +void exec_Z3_polynomial_inc_ref(z3_replayer & in) { + Z3_polynomial_inc_ref( + reinterpret_cast(in.get_obj(0)), + reinterpret_cast(in.get_obj(1)), + reinterpret_cast(in.get_obj(2))); +} +void exec_Z3_polynomial_dec_ref(z3_replayer & in) { + Z3_polynomial_dec_ref( + reinterpret_cast(in.get_obj(0)), + reinterpret_cast(in.get_obj(1)), + reinterpret_cast(in.get_obj(2))); +} +void exec_Z3_polynomial_to_string(z3_replayer & in) { + Z3_polynomial_to_string( + reinterpret_cast(in.get_obj(0)), + reinterpret_cast(in.get_obj(1)), + reinterpret_cast(in.get_obj(2))); +} void register_z3_replayer_cmds(z3_replayer & in) { in.register_cmd(0, exec_Z3_mk_config); in.register_cmd(1, exec_Z3_del_config); @@ -3481,4 +3516,10 @@ void register_z3_replayer_cmds(z3_replayer & in) { in.register_cmd(474, exec_Z3_context_to_string); in.register_cmd(475, exec_Z3_statistics_to_string); in.register_cmd(476, exec_Z3_get_context_assignment); + in.register_cmd(477, exec_Z3_mk_polynomial_manager); + in.register_cmd(478, exec_Z3_del_polynomial_manager); + in.register_cmd(479, exec_Z3_mk_zero_polynomial); + in.register_cmd(480, exec_Z3_polynomial_inc_ref); + in.register_cmd(481, exec_Z3_polynomial_dec_ref); + in.register_cmd(482, exec_Z3_polynomial_to_string); } diff --git a/lib/api_log_macros.cpp b/lib/api_log_macros.cpp index 152b8dd05..d6ab615aa 100644 --- a/lib/api_log_macros.cpp +++ b/lib/api_log_macros.cpp @@ -3315,3 +3315,41 @@ void log_Z3_get_context_assignment(Z3_context a0) { P(a0); C(476); } +void log_Z3_mk_polynomial_manager(Z3_context a0) { + R(); + P(a0); + C(477); +} +void log_Z3_del_polynomial_manager(Z3_context a0, Z3_polynomial_manager a1) { + R(); + P(a0); + P(a1); + C(478); +} +void log_Z3_mk_zero_polynomial(Z3_context a0, Z3_polynomial_manager a1) { + R(); + P(a0); + P(a1); + C(479); +} +void log_Z3_polynomial_inc_ref(Z3_context a0, Z3_polynomial_manager a1, Z3_polynomial a2) { + R(); + P(a0); + P(a1); + P(a2); + C(480); +} +void log_Z3_polynomial_dec_ref(Z3_context a0, Z3_polynomial_manager a1, Z3_polynomial a2) { + R(); + P(a0); + P(a1); + P(a2); + C(481); +} +void log_Z3_polynomial_to_string(Z3_context a0, Z3_polynomial_manager a1, Z3_polynomial a2) { + R(); + P(a0); + P(a1); + P(a2); + C(482); +} diff --git a/lib/api_log_macros.h b/lib/api_log_macros.h index 62c504372..538232fd6 100644 --- a/lib/api_log_macros.h +++ b/lib/api_log_macros.h @@ -975,3 +975,15 @@ void log_Z3_statistics_to_string(Z3_context a0); #define LOG_Z3_statistics_to_string(_ARG0) z3_log_ctx _LOG_CTX; if (_LOG_CTX.enabled()) { log_Z3_statistics_to_string(_ARG0); } void log_Z3_get_context_assignment(Z3_context a0); #define LOG_Z3_get_context_assignment(_ARG0) z3_log_ctx _LOG_CTX; if (_LOG_CTX.enabled()) { log_Z3_get_context_assignment(_ARG0); } +void log_Z3_mk_polynomial_manager(Z3_context a0); +#define LOG_Z3_mk_polynomial_manager(_ARG0) z3_log_ctx _LOG_CTX; if (_LOG_CTX.enabled()) { log_Z3_mk_polynomial_manager(_ARG0); } +void log_Z3_del_polynomial_manager(Z3_context a0, Z3_polynomial_manager a1); +#define LOG_Z3_del_polynomial_manager(_ARG0, _ARG1) z3_log_ctx _LOG_CTX; if (_LOG_CTX.enabled()) { log_Z3_del_polynomial_manager(_ARG0, _ARG1); } +void log_Z3_mk_zero_polynomial(Z3_context a0, Z3_polynomial_manager a1); +#define LOG_Z3_mk_zero_polynomial(_ARG0, _ARG1) z3_log_ctx _LOG_CTX; if (_LOG_CTX.enabled()) { log_Z3_mk_zero_polynomial(_ARG0, _ARG1); } +void log_Z3_polynomial_inc_ref(Z3_context a0, Z3_polynomial_manager a1, Z3_polynomial a2); +#define LOG_Z3_polynomial_inc_ref(_ARG0, _ARG1, _ARG2) z3_log_ctx _LOG_CTX; if (_LOG_CTX.enabled()) { log_Z3_polynomial_inc_ref(_ARG0, _ARG1, _ARG2); } +void log_Z3_polynomial_dec_ref(Z3_context a0, Z3_polynomial_manager a1, Z3_polynomial a2); +#define LOG_Z3_polynomial_dec_ref(_ARG0, _ARG1, _ARG2) z3_log_ctx _LOG_CTX; if (_LOG_CTX.enabled()) { log_Z3_polynomial_dec_ref(_ARG0, _ARG1, _ARG2); } +void log_Z3_polynomial_to_string(Z3_context a0, Z3_polynomial_manager a1, Z3_polynomial a2); +#define LOG_Z3_polynomial_to_string(_ARG0, _ARG1, _ARG2) z3_log_ctx _LOG_CTX; if (_LOG_CTX.enabled()) { log_Z3_polynomial_to_string(_ARG0, _ARG1, _ARG2); } diff --git a/lib/api_poly.cpp b/lib/api_poly.cpp new file mode 100644 index 000000000..5b4a9d58b --- /dev/null +++ b/lib/api_poly.cpp @@ -0,0 +1,78 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + api_poly.cpp + +Abstract: + + External API for polynomial package + +Author: + + Leonardo de Moura (leonardo) 2012-10-18. + +Revision History: + +--*/ +#include"z3.h" +#include"z3_internal.h" +#include"api_context.h" +#include"api_poly.h" +#include"api_util.h" +#include"api_log_macros.h" + +Z3_polynomial_manager Z3_mk_polynomial_manager(Z3_context c) { + Z3_TRY; + LOG_Z3_mk_polynomial_manager(c); + RESET_ERROR_CODE(); + _Z3_polynomial_manager * m = alloc(_Z3_polynomial_manager); + RETURN_Z3(of_poly_manager(m)); + Z3_CATCH_RETURN(0); +} + +void Z3_del_polynomial_manager(Z3_context c, Z3_polynomial_manager m) { + Z3_TRY; + LOG_Z3_del_polynomial_manager(c, m); + RESET_ERROR_CODE(); + dealloc(to_poly_manager(m)); + Z3_CATCH; +} + +Z3_polynomial Z3_mk_zero_polynomial(Z3_context c, Z3_polynomial_manager m) { + Z3_TRY; + LOG_Z3_mk_zero_polynomial(c, m); + RESET_ERROR_CODE(); + polynomial::polynomial * r = to_poly_manager(m)->m_manager.mk_zero(); + to_poly_manager(m)->m_result = r; + RETURN_Z3(of_poly(r)); + Z3_CATCH_RETURN(0); +} + +void Z3_polynomial_inc_ref(Z3_context c, Z3_polynomial_manager m, Z3_polynomial p) { + Z3_TRY; + LOG_Z3_polynomial_inc_ref(c, m, p); + RESET_ERROR_CODE(); + to_poly_manager(m)->m_manager.inc_ref(to_poly(p)); + Z3_CATCH; +} + +void Z3_polynomial_dec_ref(Z3_context c, Z3_polynomial_manager m, Z3_polynomial p) { + Z3_TRY; + LOG_Z3_polynomial_inc_ref(c, m, p); + RESET_ERROR_CODE(); + to_poly_manager(m)->m_manager.dec_ref(to_poly(p)); + Z3_CATCH; +} + +Z3_string Z3_polynomial_to_string(Z3_context c, Z3_polynomial_manager m, Z3_polynomial p) { + Z3_TRY; + LOG_Z3_polynomial_to_string(c, m, p); + RESET_ERROR_CODE(); + std::ostringstream buffer; + to_poly_manager(m)->m_manager.display(buffer, to_poly(p)); + return mk_c(c)->mk_external_string(buffer.str()); + Z3_CATCH_RETURN(""); +} + diff --git a/lib/api_poly.h b/lib/api_poly.h new file mode 100644 index 000000000..943c506fd --- /dev/null +++ b/lib/api_poly.h @@ -0,0 +1,40 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + api_poly.h + +Abstract: + External API for polynomial package + +Author: + + Leonardo de Moura (leonardo) 2012-10-18. + +Revision History: + +--*/ +#ifndef _API_POLY_H_ +#define _API_POLY_H_ + +#include"polynomial.h" + +struct _Z3_polynomial_manager { + unsynch_mpz_manager m_num_manager; + polynomial::manager m_manager; + polynomial_ref m_result; + + _Z3_polynomial_manager(): + m_manager(m_num_manager), + m_result(m_manager) { + } +}; + +inline _Z3_polynomial_manager * to_poly_manager(Z3_polynomial_manager m) { return reinterpret_cast<_Z3_polynomial_manager*>(m); } +inline Z3_polynomial_manager of_poly_manager(_Z3_polynomial_manager * m) { return reinterpret_cast(m); } + +inline polynomial::polynomial * to_poly(Z3_polynomial p) { return reinterpret_cast(p); } +inline Z3_polynomial of_poly(polynomial::polynomial * p) { return reinterpret_cast(p); } + +#endif diff --git a/lib/api_util.h b/lib/api_util.h index d7c50aec7..b08592cb7 100644 --- a/lib/api_util.h +++ b/lib/api_util.h @@ -20,6 +20,7 @@ Revision History: #include"params.h" #include"lbool.h" +#include"ast.h" #define Z3_TRY try { #define Z3_CATCH_CORE(CODE) } catch (z3_exception & ex) { mk_c(c)->handle_exception(ex); CODE } diff --git a/lib/lib.vcxproj b/lib/lib.vcxproj index 01a33e4f7..f0353db42 100644 --- a/lib/lib.vcxproj +++ b/lib/lib.vcxproj @@ -1,4 +1,4 @@ - + @@ -443,6 +443,7 @@ + diff --git a/lib/z3.h b/lib/z3.h index 8df894f40..76fe91ce1 100644 --- a/lib/z3.h +++ b/lib/z3.h @@ -24,6 +24,7 @@ Notes: #include #include"z3_macros.h" #include"z3_api.h" +#include"z3_internal_types.h" #undef __in #undef __out diff --git a/lib/z3_api.h b/lib/z3_api.h index 6eccfd6eb..29806e02e 100644 --- a/lib/z3_api.h +++ b/lib/z3_api.h @@ -1,3 +1,6 @@ +#ifndef _Z3_API_H_ +#define _Z3_API_H_ + #ifdef CAMLIDL #ifdef MLAPIV3 #define ML3only @@ -7556,3 +7559,5 @@ END_MLAPI_EXCLUDE #endif // CAMLIDL /*@}*/ + +#endif diff --git a/lib/z3_internal.h b/lib/z3_internal.h new file mode 100644 index 000000000..cbff085e8 --- /dev/null +++ b/lib/z3_internal.h @@ -0,0 +1,40 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + z3_internal.h + +Abstract: + + Z3 internal API for C and Python. + It provides access to internal Z3 components. + It should only be used by advanced users. + We used it to build regression tests in Python. + +Author: + + Leonardo de Moura (leonardo) 2012-10-18 + +Notes: + +--*/ +#ifndef _Z3_INTERNAL_H_ +#define _Z3_INTERNAL_H_ + +#include"z3_macros.h" +#include"z3_api.h" +#include"z3_internal_types.h" +#include"z3_poly.h" + +#undef __in +#undef __out +#undef __inout +#undef __in_z +#undef __out_z +#undef __ecount +#undef __in_ecount +#undef __out_ecount +#undef __inout_ecount + +#endif diff --git a/lib/z3_internal_types.h b/lib/z3_internal_types.h new file mode 100644 index 000000000..7fb7b4038 --- /dev/null +++ b/lib/z3_internal_types.h @@ -0,0 +1,34 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + z3_internal_types.h + +Abstract: + + Z3 internal API type declarations. + +Author: + + Leonardo de Moura (leonardo) 2012-10-18 + +Notes: + +--*/ +#ifndef _Z3_INTERNAL_TYPES_H_ +#define _Z3_INTERNAL_TYPES_H_ + +DEFINE_TYPE(Z3_polynomial_manager); +DEFINE_TYPE(Z3_polynomial); +DEFINE_TYPE(Z3_monomial); + +/* + Definitions for update_api.py + + def_Type('POLYNOMIAL_MANAGER', 'Z3_polynomial_manager', 'PolynomialManagerObj') + def_Type('POLYNOMIAL', 'Z3_polynomial', 'PolynomialObj') + def_Type('MONOMIAL', 'Z3_monomial', 'MonomialObj') +*/ + +#endif diff --git a/lib/z3_poly.h b/lib/z3_poly.h new file mode 100644 index 000000000..4e3e99d53 --- /dev/null +++ b/lib/z3_poly.h @@ -0,0 +1,72 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + z3_poly.h + +Abstract: + + Z3 multivariate polynomial API. + +Author: + + Leonardo de Moura (leonardo) 2012-10-18 + +Notes: + +--*/ +#ifndef _Z3_POLY_H_ +#define _Z3_POLY_H_ + +#ifdef __cplusplus +extern "C" { +#endif // __cplusplus + + /** + \brief Create a new polynomial manager. + + def_API('Z3_mk_polynomial_manager', POLYNOMIAL_MANAGER, (_in(CONTEXT),)) + */ + Z3_polynomial_manager Z3_API Z3_mk_polynomial_manager(__in Z3_context c); + + /** + \brief Delete the given polynomial manager. + + def_API('Z3_del_polynomial_manager', VOID, (_in(CONTEXT), _in(POLYNOMIAL_MANAGER))) + */ + void Z3_API Z3_del_polynomial_manager(__in Z3_context c, __in Z3_polynomial_manager m); + + /** + \brief Return the zero polynomial. + + def_API('Z3_mk_zero_polynomial', POLYNOMIAL, (_in(CONTEXT), _in(POLYNOMIAL_MANAGER))) + */ + Z3_polynomial Z3_API Z3_mk_zero_polynomial(__in Z3_context c, __in Z3_polynomial_manager m); + + /** + \brief Increment p's reference counter + + def_API('Z3_polynomial_inc_ref', VOID, (_in(CONTEXT), _in(POLYNOMIAL_MANAGER), _in(POLYNOMIAL))) + */ + void Z3_API Z3_polynomial_inc_ref(__in Z3_context c, __in Z3_polynomial_manager m, __in Z3_polynomial p); + + /** + \brief Decrement p's reference counter. + + def_API('Z3_polynomial_dec_ref', VOID, (_in(CONTEXT), _in(POLYNOMIAL_MANAGER), _in(POLYNOMIAL))) + */ + void Z3_API Z3_polynomial_dec_ref(__in Z3_context c, __in Z3_polynomial_manager m, __in Z3_polynomial p); + + /** + \brief Convert the given polynomial into a string. + + def_API('Z3_polynomial_to_string', STRING, (_in(CONTEXT), _in(POLYNOMIAL_MANAGER), _in(POLYNOMIAL))) + */ + Z3_string Z3_API Z3_polynomial_to_string(__in Z3_context c, __in Z3_polynomial_manager m, __in Z3_polynomial p); + +#ifdef __cplusplus +}; +#endif // __cplusplus + +#endif diff --git a/python/z3core.py b/python/z3core.py index 3b7ff0d4a..9d346ff90 100644 --- a/python/z3core.py +++ b/python/z3core.py @@ -904,6 +904,15 @@ def init(PATH): _lib.Z3_statistics_to_string.argtypes = [ContextObj] _lib.Z3_get_context_assignment.restype = Ast _lib.Z3_get_context_assignment.argtypes = [ContextObj] + _lib.Z3_mk_polynomial_manager.restype = PolynomialManagerObj + _lib.Z3_mk_polynomial_manager.argtypes = [ContextObj] + _lib.Z3_del_polynomial_manager.argtypes = [ContextObj, PolynomialManagerObj] + _lib.Z3_mk_zero_polynomial.restype = PolynomialObj + _lib.Z3_mk_zero_polynomial.argtypes = [ContextObj, PolynomialManagerObj] + _lib.Z3_polynomial_inc_ref.argtypes = [ContextObj, PolynomialManagerObj, PolynomialObj] + _lib.Z3_polynomial_dec_ref.argtypes = [ContextObj, PolynomialManagerObj, PolynomialObj] + _lib.Z3_polynomial_to_string.restype = ctypes.c_char_p + _lib.Z3_polynomial_to_string.argtypes = [ContextObj, PolynomialManagerObj, PolynomialObj] def Z3_mk_config(): r = lib().Z3_mk_config() @@ -4142,3 +4151,42 @@ def Z3_get_context_assignment(a0): raise Z3Exception(lib().Z3_get_error_msg_ex(a0, err)) return r +def Z3_mk_polynomial_manager(a0): + r = lib().Z3_mk_polynomial_manager(a0) + err = lib().Z3_get_error_code(a0) + if err != Z3_OK: + raise Z3Exception(lib().Z3_get_error_msg_ex(a0, err)) + return r + +def Z3_del_polynomial_manager(a0, a1): + lib().Z3_del_polynomial_manager(a0, a1) + err = lib().Z3_get_error_code(a0) + if err != Z3_OK: + raise Z3Exception(lib().Z3_get_error_msg_ex(a0, err)) + +def Z3_mk_zero_polynomial(a0, a1): + r = lib().Z3_mk_zero_polynomial(a0, a1) + err = lib().Z3_get_error_code(a0) + if err != Z3_OK: + raise Z3Exception(lib().Z3_get_error_msg_ex(a0, err)) + return r + +def Z3_polynomial_inc_ref(a0, a1, a2): + lib().Z3_polynomial_inc_ref(a0, a1, a2) + err = lib().Z3_get_error_code(a0) + if err != Z3_OK: + raise Z3Exception(lib().Z3_get_error_msg_ex(a0, err)) + +def Z3_polynomial_dec_ref(a0, a1, a2): + lib().Z3_polynomial_dec_ref(a0, a1, a2) + err = lib().Z3_get_error_code(a0) + if err != Z3_OK: + raise Z3Exception(lib().Z3_get_error_msg_ex(a0, err)) + +def Z3_polynomial_to_string(a0, a1, a2): + r = lib().Z3_polynomial_to_string(a0, a1, a2) + err = lib().Z3_get_error_code(a0) + if err != Z3_OK: + raise Z3Exception(lib().Z3_get_error_msg_ex(a0, err)) + return r + diff --git a/python/z3poly.py b/python/z3poly.py new file mode 100644 index 000000000..f8e6eb1f7 --- /dev/null +++ b/python/z3poly.py @@ -0,0 +1,67 @@ +############################################ +# Copyright (c) 2012 Microsoft Corporation +# +# Z3 Polynomial interface +# +# Author: Leonardo de Moura (leonardo) +############################################ +from z3 import * + +class PolynomialManager: + """Polynomial Manager. + """ + def __init__(self, ctx=None): + self.ctx = z3._get_ctx(ctx) + self.manager = Z3_mk_polynomial_manager(self.ctx_ref()) + + def __del__(self): + Z3_del_polynomial_manager(self.ctx_ref(), self.manager) + + def ctx_ref(self): + return self.ctx.ref() + + def m(self): + return self.manager + +_main_pmanager = None +def main_pmanager(): + """Return a reference to the global Polynomial manager. + """ + global _main_pmanager + if _main_pmanager == None: + _main_pmanager = PolynomialManager() + return _main_pmanager + +def _get_pmanager(ctx): + if ctx == None: + return main_pmanager() + else: + return ctx + +class Polynomial: + """Multivariate polynomials. + """ + def __init__(self, poly=None, m=None): + self.pmanager = _get_pmanager(m) + if poly == None: + self.poly = Z3_mk_zero_polynomial(self.ctx_ref(), self.m()) + else: + self.poly = poly + Z3_polynomial_inc_ref(self.ctx_ref(), self.m(), self.poly) + + def __del__(self): + Z3_polynomial_dec_ref(self.ctx_ref(), self.m(), self.poly) + + def m(self): + return self.pmanager.m() + + def ctx_ref(self): + return self.pmanager.ctx_ref() + + def __repr__(self): + return Z3_polynomial_to_string(self.ctx_ref(), self.m(), self.poly) + +# test +p = Polynomial() +print p + diff --git a/python/z3types.py b/python/z3types.py index f986551cb..b91a80aae 100644 --- a/python/z3types.py +++ b/python/z3types.py @@ -105,3 +105,15 @@ class FuncInterpObj(ctypes.c_void_p): class FuncEntryObj(ctypes.c_void_p): def __init__(self, e): self._as_parameter_ = e def from_param(obj): return obj + +class PolynomialManagerObj(ctypes.c_void_p): + def __init__(self, e): self._as_parameter_ = e + def from_param(obj): return obj + +class PolynomialObj(ctypes.c_void_p): + def __init__(self, e): self._as_parameter_ = e + def from_param(obj): return obj + +class MonomialObj(ctypes.c_void_p): + def __init__(self, e): self._as_parameter_ = e + def from_param(obj): return obj diff --git a/update_api.py b/update_api.py index 2f5d0a464..f250b9163 100644 --- a/update_api.py +++ b/update_api.py @@ -16,6 +16,8 @@ def add_api_file(dir, file): API_FILES.append("%s%s%s" % (dir, os.sep, file)) add_api_file('lib', 'z3_api.h') +add_api_file('lib', 'z3_internal_types.h') +add_api_file('lib', 'z3_poly.h') # Extract enumeration types from z3_api.h, and add .Net definitions def mk_z3consts_donet(): @@ -238,6 +240,7 @@ log_c.write('#include\"z3_logger.h\"\n') ## exe_c.write('// Automatically generated file, generator: update_api.py\n') exe_c.write('#include\"z3.h\"\n') +exe_c.write('#include\"z3_internal.h\"\n') exe_c.write('#include\"z3_replayer.h\"\n') ## log_h.write('extern std::ostream * g_z3_log;\n')