Skip to content

z3-4.13.4

Latest
Compare
Choose a tag to compare
@jfleisher jfleisher released this 17 Dec 04:32

4.13.4 release

Changes:

  • 6f24123 reduce hash table lookups in expr_abstract in half
  • a6e59ea fix build flags for release.yaml
  • a97ad76 publish pypi
  • 200ef23 Update RELEASE_NOTES.md
  • e40972b Update release.yml
  • b529a58 add unit test for incremental equation edit distance with repair
  • 31ee56c wip - incremental edit distance algorithm
  • 538f74d extract stats with finalize for parallel mode
  • b429562 Add enter and exit methods on Optimize class (#7477)
  • 1e5c59a add repair step for str.replace
See More
  • e8c2360 fix #7461
  • 8f5658b add another baseline heuristic for string equalities, add cases for array axioms.
  • e5f8327 Update emscripten (#7473)
  • 4fbf54a fixes to regex membership and edit updates
  • 1ab0962 partial fix to make computed term integer well-formed for solve_for functionality
  • bcb61ee v0 of edit distance repair
  • 4be4067 Typescript high-level api for Sets (#7471)
  • a17d4e6 bugfix to elim_uncnstr to ensure nodes are created. Prepare smt_internalizer to replay unit literals
  • 6ea4110 Bump docker/build-push-action from 6.9.0 to 6.10.0 (#7469)
  • aec8675 updates to equality solving search
  • e6feb84 sls: fix bug where unsat remains empty after a literal is flipped. The new satisfiable subset should be checked
  • 24c3cd3 add v0 of equality solver
  • 05e0532 add facility to solve for a linear term over API
  • d241156 add projection with witnesses
  • b7b611d inherit from std::exception
  • ab1be5c internalize the reduce_args_tactic to reduce the number of heap allocations
  • 1ccfba6 remove unreachble code
  • 1e62029 use ztring
  • fce377e add basic regex functions
  • b143a95 add notes and additional functions to sls-seq
  • aed3279 add missing new_value_eh when repaired up
  • 1e839e5 add missing new_value_eh when repaired up
  • 7ed185a add comments
  • 4559b23 add local search functionality to sls_seq_plugin
  • b4e768c adding plugin for local search strings
  • 3672575 fix typos POLING -> POLLING in setup.py and remove unused CFLAGS
  • 71bad71 #7418 - circumvent use of timer threads to make WASM integration of z3 easier
  • 94f0aff remove the use-pthread
  • 76795a4 remove -pthread from options
  • 8965123 fix type in setup.py
  • 10d9c81 adapt for pyodide built
  • 012fc1b more detailed tracing of where unmaterialized exceptions happen
  • 7de0c29 Update pyodide.yml
  • e855a50 add exception handling to easier diagnose #7418
  • 5168a13 track exceptions in reason-unknown
  • a8a5069 Update README.md
  • 15f954e add picture of z3guide
  • 24dfc17 Update README.md
  • 4b72e51 SLS: log clause , allow more frequent export of SLS state to SMT
  • 84447b7 remove incremental mode from EUF, include statistics about restart vs propagation calls to sls
  • c7ea496 bug fixes to sls
  • e380903 Update README.md
  • 2310514 fix #7454
  • 5fd1231 incorporate ls during propagation
  • 836802e Update pyodide.yml
  • cdc4833 Update pyodide.yml
  • 00c5600 Update pyodide.yml
  • 750dd68 enable par_then and par_or even if single threaded - fall back to sequential mode
  • f64d077 fix re-entrancy bug during flip in arith_base
  • e4e5735 update to set single threaded
  • b929996 update to set single threaded
  • f39198d move build-env setting to correct place
  • 197951c fixes to sls
  • 7c5ff7c moving compile time flags to setup for pyodide
  • 8bfe403 Update pyodide.yml
  • 60b14f3 Update pyodide.yml
  • e7d0833 Update pyodide.yml
  • bd5f8b1 Update pyodide.yml
  • 751d666 Update pyodide.yml
  • 24f9a86 Update pyodide.yml
  • dba1674 Update pyodide.yml
  • 704278c Update pyodide.yml
  • 231248d Update pyodide.yml
  • 329e1dd Update pyodide.yml
  • aab6c1e Update pyodide.yml
  • ccbe6c3 fixes
  • 8804890 Update pyodide.yml
  • ea590de remove breaking experiment
  • 1d8a904 build fixes
  • 77eacef build fixes
  • 3f40798 build fixes
  • ca6ec0d fixes to pyodide action
  • 8e3b9f6 add sequential option for SLS, fixes to import/export methods SLS<->SMT
  • 6a9d591 add method for resetting limit
  • 6eae3f0 add cases for unconstrained sequences and strings
  • 62db764 refine rewriting depth for lt constraints
  • 3fed840 update pyodide.yml
  • eab49da Update pyodide.yml
  • 75d0dd8 Update pyodide.yml
  • e53ea00 Update pyodide.yml
  • 4cdc3d6 Update pyodide.yml
  • 4d0394e Update pyodide.yml
  • 0dc4c5e Create pyodide.yml
  • d3009da Proposed fix for #7451 (#7452)
  • c0e748a fix #7446, by adding rewrite simplification
  • 1cc808c fix #7446, by adding rewrite simplification
  • 30ad22a fix #7449
  • 879bb4b avoid circular dependencies in justifications that get updated. fixes #7443
  • 1856ab7 fix #7448
  • 4f060dd fix #7445
  • abd1674 inherit more exceptions from std::exception
  • a38bf3e port to inherit from std::exception
  • 407bad3 add noexcept
  • 42894f7 add noexcept for signature compatibility
  • 75e4677 Make build process work with pyodide (#7442)
  • 9206546 use std::exception as base class to z3_exception
  • 1957b4d fix reporting on cancelation when based on cancel flag
  • 604714b js: Add pseudo-boolean high-level functions (#7426)
  • 91dc02d Sls (#7439) [ #7265, #7269, #7271, #7270, #7268, #7232, #7288, #7280 ]
  • ecdfab8 fix #7434
  • b0fef64 Add assert_and_track support to Optimize class in .NET binding (#7437) [ #7436 ]
  • 8b657f2 add shortcut to retrieve kind of application
  • 78d1139 add shortcut to retrieve kind of application
  • 0ebea1c remove debug out
  • 253f7d7 fix non-termination bug in elim-unconstrained, add parameter validation to fix #7432
  • d18831c Update sat_ddfw.cpp
  • 45ef6d0 js: Adding manual release methods (#7428)
  • 5cee19f It uses C++20 BTW (#7429)
  • a23a8cd add variables from definitions
  • 92376e6 better model replay for loose entries
  • 5a5e39a fix incrementality bug for pre-processing: replay has to be invoked on every push regardless.
  • 8ff4036 update unit_lim to the correct value (#7423)
  • 3896e18 fix the code to cube at the correct frequency (#7422)
  • 5993735 simplify string patterns into prefix/suffix constraints
  • 62478db Update docker-image.yml
  • 56b706a fixes for #7420 #7405
  • 3a8195b #7419
  • 7a0b58b increment minor version number
  • efde656 fix recursive self call for slice_solver check-sat-cc method

This list of changes was auto generated.