z3-4.8.6

4.8.6 release

Changes:

• 78ed71b update to pypirc
• bd26301 update to pypirc
• f8df777 na
• a1d3aca add release notes preparing for release
• 4b96238 use testpypi
• df2f041 undo atomic
• c68cfe8 #2565 use atomic
• 04ae000 fix #2567
• 9c74c05 address min-int overflow reported in #2565
• 77ef40a na

See More

• 4b51fe4 fix #2562
• 69abe16 backjump to level of clause to ensure that new atoms created by projection are assigned as assumptions fix #2557
• 0f20175 fix #2556, sign of of inequality is not restricted to -1, 0, 1, but can be -2, -3 etc
• 0c972b8 tidy
• da805f6 address perf bottleneck exposed by #2552
• fffc539 fix #2549
• 098725a fix #2553
• 67c4777 fix #2548 fix #2530
• 5d9ed5b Allow for __truediv__ and __rtruediv__ even when not using Python3
• 1b83c67 spacer: fixes lim_num_generalizer
• 6384080 fix #2546, retrieve model in optsmt lex before iterating
• 0481adb fix #2547
• 0d3fed9 spacer: lemma generalizer for small numbers
• 78a1f53 fix #2544
• b1cdb3e add mbqi to smtfd. For Nuno, of course
• c22a17f smtfd
• d3da161 smtfd
• 5ba4d8d na
• d44081d fix clang compilation errors
• 3b1a73b add smt to project.py dependencies
• 85fb6f5 disable ackermannize on goal
• ff3cff0 deal with ite
• c476c4a smtfd solver that uses lazy iteration around fd to produce theory lemmas
• e881c4a Support repr_html for jupyter
• 228d68f enhance ackermannize for constant arguments
• 18ba14c Z3str3: fix empty-string contradictions (#2538)
• bc723fb fix #2539
• 8ec6219 na
• a92c82d na
• f645f8d fix #2537
• 29f0897 tweaking nlqsat
• 5fbfc0f minor code simplification
• 8f4e7f4 fix #2533
• 9fce5e1 fix build
• 87a96d7 fix mutexes hanging due to access to free'd memory
• cb75326 minor code simplification
• 68e4ed3 fix #2531
• 000e485 add array selects to basic ackerman reduction improves performance significantly for #2525 as it now uses the SAT solver core instead of SMT core
• 7823117 Restore expected behavior to stopwatch
• e816d16 fix #2527
• 4c0db00 fix push/pop bug for ite-elimination, thanks to Nao Hirokawa for reporting it
• de43e05 fix overflow bug exposed by #2476
• a8bfab3 add model.inline_def option to make #2517 happy
• 35fa24a initialize best model
• 20dc59e fix #2523
• 2e6908b fix #2509, fix issue with model inheritance exposed by #2483
• 271cd2a disable expensive model validation
• f048cb2 revert the revert
• 75a40d8 reorder fields, rename overload name clash
• 64f4c97 fix regressions during string fixes
• 0d9cd7b addressing misc. string bugs
• a337a51 fixes for #2513
• de69b01 Lev's fixes
• f90db2b add back compression to ensure local functions are inlined #2517
• c15764e remove verbose=0 instances #2507
• ffc696e exclude built-in functions from model
• eea0413 fix #2502
• e08abb3 fix #2504
• 2f60bcb Clean up NaN return values in Z3_get_numeral_double
• 423fb73 Fix for fp.rem. Pertains to #2381.
• f22d6e3 Fix floats in Z3_get_numeral_*string.
• 79cd1f0 Fixed Z3_get_numeral_double. Fixes #2501.
• 258b798 test-z3: Improve help output. Provide help when no args.
• f02170f Clean up whitespace.
• fcc7bd3 fix #2489
• 3074e2b fix #2487
• d64dc93 Add note about minimized unsat cores to C API docs.
• 9949f16 Fix release note typos.
• e2122c0 Fix whitespace issues in *.pyg.
• 0734c5f fix is-array-sort test again
• 892aa12 Fix for fp.rem. Fixes #2381.
• 0edd587 Fix typos in examples.
• ec5b148 Add python packaging build and deployment with Azure
• eec550e fix python build break
• 2b2f016 python for accessing lambda, switch to theory branching for QF_LRA
• 520ea65 move towards theory phase selection, implement getitem on lambda
• 0eafeb9 Fix confusing tabs mixed in with spaces in C examples.
• 0093157 Handle dynamic sort of Nth()'s return value in the Python API
• e89bb37 More see also content in C API docs.
• 375c0ff Implement get_proof() in bmc and spacer engines
• 876cfb4 optimization of phase
• 7596217 fix #2481
• 9fa9aa0 fix #2468, adding assignment phase heuristic
• 42e2145 fix #2479
• ce84e0f remove strategic solver header file
• fc41a61 expose strategic solver factory prototype at level of solver module
• 1ae0a98 fix #2466
• 52acbf1 bug in qe_lite
• e2d91ce distribute concat over bvxor and bvor, #2470
• 8579a00 distribute concat over bvxor and bvor, #2470
• e950453 force propagation for smt cubing
• bbfac99 fix #2469
• 0af249d 'na
• f90439f docs: Fix a number of identifier formatting issues.
• 077f518 Fix -Wreorder warning.
• ce7f9c3 Remove unused variable.
• d977c15 Merge pull request #2462 from waywardmonkeys/fix-typo
• 6be36f1 Fix typo.
• bc3b0f6 introduce fresh term when none is available in context or model to fix #2456
• 01920ab introduce fresh term when none is available in context or model to fix #2456
• 59f69bb introduce fresh term when none is available in context or model to fix #2456
• c7dc420 let me guess, ASAN doesn't like 0-byte memcpy
• 90415a1 fix build of test
• d7ac8db fix #2458
• 3147d23 fix #2460
• 4431a53 fix #2450 - track assumptions across lazy explanations and variable equalities
• db5af30 logging for #2450
• 1d488d0 nlsat
• 2d5714a fixing #2443 #2445 #2447 #2448
• 584eee2 fixing #2448 and #2445 and #2443
• c448033 fixing #2448 and #2445 and #2443
• 3d1c40c fixing #2448
• 95eb0a0 remove an unnecessary call m_mpq_lar_core_solver.m_r_solver.track_column_feasibility(j)
• 294dcf7 Merge pull request #2455 from levnach/fix
• e9e9500 fix the build
• db5ac5a fix a bug in lar_solver in queryaing if a column is int
• 9d6728a fix unsound rewrite
• 0a29002 return unknown if m_array_weak was used and result is satisfiable
• 3f032e8 remove include of thread
• b...

Z3-4.8.5

The release contains cumulative updates to the previous release

Z3-4.8.4

z3-4.8.4

new tag

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

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

Z3 4.6.0

Official release Z3 4.6.0.

Z3 4.5.0

Official release Z3 4.5.0.

Z3 4.4.1

Official release Z3 4.4.1.

Z3 4.4.0

Official release Z3 4.4.0.