head 1.7; access; symbols pkgsrc-2026Q1:1.7.0.10 pkgsrc-2026Q1-base:1.7 pkgsrc-2025Q4:1.7.0.8 pkgsrc-2025Q4-base:1.7 pkgsrc-2025Q3:1.7.0.6 pkgsrc-2025Q3-base:1.7 pkgsrc-2025Q2:1.7.0.4 pkgsrc-2025Q2-base:1.7 pkgsrc-2025Q1:1.7.0.2 pkgsrc-2025Q1-base:1.7 pkgsrc-2024Q4:1.6.0.4 pkgsrc-2024Q4-base:1.6 pkgsrc-2024Q3:1.6.0.2 pkgsrc-2024Q3-base:1.6 pkgsrc-2024Q2:1.5.0.10 pkgsrc-2024Q2-base:1.5 pkgsrc-2024Q1:1.5.0.8 pkgsrc-2024Q1-base:1.5 pkgsrc-2023Q4:1.5.0.6 pkgsrc-2023Q4-base:1.5 pkgsrc-2023Q3:1.5.0.4 pkgsrc-2023Q3-base:1.5 pkgsrc-2023Q2:1.5.0.2 pkgsrc-2023Q2-base:1.5 pkgsrc-2023Q1:1.4.0.8 pkgsrc-2023Q1-base:1.4 pkgsrc-2022Q4:1.4.0.6 pkgsrc-2022Q4-base:1.4 pkgsrc-2022Q3:1.4.0.4 pkgsrc-2022Q3-base:1.4 pkgsrc-2022Q2:1.4.0.2 pkgsrc-2022Q2-base:1.4 pkgsrc-2022Q1:1.3.0.28 pkgsrc-2022Q1-base:1.3 pkgsrc-2021Q4:1.3.0.26 pkgsrc-2021Q4-base:1.3 pkgsrc-2021Q3:1.3.0.24 pkgsrc-2021Q3-base:1.3 pkgsrc-2021Q2:1.3.0.22 pkgsrc-2021Q2-base:1.3 pkgsrc-2021Q1:1.3.0.20 pkgsrc-2021Q1-base:1.3 pkgsrc-2020Q4:1.3.0.18 pkgsrc-2020Q4-base:1.3 pkgsrc-2020Q3:1.3.0.16 pkgsrc-2020Q3-base:1.3 pkgsrc-2020Q2:1.3.0.14 pkgsrc-2020Q2-base:1.3 pkgsrc-2020Q1:1.3.0.10 pkgsrc-2020Q1-base:1.3 pkgsrc-2019Q4:1.3.0.12 pkgsrc-2019Q4-base:1.3 pkgsrc-2019Q3:1.3.0.8 pkgsrc-2019Q3-base:1.3 pkgsrc-2019Q2:1.3.0.6 pkgsrc-2019Q2-base:1.3 pkgsrc-2019Q1:1.3.0.4 pkgsrc-2019Q1-base:1.3 pkgsrc-2018Q4:1.3.0.2 pkgsrc-2018Q4-base:1.3 pkgsrc-2018Q3:1.2.0.6 pkgsrc-2018Q3-base:1.2 pkgsrc-2018Q2:1.2.0.4 pkgsrc-2018Q2-base:1.2 pkgsrc-2018Q1:1.2.0.2 pkgsrc-2018Q1-base:1.2 pkgsrc-2017Q4:1.1.0.20 pkgsrc-2017Q4-base:1.1 pkgsrc-2017Q3:1.1.0.18 pkgsrc-2017Q3-base:1.1 pkgsrc-2017Q2:1.1.0.14 pkgsrc-2017Q2-base:1.1 pkgsrc-2017Q1:1.1.0.12 pkgsrc-2017Q1-base:1.1 pkgsrc-2016Q4:1.1.0.10 pkgsrc-2016Q4-base:1.1 pkgsrc-2016Q3:1.1.0.8 pkgsrc-2016Q3-base:1.1 pkgsrc-2016Q2:1.1.0.6 pkgsrc-2016Q2-base:1.1 pkgsrc-2016Q1:1.1.0.4 pkgsrc-2016Q1-base:1.1 pkgsrc-2015Q4:1.1.0.2 pkgsrc-2015Q4-base:1.1; locks; strict; comment @# @; 1.7 date 2025.02.20.10.27.00; author adam; state Exp; branches; next 1.6; commitid SAqjKsXdnKpX7cKF; 1.6 date 2024.08.13.09.21.07; author adam; state Exp; branches; next 1.5; commitid MhD64uLWnEU1UDlF; 1.5 date 2023.05.11.06.43.43; author adam; state Exp; branches; next 1.4; commitid NkSzgCRCxrwEOvoE; 1.4 date 2022.05.13.10.41.38; author jperkin; state Exp; branches; next 1.3; commitid n6nYwO76wYYSNSDD; 1.3 date 2018.12.18.06.46.39; author kamil; state Exp; branches; next 1.2; commitid vgESWChRmqlWof4B; 1.2 date 2018.03.13.00.31.16; author khorben; state Exp; branches; next 1.1; commitid p9NJNo2DxEyEkeuA; 1.1 date 2015.11.24.05.45.58; author dholland; state Exp; branches; next ; commitid OXRKcwxUA0WA5jKy; desc @@ 1.7 log @z3 py-z3: updated to 4.14.0 4.14.0 bump timeout for jobs Update release.yml for Azure Pipelines Update nightly.yaml for Azure Pipelines Update azure-pipelines.yml for Azure Pipelines fix unit test convert def into expression tree adjust solve_for to handle rationals fixes to failure conditions for unification remove verbose output Add unification based projection function @ text @@@comment $NetBSD: PLIST,v 1.6 2024/08/13 09:21:07 adam Exp $ bin/z3 include/z3++.h include/z3.h include/z3_algebraic.h include/z3_api.h include/z3_ast_containers.h include/z3_fixedpoint.h include/z3_fpa.h include/z3_macros.h include/z3_optimization.h include/z3_polynomial.h include/z3_rcf.h include/z3_spacer.h include/z3_v1.h include/z3_version.h lib/cmake/z3/Z3Config.cmake lib/cmake/z3/Z3ConfigVersion.cmake lib/cmake/z3/Z3Targets-relwithdebinfo.cmake lib/cmake/z3/Z3Targets.cmake lib/libz3.so lib/libz3.so.4.14 lib/libz3.so.${PKGVERSION}.0 lib/pkgconfig/z3.pc @ 1.6 log @z3 py-z3: updated to 4.13.0 Version 4.13.0 - add ARM64 wheels for Python, thanks to Steven Moy, smoy @ text @d1 1 a1 1 @@comment $NetBSD: PLIST,v 1.5 2023/05/11 06:43:43 adam Exp $ d22 1 a22 1 lib/libz3.so.4.13 @ 1.5 log @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 @ text @d1 1 a1 1 @@comment $NetBSD: PLIST,v 1.4 2022/05/13 10:41:38 jperkin Exp $ d22 1 a22 1 lib/libz3.so.4.12 @ 1.4 log @z3: Portability fixes. @ text @d1 1 a1 1 @@comment $NetBSD: PLIST,v 1.3 2018/12/18 06:46:39 kamil Exp $ d17 4 a20 1 ${PLIST.java}lib/com.microsoft.z3.jar d22 3 a24 17 ${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 @ 1.3 log @z3: Upgrade to 4.8.3 Eliminate merged patches. Improve java support. Patch by Michal Gorny. Upstream changelog ================== z3-4.8.3 This release covers bug fixes since 4.8.1 .NET bindings for dotnet standard 1.4 on windows and 64 bit Linux systems and MacOs z3-4.8.1 New requirements: A breaking change to the API is that parsers for SMT-LIB2 formulas return a vector of formulas as opposed to a conjunction of formulas. The vector of formulas correspond to the set of "assert" instructions in the SMT-LIB input. New features A parallel mode is available for select theories, including QF_BV. By setting parallel.enable=true Z3 will spawn a number of worker threads proportional to the number of available CPU cores to apply cube and conquer solving on the goal. The SAT solver by default handle cardinality and PB constraints using a custom plugin that operates directly on cardinality and PB constraints. A "cube" interface is exposed over the solver API. Model conversion is first class over the textual API, such that subgoals created from running a solver can be passed in text files and a model for the original formula can be recreated from the result. This has also led to changes in how models are tracked over tactic subgoals. The API for extracting models from apply_result have been replaced. An optional mode handles xor constraints using a custom xor propagator. It is off by default and its value not demonstrated. The SAT solver includes new inprocessing techniques that are available during simplification. It performs asymmetric tautology elimination by default, and one can turn on more powerful inprocessing techniques (known as ACCE, ABCE, CCE). Asymmetric branching also uses features introduced in Lingeling by exploiting binary implication graphs. Use sat.acce=true to enable the full repertoire of inprocessing methods. By default, clauses that are "eliminated" by acce are tagged as lemmas (redundant) and are garbage collected if their glue level is high. Substantial overhaul of the spacer horn clause engine. Added basic features to support Lambda bindings. Added model compression to eliminate local function definitions in models when inlining them does not incur substantial overhead. The old behavior, where models are left uncompressed can be replayed by setting the top-level parameter model_compress=false. Integration of a new solver for linear integer arithmetic and mixed linear integer arithmetic by Lev Nachmanson. It incorporates several improvements to QF_LIA solving based on . using a better LP engine, which is already the foundation for QF_LRA . including cuts based on Hermite Normal Form (thanks to approaches described in "cuts from proofs" and "cutting the mix"). . extracting integer solutions from LP solutions by tightening bounds selectively. We use a generalization of Bromberger and Weidenbach that allows avoiding selected bounds tighthenings (https://easychair.org/publications/paper/qGfG). It solves significantly more problems in the QF_LIA category and may at this point also be the best solver for your problem as well. The new solver is enabled only for select SMT-LIB logics. These include QF_LIA, QF_IDL, and QF_UFLIA. Other theories (still) use the legacy solver for arithmetic. You can enable the new solver by setting the parameter smt.arith.solver=6 to give it a spin. Removed features: interpolation API duality engine for constrained Horn clauses. pdr engine for constrained Horn clauses. The engine's functionality has been folded into spacer as one of optional strategies. long deprecated API functions have been removed from z3_api.h Z3 4.7.1. official release cumulative bug fix since 4.6.0 minor version incremented as API now uses stdbool and stdint: bool and int64_t, uint64_t Official release Z3 4.6.0. @ text @d1 1 a1 1 @@comment $NetBSD: PLIST,v 1.2 2018/03/13 00:31:16 khorben Exp $ d17 1 d19 1 a35 2 ${PLIST.java}lib/com.microsoft.z3.jar ${PLIST.java}lib/libz3java.so @ 1.2 log @Update math/z3 to version 4.5.0 From the release notes: New features: - New theories of strings and sequences. - Incremental consequence finder for finite domains. - CMake build system (thanks @@delcypher). - Updated and improved OCaml API (thanks @@martin-neuhaeusser). - Updated and improved Java API (thanks @@cheshire). - New resource limit facilities to avoid non-deterministic timeout behaviour. - New bit-vector simplification and ackermannization tactics (thanks @@MikolasJanota, @@nunoplopes). - QSAT: a new solver for quantified arithmetic problems. See: Bjorner, Janota: Playing with Quantified Satisfaction, LPAR 2016. A multitude of bugs has been fixed. I am about to commit a separate package for the Python bindings. Coordinated with dholland@@ @ text @d1 1 a1 1 @@comment $NetBSD$ a9 1 include/z3_interp.h d14 1 d16 1 d34 2 @ 1.1 log @Package the Z3 theorem prover / SMT solver from Microsoft Research. @ text @d7 2 d12 1 d17 16 a32 21 ${PYSITELIB}/libz3.so ${PYSITELIB}/z3.py ${PYSITELIB}/z3.pyc ${PYSITELIB}/z3consts.py ${PYSITELIB}/z3consts.pyc ${PYSITELIB}/z3core.py ${PYSITELIB}/z3core.pyc ${PYSITELIB}/z3num.py ${PYSITELIB}/z3num.pyc ${PYSITELIB}/z3poly.py ${PYSITELIB}/z3poly.pyc ${PYSITELIB}/z3printer.py ${PYSITELIB}/z3printer.pyc ${PYSITELIB}/z3rcf.py ${PYSITELIB}/z3rcf.pyc ${PYSITELIB}/z3test.py ${PYSITELIB}/z3test.pyc ${PYSITELIB}/z3types.py ${PYSITELIB}/z3types.pyc ${PYSITELIB}/z3util.py ${PYSITELIB}/z3util.pyc @