Compare commits
2 commits
| Author | SHA1 | Date | |
|---|---|---|---|
|
ee37bb9481 | ||
|
|
2fe1c8d08a |
3 changed files with 542 additions and 25 deletions
2
sources
2
sources
|
|
@ -1 +1 @@
|
|||
SHA512 (z3-5.1.0.tar.gz) = 03a854f720a56484ab99b8a5517150f1c9106400f54ad758cfa58e3ee2f95e349396a64d4f527a5bb9ee37f10ad9ecfa1916d1f5c921f04089deda409374491b
|
||||
SHA512 (z3-4.15.8.tar.gz) = e31df90b0edb3fd4a49a1069d78135d03c6b196c2bc8359a67273e02eba7214a7ff8654488f076ce7a0cf6edffdff9afc403799db3a6e5a1585a6d4c99c4df2a
|
||||
|
|
|
|||
505
z3-s390x-doc.patch
Normal file
505
z3-s390x-doc.patch
Normal file
|
|
@ -0,0 +1,505 @@
|
|||
--- a/doc/api/html/z3.z3core.html
|
||||
+++ b/doc/api/html/z3.z3core.html
|
||||
@@ -277,13 +277,21 @@ Data descriptors defined here:<br>
|
||||
a3,
|
||||
_elems=<z3.z3core.Elementaries object>
|
||||
)</dt></dl>
|
||||
- <dl><dt><a name="-Z3_ast_map_keys"><strong>Z3_ast_map_keys</strong></a>(a0, a1, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
+ <dl><dt><a name="-Z3_ast_map_keys"><strong>Z3_ast_map_keys</strong></a>(
|
||||
+ a0,
|
||||
+ a1,
|
||||
+ _elems=<z3.z3core.Elementaries object>
|
||||
+)</dt></dl>
|
||||
<dl><dt><a name="-Z3_ast_map_reset"><strong>Z3_ast_map_reset</strong></a>(
|
||||
a0,
|
||||
a1,
|
||||
_elems=<z3.z3core.Elementaries object>
|
||||
)</dt></dl>
|
||||
- <dl><dt><a name="-Z3_ast_map_size"><strong>Z3_ast_map_size</strong></a>(a0, a1, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
+ <dl><dt><a name="-Z3_ast_map_size"><strong>Z3_ast_map_size</strong></a>(
|
||||
+ a0,
|
||||
+ a1,
|
||||
+ _elems=<z3.z3core.Elementaries object>
|
||||
+)</dt></dl>
|
||||
<dl><dt><a name="-Z3_ast_map_to_string"><strong>Z3_ast_map_to_string</strong></a>(
|
||||
a0,
|
||||
a1,
|
||||
@@ -833,7 +841,11 @@ Data descriptors defined here:<br>
|
||||
a2,
|
||||
_elems=<z3.z3core.Elementaries object>
|
||||
)</dt></dl>
|
||||
- <dl><dt><a name="-Z3_get_app_decl"><strong>Z3_get_app_decl</strong></a>(a0, a1, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
+ <dl><dt><a name="-Z3_get_app_decl"><strong>Z3_get_app_decl</strong></a>(
|
||||
+ a0,
|
||||
+ a1,
|
||||
+ _elems=<z3.z3core.Elementaries object>
|
||||
+)</dt></dl>
|
||||
<dl><dt><a name="-Z3_get_app_num_args"><strong>Z3_get_app_num_args</strong></a>(
|
||||
a0,
|
||||
a1,
|
||||
@@ -866,9 +878,17 @@ Data descriptors defined here:<br>
|
||||
a1,
|
||||
_elems=<z3.z3core.Elementaries object>
|
||||
)</dt></dl>
|
||||
- <dl><dt><a name="-Z3_get_ast_hash"><strong>Z3_get_ast_hash</strong></a>(a0, a1, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
+ <dl><dt><a name="-Z3_get_ast_hash"><strong>Z3_get_ast_hash</strong></a>(
|
||||
+ a0,
|
||||
+ a1,
|
||||
+ _elems=<z3.z3core.Elementaries object>
|
||||
+)</dt></dl>
|
||||
<dl><dt><a name="-Z3_get_ast_id"><strong>Z3_get_ast_id</strong></a>(a0, a1, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
- <dl><dt><a name="-Z3_get_ast_kind"><strong>Z3_get_ast_kind</strong></a>(a0, a1, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
+ <dl><dt><a name="-Z3_get_ast_kind"><strong>Z3_get_ast_kind</strong></a>(
|
||||
+ a0,
|
||||
+ a1,
|
||||
+ _elems=<z3.z3core.Elementaries object>
|
||||
+)</dt></dl>
|
||||
<dl><dt><a name="-Z3_get_bool_value"><strong>Z3_get_bool_value</strong></a>(
|
||||
a0,
|
||||
a1,
|
||||
@@ -1347,7 +1367,11 @@ Data descriptors defined here:<br>
|
||||
a2,
|
||||
_elems=<z3.z3core.Elementaries object>
|
||||
)</dt></dl>
|
||||
- <dl><dt><a name="-Z3_goal_dec_ref"><strong>Z3_goal_dec_ref</strong></a>(a0, a1, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
+ <dl><dt><a name="-Z3_goal_dec_ref"><strong>Z3_goal_dec_ref</strong></a>(
|
||||
+ a0,
|
||||
+ a1,
|
||||
+ _elems=<z3.z3core.Elementaries object>
|
||||
+)</dt></dl>
|
||||
<dl><dt><a name="-Z3_goal_depth"><strong>Z3_goal_depth</strong></a>(a0, a1, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
<dl><dt><a name="-Z3_goal_formula"><strong>Z3_goal_formula</strong></a>(
|
||||
a0,
|
||||
@@ -1355,7 +1379,11 @@ Data descriptors defined here:<br>
|
||||
a2,
|
||||
_elems=<z3.z3core.Elementaries object>
|
||||
)</dt></dl>
|
||||
- <dl><dt><a name="-Z3_goal_inc_ref"><strong>Z3_goal_inc_ref</strong></a>(a0, a1, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
+ <dl><dt><a name="-Z3_goal_inc_ref"><strong>Z3_goal_inc_ref</strong></a>(
|
||||
+ a0,
|
||||
+ a1,
|
||||
+ _elems=<z3.z3core.Elementaries object>
|
||||
+)</dt></dl>
|
||||
<dl><dt><a name="-Z3_goal_inconsistent"><strong>Z3_goal_inconsistent</strong></a>(
|
||||
a0,
|
||||
a1,
|
||||
@@ -1420,7 +1448,11 @@ Data descriptors defined here:<br>
|
||||
)</dt></dl>
|
||||
<dl><dt><a name="-Z3_is_app"><strong>Z3_is_app</strong></a>(a0, a1, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
<dl><dt><a name="-Z3_is_as_array"><strong>Z3_is_as_array</strong></a>(a0, a1, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
- <dl><dt><a name="-Z3_is_char_sort"><strong>Z3_is_char_sort</strong></a>(a0, a1, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
+ <dl><dt><a name="-Z3_is_char_sort"><strong>Z3_is_char_sort</strong></a>(
|
||||
+ a0,
|
||||
+ a1,
|
||||
+ _elems=<z3.z3core.Elementaries object>
|
||||
+)</dt></dl>
|
||||
<dl><dt><a name="-Z3_is_eq_ast"><strong>Z3_is_eq_ast</strong></a>(
|
||||
a0,
|
||||
a1,
|
||||
@@ -1532,7 +1564,12 @@ Data descriptors defined here:<br>
|
||||
_elems=<z3.z3core.Elementaries object>
|
||||
)</dt></dl>
|
||||
<dl><dt><a name="-Z3_mk_bool_sort"><strong>Z3_mk_bool_sort</strong></a>(a0, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
- <dl><dt><a name="-Z3_mk_bound"><strong>Z3_mk_bound</strong></a>(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
+ <dl><dt><a name="-Z3_mk_bound"><strong>Z3_mk_bound</strong></a>(
|
||||
+ a0,
|
||||
+ a1,
|
||||
+ a2,
|
||||
+ _elems=<z3.z3core.Elementaries object>
|
||||
+)</dt></dl>
|
||||
<dl><dt><a name="-Z3_mk_bv2int"><strong>Z3_mk_bv2int</strong></a>(
|
||||
a0,
|
||||
a1,
|
||||
@@ -1546,7 +1583,12 @@ Data descriptors defined here:<br>
|
||||
_elems=<z3.z3core.Elementaries object>
|
||||
)</dt></dl>
|
||||
<dl><dt><a name="-Z3_mk_bv_sort"><strong>Z3_mk_bv_sort</strong></a>(a0, a1, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
- <dl><dt><a name="-Z3_mk_bvadd"><strong>Z3_mk_bvadd</strong></a>(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
+ <dl><dt><a name="-Z3_mk_bvadd"><strong>Z3_mk_bvadd</strong></a>(
|
||||
+ a0,
|
||||
+ a1,
|
||||
+ a2,
|
||||
+ _elems=<z3.z3core.Elementaries object>
|
||||
+)</dt></dl>
|
||||
<dl><dt><a name="-Z3_mk_bvadd_no_overflow"><strong>Z3_mk_bvadd_no_overflow</strong></a>(
|
||||
a0,
|
||||
a1,
|
||||
@@ -1560,7 +1602,12 @@ Data descriptors defined here:<br>
|
||||
a2,
|
||||
_elems=<z3.z3core.Elementaries object>
|
||||
)</dt></dl>
|
||||
- <dl><dt><a name="-Z3_mk_bvand"><strong>Z3_mk_bvand</strong></a>(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
+ <dl><dt><a name="-Z3_mk_bvand"><strong>Z3_mk_bvand</strong></a>(
|
||||
+ a0,
|
||||
+ a1,
|
||||
+ a2,
|
||||
+ _elems=<z3.z3core.Elementaries object>
|
||||
+)</dt></dl>
|
||||
<dl><dt><a name="-Z3_mk_bvashr"><strong>Z3_mk_bvashr</strong></a>(
|
||||
a0,
|
||||
a1,
|
||||
@@ -1573,7 +1620,12 @@ Data descriptors defined here:<br>
|
||||
a2,
|
||||
_elems=<z3.z3core.Elementaries object>
|
||||
)</dt></dl>
|
||||
- <dl><dt><a name="-Z3_mk_bvmul"><strong>Z3_mk_bvmul</strong></a>(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
+ <dl><dt><a name="-Z3_mk_bvmul"><strong>Z3_mk_bvmul</strong></a>(
|
||||
+ a0,
|
||||
+ a1,
|
||||
+ a2,
|
||||
+ _elems=<z3.z3core.Elementaries object>
|
||||
+)</dt></dl>
|
||||
<dl><dt><a name="-Z3_mk_bvmul_no_overflow"><strong>Z3_mk_bvmul_no_overflow</strong></a>(
|
||||
a0,
|
||||
a1,
|
||||
@@ -1599,7 +1651,12 @@ Data descriptors defined here:<br>
|
||||
a1,
|
||||
_elems=<z3.z3core.Elementaries object>
|
||||
)</dt></dl>
|
||||
- <dl><dt><a name="-Z3_mk_bvnor"><strong>Z3_mk_bvnor</strong></a>(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
+ <dl><dt><a name="-Z3_mk_bvnor"><strong>Z3_mk_bvnor</strong></a>(
|
||||
+ a0,
|
||||
+ a1,
|
||||
+ a2,
|
||||
+ _elems=<z3.z3core.Elementaries object>
|
||||
+)</dt></dl>
|
||||
<dl><dt><a name="-Z3_mk_bvnot"><strong>Z3_mk_bvnot</strong></a>(a0, a1, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
<dl><dt><a name="-Z3_mk_bvor"><strong>Z3_mk_bvor</strong></a>(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
<dl><dt><a name="-Z3_mk_bvredand"><strong>Z3_mk_bvredand</strong></a>(a0, a1, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
@@ -1616,11 +1673,36 @@ Data descriptors defined here:<br>
|
||||
a2,
|
||||
_elems=<z3.z3core.Elementaries object>
|
||||
)</dt></dl>
|
||||
- <dl><dt><a name="-Z3_mk_bvsge"><strong>Z3_mk_bvsge</strong></a>(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
- <dl><dt><a name="-Z3_mk_bvsgt"><strong>Z3_mk_bvsgt</strong></a>(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
- <dl><dt><a name="-Z3_mk_bvshl"><strong>Z3_mk_bvshl</strong></a>(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
- <dl><dt><a name="-Z3_mk_bvsle"><strong>Z3_mk_bvsle</strong></a>(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
- <dl><dt><a name="-Z3_mk_bvslt"><strong>Z3_mk_bvslt</strong></a>(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
+ <dl><dt><a name="-Z3_mk_bvsge"><strong>Z3_mk_bvsge</strong></a>(
|
||||
+ a0,
|
||||
+ a1,
|
||||
+ a2,
|
||||
+ _elems=<z3.z3core.Elementaries object>
|
||||
+)</dt></dl>
|
||||
+ <dl><dt><a name="-Z3_mk_bvsgt"><strong>Z3_mk_bvsgt</strong></a>(
|
||||
+ a0,
|
||||
+ a1,
|
||||
+ a2,
|
||||
+ _elems=<z3.z3core.Elementaries object>
|
||||
+)</dt></dl>
|
||||
+ <dl><dt><a name="-Z3_mk_bvshl"><strong>Z3_mk_bvshl</strong></a>(
|
||||
+ a0,
|
||||
+ a1,
|
||||
+ a2,
|
||||
+ _elems=<z3.z3core.Elementaries object>
|
||||
+)</dt></dl>
|
||||
+ <dl><dt><a name="-Z3_mk_bvsle"><strong>Z3_mk_bvsle</strong></a>(
|
||||
+ a0,
|
||||
+ a1,
|
||||
+ a2,
|
||||
+ _elems=<z3.z3core.Elementaries object>
|
||||
+)</dt></dl>
|
||||
+ <dl><dt><a name="-Z3_mk_bvslt"><strong>Z3_mk_bvslt</strong></a>(
|
||||
+ a0,
|
||||
+ a1,
|
||||
+ a2,
|
||||
+ _elems=<z3.z3core.Elementaries object>
|
||||
+)</dt></dl>
|
||||
<dl><dt><a name="-Z3_mk_bvsmod"><strong>Z3_mk_bvsmod</strong></a>(
|
||||
a0,
|
||||
a1,
|
||||
@@ -1633,7 +1715,12 @@ Data descriptors defined here:<br>
|
||||
a2,
|
||||
_elems=<z3.z3core.Elementaries object>
|
||||
)</dt></dl>
|
||||
- <dl><dt><a name="-Z3_mk_bvsub"><strong>Z3_mk_bvsub</strong></a>(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
+ <dl><dt><a name="-Z3_mk_bvsub"><strong>Z3_mk_bvsub</strong></a>(
|
||||
+ a0,
|
||||
+ a1,
|
||||
+ a2,
|
||||
+ _elems=<z3.z3core.Elementaries object>
|
||||
+)</dt></dl>
|
||||
<dl><dt><a name="-Z3_mk_bvsub_no_overflow"><strong>Z3_mk_bvsub_no_overflow</strong></a>(
|
||||
a0,
|
||||
a1,
|
||||
@@ -1653,10 +1740,30 @@ Data descriptors defined here:<br>
|
||||
a2,
|
||||
_elems=<z3.z3core.Elementaries object>
|
||||
)</dt></dl>
|
||||
- <dl><dt><a name="-Z3_mk_bvuge"><strong>Z3_mk_bvuge</strong></a>(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
- <dl><dt><a name="-Z3_mk_bvugt"><strong>Z3_mk_bvugt</strong></a>(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
- <dl><dt><a name="-Z3_mk_bvule"><strong>Z3_mk_bvule</strong></a>(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
- <dl><dt><a name="-Z3_mk_bvult"><strong>Z3_mk_bvult</strong></a>(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
+ <dl><dt><a name="-Z3_mk_bvuge"><strong>Z3_mk_bvuge</strong></a>(
|
||||
+ a0,
|
||||
+ a1,
|
||||
+ a2,
|
||||
+ _elems=<z3.z3core.Elementaries object>
|
||||
+)</dt></dl>
|
||||
+ <dl><dt><a name="-Z3_mk_bvugt"><strong>Z3_mk_bvugt</strong></a>(
|
||||
+ a0,
|
||||
+ a1,
|
||||
+ a2,
|
||||
+ _elems=<z3.z3core.Elementaries object>
|
||||
+)</dt></dl>
|
||||
+ <dl><dt><a name="-Z3_mk_bvule"><strong>Z3_mk_bvule</strong></a>(
|
||||
+ a0,
|
||||
+ a1,
|
||||
+ a2,
|
||||
+ _elems=<z3.z3core.Elementaries object>
|
||||
+)</dt></dl>
|
||||
+ <dl><dt><a name="-Z3_mk_bvult"><strong>Z3_mk_bvult</strong></a>(
|
||||
+ a0,
|
||||
+ a1,
|
||||
+ a2,
|
||||
+ _elems=<z3.z3core.Elementaries object>
|
||||
+)</dt></dl>
|
||||
<dl><dt><a name="-Z3_mk_bvurem"><strong>Z3_mk_bvurem</strong></a>(
|
||||
a0,
|
||||
a1,
|
||||
@@ -1669,7 +1776,12 @@ Data descriptors defined here:<br>
|
||||
a2,
|
||||
_elems=<z3.z3core.Elementaries object>
|
||||
)</dt></dl>
|
||||
- <dl><dt><a name="-Z3_mk_bvxor"><strong>Z3_mk_bvxor</strong></a>(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
+ <dl><dt><a name="-Z3_mk_bvxor"><strong>Z3_mk_bvxor</strong></a>(
|
||||
+ a0,
|
||||
+ a1,
|
||||
+ a2,
|
||||
+ _elems=<z3.z3core.Elementaries object>
|
||||
+)</dt></dl>
|
||||
<dl><dt><a name="-Z3_mk_char"><strong>Z3_mk_char</strong></a>(a0, a1, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
<dl><dt><a name="-Z3_mk_char_from_bv"><strong>Z3_mk_char_from_bv</strong></a>(
|
||||
a0,
|
||||
@@ -1705,7 +1817,12 @@ Data descriptors defined here:<br>
|
||||
_elems=<z3.z3core.Elementaries object>
|
||||
)</dt></dl>
|
||||
<dl><dt><a name="-Z3_mk_config"><strong>Z3_mk_config</strong></a>(_elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
- <dl><dt><a name="-Z3_mk_const"><strong>Z3_mk_const</strong></a>(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
+ <dl><dt><a name="-Z3_mk_const"><strong>Z3_mk_const</strong></a>(
|
||||
+ a0,
|
||||
+ a1,
|
||||
+ a2,
|
||||
+ _elems=<z3.z3core.Elementaries object>
|
||||
+)</dt></dl>
|
||||
<dl><dt><a name="-Z3_mk_const_array"><strong>Z3_mk_const_array</strong></a>(
|
||||
a0,
|
||||
a1,
|
||||
@@ -1765,7 +1882,11 @@ Data descriptors defined here:<br>
|
||||
a2,
|
||||
_elems=<z3.z3core.Elementaries object>
|
||||
)</dt></dl>
|
||||
- <dl><dt><a name="-Z3_mk_empty_set"><strong>Z3_mk_empty_set</strong></a>(a0, a1, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
+ <dl><dt><a name="-Z3_mk_empty_set"><strong>Z3_mk_empty_set</strong></a>(
|
||||
+ a0,
|
||||
+ a1,
|
||||
+ _elems=<z3.z3core.Elementaries object>
|
||||
+)</dt></dl>
|
||||
<dl><dt><a name="-Z3_mk_enumeration_sort"><strong>Z3_mk_enumeration_sort</strong></a>(
|
||||
a0,
|
||||
a1,
|
||||
@@ -2056,7 +2177,10 @@ Data descriptors defined here:<br>
|
||||
a0,
|
||||
_elems=<z3.z3core.Elementaries object>
|
||||
)</dt></dl>
|
||||
- <dl><dt><a name="-Z3_mk_fpa_sort_half"><strong>Z3_mk_fpa_sort_half</strong></a>(a0, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
+ <dl><dt><a name="-Z3_mk_fpa_sort_half"><strong>Z3_mk_fpa_sort_half</strong></a>(
|
||||
+ a0,
|
||||
+ _elems=<z3.z3core.Elementaries object>
|
||||
+)</dt></dl>
|
||||
<dl><dt><a name="-Z3_mk_fpa_sort_quadruple"><strong>Z3_mk_fpa_sort_quadruple</strong></a>(
|
||||
a0,
|
||||
_elems=<z3.z3core.Elementaries object>
|
||||
@@ -2197,7 +2321,12 @@ Data descriptors defined here:<br>
|
||||
_elems=<z3.z3core.Elementaries object>
|
||||
)</dt></dl>
|
||||
<dl><dt><a name="-Z3_mk_int2real"><strong>Z3_mk_int2real</strong></a>(a0, a1, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
- <dl><dt><a name="-Z3_mk_int64"><strong>Z3_mk_int64</strong></a>(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
+ <dl><dt><a name="-Z3_mk_int64"><strong>Z3_mk_int64</strong></a>(
|
||||
+ a0,
|
||||
+ a1,
|
||||
+ a2,
|
||||
+ _elems=<z3.z3core.Elementaries object>
|
||||
+)</dt></dl>
|
||||
<dl><dt><a name="-Z3_mk_int_sort"><strong>Z3_mk_int_sort</strong></a>(a0, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
<dl><dt><a name="-Z3_mk_int_symbol"><strong>Z3_mk_int_symbol</strong></a>(
|
||||
a0,
|
||||
@@ -2333,7 +2462,12 @@ Data descriptors defined here:<br>
|
||||
a5,
|
||||
_elems=<z3.z3core.Elementaries object>
|
||||
)</dt></dl>
|
||||
- <dl><dt><a name="-Z3_mk_power"><strong>Z3_mk_power</strong></a>(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
+ <dl><dt><a name="-Z3_mk_power"><strong>Z3_mk_power</strong></a>(
|
||||
+ a0,
|
||||
+ a1,
|
||||
+ a2,
|
||||
+ _elems=<z3.z3core.Elementaries object>
|
||||
+)</dt></dl>
|
||||
<dl><dt><a name="-Z3_mk_probe"><strong>Z3_mk_probe</strong></a>(a0, a1, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
<dl><dt><a name="-Z3_mk_quantifier"><strong>Z3_mk_quantifier</strong></a>(
|
||||
a0,
|
||||
@@ -2426,7 +2560,11 @@ Data descriptors defined here:<br>
|
||||
a3,
|
||||
_elems=<z3.z3core.Elementaries object>
|
||||
)</dt></dl>
|
||||
- <dl><dt><a name="-Z3_mk_re_option"><strong>Z3_mk_re_option</strong></a>(a0, a1, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
+ <dl><dt><a name="-Z3_mk_re_option"><strong>Z3_mk_re_option</strong></a>(
|
||||
+ a0,
|
||||
+ a1,
|
||||
+ _elems=<z3.z3core.Elementaries object>
|
||||
+)</dt></dl>
|
||||
<dl><dt><a name="-Z3_mk_re_plus"><strong>Z3_mk_re_plus</strong></a>(a0, a1, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
<dl><dt><a name="-Z3_mk_re_power"><strong>Z3_mk_re_power</strong></a>(
|
||||
a0,
|
||||
@@ -2520,7 +2658,11 @@ Data descriptors defined here:<br>
|
||||
a2,
|
||||
_elems=<z3.z3core.Elementaries object>
|
||||
)</dt></dl>
|
||||
- <dl><dt><a name="-Z3_mk_seq_empty"><strong>Z3_mk_seq_empty</strong></a>(a0, a1, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
+ <dl><dt><a name="-Z3_mk_seq_empty"><strong>Z3_mk_seq_empty</strong></a>(
|
||||
+ a0,
|
||||
+ a1,
|
||||
+ _elems=<z3.z3core.Elementaries object>
|
||||
+)</dt></dl>
|
||||
<dl><dt><a name="-Z3_mk_seq_extract"><strong>Z3_mk_seq_extract</strong></a>(
|
||||
a0,
|
||||
a1,
|
||||
@@ -2627,7 +2769,11 @@ Data descriptors defined here:<br>
|
||||
a2,
|
||||
_elems=<z3.z3core.Elementaries object>
|
||||
)</dt></dl>
|
||||
- <dl><dt><a name="-Z3_mk_seq_to_re"><strong>Z3_mk_seq_to_re</strong></a>(a0, a1, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
+ <dl><dt><a name="-Z3_mk_seq_to_re"><strong>Z3_mk_seq_to_re</strong></a>(
|
||||
+ a0,
|
||||
+ a1,
|
||||
+ _elems=<z3.z3core.Elementaries object>
|
||||
+)</dt></dl>
|
||||
<dl><dt><a name="-Z3_mk_seq_unit"><strong>Z3_mk_seq_unit</strong></a>(a0, a1, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
<dl><dt><a name="-Z3_mk_set_add"><strong>Z3_mk_set_add</strong></a>(
|
||||
a0,
|
||||
@@ -2683,7 +2829,10 @@ Data descriptors defined here:<br>
|
||||
a2,
|
||||
_elems=<z3.z3core.Elementaries object>
|
||||
)</dt></dl>
|
||||
- <dl><dt><a name="-Z3_mk_simple_solver"><strong>Z3_mk_simple_solver</strong></a>(a0, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
+ <dl><dt><a name="-Z3_mk_simple_solver"><strong>Z3_mk_simple_solver</strong></a>(
|
||||
+ a0,
|
||||
+ _elems=<z3.z3core.Elementaries object>
|
||||
+)</dt></dl>
|
||||
<dl><dt><a name="-Z3_mk_simplifier"><strong>Z3_mk_simplifier</strong></a>(
|
||||
a0,
|
||||
a1,
|
||||
@@ -3052,7 +3201,11 @@ Data descriptors defined here:<br>
|
||||
a2,
|
||||
_elems=<z3.z3core.Elementaries object>
|
||||
)</dt></dl>
|
||||
- <dl><dt><a name="-Z3_optimize_pop"><strong>Z3_optimize_pop</strong></a>(a0, a1, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
+ <dl><dt><a name="-Z3_optimize_pop"><strong>Z3_optimize_pop</strong></a>(
|
||||
+ a0,
|
||||
+ a1,
|
||||
+ _elems=<z3.z3core.Elementaries object>
|
||||
+)</dt></dl>
|
||||
<dl><dt><a name="-Z3_optimize_push"><strong>Z3_optimize_push</strong></a>(
|
||||
a0,
|
||||
a1,
|
||||
@@ -3288,8 +3441,18 @@ Data descriptors defined here:<br>
|
||||
a1,
|
||||
_elems=<z3.z3core.Elementaries object>
|
||||
)</dt></dl>
|
||||
- <dl><dt><a name="-Z3_probe_eq"><strong>Z3_probe_eq</strong></a>(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
- <dl><dt><a name="-Z3_probe_ge"><strong>Z3_probe_ge</strong></a>(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
+ <dl><dt><a name="-Z3_probe_eq"><strong>Z3_probe_eq</strong></a>(
|
||||
+ a0,
|
||||
+ a1,
|
||||
+ a2,
|
||||
+ _elems=<z3.z3core.Elementaries object>
|
||||
+)</dt></dl>
|
||||
+ <dl><dt><a name="-Z3_probe_ge"><strong>Z3_probe_ge</strong></a>(
|
||||
+ a0,
|
||||
+ a1,
|
||||
+ a2,
|
||||
+ _elems=<z3.z3core.Elementaries object>
|
||||
+)</dt></dl>
|
||||
<dl><dt><a name="-Z3_probe_get_descr"><strong>Z3_probe_get_descr</strong></a>(
|
||||
a0,
|
||||
a1,
|
||||
@@ -3300,16 +3463,36 @@ Data descriptors defined here:<br>
|
||||
a1,
|
||||
_elems=<z3.z3core.Elementaries object>
|
||||
)</dt></dl>
|
||||
- <dl><dt><a name="-Z3_probe_gt"><strong>Z3_probe_gt</strong></a>(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
+ <dl><dt><a name="-Z3_probe_gt"><strong>Z3_probe_gt</strong></a>(
|
||||
+ a0,
|
||||
+ a1,
|
||||
+ a2,
|
||||
+ _elems=<z3.z3core.Elementaries object>
|
||||
+)</dt></dl>
|
||||
<dl><dt><a name="-Z3_probe_inc_ref"><strong>Z3_probe_inc_ref</strong></a>(
|
||||
a0,
|
||||
a1,
|
||||
_elems=<z3.z3core.Elementaries object>
|
||||
)</dt></dl>
|
||||
- <dl><dt><a name="-Z3_probe_le"><strong>Z3_probe_le</strong></a>(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
- <dl><dt><a name="-Z3_probe_lt"><strong>Z3_probe_lt</strong></a>(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
+ <dl><dt><a name="-Z3_probe_le"><strong>Z3_probe_le</strong></a>(
|
||||
+ a0,
|
||||
+ a1,
|
||||
+ a2,
|
||||
+ _elems=<z3.z3core.Elementaries object>
|
||||
+)</dt></dl>
|
||||
+ <dl><dt><a name="-Z3_probe_lt"><strong>Z3_probe_lt</strong></a>(
|
||||
+ a0,
|
||||
+ a1,
|
||||
+ a2,
|
||||
+ _elems=<z3.z3core.Elementaries object>
|
||||
+)</dt></dl>
|
||||
<dl><dt><a name="-Z3_probe_not"><strong>Z3_probe_not</strong></a>(a0, a1, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
- <dl><dt><a name="-Z3_probe_or"><strong>Z3_probe_or</strong></a>(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
+ <dl><dt><a name="-Z3_probe_or"><strong>Z3_probe_or</strong></a>(
|
||||
+ a0,
|
||||
+ a1,
|
||||
+ a2,
|
||||
+ _elems=<z3.z3core.Elementaries object>
|
||||
+)</dt></dl>
|
||||
<dl><dt><a name="-Z3_qe_lite"><strong>Z3_qe_lite</strong></a>(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
<dl><dt><a name="-Z3_qe_model_project"><strong>Z3_qe_model_project</strong></a>(
|
||||
a0,
|
||||
@@ -3605,7 +3788,11 @@ Data descriptors defined here:<br>
|
||||
a3,
|
||||
_elems=<z3.z3core.Elementaries object>
|
||||
)</dt></dl>
|
||||
- <dl><dt><a name="-Z3_solver_check"><strong>Z3_solver_check</strong></a>(a0, a1, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
+ <dl><dt><a name="-Z3_solver_check"><strong>Z3_solver_check</strong></a>(
|
||||
+ a0,
|
||||
+ a1,
|
||||
+ _elems=<z3.z3core.Elementaries object>
|
||||
+)</dt></dl>
|
||||
<dl><dt><a name="-Z3_solver_check_assumptions"><strong>Z3_solver_check_assumptions</strong></a>(
|
||||
a0,
|
||||
a1,
|
||||
@@ -3862,7 +4049,11 @@ Data descriptors defined here:<br>
|
||||
a3,
|
||||
_elems=<z3.z3core.Elementaries object>
|
||||
)</dt></dl>
|
||||
- <dl><dt><a name="-Z3_solver_reset"><strong>Z3_solver_reset</strong></a>(a0, a1, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
+ <dl><dt><a name="-Z3_solver_reset"><strong>Z3_solver_reset</strong></a>(
|
||||
+ a0,
|
||||
+ a1,
|
||||
+ _elems=<z3.z3core.Elementaries object>
|
||||
+)</dt></dl>
|
||||
<dl><dt><a name="-Z3_solver_set_initial_value"><strong>Z3_solver_set_initial_value</strong></a>(
|
||||
a0,
|
||||
a1,
|
||||
@@ -4118,7 +4309,11 @@ Data descriptors defined here:<br>
|
||||
_elems=<z3.z3core.Elementaries object>
|
||||
)</dt></dl>
|
||||
<dl><dt><a name="-Z3_to_app"><strong>Z3_to_app</strong></a>(a0, a1, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
- <dl><dt><a name="-Z3_to_func_decl"><strong>Z3_to_func_decl</strong></a>(a0, a1, _elems=<z3.z3core.Elementaries object>)</dt></dl>
|
||||
+ <dl><dt><a name="-Z3_to_func_decl"><strong>Z3_to_func_decl</strong></a>(
|
||||
+ a0,
|
||||
+ a1,
|
||||
+ _elems=<z3.z3core.Elementaries object>
|
||||
+)</dt></dl>
|
||||
<dl><dt><a name="-Z3_toggle_warning_messages"><strong>Z3_toggle_warning_messages</strong></a>(
|
||||
a0,
|
||||
_elems=<z3.z3core.Elementaries object>
|
||||
60
z3.spec
60
z3.spec
|
|
@ -7,15 +7,12 @@
|
|||
# unless somebody is really, really persuasive and available to help fix it
|
||||
# if it breaks.
|
||||
|
||||
# A Go interface is now available, but Fedora no longer builds Go library
|
||||
# packages (https://docs.fedoraproject.org/en-US/packaging-guidelines/Golang/).
|
||||
|
||||
# Tests are off by default because some of the tests require more memory than
|
||||
# the koji builders have available.
|
||||
%bcond test 0
|
||||
|
||||
Name: z3
|
||||
Version: 5.1.0
|
||||
Version: 4.15.8
|
||||
Release: %autorelease
|
||||
Summary: Satisfiability Modulo Theories (SMT) solver
|
||||
|
||||
|
|
@ -28,22 +25,13 @@ VCS : git:%{giturl}.git
|
|||
Source: %{giturl}/archive/%{name}-%{version}.tar.gz
|
||||
# Do not try to build or install native OCaml artifacts on bytecode-only arches
|
||||
Patch: %{name}-ocaml.patch
|
||||
# Fix up the s390x docs so they look like other arches
|
||||
Patch: %{name}-s390x-doc.patch
|
||||
|
||||
# See https://fedoraproject.org/wiki/Changes/EncourageI686LeafRemoval
|
||||
ExcludeArch: %{ix86}
|
||||
BuildSystem: cmake
|
||||
BuildOption(conf): -G Ninja
|
||||
BuildOption(conf): -DCMAKE_INSTALL_INCLUDEDIR=%{_includedir}/z3
|
||||
BuildOption(conf): -DZ3_BUILD_DOCUMENTATION:BOOL=ON
|
||||
%ifarch %{java_arches}
|
||||
BuildOption(conf): -DZ3_BUILD_JAVA_BINDINGS:BOOL=ON
|
||||
%endif
|
||||
BuildOption(conf): -DZ3_BUILD_PYTHON_BINDINGS:BOOL=ON
|
||||
BuildOption(conf): -DCMAKE_INSTALL_PYTHON_PKG_DIR=%{python3_sitelib}
|
||||
BuildOption(conf): -DZ3_INCLUDE_GIT_HASH:BOOL=OFF
|
||||
BuildOption(conf): -DZ3_INCLUDE_GIT_DESCRIBE:BOOL=OFF
|
||||
BuildOption(conf): -DZ3_USE_LIB_GMP:BOOL=ON
|
||||
|
||||
BuildRequires: cmake
|
||||
BuildRequires: doxygen
|
||||
BuildRequires: gcc-c++
|
||||
BuildRequires: gmp-devel
|
||||
|
|
@ -57,6 +45,7 @@ BuildRequires: make
|
|||
BuildRequires: ninja-build
|
||||
BuildRequires: ocaml
|
||||
BuildRequires: ocaml-findlib
|
||||
BuildRequires: ocaml-ocamldoc
|
||||
BuildRequires: ocaml-zarith-devel
|
||||
BuildRequires: python3-devel
|
||||
BuildRequires: %{py3_dist setuptools}
|
||||
|
|
@ -148,6 +137,7 @@ Python 3 interface to z3.
|
|||
%patch 0 -p1
|
||||
%endif
|
||||
|
||||
%conf
|
||||
# Enable verbose builds, use Fedora CFLAGS, preserve timestamps when installing,
|
||||
# include the entire contents of the archives in the library, link the library
|
||||
# with the correct flags, and build the ocaml files with debuginfo.
|
||||
|
|
@ -157,7 +147,7 @@ sed \
|
|||
-e "s/\(['\"]\)cp\([^[:alnum:]]\)/\1cp -p\2/" \
|
||||
-e "s/\(SLIBEXTRAFLAGS = '\)'/\1-Wl,--no-whole-archive'/" \
|
||||
-e '/SLIBFLAGS/s|-shared|& %{build_ldflags} -Wl,--whole-archive|' \
|
||||
-e 's/\(libz3$(SO_EXT)\)\( \$(SLINK\)/\1 -Wl,--no-whole-archive\2/' \
|
||||
-e 's/\(libz3$(SO_EXT)\)\(\\n\)/\1 -Wl,--no-whole-archive\2/' \
|
||||
-e "s/OCAML_FLAGS = ''/OCAML_FLAGS = '-g'/" \
|
||||
-i scripts/mk_util.py
|
||||
|
||||
|
|
@ -169,16 +159,35 @@ sed -e '/libz3java/s,\(System\.load\)Library("\(.*\)"),\1("%{_libdir}/z3/\2.so")
|
|||
# Turn off HTML timestamps for reproducible builds
|
||||
sed -i '/HTML_TIMESTAMP/s/YES/NO/' doc/z3api.cfg.in doc/z3code.dox
|
||||
|
||||
%build -p
|
||||
%build
|
||||
export PYTHON=%{python3}
|
||||
|
||||
%build -a
|
||||
%cmake -G Ninja \
|
||||
-DCMAKE_INSTALL_INCLUDEDIR=%{_includedir}/z3 \
|
||||
-DZ3_BUILD_DOCUMENTATION:BOOL=ON \
|
||||
%ifarch %{java_arches}
|
||||
-DZ3_BUILD_JAVA_BINDINGS:BOOL=ON \
|
||||
%endif
|
||||
-DZ3_BUILD_PYTHON_BINDINGS:BOOL=ON \
|
||||
-DCMAKE_INSTALL_PYTHON_PKG_DIR=%{python3_sitelib} \
|
||||
-DZ3_INCLUDE_GIT_HASH:BOOL=OFF \
|
||||
-DZ3_INCLUDE_GIT_DESCRIBE:BOOL=OFF \
|
||||
-DZ3_USE_LIB_GMP:BOOL=ON
|
||||
|
||||
%cmake_build
|
||||
|
||||
# Remove meaningless memory addresses from the pydoc documentation
|
||||
# See https://github.com/python/cpython/issues/83572
|
||||
sed -ri 's/, handle [0-9a-fA-F]+//' \
|
||||
%{_vpath_builddir}/doc/api/html/z3{,.z3{,num,poly,printer,rcf,util}}.html
|
||||
sed -ri 's/ at 0x[0-9a-fA-F]+//g' \
|
||||
%{_vpath_builddir}/doc/api/html/z3.z3core.html
|
||||
# For unknown reasons, the s390x documentation build has fewer newlines than
|
||||
# the builds on other architectures. Make the outputs match so the doc
|
||||
# package can be noarch.
|
||||
%ifarch s390x
|
||||
patch -p1 -T -d %{_vpath_builddir} < %{PATCH1}
|
||||
%endif
|
||||
|
||||
# The cmake build system does not build the OCaml interface. Do that manually.
|
||||
#
|
||||
|
|
@ -197,7 +206,10 @@ sed -i '/^api/s/ libz3\$(SO_EXT)//g' build/Makefile
|
|||
# Fourth, build the OCaml interface
|
||||
%make_build -C build ml
|
||||
|
||||
%install -a
|
||||
%install
|
||||
# Install the C++, python3, and Java interfaces
|
||||
%cmake_install
|
||||
|
||||
%ifarch %{java_arches}
|
||||
# Move the Java interface to its correct location
|
||||
mkdir -p %{buildroot}%{_libdir}/z3
|
||||
|
|
@ -229,8 +241,8 @@ help2man -N -o %{buildroot}%{_mandir}/man1/z3.1 \
|
|||
# Fix the pkgconfig file
|
||||
sed -i 's,//usr,,' %{buildroot}%{_libdir}/pkgconfig/z3.pc
|
||||
|
||||
%check
|
||||
%if %{with test}
|
||||
%check
|
||||
cd build
|
||||
make test-z3
|
||||
./test-z3 /a
|
||||
|
|
@ -244,7 +256,7 @@ cd -
|
|||
|
||||
%files libs
|
||||
%license LICENSE.txt
|
||||
%{_libdir}/libz3.so.5.1{,.*}
|
||||
%{_libdir}/libz3.so.4.15{,.*}
|
||||
|
||||
%files devel
|
||||
%{_includedir}/z3/
|
||||
|
|
@ -259,7 +271,7 @@ cd -
|
|||
%ifarch %{java_arches}
|
||||
%files -n java-z3
|
||||
%{_libdir}/z3/
|
||||
%{_jnidir}/com.microsoft.z3.jar
|
||||
%{_jnidir}/com.microsoft.z3*jar
|
||||
%endif
|
||||
|
||||
%files -n ocaml-z3
|
||||
|
|
@ -270,7 +282,7 @@ cd -
|
|||
%ifarch %{ocaml_native_compiler}
|
||||
%{ocamldir}/Z3/*.cmxs
|
||||
%endif
|
||||
%{ocamldir}/stublibs/dllz3ml.so
|
||||
%{ocamldir}/stublibs/*.so
|
||||
|
||||
%files -n ocaml-z3-devel
|
||||
%{ocamldir}/Z3/*.a
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue