CVS commit: pkgsrc/math/py-z3solver

To: pkgsrc-changes%NetBSD.org@localhost
Subject: CVS commit: pkgsrc/math/py-z3solver
From: "Pierre Pronchery" <khorben%netbsd.org@localhost>
Date: Fri, 18 Sep 2020 05:00:48 +0000

Module Name:    pkgsrc
Committed By:   khorben
Date:           Fri Sep 18 05:00:48 UTC 2020

Modified Files:
        pkgsrc/math/py-z3solver: Makefile PLIST distinfo
Removed Files:
        pkgsrc/math/py-z3solver/patches: patch-core_scripts_mk__util.py
            patch-core_src_util_lp_permutation__matrix.h
            patch-core_src_util_stopwatch.h

Log Message:
py-z3solver: update to version 4.8.9.0

Version 4.8.9
=============
- New features
  - significant improvements to regular expression solving
  - expose user theory plugin. It is a leaner user theory plugin that was once available.
    It allows for registering callbacks that react to when bit-vector and Boolean variables
    receive fixed values.
- Bug fixes
  - many
- Notes
  - the new arithmetic theory is turned on by default. It _does_ introduce regressions on
    several scenarios, but has its own advantages. Users can turn on the old solver by setting smt.arith.solver=2.
    Depending on feedback, we may turn toggle this default setting again back to smt.arith.solver=2.

Version 4.8.8
=============
- New features
  - rewritten NIA (non-linear integer arithmetic) core solver
    It is enabled in selected theories as default.
    The legacy arithmetic solver remains the overall default in this release
    as the rewritten solver shows regressions (on mainly NRA problems).
  - recursive function representation without hoisting ite expressions. Issue #2601
  - model-based interpolation for quantifier-free UF, arithmetic
  - Julia bindings over the C++ API, thanks to ahumenberger
- Bug fixes
  - numerous, many based on extensive fuzz testing.
    Thanks to 5hadowblad3, muchang, numairmansur, rainoftime, wintered
- Notes
  - recursive functions are unfolded with separate increments based on unsat core
    analysis of blocking literals that are separate for different recursive functions.
  - the seq (string) solver has been revised in several ways and likely shows some
    regressions in this release.

Version 4.8.7
=============
- New features
  - setting parameter on solver over the API by
    solver.smtlib2_log=<filename>
    enables tracing calls into the solver as SMTLIB2 commands.
    It traces, assert, push, pop, check_sat, get_consequences.
- Notes
  - various bug fixes
  - remove model_compress. Use model.compact
  - print weights with quantifiers when weight is != 1

Version 4.8.6
=============
- Notes
  - various bug fixes
  - built in support for PIP, thanks to Audrey Dutcher
  - VS compilation mode including misc flags for managed packages

Version 4.8.5
=============
- Notes
  - various bug fixes

Version 4.8.4
=============

- Notes
  - fixes bugs
  - a substantial update to how the seq theory solver handles regular
    expressions. Other performance improvements to the seq solver.
  - Managed .NET DLLs include dotnet standard 1.4 on supported platforms.
  - Windows Managed DLLs are strong signed in the released binaries.

Version 4.8.3
=============
- New features
  - Native handling of recursive function definitions, thanks to Simon Cruanes
  - PB rounding based option for conflict resolution when reasoning about PB constraints.
  - Access to numeral constants as a double from the native API.

- Notes
  - fixes several bugs discovered since the 4.8.1 release.

Version 4.8.2
=============
- Post-Release.

Version 4.8.1
=============
- Release. Bug-fix for 4.8.0

Version 4.8.0
=============

- 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 tightenings (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

Version 4.7.1
=============

- New requirements:
  - uses stdbool and stdint as part of z3.

- New features:
  - none

- Removed features:
  - none

- Notes:
   This is a minor release prior to a set of planned major updates.
   It uses minor version 7 to indicate that the use of stdbool and
   stdint are breaking changes to consumers of the C-based API.

Version 4.6.0
=============

- New requirements:
  - C++11 capable compiler to build Z3.
  - C++ API now requires C++11 or newer.

- New features (including):
  - A new string solver from University of Waterloo
  - A new linear real arithmetic solver
  - Changed behavior for optimization commands from the SMT2 command-line interface.
    Objective values are no longer printed by default. They can be retrieved by
    issuing the command (get-objectives). Pareto front objectives are accessed by
    issuing multiple (check-sat) calls until it returns unsat.

- Removed features:
  - Removed support for SMT-LIB 1.x


To generate a diff of this commit:
cvs rdiff -u -r1.3 -r1.4 pkgsrc/math/py-z3solver/Makefile
cvs rdiff -u -r1.1 -r1.2 pkgsrc/math/py-z3solver/PLIST
cvs rdiff -u -r1.2 -r1.3 pkgsrc/math/py-z3solver/distinfo
cvs rdiff -u -r1.1 -r0 \
    pkgsrc/math/py-z3solver/patches/patch-core_scripts_mk__util.py \
    pkgsrc/math/py-z3solver/patches/patch-core_src_util_lp_permutation__matrix.h \
    pkgsrc/math/py-z3solver/patches/patch-core_src_util_stopwatch.h

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-z3solver/Makefile
diff -u pkgsrc/math/py-z3solver/Makefile:1.3 pkgsrc/math/py-z3solver/Makefile:1.4
--- pkgsrc/math/py-z3solver/Makefile:1.3        Tue Mar 20 16:24:34 2018
+++ pkgsrc/math/py-z3solver/Makefile    Fri Sep 18 05:00:48 2020
@@ -1,7 +1,7 @@
-# $NetBSD: Makefile,v 1.3 2018/03/20 16:24:34 khorben Exp $
+# $NetBSD: Makefile,v 1.4 2020/09/18 05:00:48 khorben Exp $
 
-DISTNAME=      z3-solver-4.5.1.0.post2
-PKGNAME=       ${PYPKGPREFIX}-z3solver-4.5.1.0.post2
+DISTNAME=      z3-solver-4.8.9.0
+PKGNAME=       ${PYPKGPREFIX}-z3solver-4.8.9.0
 CATEGORIES=    math
 MASTER_SITES=  ${MASTER_SITE_PYPI:=z/z3-solver/}
 
@@ -12,8 +12,6 @@ LICENSE=      mit
 
 USE_LANGUAGES= c c++
 
-PYTHON_VERSIONS_ACCEPTED=      27
-
 CONFLICTS+=    z3-[0-9]*
 
 .include "../../lang/python/egg.mk"

Index: pkgsrc/math/py-z3solver/PLIST
diff -u pkgsrc/math/py-z3solver/PLIST:1.1 pkgsrc/math/py-z3solver/PLIST:1.2
--- pkgsrc/math/py-z3solver/PLIST:1.1   Tue Mar 20 15:47:36 2018
+++ pkgsrc/math/py-z3solver/PLIST       Fri Sep 18 05:00:48 2020
@@ -1,17 +1,35 @@
-@comment $NetBSD: PLIST,v 1.1 2018/03/20 15:47:36 khorben Exp $
+@comment $NetBSD: PLIST,v 1.2 2020/09/18 05:00:48 khorben Exp $
 bin/z3
 ${PYSITELIB}/z3/__init__.py
 ${PYSITELIB}/z3/__init__.pyc
 ${PYSITELIB}/z3/__init__.pyo
-${PYSITELIB}/z3/include/c++/z3++.h
+${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_log_macros.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_interp.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/z3.py

Index: pkgsrc/math/py-z3solver/distinfo
diff -u pkgsrc/math/py-z3solver/distinfo:1.2 pkgsrc/math/py-z3solver/distinfo:1.3
--- pkgsrc/math/py-z3solver/distinfo:1.2        Wed Mar 18 17:57:02 2020
+++ pkgsrc/math/py-z3solver/distinfo    Fri Sep 18 05:00:48 2020
@@ -1,9 +1,6 @@
-$NetBSD: distinfo,v 1.2 2020/03/18 17:57:02 joerg Exp $
+$NetBSD: distinfo,v 1.3 2020/09/18 05:00:48 khorben Exp $
 
-SHA1 (z3-solver-4.5.1.0.post2.tar.gz) = 6cc67617079010179308cf8ffe5b0098d4152fdd
-RMD160 (z3-solver-4.5.1.0.post2.tar.gz) = 97055f883f7567a53517cceda915a4e34d058452
-SHA512 (z3-solver-4.5.1.0.post2.tar.gz) = babbca25de59638c52b91953030cd7af20d1e795af7da760f71bb43940116a4415fdf7208b967bf5eb54435780d21cdc7740faac9cf81cee59005f16f4af09a0
-Size (z3-solver-4.5.1.0.post2.tar.gz) = 3891600 bytes
-SHA1 (patch-core_scripts_mk__util.py) = 45d2cd60977cfa6b89d9033586b8467af0a79cfd
-SHA1 (patch-core_src_util_lp_permutation__matrix.h) = 2ceb66d811664f5b1396137f3f40579b9c474496
-SHA1 (patch-core_src_util_stopwatch.h) = 3163302c46a6315530f9bfb25be93a1efed814a7
+SHA1 (z3-solver-4.8.9.0.tar.gz) = ac47b179505c2529bb42b03faf6d5b1174a4f321
+RMD160 (z3-solver-4.8.9.0.tar.gz) = 3427e05e0d0f4aec20cdd5d01d34d0a9b1676e5b
+SHA512 (z3-solver-4.8.9.0.tar.gz) = bc137b505cc24e54e50b1aa3d7ee4161593de17f14198f926beaaf285f210742635f4be22d61456d19688a73f422ca60a24c84eeecf5e783d1dcf26f65a1b8ab
+Size (z3-solver-4.8.9.0.tar.gz) = 4503933 bytes

Prev by Date: Re: CVS commit: pkgsrc/parallel/threadingbuildingblocks
Next by Date: CVS commit: pkgsrc/doc
Previous by Thread: CVS commit: pkgsrc/doc
Next by Thread: CVS commit: pkgsrc/doc
Indexes:

Home | Main Index | Thread Index | Old Index