Skip to content

Releases: Z3Prover/z3

z3-4.8.8

08 May 22:02
@NikolajBjorner NikolajBjorner
z3-4.8.8
ad55a1f
Compare
Choose a tag to compare
z3-4.8.8

4.8.8 release

Changes:

See More
Read more
Loading

z3-4.8.7

19 Nov 21:48
@NikolajBjorner NikolajBjorner
z3-4.8.7
30e7c22
Compare
Choose a tag to compare
z3-4.8.7

4.8.7 release

Changes:

See More
Read more
Loading

Nightly

13 May 04:21
@jfleisher jfleisher
Nightly
09523a4
Compare
Choose a tag to compare
Nightly Pre-release
Pre-release

nightly build

Changes:

  • 6b32aae remove slack heuristic
  • a5e5d4d testing
  • bbaec0b trying randomly shuffle the indices in the slack utilization
  • 52241b6 some refactoring of lar_solver.h
  • fef954c shring lar_solver.h
  • 4abd984 fix the build
  • e3f5e8c restore lar_solver::add_named_var
  • b375faa continue PIMPL refactor in lar_solver
  • b7ffcb7 implement imp of lar_solver as lar_solver::imp
  • 39955f1 remove a function from lar_solver
See More
  • 4e56834 test
  • a527667 shuffle more functionality from lar_solver.h to lar_solver::imp
  • c81eb74 apply the slack idea in a loop
  • e041fe9 slack
  • 7ca94e8 add E-matching to EUF completion

This list of changes was auto generated.

Loading

z3-4.8.6

20 Sep 00:58
@NikolajBjorner NikolajBjorner
z3-4.8.6
78ed71b
Compare
Choose a tag to compare
z3-4.8.6

4.8.6 release

Changes:

See More
Read more
Loading

Z3-4.8.5

03 Jun 01:50
@NikolajBjorner NikolajBjorner
Z3-4.8.5
e79542c
Compare
Choose a tag to compare
Z3-4.8.5

The release contains cumulative updates to the previous release

Loading

Z3-4.8.4

20 Dec 20:27
@NikolajBjorner NikolajBjorner
z3-4.8.4
d6df519
Compare
Choose a tag to compare
Z3-4.8.4 
z3-4.8.4

new tag
Loading

z3-4.8.3

19 Nov 23:05
@NikolajBjorner NikolajBjorner
z3-4.8.3
7f5d66c
Compare
Choose a tag to compare
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
Loading

z3-4.8.1

15 Oct 22:44
@NikolajBjorner NikolajBjorner
z3-4.8.1
b301a59
This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
GPG key ID: 4AEE18F83AFDEB23
Expired
Verified
Learn about vigilant mode.
Compare
Choose a tag to compare
z3-4.8.1

new in 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
Loading

Z3 4.7.1

22 May 23:58
@NikolajBjorner NikolajBjorner
z3-4.7.1
3b1b82b
Compare
Choose a tag to compare
Z3 4.7.1

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
Loading

Z3 4.6.0

18 Dec 18:41
@wintersteiger wintersteiger
z3-4.6.0
b0aaa4c
Compare
Choose a tag to compare
Z3 4.6.0

Official release Z3 4.6.0.

Loading