pkgsrc-Changes-HG archive
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index][Old Index]
[pkgsrc/trunk]: pkgsrc/math/z3 math/z3: make this build on NetBSD/macppc 9.99...
details: https://anonhg.NetBSD.org/pkgsrc/rev/8646d2950d51
branches: trunk
changeset: 385720:8646d2950d51
user: he <he%pkgsrc.org@localhost>
date: Sun Sep 25 11:01:34 2022 +0000
description:
math/z3: make this build on NetBSD/macppc 9.99.99.
Fixes two issues:
* <immintrin.h> is only available on amd64 and i386 (I think...)
* The scanner depends on signed chars a number of places. Sprinkle
"signed" a minimal set of places to make this explicit, to deal
with powerpc where "char" == "unsigned char".
Bump PKGREVISION.
diffstat:
math/z3/Makefile | 4 +-
math/z3/distinfo | 5 +-
math/z3/patches/patch-src_parsers_util_scanner.cpp | 96 ++++++++++++++++++++++
math/z3/patches/patch-src_parsers_util_scanner.h | 26 +++++
math/z3/patches/patch-src_util_mpz.cpp | 16 +++
5 files changed, 144 insertions(+), 3 deletions(-)
diffs (182 lines):
diff -r a9230b3884dc -r 8646d2950d51 math/z3/Makefile
--- a/math/z3/Makefile Sun Sep 25 10:23:10 2022 +0000
+++ b/math/z3/Makefile Sun Sep 25 11:01:34 2022 +0000
@@ -1,7 +1,7 @@
-# $NetBSD: Makefile,v 1.16 2022/05/24 18:51:53 jaapb Exp $
+# $NetBSD: Makefile,v 1.17 2022/09/25 11:01:34 he Exp $
.include "Makefile.common"
-PKGREVISION= 3
+PKGREVISION= 4
COMMENT= The Z3 theorem prover / SMT solver
.include "options.mk"
diff -r a9230b3884dc -r 8646d2950d51 math/z3/distinfo
--- a/math/z3/distinfo Sun Sep 25 10:23:10 2022 +0000
+++ b/math/z3/distinfo Sun Sep 25 11:01:34 2022 +0000
@@ -1,11 +1,14 @@
-$NetBSD: distinfo,v 1.12 2022/05/13 10:41:38 jperkin Exp $
+$NetBSD: distinfo,v 1.13 2022/09/25 11:01:34 he Exp $
BLAKE2s (z3-4.8.3.tar.gz) = 18b9f2b708f35c57c4dfb425521106dd7f938296738087ff761f030bff7a3491
SHA512 (z3-4.8.3.tar.gz) = 34a2dca0083ed469fdaf5ac062dda26248633245607ddd9ef90629c5f76ae30f87bfa4191c04ba9be7a617bf182a1bd00b59fd2274699e12ece69b86088c8044
Size (z3-4.8.3.tar.gz) = 4119116 bytes
SHA1 (patch-scripts_mk__genfile__common.py) = 442da5eb2dcdfa4e4a5d70dc377c29053f58be5a
SHA1 (patch-scripts_mk__util.py) = f7059330a8ea44a566448557fae3967051e237cb
+SHA1 (patch-src_parsers_util_scanner.cpp) = 284f9ef965c4d4f4954fcbb6437c143c57dde516
+SHA1 (patch-src_parsers_util_scanner.h) = ad1b385672615501a9249b20829256052ce82dbd
SHA1 (patch-src_sat_ba__solver.cpp) = 1e80b79c76f8e3766a60be3065ff8bd932249178
SHA1 (patch-src_sat_sat__lookahead.cpp) = c091d8b267b5476e438888e82c9161599873264c
SHA1 (patch-src_sat_sat__solver.cpp) = 3421afbf641c47cf3b44ece9168ff3f768168343
SHA1 (patch-src_solver_parallel__tactic.cpp) = 029a2625e19cfcfb18c4b69279dea257cfd5482f
+SHA1 (patch-src_util_mpz.cpp) = 499062b5107572184adcb7353ccde7c9f7b28951
diff -r a9230b3884dc -r 8646d2950d51 math/z3/patches/patch-src_parsers_util_scanner.cpp
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/math/z3/patches/patch-src_parsers_util_scanner.cpp Sun Sep 25 11:01:34 2022 +0000
@@ -0,0 +1,96 @@
+$NetBSD: patch-src_parsers_util_scanner.cpp,v 1.1 2022/09/25 11:01:34 he Exp $
+
+Adapt to system where char == unsigned char.
+
+--- src/parsers/util/scanner.cpp.orig 2018-11-19 20:21:17.000000000 +0000
++++ src/parsers/util/scanner.cpp
+@@ -18,7 +18,7 @@ Revision History:
+ --*/
+ #include "parsers/util/scanner.h"
+
+-inline char scanner::read_char() {
++inline signed char scanner::read_char() {
+ if (m_is_interactive) {
+ ++m_pos;
+ return m_stream.get();
+@@ -58,7 +58,7 @@ inline bool scanner::state_ok() {
+
+ void scanner::comment(char delimiter) {
+ while(state_ok()) {
+- char ch = read_char();
++ signed char ch = read_char();
+ if ('\n' == ch) {
+ ++m_line;
+ }
+@@ -68,7 +68,7 @@ void scanner::comment(char delimiter) {
+ }
+ }
+
+-scanner::token scanner::read_symbol(char ch) {
++scanner::token scanner::read_symbol(signed char ch) {
+ bool escape = false;
+ if (m_smt2)
+ m_string.pop_back(); // remove leading '|'
+@@ -94,7 +94,7 @@ scanner::token scanner::read_symbol(char
+
+
+ scanner::token scanner::read_id(char first_char) {
+- char ch;
++ signed char ch;
+ m_string.reset();
+ m_params.reset();
+ m_string.push_back(first_char);
+@@ -159,7 +159,7 @@ bool scanner::read_params() {
+ unsigned param_num = 0;
+
+ while (state_ok()) {
+- char ch = read_char();
++ signed char ch = read_char();
+ switch (m_normalized[(unsigned char) ch]) {
+ case '0':
+ param_num = 10*param_num + (ch - '0');
+@@ -208,7 +208,7 @@ scanner::token scanner::read_number(char
+ m_state = INT_TOKEN;
+
+ while (true) {
+- char ch = read_char();
++ signed char ch = read_char();
+ if (m_normalized[(unsigned char) ch] == '0') {
+ m_number = rational(10)*m_number + rational(ch - '0');
+ if (m_state == FLOAT_TOKEN) {
+@@ -236,7 +236,7 @@ scanner::token scanner::read_string(char
+ m_string.reset();
+ m_params.reset();
+ while (true) {
+- char ch = read_char();
++ signed char ch = read_char();
+
+ if (!state_ok()) {
+ return m_state;
+@@ -265,7 +265,7 @@ scanner::token scanner::read_string(char
+ scanner::token scanner::read_bv_literal() {
+ TRACE("scanner", tout << "read_bv_literal\n";);
+ if (m_bv_token) {
+- char ch = read_char();
++ signed char ch = read_char();
+ if (ch == 'x') {
+ ch = read_char();
+ m_number = rational(0);
+@@ -315,7 +315,7 @@ scanner::token scanner::read_bv_literal(
+ }
+ else {
+ // hack for the old parser
+- char ch = read_char();
++ signed char ch = read_char();
+ bool is_hex = false;
+
+ m_state = ID_TOKEN;
+@@ -449,7 +449,7 @@ scanner::scanner(std::istream& stream, s
+
+ scanner::token scanner::scan() {
+ while (state_ok()) {
+- char ch = read_char();
++ signed char ch = read_char();
+ switch (m_normalized[(unsigned char) ch]) {
+ case ' ':
+ break;
diff -r a9230b3884dc -r 8646d2950d51 math/z3/patches/patch-src_parsers_util_scanner.h
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/math/z3/patches/patch-src_parsers_util_scanner.h Sun Sep 25 11:01:34 2022 +0000
@@ -0,0 +1,26 @@
+$NetBSD: patch-src_parsers_util_scanner.h,v 1.1 2022/09/25 11:01:34 he Exp $
+
+Adapt to systems where char == unsigned char.
+
+--- src/parsers/util/scanner.h.orig 2018-11-19 20:21:17.000000000 +0000
++++ src/parsers/util/scanner.h
+@@ -63,7 +63,7 @@ private:
+ rational m_number;
+ unsigned m_bv_size;
+ token m_state;
+- char m_normalized[256];
++ signed char m_normalized[256];
+ vector<char> m_string;
+ std::istream& m_stream;
+ std::ostream& m_err;
+@@ -76,8 +76,8 @@ private:
+ bool m_smt2;
+ bool m_bv_token;
+
+- char read_char();
+- token read_symbol(char ch);
++ signed char read_char();
++ token read_symbol(signed char ch);
+ void unread_char();
+ void comment(char delimiter);
+ token read_id(char first_char);
diff -r a9230b3884dc -r 8646d2950d51 math/z3/patches/patch-src_util_mpz.cpp
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/math/z3/patches/patch-src_util_mpz.cpp Sun Sep 25 11:01:34 2022 +0000
@@ -0,0 +1,16 @@
+$NetBSD: patch-src_util_mpz.cpp,v 1.3 2022/09/25 11:01:34 he Exp $
+
+<immintrin.h> is Intel-only(?)
+
+--- src/util/mpz.cpp.orig 2018-11-19 20:21:17.000000000 +0000
++++ src/util/mpz.cpp
+@@ -30,7 +30,9 @@ Revision History:
+ #else
+ #error No multi-precision library selected.
+ #endif
++#if defined(_AMD64_) || defined(__i386__)
+ #include <immintrin.h>
++#endif
+
+ // Available GCD algorithms
+ // #define EUCLID_GCD
Home |
Main Index |
Thread Index |
Old Index