CVS commit: pkgsrc/math

To: pkgsrc-changes%NetBSD.org@localhost
Subject: CVS commit: pkgsrc/math
From: "Adam Ciarcinski" <adam%netbsd.org@localhost>
Date: Thu, 11 May 2023 06:43:43 +0000

Module Name:    pkgsrc
Committed By:   adam
Date:           Thu May 11 06:43:43 UTC 2023

Modified Files:
        pkgsrc/math/py-z3: Makefile PLIST
        pkgsrc/math/z3: Makefile Makefile.common PLIST distinfo
        pkgsrc/math/z3/patches: patch-scripts_mk__util.py
            patch-src_sat_sat__solver.cpp
Added Files:
        pkgsrc/math/z3/patches: patch-src_api_python_setup.py
Removed Files:
        pkgsrc/math/z3: options.mk
        pkgsrc/math/z3/patches: patch-scripts_mk__genfile__common.py
            patch-src_parsers_util_scanner.cpp patch-src_parsers_util_scanner.h
            patch-src_sat_ba__solver.cpp patch-src_solver_parallel__tactic.cpp
            patch-src_util_mpz.cpp

Log Message:
z3 py-z3: updated to 4.12.1

Version 4.12.1
==============
- change macos build to use explicit reference to Macos version 11. Hosted builds are migrating to macos-12 and it broke a user

Version 4.12.0
==============
- add clause logging API.
  - The purpose of logging API and self-checking is to enable an array of use cases.
    - proof mining (what instantiations did Z3 use)?
      - A refresh of the AxiomProfiler could use the logging API.
        The (brittle) trace feature should be deprecated.
    - debugging
      - a built-in self certifier implements a custom proof checker for
        the format used by the new solver (sat.euf=true).
    - other potential options:
      - integration into certified tool chains
      - interpolation
  - Z3_register_on_clause (also exposed over C++, Python and .Net)
  - it applies to z3's main CDCL(T) core and a new CDCL(T) core (sat.euf=true).
  - The added API function allows to register a callback for when clauses
    are inferred. More precisely, when clauses are assumed (as part of input),
    deleted, or deduced.
    Clauses that are deduced by the CDCL SAT engine using standard
    inferences are marked as 'rup'.
    Clauses that are deduced by theories are marked by default
    by 'smt', and when more detailed information
    is available with proof hints or proof objects.
    Instantations are considered useful to track so they
    are logged using terms of the form

         (inst (not (forall (x) body)) body[t/x] (bind t)), where

    'inst' is a name of a function that produces a proof term representing
    the instantiation.
- add options for proof logging, trimming, and checking for the new core.
  - sat.smt.proof (symbol) add SMT proof to file (default: )
  - sat.smt.proof.check (bool) check SMT proof while it is created (default: false)
    - it applies a custom self-validator. The self-validator comprises of
      several small checkers and represent a best-effort validation mechanism.
      If there are no custom validators associated with inferences, or the custom
      validators fail to certify inferences, the self-validator falls back to
      invoking z3 (SMT) solving on the lemma.
      - euf - propagations and conflicts from congruence closure
              (theory of equality and uninterpreted functions) are checked
              based on a proof format that tracks uses of congruence closure and
              equalities. It only performs union find operations.
      - tseitin - clausification steps are checked for Boolean operators.
      - farkas, bound, implies_eq - arithmetic inferences that can be justified using
              a combination of Farkas lemma and cuts are checked.
              Note: the arithmetic solver may produce proof hints that the proof
              checker cannot check. It is mainly a limitation
              of the arithmetic solver not pulling relevant information.
              Ensuring a tight coupling with proof hints and the validator
              capabilites is open ended future work and good material for theses.
      - bit-vector inferences - are treated as trusted
        (there is no validation, it always blindly succeeds)
      - arrays, datatypes - there is no custom validation for
        other theories at present. Lemmas are validated using SMT.
  - sat.smt.proof.check_rup (bool) apply forward RUP proof checking (default: true)
    - this option can incur significant runtime overhead.
      Effective proof checking relies on first trimming proofs into a
      format where dependencies are tracked and then checking relevant inferences.
      Turn this option off if you just want to check theory inferences.
- add options to validate proofs offline. It applies to proofs
  saved when sat.smt.proof is set to a valid file name.
  - solver.proof.check (bool) check proof logs (default: true)
    - the option sat.smt.proof_check_rup can be used to control what is checked
  - solver.proof.save (bool) save proof log into a proof object
      that can be extracted using (get-proof) (default: false)
    - experimental: saves a proof log into a term
  - solver.proof.trim (bool) trim the offline proof and print the trimmed proof to the console
    - experimental: performs DRUP trimming to reduce the set of hypotheses
      and inferences relevant to derive the empty clause.
- JS support for Arrays, thanks to Walden Yan
- More portable memory allocation, thanks to Nuno Lopes
  (avoid custom handling to calculate memory usage)

- clause logging and proofs: many open-ended directions.
  Many directions and functionality features remain in an open-ended state,
  subject to fixes, improvements, and contributions.
  We list a few of them here:
  - comprehensive efficient self-validators for arithmetic, and other theories
  - an efficient proof checker when several theory solvers cooperate in a propagation or
    conflict. The theory combination case is currently delegated to the smt solver.
    The proper setup for integrating theory lemmas is in principle not complicated,
    but the implementation requires some changes.
  - external efficient proof validators (based on certified tool chains)
    can be integrated over the API.
  - dampening repeated clauses: A side-effect of conflict resolution is to
    log theory lemmas. It often happens that the theory lemma becomes
    the conflict clause, that is then logged as rup. Thus, two clauses are
    logged.
  - support for online trim so that proofs generated using clause logging can be used for SPACER
    - SPACER also would benefit from more robust proof hints for arithmetic
      lemmas (bounds and implied equalities are sometimes not logged correctly)
  - integration into axiom profiling through online and/or offline interfaces.
    - an online interface attaches a callback with a running solver. This is available.
    - an offline interface saves a clause proof to a file (currently just
      supported for sat.euf) and then reads the file in a separate process
      The separate process attaches a callback on inferred clauses.
      This is currently not available but a relatively small feature.
  - more detailed proof hints for the legacy solver clause logger.
    Other than quantifier instantiations, no detailed information is retained for
    theory clauses.
  - integration of pre-processing proofs with logging proofs. There is
    currently no supported bridge to create a end-to-end proof objects.
- experimental API for accessing E-graphs. Exposed over Python. This API should be considered temporary
and subject to be changed depending on use cases or removed. The functions are `Z3_solver_congruence_root`, `Z3_solver_congruence_next`.

Version 4.11.2
==============
- add error handling to fromString method in JavaScript
- fix regression in default parameters for CDCL, thanks to Nuno Lopes
- fix model evaluation bugs for as-array nested under functions (data-type constructors)
- add rewrite simplifications for datatypes with a single constructor
- add "Global Guidance" capability to SPACER, thanks to Arie Gurfinkel and Hari Gorvind.
  The commit logs related to Global Guidance contain detailed information.
- change proof logging format for the new core to use SMTLIB commands.
  The format was so far an extension of DRAT used by SAT solvers, but not well compatible
  with SMT format that is extensible. The resulting format is a mild extension of SMTLIB with
  three extra commands assume, learn, del. They track input clauses, generated clauses and deleted clauses.
  They are optionally augmented by proof hints. Two proof hints are used in the current version: "rup" and "farkas".
  "rup" is used whent the generated clause can be justified by reverse unit propagation. "farkas" is used when
  the clause can be justified by a combination of Farkas cutting planes. There is a built-in proof checker for the
  format. Quantifier instantiations are also tracked as proof hints.
  Other proof hints are to be added as the feature set is tested and developed. The fallback, buit-in,
  self-checker uses z3 to check that the generated clause is a consequence. Note that this is generally
  insufficient as generated clauses are in principle required to only be satisfiability preserving.
  Proof checking and tranformation operations is overall open ended.
  The log for the first commit introducing this change contains further information on the format.
- fix to re-entrancy bug in user propagator (thanks to Clemens Eisenhofer).
- handle _toExpr for quantified formulas in JS bindings


To generate a diff of this commit:
cvs rdiff -u -r1.4 -r1.5 pkgsrc/math/py-z3/Makefile
cvs rdiff -u -r1.1 -r1.2 pkgsrc/math/py-z3/PLIST
cvs rdiff -u -r1.17 -r1.18 pkgsrc/math/z3/Makefile
cvs rdiff -u -r1.4 -r1.5 pkgsrc/math/z3/Makefile.common pkgsrc/math/z3/PLIST
cvs rdiff -u -r1.13 -r1.14 pkgsrc/math/z3/distinfo
cvs rdiff -u -r1.4 -r0 pkgsrc/math/z3/options.mk
cvs rdiff -u -r1.2 -r0 \
    pkgsrc/math/z3/patches/patch-scripts_mk__genfile__common.py
cvs rdiff -u -r1.7 -r1.8 pkgsrc/math/z3/patches/patch-scripts_mk__util.py
cvs rdiff -u -r0 -r1.1 pkgsrc/math/z3/patches/patch-src_api_python_setup.py
cvs rdiff -u -r1.1 -r0 \
    pkgsrc/math/z3/patches/patch-src_parsers_util_scanner.cpp \
    pkgsrc/math/z3/patches/patch-src_parsers_util_scanner.h \
    pkgsrc/math/z3/patches/patch-src_sat_ba__solver.cpp \
    pkgsrc/math/z3/patches/patch-src_solver_parallel__tactic.cpp
cvs rdiff -u -r1.1 -r1.2 pkgsrc/math/z3/patches/patch-src_sat_sat__solver.cpp
cvs rdiff -u -r1.3 -r0 pkgsrc/math/z3/patches/patch-src_util_mpz.cpp

Please note that diffs are not public domain; they are subject to the
copyright notices on the relevant files.

Modified files:

Index: pkgsrc/math/py-z3/Makefile
diff -u pkgsrc/math/py-z3/Makefile:1.4 pkgsrc/math/py-z3/Makefile:1.5
--- pkgsrc/math/py-z3/Makefile:1.4      Sun May 31 20:47:23 2020
+++ pkgsrc/math/py-z3/Makefile  Thu May 11 06:43:43 2023
@@ -1,25 +1,26 @@
-# $NetBSD: Makefile,v 1.4 2020/05/31 20:47:23 joerg Exp $
+# $NetBSD: Makefile,v 1.5 2023/05/11 06:43:43 adam Exp $
 
 .include "../../math/z3/Makefile.common"
 
 PKGNAME=       ${PYPKGPREFIX}-${DISTNAME}
-GITHUB_PROJECT=        z3
+COMMENT=       Efficient SMT solver library
 
-COMMENT=       Python bindings for the Z3 theorem prover / SMT solver
+USE_TOOLS+=    cmake ninja
+PYSETUPSUBDIR= src/api/python
+EGG_NAME=      ${DISTNAME:S/z3/z3_solver/}.0
+
+.include "../../mk/bsd.prefs.mk"
+
+post-install:
+       # same binary as in math/z3
+       ${RM} ${DESTDIR}${PREFIX}/bin/z3
+.if ${OPSYS} == "Darwin"
+       install_name_tool -id ${PREFIX}/${PYSITELIB}/z3/lib/libz3.${PKGVERSION_NOREV:R}.dylib \
+       ${DESTDIR}${PREFIX}/${PYSITELIB}/z3/lib/libz3.${PKGVERSION_NOREV:R}.dylib
+       install_name_tool -id ${PREFIX}/${PYSITELIB}/z3/lib/libz3.dylib \
+       ${DESTDIR}${PREFIX}/${PYSITELIB}/z3/lib/libz3.dylib
+.endif
 
-CONFIGURE_ARGS+=       --python
-NO_BUILD=              yes
-PY_PATCHPLIST=         yes
-
-PYZ3DIR=               ${PREFIX}/${PYSITELIB}/z3
-INSTALLATION_DIRS+=    ${PYZ3DIR}
-INSTALLATION_DIRS+=    ${PYZ3DIR}/lib
-
-do-install:
-       ${LN} -s ${LIBDIR}/libz3.so ${DESTDIR}${PYZ3DIR}/lib/libz3.so
-       ${INSTALL_DATA} ${WRKSRC}/build/python/z3/*.py ${DESTDIR}${PYZ3DIR}
-       ${PY_COMPILE_ALL} ${DESTDIR}${PYZ3DIR}
-
-.include "../../lang/python/extension.mk"
+.include "../../lang/python/egg.mk"
 .include "../../math/z3/buildlink3.mk"
 .include "../../mk/bsd.pkg.mk"

Index: pkgsrc/math/py-z3/PLIST
diff -u pkgsrc/math/py-z3/PLIST:1.1 pkgsrc/math/py-z3/PLIST:1.2
--- pkgsrc/math/py-z3/PLIST:1.1 Tue Mar 13 00:36:05 2018
+++ pkgsrc/math/py-z3/PLIST     Thu May 11 06:43:43 2023
@@ -1,22 +1,64 @@
-@comment $NetBSD: PLIST,v 1.1 2018/03/13 00:36:05 khorben Exp $
+@comment $NetBSD: PLIST,v 1.2 2023/05/11 06:43:43 adam Exp $
+${PYSITELIB}/${EGG_INFODIR}/PKG-INFO
+${PYSITELIB}/${EGG_INFODIR}/SOURCES.txt
+${PYSITELIB}/${EGG_INFODIR}/dependency_links.txt
+${PYSITELIB}/${EGG_INFODIR}/top_level.txt
 ${PYSITELIB}/z3/__init__.py
 ${PYSITELIB}/z3/__init__.pyc
+${PYSITELIB}/z3/__init__.pyo
+${PYSITELIB}/z3/include/api_ast_map.h
+${PYSITELIB}/z3/include/api_ast_vector.h
+${PYSITELIB}/z3/include/api_context.h
+${PYSITELIB}/z3/include/api_datalog.h
+${PYSITELIB}/z3/include/api_goal.h
+${PYSITELIB}/z3/include/api_model.h
+${PYSITELIB}/z3/include/api_polynomial.h
+${PYSITELIB}/z3/include/api_solver.h
+${PYSITELIB}/z3/include/api_stats.h
+${PYSITELIB}/z3/include/api_tactic.h
+${PYSITELIB}/z3/include/api_util.h
+${PYSITELIB}/z3/include/z3++.h
+${PYSITELIB}/z3/include/z3.h
+${PYSITELIB}/z3/include/z3_algebraic.h
+${PYSITELIB}/z3/include/z3_api.h
+${PYSITELIB}/z3/include/z3_ast_containers.h
+${PYSITELIB}/z3/include/z3_fixedpoint.h
+${PYSITELIB}/z3/include/z3_fpa.h
+${PYSITELIB}/z3/include/z3_logger.h
+${PYSITELIB}/z3/include/z3_macros.h
+${PYSITELIB}/z3/include/z3_optimization.h
+${PYSITELIB}/z3/include/z3_polynomial.h
+${PYSITELIB}/z3/include/z3_private.h
+${PYSITELIB}/z3/include/z3_rcf.h
+${PYSITELIB}/z3/include/z3_replayer.h
+${PYSITELIB}/z3/include/z3_spacer.h
+${PYSITELIB}/z3/include/z3_v1.h
 ${PYSITELIB}/z3/lib/libz3.so
+${PYSITELIB}/z3/lib/libz3.so.4.12
 ${PYSITELIB}/z3/z3.py
 ${PYSITELIB}/z3/z3.pyc
+${PYSITELIB}/z3/z3.pyo
 ${PYSITELIB}/z3/z3consts.py
 ${PYSITELIB}/z3/z3consts.pyc
+${PYSITELIB}/z3/z3consts.pyo
 ${PYSITELIB}/z3/z3core.py
 ${PYSITELIB}/z3/z3core.pyc
+${PYSITELIB}/z3/z3core.pyo
 ${PYSITELIB}/z3/z3num.py
 ${PYSITELIB}/z3/z3num.pyc
+${PYSITELIB}/z3/z3num.pyo
 ${PYSITELIB}/z3/z3poly.py
 ${PYSITELIB}/z3/z3poly.pyc
+${PYSITELIB}/z3/z3poly.pyo
 ${PYSITELIB}/z3/z3printer.py
 ${PYSITELIB}/z3/z3printer.pyc
+${PYSITELIB}/z3/z3printer.pyo
 ${PYSITELIB}/z3/z3rcf.py
 ${PYSITELIB}/z3/z3rcf.pyc
+${PYSITELIB}/z3/z3rcf.pyo
 ${PYSITELIB}/z3/z3types.py
 ${PYSITELIB}/z3/z3types.pyc
+${PYSITELIB}/z3/z3types.pyo
 ${PYSITELIB}/z3/z3util.py
 ${PYSITELIB}/z3/z3util.pyc
+${PYSITELIB}/z3/z3util.pyo

Index: pkgsrc/math/z3/Makefile
diff -u pkgsrc/math/z3/Makefile:1.17 pkgsrc/math/z3/Makefile:1.18
--- pkgsrc/math/z3/Makefile:1.17        Sun Sep 25 11:01:34 2022
+++ pkgsrc/math/z3/Makefile     Thu May 11 06:43:43 2023
@@ -1,9 +1,8 @@
-# $NetBSD: Makefile,v 1.17 2022/09/25 11:01:34 he Exp $
+# $NetBSD: Makefile,v 1.18 2023/05/11 06:43:43 adam Exp $
 
 .include "Makefile.common"
-PKGREVISION=   4
-COMMENT=       The Z3 theorem prover / SMT solver
 
-.include "options.mk"
+COMMENT=       The Z3 theorem prover / SMT solver
 
+.include "../../devel/cmake/build.mk"
 .include "../../mk/bsd.pkg.mk"

Index: pkgsrc/math/z3/Makefile.common
diff -u pkgsrc/math/z3/Makefile.common:1.4 pkgsrc/math/z3/Makefile.common:1.5
--- pkgsrc/math/z3/Makefile.common:1.4  Tue Dec 18 06:46:39 2018
+++ pkgsrc/math/z3/Makefile.common      Thu May 11 06:43:43 2023
@@ -1,24 +1,21 @@
-# $NetBSD: Makefile.common,v 1.4 2018/12/18 06:46:39 kamil Exp $
+# $NetBSD: Makefile.common,v 1.5 2023/05/11 06:43:43 adam Exp $
 #
 # used by math/py-z3/Makefile
 # used by math/z3/Makefile
 
-DISTNAME=      z3-4.8.3
-GITHUB_TAG=    ${DISTNAME}
+DISTNAME=      z3-4.12.1
 CATEGORIES=    math
 MASTER_SITES=  ${MASTER_SITE_GITHUB:=Z3Prover/}
+GITHUB_PROJECT=        z3
+GITHUB_TAG=    ${DISTNAME}
+
 DISTINFO_FILE= ${.CURDIR}/../../math/z3/distinfo
 PATCHDIR?=     ${.CURDIR}/../../math/z3/patches
 
 MAINTAINER=    dholland%NetBSD.org@localhost
-HOMEPAGE=      https://github.com/Z3Prover/z3/
+HOMEPAGE=      https://github.com/Z3Prover/z3
 LICENSE=       mit
 
-WRKSRC=                ${WRKDIR}/z3-${DISTNAME}
-HAS_CONFIGURE= yes
 USE_LANGUAGES= c c++
-BUILD_DIRS=    build
-
-CONFIGURE_ENV+=                PYTHON=${PYTHONBIN}
 
 .include "../../lang/python/tool.mk"
Index: pkgsrc/math/z3/PLIST
diff -u pkgsrc/math/z3/PLIST:1.4 pkgsrc/math/z3/PLIST:1.5
--- pkgsrc/math/z3/PLIST:1.4    Fri May 13 10:41:38 2022
+++ pkgsrc/math/z3/PLIST        Thu May 11 06:43:43 2023
@@ -1,4 +1,4 @@
-@comment $NetBSD: PLIST,v 1.4 2022/05/13 10:41:38 jperkin Exp $
+@comment $NetBSD: PLIST,v 1.5 2023/05/11 06:43:43 adam Exp $
 bin/z3
 include/z3++.h
 include/z3.h
@@ -14,22 +14,11 @@ include/z3_rcf.h
 include/z3_spacer.h
 include/z3_v1.h
 include/z3_version.h
-${PLIST.java}lib/com.microsoft.z3.jar
+lib/cmake/z3/Z3Config.cmake
+lib/cmake/z3/Z3ConfigVersion.cmake
+lib/cmake/z3/Z3Targets-relwithdebinfo.cmake
+lib/cmake/z3/Z3Targets.cmake
 lib/libz3.so
-${PLIST.java}lib/libz3java.so
-${PLIST.ocaml}lib/ocaml/site-lib/Z3/META
-${PLIST.ocaml}lib/ocaml/site-lib/Z3/dllz3ml.so
-${PLIST.ocaml}lib/ocaml/site-lib/Z3/libz3ml.a
-${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3.cmi
-${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3.cmx
-${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3.mli
-${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3enums.cmi
-${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3enums.cmx
-${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3enums.mli
-${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3ml.a
-${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3ml.cma
-${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3ml.cmxa
-${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3ml.cmxs
-${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3native.cmi
-${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3native.cmx
-${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3native.mli
+lib/libz3.so.4.12
+lib/libz3.so.${PKGVERSION}.0
+lib/pkgconfig/z3.pc

Index: pkgsrc/math/z3/distinfo
diff -u pkgsrc/math/z3/distinfo:1.13 pkgsrc/math/z3/distinfo:1.14
--- pkgsrc/math/z3/distinfo:1.13        Sun Sep 25 11:01:34 2022
+++ pkgsrc/math/z3/distinfo     Thu May 11 06:43:43 2023
@@ -1,14 +1,9 @@
-$NetBSD: distinfo,v 1.13 2022/09/25 11:01:34 he Exp $
+$NetBSD: distinfo,v 1.14 2023/05/11 06:43:43 adam 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
+BLAKE2s (z3-4.12.1.tar.gz) = 375c80eb90c2cf43b6d42006fcb6618a30a4ce6bb8a761dd8849565ed3ba1ca9
+SHA512 (z3-4.12.1.tar.gz) = 031fba9cc000a8da0025f95fa3f1c7519071d1b7775b377ff3192c505bb4c7e3d267da246c9ae68c940224e055a3c30571d2c0d7fbb042ec9a3d5849543a385c
+Size (z3-4.12.1.tar.gz) = 5470095 bytes
+SHA1 (patch-scripts_mk__util.py) = f092c9aed3c81408a485e9c92d8dddf5db86d6fe
+SHA1 (patch-src_api_python_setup.py) = cfc4a0a388d2a096ce86cbe3ca76b32502ec380e
 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
+SHA1 (patch-src_sat_sat__solver.cpp) = 0e279f291801901eabb11b7cb0268c137a3b41fe

Index: pkgsrc/math/z3/patches/patch-scripts_mk__util.py
diff -u pkgsrc/math/z3/patches/patch-scripts_mk__util.py:1.7 pkgsrc/math/z3/patches/patch-scripts_mk__util.py:1.8
--- pkgsrc/math/z3/patches/patch-scripts_mk__util.py:1.7        Fri May 13 10:41:38 2022
+++ pkgsrc/math/z3/patches/patch-scripts_mk__util.py    Thu May 11 06:43:43 2023
@@ -1,39 +1,29 @@
-$NetBSD: patch-scripts_mk__util.py,v 1.7 2022/05/13 10:41:38 jperkin Exp $
+$NetBSD: patch-scripts_mk__util.py,v 1.8 2023/05/11 06:43:43 adam Exp $
 
 Try to at least be slightly more portable.
 
---- scripts/mk_util.py.orig    2018-11-19 20:21:17.000000000 +0000
+--- scripts/mk_util.py.orig    2023-01-18 03:10:26.000000000 +0000
 +++ scripts/mk_util.py
-@@ -803,7 +803,8 @@ def extract_c_includes(fname):
-     # We should generate and error for any occurrence of #include that does not match the previous pattern.
-     non_std_inc_pat = re.compile(".*#include.*")
- 
--    f = open(fname, 'r')
-+    py3args = { 'encoding': 'UTF-8' } if sys.version_info.major >= 3 else {}
-+    f = open(fname, 'r', **py3args)
-     linenum = 1
-     for line in f:
-         m1 = std_inc_pat.match(line)
-@@ -2001,7 +2002,7 @@ class JavaDLLComponent(Component):
-                 out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(LIB_EXT)\n' %
-                           os.path.join('api', 'java', 'Native'))
+@@ -1858,7 +1858,7 @@ class JavaDLLComponent(Component):
+                 out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) -arch arm64 %s$(OBJ_EXT) libz3$(SO_EXT)\n' %
+                           os.path.join('api', 'java', 'Native'))                
              else:
 -                out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(SO_EXT)\n' %
 +                out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) $(JAVA_LINK_EXTRA_FLAGS) %s$(OBJ_EXT) libz3$(SO_EXT)\n' %
                            os.path.join('api', 'java', 'Native'))
              out.write('%s.jar: libz3java$(SO_EXT) ' % self.package_name)
              deps = ''
-@@ -2694,7 +2695,8 @@ def mk_config():
+@@ -2577,7 +2577,8 @@ def mk_config():
          check_ar()
          CXX = find_cxx_compiler()
          CC  = find_c_compiler()
 -        SLIBEXTRAFLAGS = ''
 +        SLIBEXTRAFLAGS = LDFLAGS
 +        JAVALIBEXTRAFLAGS = LDFLAGS
+ #       SLIBEXTRAFLAGS = '%s -Wl,-soname,libz3.so.0' % LDFLAGS
          EXE_EXT = ''
          LIB_EXT = '.a'
-         if GPROF:
-@@ -2778,7 +2780,8 @@ def mk_config():
+@@ -2647,7 +2648,8 @@ def mk_config():
              EXE_EXT        = '.exe'
              LIB_EXT        = '.lib'
          else:
@@ -43,9 +33,9 @@ Try to at least be slightly more portabl
          if is64():
              if not sysname.startswith('CYGWIN') and not sysname.startswith('MSYS') and not sysname.startswith('MINGW'):
                  CXXFLAGS     = '%s -fPIC' % CXXFLAGS
-@@ -2822,6 +2825,7 @@ def mk_config():
+@@ -2696,6 +2698,7 @@ def mk_config():
          config.write('SLINK_FLAGS=%s\n' % SLIBFLAGS)
-         config.write('SLINK_EXTRA_FLAGS=%s\n' % SLIBEXTRAFLAGS)
+         config.write('SLINK_EXTRA_FLAGS=-lpthread %s\n' % SLIBEXTRAFLAGS)
          config.write('SLINK_OUT_FLAG=-o \n')
 +        config.write('JAVA_LINK_EXTRA_FLAGS=%s\n' % JAVALIBEXTRAFLAGS)
          config.write('OS_DEFINES=%s\n' % OS_DEFINES)

Index: pkgsrc/math/z3/patches/patch-src_sat_sat__solver.cpp
diff -u pkgsrc/math/z3/patches/patch-src_sat_sat__solver.cpp:1.1 pkgsrc/math/z3/patches/patch-src_sat_sat__solver.cpp:1.2
--- pkgsrc/math/z3/patches/patch-src_sat_sat__solver.cpp:1.1    Fri May 13 10:41:38 2022
+++ pkgsrc/math/z3/patches/patch-src_sat_sat__solver.cpp        Thu May 11 06:43:43 2023
@@ -1,15 +1,14 @@
-$NetBSD: patch-src_sat_sat__solver.cpp,v 1.1 2022/05/13 10:41:38 jperkin Exp $
+$NetBSD: patch-src_sat_sat__solver.cpp,v 1.2 2023/05/11 06:43:43 adam Exp $
 
 Avoid ambiguous function call.
 
---- src/sat/sat_solver.cpp.orig        2018-11-19 20:21:17.000000000 +0000
+--- src/sat/sat_solver.cpp.orig        2023-05-08 13:23:26.000000000 +0000
 +++ src/sat/sat_solver.cpp
-@@ -31,6 +31,8 @@ Revision History:
- // define to update glue during propagation
- #define UPDATE_GLUE
+@@ -37,6 +37,7 @@ Revision History:
+ # include <xmmintrin.h>
+ #endif
  
 +using std::pow;
-+
+ 
  namespace sat {
  
-     solver::solver(params_ref const & p, reslimit& l):

Added files:

Index: pkgsrc/math/z3/patches/patch-src_api_python_setup.py
diff -u /dev/null pkgsrc/math/z3/patches/patch-src_api_python_setup.py:1.1
--- /dev/null   Thu May 11 06:43:43 2023
+++ pkgsrc/math/z3/patches/patch-src_api_python_setup.py        Thu May 11 06:43:43 2023
@@ -0,0 +1,15 @@
+$NetBSD: patch-src_api_python_setup.py,v 1.1 2023/05/11 06:43:43 adam Exp $
+
+Some platforms do not support LTO.
+
+--- src/api/python/setup.py.orig       2023-05-10 16:39:33.324575995 +0000
++++ src/api/python/setup.py
+@@ -110,7 +110,7 @@ def _configure_z3():
+         'CMAKE_BUILD_TYPE' : 'Release',
+         'Z3_BUILD_EXECUTABLE' : True,
+         'Z3_BUILD_LIBZ3_SHARED' : True,
+-        'Z3_LINK_TIME_OPTIMIZATION' : True,
++        'Z3_LINK_TIME_OPTIMIZATION' : False,
+         'WARNINGS_AS_ERRORS' : 'SERIOUS_ONLY',
+         # Disable Unwanted Options
+         'Z3_USE_LIB_GMP' : False, # Is default false in python build

Prev by Date: CVS commit: pkgsrc/doc
Next by Date: CVS commit: pkgsrc/emulators
Previous by Thread: CVS commit: pkgsrc/doc
Next by Thread: CVS commit: pkgsrc/emulators
Indexes:

Home | Main Index | Thread Index | Old Index