Page MenuHomeSolus
Files F11047323

D9754.diff
No OneTemporary
Actions

D9754.diff
View Options

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 @@
+<PISI>
+ <Source>
+ <Name>z3</Name>
+ <Packager>
+ <Name>Silke Hofstra</Name>
+ <Email>silke@slxh.eu</Email>
+ </Packager>
+ <License>MIT</License>
+ <PartOf>programming.library</PartOf>
+ <Summary xml:lang="en">The Z3 Theorem Prover</Summary>
+ <Description xml:lang="en">Z3 is a theorem prover from Microsoft Research.
+</Description>
+ <Archive type="binary" sha1sum="79eb0752a961b8e0d15c77d298c97498fbc89c5a">https://getsol.us/sources/README.Solus</Archive>
+ </Source>
+ <Package>
+ <Name>z3</Name>
+ <Summary xml:lang="en">The Z3 Theorem Prover</Summary>
+ <Description xml:lang="en">Z3 is a theorem prover from Microsoft Research.
+</Description>
+ <PartOf>programming.library</PartOf>
+ <Files>
+ <Path fileType="executable">/usr/bin/z3</Path>
+ <Path fileType="library">/usr/lib64/libz3.so.4.8</Path>
+ <Path fileType="library">/usr/lib64/libz3.so.4.8.9.0</Path>
+ </Files>
+ </Package>
+ <Package>
+ <Name>z3-devel</Name>
+ <Summary xml:lang="en">Development files for z3</Summary>
+ <Description xml:lang="en">Z3 is a theorem prover from Microsoft Research.
+</Description>
+ <PartOf>programming.devel</PartOf>
+ <RuntimeDependencies>
+ <Dependency release="1">z3</Dependency>
+ </RuntimeDependencies>
+ <Files>
+ <Path fileType="header">/usr/include/z3++.h</Path>
+ <Path fileType="header">/usr/include/z3.h</Path>
+ <Path fileType="header">/usr/include/z3_algebraic.h</Path>
+ <Path fileType="header">/usr/include/z3_api.h</Path>
+ <Path fileType="header">/usr/include/z3_ast_containers.h</Path>
+ <Path fileType="header">/usr/include/z3_fixedpoint.h</Path>
+ <Path fileType="header">/usr/include/z3_fpa.h</Path>
+ <Path fileType="header">/usr/include/z3_macros.h</Path>
+ <Path fileType="header">/usr/include/z3_optimization.h</Path>
+ <Path fileType="header">/usr/include/z3_polynomial.h</Path>
+ <Path fileType="header">/usr/include/z3_rcf.h</Path>
+ <Path fileType="header">/usr/include/z3_spacer.h</Path>
+ <Path fileType="header">/usr/include/z3_v1.h</Path>
+ <Path fileType="header">/usr/include/z3_version.h</Path>
+ <Path fileType="library">/usr/lib64/cmake/z3/Z3Config.cmake</Path>
+ <Path fileType="library">/usr/lib64/cmake/z3/Z3ConfigVersion.cmake</Path>
+ <Path fileType="library">/usr/lib64/cmake/z3/Z3Targets-relwithdebinfo.cmake</Path>
+ <Path fileType="library">/usr/lib64/cmake/z3/Z3Targets.cmake</Path>
+ <Path fileType="library">/usr/lib64/libz3.so</Path>
+ <Path fileType="data">/usr/lib64/pkgconfig/z3.pc</Path>
+ </Files>
+ </Package>
+ <History>
+ <Update release="1">
+ <Date>2020-09-30</Date>
+ <Version>4.8.9</Version>
+ <Comment>Packaging update</Comment>
+ <Name>Silke Hofstra</Name>
+ <Email>silke@slxh.eu</Email>
+ </Update>
+ </History>
+</PISI>
\ No newline at end of file

File Metadata

Mime Type
text/plain
Expires
Fri, Aug 11, 3:15 PM (3 h, 3 m ago)
Storage Engine
blob
Storage Format
Raw Data
Storage Handle
5834115
Default Alt Text
D9754.diff (28 KB)

Event Timeline

Copyright © 2015-2021 Solus Project. The Solus logo is Copyright © 2016-2021 Solus Project. All Rights Reserved.