diff --git a/MAINTAINERS.md b/MAINTAINERS.md new file mode 100644 --- /dev/null +++ b/MAINTAINERS.md @@ -0,0 +1,5 @@ +This file is used to indicate responsibility for the maintenance of this package. Individuals on this list should be the sole modifiers of the package, excluding cases where the Solus Team may need to perform necessary rebuilds, upgrades, or security fixes. This list should not be used for any direct contact usage. If you believe this package requires a package update, follow documentation from https://getsol.us/articles/packaging/request-a-package-update/en/. In the event this package no longer becomes sufficiently maintained, Core Team reserves the right to request a new maintainer or remove this package from the repository. + +- Silke Hofstra + - IRC: silkeh + - Email: silke@slxh.eu diff --git a/Makefile b/Makefile new file mode 100644 --- /dev/null +++ b/Makefile @@ -0,0 +1 @@ +include ../Makefile.common diff --git a/abi_symbols b/abi_symbols new file mode 100644 --- /dev/null +++ b/abi_symbols @@ -0,0 +1,707 @@ +libz3.so.4.8:Z3_add_const_interp +libz3.so.4.8:Z3_add_func_interp +libz3.so.4.8:Z3_add_rec_def +libz3.so.4.8:Z3_algebraic_add +libz3.so.4.8:Z3_algebraic_div +libz3.so.4.8:Z3_algebraic_eq +libz3.so.4.8:Z3_algebraic_eval +libz3.so.4.8:Z3_algebraic_ge +libz3.so.4.8:Z3_algebraic_get_i +libz3.so.4.8:Z3_algebraic_get_poly +libz3.so.4.8:Z3_algebraic_gt +libz3.so.4.8:Z3_algebraic_is_neg +libz3.so.4.8:Z3_algebraic_is_pos +libz3.so.4.8:Z3_algebraic_is_value +libz3.so.4.8:Z3_algebraic_is_zero +libz3.so.4.8:Z3_algebraic_le +libz3.so.4.8:Z3_algebraic_lt +libz3.so.4.8:Z3_algebraic_mul +libz3.so.4.8:Z3_algebraic_neq +libz3.so.4.8:Z3_algebraic_power +libz3.so.4.8:Z3_algebraic_root +libz3.so.4.8:Z3_algebraic_roots +libz3.so.4.8:Z3_algebraic_sign +libz3.so.4.8:Z3_algebraic_sub +libz3.so.4.8:Z3_app_to_ast +libz3.so.4.8:Z3_append_log +libz3.so.4.8:Z3_apply_result_dec_ref +libz3.so.4.8:Z3_apply_result_get_num_subgoals +libz3.so.4.8:Z3_apply_result_get_subgoal +libz3.so.4.8:Z3_apply_result_inc_ref +libz3.so.4.8:Z3_apply_result_to_string +libz3.so.4.8:Z3_ast_map_contains +libz3.so.4.8:Z3_ast_map_dec_ref +libz3.so.4.8:Z3_ast_map_erase +libz3.so.4.8:Z3_ast_map_find +libz3.so.4.8:Z3_ast_map_inc_ref +libz3.so.4.8:Z3_ast_map_insert +libz3.so.4.8:Z3_ast_map_keys +libz3.so.4.8:Z3_ast_map_reset +libz3.so.4.8:Z3_ast_map_size +libz3.so.4.8:Z3_ast_map_to_string +libz3.so.4.8:Z3_ast_to_string +libz3.so.4.8:Z3_ast_vector_dec_ref +libz3.so.4.8:Z3_ast_vector_get +libz3.so.4.8:Z3_ast_vector_inc_ref +libz3.so.4.8:Z3_ast_vector_push +libz3.so.4.8:Z3_ast_vector_resize +libz3.so.4.8:Z3_ast_vector_set +libz3.so.4.8:Z3_ast_vector_size +libz3.so.4.8:Z3_ast_vector_to_string +libz3.so.4.8:Z3_ast_vector_translate +libz3.so.4.8:Z3_benchmark_to_smtlib_string +libz3.so.4.8:Z3_close_log +libz3.so.4.8:Z3_datatype_update_field +libz3.so.4.8:Z3_dec_ref +libz3.so.4.8:Z3_del_config +libz3.so.4.8:Z3_del_constructor +libz3.so.4.8:Z3_del_constructor_list +libz3.so.4.8:Z3_del_context +libz3.so.4.8:Z3_disable_trace +libz3.so.4.8:Z3_enable_trace +libz3.so.4.8:Z3_eval_smtlib2_string +libz3.so.4.8:Z3_finalize_memory +libz3.so.4.8:Z3_fixedpoint_add_callback +libz3.so.4.8:Z3_fixedpoint_add_constraint +libz3.so.4.8:Z3_fixedpoint_add_cover +libz3.so.4.8:Z3_fixedpoint_add_fact +libz3.so.4.8:Z3_fixedpoint_add_invariant +libz3.so.4.8:Z3_fixedpoint_add_rule +libz3.so.4.8:Z3_fixedpoint_assert +libz3.so.4.8:Z3_fixedpoint_dec_ref +libz3.so.4.8:Z3_fixedpoint_from_file +libz3.so.4.8:Z3_fixedpoint_from_string +libz3.so.4.8:Z3_fixedpoint_get_answer +libz3.so.4.8:Z3_fixedpoint_get_assertions +libz3.so.4.8:Z3_fixedpoint_get_cover_delta +libz3.so.4.8:Z3_fixedpoint_get_ground_sat_answer +libz3.so.4.8:Z3_fixedpoint_get_help +libz3.so.4.8:Z3_fixedpoint_get_num_levels +libz3.so.4.8:Z3_fixedpoint_get_param_descrs +libz3.so.4.8:Z3_fixedpoint_get_reachable +libz3.so.4.8:Z3_fixedpoint_get_reason_unknown +libz3.so.4.8:Z3_fixedpoint_get_rule_names_along_trace +libz3.so.4.8:Z3_fixedpoint_get_rules +libz3.so.4.8:Z3_fixedpoint_get_rules_along_trace +libz3.so.4.8:Z3_fixedpoint_get_statistics +libz3.so.4.8:Z3_fixedpoint_inc_ref +libz3.so.4.8:Z3_fixedpoint_init +libz3.so.4.8:Z3_fixedpoint_query +libz3.so.4.8:Z3_fixedpoint_query_from_lvl +libz3.so.4.8:Z3_fixedpoint_query_relations +libz3.so.4.8:Z3_fixedpoint_register_relation +libz3.so.4.8:Z3_fixedpoint_set_params +libz3.so.4.8:Z3_fixedpoint_set_predicate_representation +libz3.so.4.8:Z3_fixedpoint_set_reduce_app_callback +libz3.so.4.8:Z3_fixedpoint_set_reduce_assign_callback +libz3.so.4.8:Z3_fixedpoint_to_string +libz3.so.4.8:Z3_fixedpoint_update_rule +libz3.so.4.8:Z3_fpa_get_ebits +libz3.so.4.8:Z3_fpa_get_numeral_exponent_bv +libz3.so.4.8:Z3_fpa_get_numeral_exponent_int64 +libz3.so.4.8:Z3_fpa_get_numeral_exponent_string +libz3.so.4.8:Z3_fpa_get_numeral_sign +libz3.so.4.8:Z3_fpa_get_numeral_sign_bv +libz3.so.4.8:Z3_fpa_get_numeral_significand_bv +libz3.so.4.8:Z3_fpa_get_numeral_significand_string +libz3.so.4.8:Z3_fpa_get_numeral_significand_uint64 +libz3.so.4.8:Z3_fpa_get_sbits +libz3.so.4.8:Z3_fpa_is_numeral_inf +libz3.so.4.8:Z3_fpa_is_numeral_nan +libz3.so.4.8:Z3_fpa_is_numeral_negative +libz3.so.4.8:Z3_fpa_is_numeral_normal +libz3.so.4.8:Z3_fpa_is_numeral_positive +libz3.so.4.8:Z3_fpa_is_numeral_subnormal +libz3.so.4.8:Z3_fpa_is_numeral_zero +libz3.so.4.8:Z3_func_decl_to_ast +libz3.so.4.8:Z3_func_decl_to_string +libz3.so.4.8:Z3_func_entry_dec_ref +libz3.so.4.8:Z3_func_entry_get_arg +libz3.so.4.8:Z3_func_entry_get_num_args +libz3.so.4.8:Z3_func_entry_get_value +libz3.so.4.8:Z3_func_entry_inc_ref +libz3.so.4.8:Z3_func_interp_add_entry +libz3.so.4.8:Z3_func_interp_dec_ref +libz3.so.4.8:Z3_func_interp_get_arity +libz3.so.4.8:Z3_func_interp_get_else +libz3.so.4.8:Z3_func_interp_get_entry +libz3.so.4.8:Z3_func_interp_get_num_entries +libz3.so.4.8:Z3_func_interp_inc_ref +libz3.so.4.8:Z3_func_interp_set_else +libz3.so.4.8:Z3_get_algebraic_number_lower +libz3.so.4.8:Z3_get_algebraic_number_upper +libz3.so.4.8:Z3_get_app_arg +libz3.so.4.8:Z3_get_app_decl +libz3.so.4.8:Z3_get_app_num_args +libz3.so.4.8:Z3_get_arity +libz3.so.4.8:Z3_get_array_sort_domain +libz3.so.4.8:Z3_get_array_sort_range +libz3.so.4.8:Z3_get_as_array_func_decl +libz3.so.4.8:Z3_get_ast_hash +libz3.so.4.8:Z3_get_ast_id +libz3.so.4.8:Z3_get_ast_kind +libz3.so.4.8:Z3_get_bool_value +libz3.so.4.8:Z3_get_bv_sort_size +libz3.so.4.8:Z3_get_datatype_sort_constructor +libz3.so.4.8:Z3_get_datatype_sort_constructor_accessor +libz3.so.4.8:Z3_get_datatype_sort_num_constructors +libz3.so.4.8:Z3_get_datatype_sort_recognizer +libz3.so.4.8:Z3_get_decl_ast_parameter +libz3.so.4.8:Z3_get_decl_double_parameter +libz3.so.4.8:Z3_get_decl_func_decl_parameter +libz3.so.4.8:Z3_get_decl_int_parameter +libz3.so.4.8:Z3_get_decl_kind +libz3.so.4.8:Z3_get_decl_name +libz3.so.4.8:Z3_get_decl_num_parameters +libz3.so.4.8:Z3_get_decl_parameter_kind +libz3.so.4.8:Z3_get_decl_rational_parameter +libz3.so.4.8:Z3_get_decl_sort_parameter +libz3.so.4.8:Z3_get_decl_symbol_parameter +libz3.so.4.8:Z3_get_denominator +libz3.so.4.8:Z3_get_domain +libz3.so.4.8:Z3_get_domain_size +libz3.so.4.8:Z3_get_error_code +libz3.so.4.8:Z3_get_error_msg +libz3.so.4.8:Z3_get_estimated_alloc_size +libz3.so.4.8:Z3_get_finite_domain_sort_size +libz3.so.4.8:Z3_get_full_version +libz3.so.4.8:Z3_get_func_decl_id +libz3.so.4.8:Z3_get_implied_equalities +libz3.so.4.8:Z3_get_index_value +libz3.so.4.8:Z3_get_lstring +libz3.so.4.8:Z3_get_num_probes +libz3.so.4.8:Z3_get_num_tactics +libz3.so.4.8:Z3_get_numeral_binary_string +libz3.so.4.8:Z3_get_numeral_decimal_string +libz3.so.4.8:Z3_get_numeral_double +libz3.so.4.8:Z3_get_numeral_int +libz3.so.4.8:Z3_get_numeral_int64 +libz3.so.4.8:Z3_get_numeral_rational +libz3.so.4.8:Z3_get_numeral_rational_int64 +libz3.so.4.8:Z3_get_numeral_small +libz3.so.4.8:Z3_get_numeral_string +libz3.so.4.8:Z3_get_numeral_uint +libz3.so.4.8:Z3_get_numeral_uint64 +libz3.so.4.8:Z3_get_numerator +libz3.so.4.8:Z3_get_pattern +libz3.so.4.8:Z3_get_pattern_num_terms +libz3.so.4.8:Z3_get_probe_name +libz3.so.4.8:Z3_get_quantifier_body +libz3.so.4.8:Z3_get_quantifier_bound_name +libz3.so.4.8:Z3_get_quantifier_bound_sort +libz3.so.4.8:Z3_get_quantifier_no_pattern_ast +libz3.so.4.8:Z3_get_quantifier_num_bound +libz3.so.4.8:Z3_get_quantifier_num_no_patterns +libz3.so.4.8:Z3_get_quantifier_num_patterns +libz3.so.4.8:Z3_get_quantifier_pattern_ast +libz3.so.4.8:Z3_get_quantifier_weight +libz3.so.4.8:Z3_get_range +libz3.so.4.8:Z3_get_re_sort_basis +libz3.so.4.8:Z3_get_relation_arity +libz3.so.4.8:Z3_get_relation_column +libz3.so.4.8:Z3_get_seq_sort_basis +libz3.so.4.8:Z3_get_sort +libz3.so.4.8:Z3_get_sort_id +libz3.so.4.8:Z3_get_sort_kind +libz3.so.4.8:Z3_get_sort_name +libz3.so.4.8:Z3_get_string +libz3.so.4.8:Z3_get_symbol_int +libz3.so.4.8:Z3_get_symbol_kind +libz3.so.4.8:Z3_get_symbol_string +libz3.so.4.8:Z3_get_tactic_name +libz3.so.4.8:Z3_get_tuple_sort_field_decl +libz3.so.4.8:Z3_get_tuple_sort_mk_decl +libz3.so.4.8:Z3_get_tuple_sort_num_fields +libz3.so.4.8:Z3_get_version +libz3.so.4.8:Z3_global_param_get +libz3.so.4.8:Z3_global_param_reset_all +libz3.so.4.8:Z3_global_param_set +libz3.so.4.8:Z3_goal_assert +libz3.so.4.8:Z3_goal_convert_model +libz3.so.4.8:Z3_goal_dec_ref +libz3.so.4.8:Z3_goal_depth +libz3.so.4.8:Z3_goal_formula +libz3.so.4.8:Z3_goal_inc_ref +libz3.so.4.8:Z3_goal_inconsistent +libz3.so.4.8:Z3_goal_is_decided_sat +libz3.so.4.8:Z3_goal_is_decided_unsat +libz3.so.4.8:Z3_goal_num_exprs +libz3.so.4.8:Z3_goal_precision +libz3.so.4.8:Z3_goal_reset +libz3.so.4.8:Z3_goal_size +libz3.so.4.8:Z3_goal_to_dimacs_string +libz3.so.4.8:Z3_goal_to_string +libz3.so.4.8:Z3_goal_translate +libz3.so.4.8:Z3_inc_ref +libz3.so.4.8:Z3_interrupt +libz3.so.4.8:Z3_is_algebraic_number +libz3.so.4.8:Z3_is_app +libz3.so.4.8:Z3_is_as_array +libz3.so.4.8:Z3_is_eq_ast +libz3.so.4.8:Z3_is_eq_func_decl +libz3.so.4.8:Z3_is_eq_sort +libz3.so.4.8:Z3_is_lambda +libz3.so.4.8:Z3_is_numeral_ast +libz3.so.4.8:Z3_is_quantifier_exists +libz3.so.4.8:Z3_is_quantifier_forall +libz3.so.4.8:Z3_is_re_sort +libz3.so.4.8:Z3_is_seq_sort +libz3.so.4.8:Z3_is_string +libz3.so.4.8:Z3_is_string_sort +libz3.so.4.8:Z3_is_well_sorted +libz3.so.4.8:Z3_mk_add +libz3.so.4.8:Z3_mk_and +libz3.so.4.8:Z3_mk_app +libz3.so.4.8:Z3_mk_array_default +libz3.so.4.8:Z3_mk_array_ext +libz3.so.4.8:Z3_mk_array_sort +libz3.so.4.8:Z3_mk_array_sort_n +libz3.so.4.8:Z3_mk_as_array +libz3.so.4.8:Z3_mk_ast_map +libz3.so.4.8:Z3_mk_ast_vector +libz3.so.4.8:Z3_mk_atleast +libz3.so.4.8:Z3_mk_atmost +libz3.so.4.8:Z3_mk_bool_sort +libz3.so.4.8:Z3_mk_bound +libz3.so.4.8:Z3_mk_bv2int +libz3.so.4.8:Z3_mk_bv_numeral +libz3.so.4.8:Z3_mk_bv_sort +libz3.so.4.8:Z3_mk_bvadd +libz3.so.4.8:Z3_mk_bvadd_no_overflow +libz3.so.4.8:Z3_mk_bvadd_no_underflow +libz3.so.4.8:Z3_mk_bvand +libz3.so.4.8:Z3_mk_bvashr +libz3.so.4.8:Z3_mk_bvlshr +libz3.so.4.8:Z3_mk_bvmsb +libz3.so.4.8:Z3_mk_bvmul +libz3.so.4.8:Z3_mk_bvmul_no_overflow +libz3.so.4.8:Z3_mk_bvmul_no_underflow +libz3.so.4.8:Z3_mk_bvnand +libz3.so.4.8:Z3_mk_bvneg +libz3.so.4.8:Z3_mk_bvneg_no_overflow +libz3.so.4.8:Z3_mk_bvnor +libz3.so.4.8:Z3_mk_bvnot +libz3.so.4.8:Z3_mk_bvor +libz3.so.4.8:Z3_mk_bvredand +libz3.so.4.8:Z3_mk_bvredor +libz3.so.4.8:Z3_mk_bvsdiv +libz3.so.4.8:Z3_mk_bvsdiv_no_overflow +libz3.so.4.8:Z3_mk_bvsge +libz3.so.4.8:Z3_mk_bvsgt +libz3.so.4.8:Z3_mk_bvshl +libz3.so.4.8:Z3_mk_bvsle +libz3.so.4.8:Z3_mk_bvslt +libz3.so.4.8:Z3_mk_bvsmod +libz3.so.4.8:Z3_mk_bvsrem +libz3.so.4.8:Z3_mk_bvsub +libz3.so.4.8:Z3_mk_bvsub_no_overflow +libz3.so.4.8:Z3_mk_bvsub_no_underflow +libz3.so.4.8:Z3_mk_bvudiv +libz3.so.4.8:Z3_mk_bvuge +libz3.so.4.8:Z3_mk_bvugt +libz3.so.4.8:Z3_mk_bvule +libz3.so.4.8:Z3_mk_bvult +libz3.so.4.8:Z3_mk_bvurem +libz3.so.4.8:Z3_mk_bvxnor +libz3.so.4.8:Z3_mk_bvxor +libz3.so.4.8:Z3_mk_concat +libz3.so.4.8:Z3_mk_config +libz3.so.4.8:Z3_mk_const +libz3.so.4.8:Z3_mk_const_array +libz3.so.4.8:Z3_mk_constructor +libz3.so.4.8:Z3_mk_constructor_list +libz3.so.4.8:Z3_mk_context +libz3.so.4.8:Z3_mk_context_rc +libz3.so.4.8:Z3_mk_datatype +libz3.so.4.8:Z3_mk_datatypes +libz3.so.4.8:Z3_mk_distinct +libz3.so.4.8:Z3_mk_div +libz3.so.4.8:Z3_mk_divides +libz3.so.4.8:Z3_mk_empty_set +libz3.so.4.8:Z3_mk_enumeration_sort +libz3.so.4.8:Z3_mk_eq +libz3.so.4.8:Z3_mk_exists +libz3.so.4.8:Z3_mk_exists_const +libz3.so.4.8:Z3_mk_ext_rotate_left +libz3.so.4.8:Z3_mk_ext_rotate_right +libz3.so.4.8:Z3_mk_extract +libz3.so.4.8:Z3_mk_false +libz3.so.4.8:Z3_mk_finite_domain_sort +libz3.so.4.8:Z3_mk_fixedpoint +libz3.so.4.8:Z3_mk_forall +libz3.so.4.8:Z3_mk_forall_const +libz3.so.4.8:Z3_mk_fpa_abs +libz3.so.4.8:Z3_mk_fpa_add +libz3.so.4.8:Z3_mk_fpa_div +libz3.so.4.8:Z3_mk_fpa_eq +libz3.so.4.8:Z3_mk_fpa_fma +libz3.so.4.8:Z3_mk_fpa_fp +libz3.so.4.8:Z3_mk_fpa_geq +libz3.so.4.8:Z3_mk_fpa_gt +libz3.so.4.8:Z3_mk_fpa_inf +libz3.so.4.8:Z3_mk_fpa_is_infinite +libz3.so.4.8:Z3_mk_fpa_is_nan +libz3.so.4.8:Z3_mk_fpa_is_negative +libz3.so.4.8:Z3_mk_fpa_is_normal +libz3.so.4.8:Z3_mk_fpa_is_positive +libz3.so.4.8:Z3_mk_fpa_is_subnormal +libz3.so.4.8:Z3_mk_fpa_is_zero +libz3.so.4.8:Z3_mk_fpa_leq +libz3.so.4.8:Z3_mk_fpa_lt +libz3.so.4.8:Z3_mk_fpa_max +libz3.so.4.8:Z3_mk_fpa_min +libz3.so.4.8:Z3_mk_fpa_mul +libz3.so.4.8:Z3_mk_fpa_nan +libz3.so.4.8:Z3_mk_fpa_neg +libz3.so.4.8:Z3_mk_fpa_numeral_double +libz3.so.4.8:Z3_mk_fpa_numeral_float +libz3.so.4.8:Z3_mk_fpa_numeral_int +libz3.so.4.8:Z3_mk_fpa_numeral_int64_uint64 +libz3.so.4.8:Z3_mk_fpa_numeral_int_uint +libz3.so.4.8:Z3_mk_fpa_rem +libz3.so.4.8:Z3_mk_fpa_rna +libz3.so.4.8:Z3_mk_fpa_rne +libz3.so.4.8:Z3_mk_fpa_round_nearest_ties_to_away +libz3.so.4.8:Z3_mk_fpa_round_nearest_ties_to_even +libz3.so.4.8:Z3_mk_fpa_round_to_integral +libz3.so.4.8:Z3_mk_fpa_round_toward_negative +libz3.so.4.8:Z3_mk_fpa_round_toward_positive +libz3.so.4.8:Z3_mk_fpa_round_toward_zero +libz3.so.4.8:Z3_mk_fpa_rounding_mode_sort +libz3.so.4.8:Z3_mk_fpa_rtn +libz3.so.4.8:Z3_mk_fpa_rtp +libz3.so.4.8:Z3_mk_fpa_rtz +libz3.so.4.8:Z3_mk_fpa_sort +libz3.so.4.8:Z3_mk_fpa_sort_128 +libz3.so.4.8:Z3_mk_fpa_sort_16 +libz3.so.4.8:Z3_mk_fpa_sort_32 +libz3.so.4.8:Z3_mk_fpa_sort_64 +libz3.so.4.8:Z3_mk_fpa_sort_double +libz3.so.4.8:Z3_mk_fpa_sort_half +libz3.so.4.8:Z3_mk_fpa_sort_quadruple +libz3.so.4.8:Z3_mk_fpa_sort_single +libz3.so.4.8:Z3_mk_fpa_sqrt +libz3.so.4.8:Z3_mk_fpa_sub +libz3.so.4.8:Z3_mk_fpa_to_fp_bv +libz3.so.4.8:Z3_mk_fpa_to_fp_float +libz3.so.4.8:Z3_mk_fpa_to_fp_int_real +libz3.so.4.8:Z3_mk_fpa_to_fp_real +libz3.so.4.8:Z3_mk_fpa_to_fp_signed +libz3.so.4.8:Z3_mk_fpa_to_fp_unsigned +libz3.so.4.8:Z3_mk_fpa_to_ieee_bv +libz3.so.4.8:Z3_mk_fpa_to_real +libz3.so.4.8:Z3_mk_fpa_to_sbv +libz3.so.4.8:Z3_mk_fpa_to_ubv +libz3.so.4.8:Z3_mk_fpa_zero +libz3.so.4.8:Z3_mk_fresh_const +libz3.so.4.8:Z3_mk_fresh_func_decl +libz3.so.4.8:Z3_mk_full_set +libz3.so.4.8:Z3_mk_func_decl +libz3.so.4.8:Z3_mk_ge +libz3.so.4.8:Z3_mk_goal +libz3.so.4.8:Z3_mk_gt +libz3.so.4.8:Z3_mk_iff +libz3.so.4.8:Z3_mk_implies +libz3.so.4.8:Z3_mk_int +libz3.so.4.8:Z3_mk_int2bv +libz3.so.4.8:Z3_mk_int2real +libz3.so.4.8:Z3_mk_int64 +libz3.so.4.8:Z3_mk_int_sort +libz3.so.4.8:Z3_mk_int_symbol +libz3.so.4.8:Z3_mk_int_to_str +libz3.so.4.8:Z3_mk_is_int +libz3.so.4.8:Z3_mk_ite +libz3.so.4.8:Z3_mk_lambda +libz3.so.4.8:Z3_mk_lambda_const +libz3.so.4.8:Z3_mk_le +libz3.so.4.8:Z3_mk_linear_order +libz3.so.4.8:Z3_mk_list_sort +libz3.so.4.8:Z3_mk_lstring +libz3.so.4.8:Z3_mk_lt +libz3.so.4.8:Z3_mk_map +libz3.so.4.8:Z3_mk_mod +libz3.so.4.8:Z3_mk_model +libz3.so.4.8:Z3_mk_mul +libz3.so.4.8:Z3_mk_not +libz3.so.4.8:Z3_mk_numeral +libz3.so.4.8:Z3_mk_optimize +libz3.so.4.8:Z3_mk_or +libz3.so.4.8:Z3_mk_params +libz3.so.4.8:Z3_mk_partial_order +libz3.so.4.8:Z3_mk_pattern +libz3.so.4.8:Z3_mk_pbeq +libz3.so.4.8:Z3_mk_pbge +libz3.so.4.8:Z3_mk_pble +libz3.so.4.8:Z3_mk_piecewise_linear_order +libz3.so.4.8:Z3_mk_power +libz3.so.4.8:Z3_mk_probe +libz3.so.4.8:Z3_mk_quantifier +libz3.so.4.8:Z3_mk_quantifier_const +libz3.so.4.8:Z3_mk_quantifier_const_ex +libz3.so.4.8:Z3_mk_quantifier_ex +libz3.so.4.8:Z3_mk_re_complement +libz3.so.4.8:Z3_mk_re_concat +libz3.so.4.8:Z3_mk_re_empty +libz3.so.4.8:Z3_mk_re_full +libz3.so.4.8:Z3_mk_re_intersect +libz3.so.4.8:Z3_mk_re_loop +libz3.so.4.8:Z3_mk_re_option +libz3.so.4.8:Z3_mk_re_plus +libz3.so.4.8:Z3_mk_re_range +libz3.so.4.8:Z3_mk_re_sort +libz3.so.4.8:Z3_mk_re_star +libz3.so.4.8:Z3_mk_re_union +libz3.so.4.8:Z3_mk_real +libz3.so.4.8:Z3_mk_real2int +libz3.so.4.8:Z3_mk_real_sort +libz3.so.4.8:Z3_mk_rec_func_decl +libz3.so.4.8:Z3_mk_rem +libz3.so.4.8:Z3_mk_repeat +libz3.so.4.8:Z3_mk_rotate_left +libz3.so.4.8:Z3_mk_rotate_right +libz3.so.4.8:Z3_mk_select +libz3.so.4.8:Z3_mk_select_n +libz3.so.4.8:Z3_mk_seq_at +libz3.so.4.8:Z3_mk_seq_concat +libz3.so.4.8:Z3_mk_seq_contains +libz3.so.4.8:Z3_mk_seq_empty +libz3.so.4.8:Z3_mk_seq_extract +libz3.so.4.8:Z3_mk_seq_in_re +libz3.so.4.8:Z3_mk_seq_index +libz3.so.4.8:Z3_mk_seq_last_index +libz3.so.4.8:Z3_mk_seq_length +libz3.so.4.8:Z3_mk_seq_nth +libz3.so.4.8:Z3_mk_seq_prefix +libz3.so.4.8:Z3_mk_seq_replace +libz3.so.4.8:Z3_mk_seq_sort +libz3.so.4.8:Z3_mk_seq_suffix +libz3.so.4.8:Z3_mk_seq_to_re +libz3.so.4.8:Z3_mk_seq_unit +libz3.so.4.8:Z3_mk_set_add +libz3.so.4.8:Z3_mk_set_complement +libz3.so.4.8:Z3_mk_set_del +libz3.so.4.8:Z3_mk_set_difference +libz3.so.4.8:Z3_mk_set_has_size +libz3.so.4.8:Z3_mk_set_intersect +libz3.so.4.8:Z3_mk_set_member +libz3.so.4.8:Z3_mk_set_sort +libz3.so.4.8:Z3_mk_set_subset +libz3.so.4.8:Z3_mk_set_union +libz3.so.4.8:Z3_mk_sign_ext +libz3.so.4.8:Z3_mk_simple_solver +libz3.so.4.8:Z3_mk_solver +libz3.so.4.8:Z3_mk_solver_for_logic +libz3.so.4.8:Z3_mk_solver_from_tactic +libz3.so.4.8:Z3_mk_store +libz3.so.4.8:Z3_mk_store_n +libz3.so.4.8:Z3_mk_str_le +libz3.so.4.8:Z3_mk_str_lt +libz3.so.4.8:Z3_mk_str_to_int +libz3.so.4.8:Z3_mk_string +libz3.so.4.8:Z3_mk_string_sort +libz3.so.4.8:Z3_mk_string_symbol +libz3.so.4.8:Z3_mk_sub +libz3.so.4.8:Z3_mk_tactic +libz3.so.4.8:Z3_mk_transitive_closure +libz3.so.4.8:Z3_mk_tree_order +libz3.so.4.8:Z3_mk_true +libz3.so.4.8:Z3_mk_tuple_sort +libz3.so.4.8:Z3_mk_unary_minus +libz3.so.4.8:Z3_mk_uninterpreted_sort +libz3.so.4.8:Z3_mk_unsigned_int +libz3.so.4.8:Z3_mk_unsigned_int64 +libz3.so.4.8:Z3_mk_xor +libz3.so.4.8:Z3_mk_zero_ext +libz3.so.4.8:Z3_model_dec_ref +libz3.so.4.8:Z3_model_eval +libz3.so.4.8:Z3_model_extrapolate +libz3.so.4.8:Z3_model_get_const_decl +libz3.so.4.8:Z3_model_get_const_interp +libz3.so.4.8:Z3_model_get_func_decl +libz3.so.4.8:Z3_model_get_func_interp +libz3.so.4.8:Z3_model_get_num_consts +libz3.so.4.8:Z3_model_get_num_funcs +libz3.so.4.8:Z3_model_get_num_sorts +libz3.so.4.8:Z3_model_get_sort +libz3.so.4.8:Z3_model_get_sort_universe +libz3.so.4.8:Z3_model_has_interp +libz3.so.4.8:Z3_model_inc_ref +libz3.so.4.8:Z3_model_to_string +libz3.so.4.8:Z3_model_translate +libz3.so.4.8:Z3_open_log +libz3.so.4.8:Z3_optimize_assert +libz3.so.4.8:Z3_optimize_assert_and_track +libz3.so.4.8:Z3_optimize_assert_soft +libz3.so.4.8:Z3_optimize_check +libz3.so.4.8:Z3_optimize_dec_ref +libz3.so.4.8:Z3_optimize_from_file +libz3.so.4.8:Z3_optimize_from_string +libz3.so.4.8:Z3_optimize_get_assertions +libz3.so.4.8:Z3_optimize_get_help +libz3.so.4.8:Z3_optimize_get_lower +libz3.so.4.8:Z3_optimize_get_lower_as_vector +libz3.so.4.8:Z3_optimize_get_model +libz3.so.4.8:Z3_optimize_get_objectives +libz3.so.4.8:Z3_optimize_get_param_descrs +libz3.so.4.8:Z3_optimize_get_reason_unknown +libz3.so.4.8:Z3_optimize_get_statistics +libz3.so.4.8:Z3_optimize_get_unsat_core +libz3.so.4.8:Z3_optimize_get_upper +libz3.so.4.8:Z3_optimize_get_upper_as_vector +libz3.so.4.8:Z3_optimize_inc_ref +libz3.so.4.8:Z3_optimize_maximize +libz3.so.4.8:Z3_optimize_minimize +libz3.so.4.8:Z3_optimize_pop +libz3.so.4.8:Z3_optimize_push +libz3.so.4.8:Z3_optimize_set_params +libz3.so.4.8:Z3_optimize_to_string +libz3.so.4.8:Z3_param_descrs_dec_ref +libz3.so.4.8:Z3_param_descrs_get_documentation +libz3.so.4.8:Z3_param_descrs_get_kind +libz3.so.4.8:Z3_param_descrs_get_name +libz3.so.4.8:Z3_param_descrs_inc_ref +libz3.so.4.8:Z3_param_descrs_size +libz3.so.4.8:Z3_param_descrs_to_string +libz3.so.4.8:Z3_params_dec_ref +libz3.so.4.8:Z3_params_inc_ref +libz3.so.4.8:Z3_params_set_bool +libz3.so.4.8:Z3_params_set_double +libz3.so.4.8:Z3_params_set_symbol +libz3.so.4.8:Z3_params_set_uint +libz3.so.4.8:Z3_params_to_string +libz3.so.4.8:Z3_params_validate +libz3.so.4.8:Z3_parse_smtlib2_file +libz3.so.4.8:Z3_parse_smtlib2_string +libz3.so.4.8:Z3_pattern_to_ast +libz3.so.4.8:Z3_pattern_to_string +libz3.so.4.8:Z3_polynomial_subresultants +libz3.so.4.8:Z3_probe_and +libz3.so.4.8:Z3_probe_apply +libz3.so.4.8:Z3_probe_const +libz3.so.4.8:Z3_probe_dec_ref +libz3.so.4.8:Z3_probe_eq +libz3.so.4.8:Z3_probe_ge +libz3.so.4.8:Z3_probe_get_descr +libz3.so.4.8:Z3_probe_gt +libz3.so.4.8:Z3_probe_inc_ref +libz3.so.4.8:Z3_probe_le +libz3.so.4.8:Z3_probe_lt +libz3.so.4.8:Z3_probe_not +libz3.so.4.8:Z3_probe_or +libz3.so.4.8:Z3_qe_lite +libz3.so.4.8:Z3_qe_model_project +libz3.so.4.8:Z3_qe_model_project_skolem +libz3.so.4.8:Z3_query_constructor +libz3.so.4.8:Z3_rcf_add +libz3.so.4.8:Z3_rcf_del +libz3.so.4.8:Z3_rcf_div +libz3.so.4.8:Z3_rcf_eq +libz3.so.4.8:Z3_rcf_ge +libz3.so.4.8:Z3_rcf_get_numerator_denominator +libz3.so.4.8:Z3_rcf_gt +libz3.so.4.8:Z3_rcf_inv +libz3.so.4.8:Z3_rcf_le +libz3.so.4.8:Z3_rcf_lt +libz3.so.4.8:Z3_rcf_mk_e +libz3.so.4.8:Z3_rcf_mk_infinitesimal +libz3.so.4.8:Z3_rcf_mk_pi +libz3.so.4.8:Z3_rcf_mk_rational +libz3.so.4.8:Z3_rcf_mk_roots +libz3.so.4.8:Z3_rcf_mk_small_int +libz3.so.4.8:Z3_rcf_mul +libz3.so.4.8:Z3_rcf_neg +libz3.so.4.8:Z3_rcf_neq +libz3.so.4.8:Z3_rcf_num_to_decimal_string +libz3.so.4.8:Z3_rcf_num_to_string +libz3.so.4.8:Z3_rcf_power +libz3.so.4.8:Z3_rcf_sub +libz3.so.4.8:Z3_reset_memory +libz3.so.4.8:Z3_set_ast_print_mode +libz3.so.4.8:Z3_set_error +libz3.so.4.8:Z3_set_error_handler +libz3.so.4.8:Z3_set_param_value +libz3.so.4.8:Z3_simplify +libz3.so.4.8:Z3_simplify_ex +libz3.so.4.8:Z3_simplify_get_help +libz3.so.4.8:Z3_simplify_get_param_descrs +libz3.so.4.8:Z3_solver_assert +libz3.so.4.8:Z3_solver_assert_and_track +libz3.so.4.8:Z3_solver_check +libz3.so.4.8:Z3_solver_check_assumptions +libz3.so.4.8:Z3_solver_cube +libz3.so.4.8:Z3_solver_dec_ref +libz3.so.4.8:Z3_solver_from_file +libz3.so.4.8:Z3_solver_from_string +libz3.so.4.8:Z3_solver_get_assertions +libz3.so.4.8:Z3_solver_get_consequences +libz3.so.4.8:Z3_solver_get_help +libz3.so.4.8:Z3_solver_get_implied_lower +libz3.so.4.8:Z3_solver_get_implied_upper +libz3.so.4.8:Z3_solver_get_implied_value +libz3.so.4.8:Z3_solver_get_levels +libz3.so.4.8:Z3_solver_get_model +libz3.so.4.8:Z3_solver_get_non_units +libz3.so.4.8:Z3_solver_get_num_scopes +libz3.so.4.8:Z3_solver_get_param_descrs +libz3.so.4.8:Z3_solver_get_proof +libz3.so.4.8:Z3_solver_get_reason_unknown +libz3.so.4.8:Z3_solver_get_statistics +libz3.so.4.8:Z3_solver_get_trail +libz3.so.4.8:Z3_solver_get_units +libz3.so.4.8:Z3_solver_get_unsat_core +libz3.so.4.8:Z3_solver_import_model_converter +libz3.so.4.8:Z3_solver_inc_ref +libz3.so.4.8:Z3_solver_interrupt +libz3.so.4.8:Z3_solver_pop +libz3.so.4.8:Z3_solver_propagate_consequence +libz3.so.4.8:Z3_solver_propagate_diseq +libz3.so.4.8:Z3_solver_propagate_eq +libz3.so.4.8:Z3_solver_propagate_final +libz3.so.4.8:Z3_solver_propagate_fixed +libz3.so.4.8:Z3_solver_propagate_init +libz3.so.4.8:Z3_solver_propagate_register +libz3.so.4.8:Z3_solver_push +libz3.so.4.8:Z3_solver_reset +libz3.so.4.8:Z3_solver_set_params +libz3.so.4.8:Z3_solver_to_dimacs_string +libz3.so.4.8:Z3_solver_to_string +libz3.so.4.8:Z3_solver_translate +libz3.so.4.8:Z3_sort_to_ast +libz3.so.4.8:Z3_sort_to_string +libz3.so.4.8:Z3_stats_dec_ref +libz3.so.4.8:Z3_stats_get_double_value +libz3.so.4.8:Z3_stats_get_key +libz3.so.4.8:Z3_stats_get_uint_value +libz3.so.4.8:Z3_stats_inc_ref +libz3.so.4.8:Z3_stats_is_double +libz3.so.4.8:Z3_stats_is_uint +libz3.so.4.8:Z3_stats_size +libz3.so.4.8:Z3_stats_to_string +libz3.so.4.8:Z3_substitute +libz3.so.4.8:Z3_substitute_vars +libz3.so.4.8:Z3_tactic_and_then +libz3.so.4.8:Z3_tactic_apply +libz3.so.4.8:Z3_tactic_apply_ex +libz3.so.4.8:Z3_tactic_cond +libz3.so.4.8:Z3_tactic_dec_ref +libz3.so.4.8:Z3_tactic_fail +libz3.so.4.8:Z3_tactic_fail_if +libz3.so.4.8:Z3_tactic_fail_if_not_decided +libz3.so.4.8:Z3_tactic_get_descr +libz3.so.4.8:Z3_tactic_get_help +libz3.so.4.8:Z3_tactic_get_param_descrs +libz3.so.4.8:Z3_tactic_inc_ref +libz3.so.4.8:Z3_tactic_or_else +libz3.so.4.8:Z3_tactic_par_and_then +libz3.so.4.8:Z3_tactic_par_or +libz3.so.4.8:Z3_tactic_repeat +libz3.so.4.8:Z3_tactic_skip +libz3.so.4.8:Z3_tactic_try_for +libz3.so.4.8:Z3_tactic_using_params +libz3.so.4.8:Z3_tactic_when +libz3.so.4.8:Z3_to_app +libz3.so.4.8:Z3_to_func_decl +libz3.so.4.8:Z3_toggle_warning_messages +libz3.so.4.8:Z3_translate +libz3.so.4.8:Z3_update_param_value +libz3.so.4.8:Z3_update_term diff --git a/abi_used_libs b/abi_used_libs new file mode 100644 --- /dev/null +++ b/abi_used_libs @@ -0,0 +1,6 @@ +ld-linux-x86-64.so.2 +libc.so.6 +libgcc_s.so.1 +libm.so.6 +libpthread.so.0 +libstdc++.so.6 diff --git a/package.yml b/package.yml new file mode 100644 --- /dev/null +++ b/package.yml @@ -0,0 +1,16 @@ +name : z3 +version : 4.8.9 +release : 1 +source : + - https://github.com/Z3Prover/z3/archive/z3-4.8.9.tar.gz : c9fd04b9b33be74fffaac3ec2bc2c320d1a4cc32e395203c55126b12a14ff3f4 +license : MIT +component : programming.library +summary : The Z3 Theorem Prover +description: | + Z3 is a theorem prover from Microsoft Research. +setup : | + %cmake_ninja +build : | + %ninja_build +install : | + %ninja_install diff --git a/pspec_x86_64.xml b/pspec_x86_64.xml new file mode 100644 --- /dev/null +++ b/pspec_x86_64.xml @@ -0,0 +1,68 @@ + + + z3 + + Silke Hofstra + silke@slxh.eu + + MIT + programming.library + The Z3 Theorem Prover + Z3 is a theorem prover from Microsoft Research. + + https://getsol.us/sources/README.Solus + + + z3 + The Z3 Theorem Prover + Z3 is a theorem prover from Microsoft Research. + + programming.library + + /usr/bin/z3 + /usr/lib64/libz3.so.4.8 + /usr/lib64/libz3.so.4.8.9.0 + + + + z3-devel + Development files for z3 + Z3 is a theorem prover from Microsoft Research. + + programming.devel + + z3 + + + /usr/include/z3++.h + /usr/include/z3.h + /usr/include/z3_algebraic.h + /usr/include/z3_api.h + /usr/include/z3_ast_containers.h + /usr/include/z3_fixedpoint.h + /usr/include/z3_fpa.h + /usr/include/z3_macros.h + /usr/include/z3_optimization.h + /usr/include/z3_polynomial.h + /usr/include/z3_rcf.h + /usr/include/z3_spacer.h + /usr/include/z3_v1.h + /usr/include/z3_version.h + /usr/lib64/cmake/z3/Z3Config.cmake + /usr/lib64/cmake/z3/Z3ConfigVersion.cmake + /usr/lib64/cmake/z3/Z3Targets-relwithdebinfo.cmake + /usr/lib64/cmake/z3/Z3Targets.cmake + /usr/lib64/libz3.so + /usr/lib64/pkgconfig/z3.pc + + + + + 2020-09-30 + 4.8.9 + Packaging update + Silke Hofstra + silke@slxh.eu + + + \ No newline at end of file