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.

5 files changed, 144 insertions, 3 deletions

diff --git a/math/z3/Makefile b/math/z3/Makefile
index 419b147c0b9..f5f19668a6b 100644
--- a/math/z3/Makefile
+++ b/math/z3/Makefile
@@ -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 --git a/math/z3/distinfo b/math/z3/distinfo
index 6e000ca7815..4b2995a823b 100644
--- a/math/z3/distinfo
+++ b/math/z3/distinfo
@@ -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 --git a/math/z3/patches/patch-src_parsers_util_scanner.cpp b/math/z3/patches/patch-src_parsers_util_scanner.cpp
new file mode 100644
index 00000000000..3ca579d39b9
--- /dev/null
+++ b/math/z3/patches/patch-src_parsers_util_scanner.cpp
@@ -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 --git a/math/z3/patches/patch-src_parsers_util_scanner.h b/math/z3/patches/patch-src_parsers_util_scanner.h
new file mode 100644
index 00000000000..e3112e4078d
--- /dev/null
+++ b/math/z3/patches/patch-src_parsers_util_scanner.h
@@ -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 --git a/math/z3/patches/patch-src_util_mpz.cpp b/math/z3/patches/patch-src_util_mpz.cpp
new file mode 100644
index 00000000000..910d05025fa
--- /dev/null
+++ b/math/z3/patches/patch-src_util_mpz.cpp
@@ -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