kpriv/pkgsrc
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity
pkgsrc/math/py-z3solver/distinfo

6 lines
345 B
Text
Raw Normal View History

math: Remove SHA1 hashes for distfiles
2021-10-07 16:27:43 +02:00
$NetBSD: distinfo,v 1.4 2021/10/07 14:28:28 nia Exp $
Import math/py-z3solver version 4.5.0.1 Z3 is a theorem prover from Microsoft Research with support for bitvectors, booleans, arrays, floating point numbers, strings, and other data types. This is a fork of the original Z3. Unfortunately it conflicts with the math/z3 package as a result.
2018-03-20 16:47:36 +01:00
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
2020-09-18 07:00:48 +02:00
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
Reference in a new issue Copy permalink