Releases: Z3Prover/z3
Releases · Z3Prover/z3
z3-4.15.0
4.15.0 release
Changes:
- 9232ef5 remove copy of LICENSE.txt - pypi doesn't take it
- 49dffae enable pypi
- b54ed38 enable pypi
- 59a7e00 disable pypi
- d4b622e update version number
- a51239c update namespace, hoist exported functions outside of embedded namespace
- 6441186 list euf dependency in api cmakefile
- eca5cd1 mark virtual methods as override
- 9a299eb move mam to euf
- 0e4c033 fix #7639
See More
- 4bedb5f fix #7638
- dd211ba filter out terms that are not solved
- f89e133 revert the behavior of add_zero_assumption (#7631)
- 6af61fa remove experiment
- b502126 fix #7634
- 24090fc move flush smc to first use
- a626cd0 flush smc before use in model construction
- 71b5e44 #7596 - flush smc before copy
- 7a30223 fix #7630
- d581dc1 #7630 propagate parameters on lazy tactics
- 322e444 Fix conversion of signed 1-bit BV to FP
- 792ffee fix latent sign bug
- fe1fff3 add scaffolding for experiments with slack
- 12ccf59 rename fields to compile on c++ platforms
- e41acd7 convert m_r_upper and m_r_lower bounds to plain vectors
- fae6094 consolidate some bounds references
- f6fbeda fix #7629
- 7641393 use inlined functions
- 5cc57b8 coalesce updates to bounds
- 579ba8b add power axioms to arith_solver
- d73d104 remove overwriting x,y,rval
- ff920ba handle root expressions, and checking exponentiation with nlsat
- 2fe2735 Replace
_DEBUGwithZ3DEBUG(#7628) - a1673f2 fallback to Gomory cuts and gcd conflicts if dio fails
- cc1bb0a remove superfluous makefile
- 17cac7d provide shortcut to command-line version to retrieve parameters
- 6e88d91 add badge for ocaml cmake
- 3761dd8 address build warning with overloaded virtual operators
- f7aec02 WIP: Migrating OCaml binding to CMake (#7254)
- ab9f330 change the default of running dio to true, and running gcd to false, remove branching in dio
- dbde713 remove testing code in is_big_term_on_no_term
- 1131d52 fix a bug in tracking the changes in dio
- d289495 allow gcd when dio ignores some terms
- 17af18f make gcd call in dio optional
- 436eefb always remove the tightened term
- dc7185d change the name of m_changed_columns to m_changed_f_columns
- 32e77d8 typo
- cb1818f reject more terms with big numbers
- 1cde40b dio_calls_period=4
- 87e2ce8 Update lp_settings.h - m_dio_calls_period = 4
- 59edb81 Update lp_settings.cpp
- 8db9f52 add parameter m_dio_calls_period
- ae97ee0 throttle dio
- 972f801 throttle dio for big numbers
- 3e49d9f reuse dio branch
- e31e981 Add an option "ctrl_c" that can be used to disable Ctrl-C signal handling (#7619)
- ed5dd26 remove non-working ts mcp server, settle with python variant
- 741cb5c minimal z3 MCP server
- f63c9e3 disable assignment for param_descrs
- 3f73c8b stab at SMTLIB REL mcp server
- 755f579 fix #7622
- 81f1091 remove unused bdd based variable elimination
- e41090d fix #7602
- 8035edb remove lp_assert
- 1510b31 fix build warnings
- 5ad79f2 Add Iterators as acceptable arguments to functions (#7620)
- 6ecc7a2 Fix a race condition in scoped_timer::finalize (#7618)
- a83efa6 spacing
- 8138829 fix #7616
- d792840 Add Z3_is_recursive_datatype_sort to the API (#7615)
- 14e2aad include LICENSE.txt in wheels (#7614) [ #7604 ]
- 0b7a81b list[ExprRef] doesn't build for python
- 2b60550 update agentz3 sample based on hugging face training/test data
- e7ff600 #7605
- a39efbb fix #7607
- 9d8291a remove type annotation Context | None to ensure Centos ARM Build pass
- f607331 type annotations across Python versions
- bd2c7aa remove downlevel version incompatible elements of typing
- 305f1e8 remove references to TypeGuard
- a5048e4 add initial sample agent use case
- 0a37194 fix #7609
- 5e10fd3 add selected type annotations to python API
- 26ab0de rename function
- eb4e28d [z3.py] Fix incorrect call to _get_ctx in SeqMapI (#7610)
- 8d81a2d Note that Z3_get_numeral_small is essentially redundant (#7599)
- 63ad283 Add Z3_get_array_arity (#7598)
- 934455a Remove vestiges of old ml api (#7597)
- e4897ff replace Exists by ForAll in the mathematica lemmas
- 39df899 enable shorterter mathematica printouts in nlsat
- e86a918 turn on ite simplification by default
- 8368094 fix indentation
- 4fd6ba4 replace costly ite reduction by disjointnes check
- 392bc16 optimize bool rewriter
- 2971250 add option to rewrite ite value trees
- e92ccdd change line breaks
- 17bd02d change a comment
- 8bbe752 remove dead code
- 7e4a1f2 fix crash in elim_constr2
- 93cf989 household chores - move to iterators
- dee3cf8 remove an unused field
- 9302a02 reintroduce m_var_register, and avoid modulo gcd in normalize conflicts
- 9a62ed5 added some comments
- c634701 formatting
- f073da9 cleaning up the inner tightening code
- 8c96178 avoid the variable mapping to m_ematrix and suppressing redundand constraints
- 29c5c20 use more descriptive functions than casting comparisons
- 7fb40e8 tidy
- a41bd38 use pattern of matching with undef instead of matching with conflict to reduce assumptions on procedure contracts
- 676a536 fix a print out
- d507d0f attempt to use the gcd of fixed vars
- f181e3a add comment on derivation of bound
- dd19b38 detect more m_terms_to_tighten
- 307af0f remove an unused field
- fc1c8c4 add public access to bijection key_val iterator
- 8b5510b nit
- 7577f6f neatify loops
- f091b6f remove 'unsat' move, we already have 'conflict'. Add display for cancelled
- 1af2474 code review updates, tidy pretty printer for column info
- 3202808 fix bug introduced while absstracting m_conflict_index
- f3b34fd isolate m_conflict_index functionality
- ff5ae4d add systematic way to combine lia_move results
- 00277ba nits
- 488c74d print also column values
- 22cfab3 remove term sorting by the span
- 12203fc sort terms by weight for tightening
- 0a3c118...
z3-4.14.1
4.14.1 release
Changes:
- 3c0d786 install setup tools for python packaging
- e05f75d switch to ubuntu 24 for python packaging
- 07fa36e fix #7466
- ab0323c update release notes
- ea1360e fix #7578
- c002c77 fix #7569
- 54c6b11 Update README.md
- 80f00f1 fix #7572 and fix #7574
- 8df45b4 try ubuntu 24
- b47ec20 try version 75
See More
- 3e7f483 68
- dedfe90 remove downlevel setup in nightly.yaml
- f698dea downlevel setup
- e6855bb disable setup tool install
- d714f1b update path
- 7eb401b extract paths within zip file
- 476c5ee improve diagnostics
- f74d846 use single thread for win-dist
- 14390ee fix typo
- 62616cf fixup nuget task
- d24c488 fix error in mk_nuget_task.py
- a97e5fc fix error in mk_nuget_task.py
- cd95c7e add diagnostics to extraction of Microsoft.pdb/xml/dll
- ec93972 fixup unit tests
- b784b74 fix #7550
- 83ee21c streamline tracing
- db997cd fix regression, missing idx increment in iterator loop #7566
- a731046 throttle down cuts from proofs
- be8febe add throttle, fixup bp.init() for proper initialization
- c79967b using iterators
- 17f239c base line specbot
- 589fb1b base line specbot
- 67d77e2 remove a parameter when calling bound_analyzer_on_row
- b985838 do not pass row index to bound_analyzer_on_row
- 10c2af8 try for mixed-mode
- ead8478 fix build per new API for analyze_row
- 1a3d1ad add base line bounds tightening utility
- 7044bb8 remove an unused parameter in bound_analyzer_on_row
- fbfbfa5 print column value
- f50f211 Fix #7505 (#7565)
- bd3d288 tighten only core constrants
- 45ad614 added logging
- 1fec0fa remove verbose output
- 01fbc0e fix #7563
- 712231d fix #7560
- 075773e remove proviso for single index arrays
- 3e5abef fix #7549
- e0945f5 fix #7554
- 28f3f80 #7559
- 1106648 #7559
- 991cffb handle multi-arity arrays
- 674e1b8 remove equality check on container
- ce69b54 adjust select/store rule for n-ary arrays
- 42f6e13 more review of mbp_arrays
- a4a84ed arrays are not necessarily unary
- a5e5a35 code simplification
- a143ed3 taking a look at mbp_qel for arrays
- dda6073 updated release notes
- fb6ec7d increase version number
- 30dba9b use down-level setup tools on hosted machines to avoid https://stackoverflow.com/questions/79252233/canonicalize-versionversion-strip-trailing-zero-false-while-doing-colcon-buil
This list of changes was auto generated.
z3-4.14.0
4.14.0 release
Changes:
- 3c47fd9 bump timeout for jobs
- 2e008a9 Update release.yml for Azure Pipelines
- d1575af Update nightly.yaml for Azure Pipelines
- 96e3233 Update azure-pipelines.yml for Azure Pipelines
- 813da35 fix unit test
- f8f2678 convert def into expression tree
- f977b48 adjust solve_for to handle rationals
- 528efbb fixes to failure conditions for unification
- fe27ca1 remove verbose output
- 50f9fdd Add unification based projection function
See More
- b27a2aa remove calls to removed def constructor
- a703cf8 replace model_ref by model* in tg_project,
- eee96ec bug fixes and cleanup in projection functions
- 0cf2b5f add retry, rename to optibot
- 6b9ce86 fixes to opt-tool
- 719ea6a added ai scripts
- 9fad15e adding mergeopt
- 01ba749 focused query to optimize
- a003139 update description
- 45f3ea3 add treesitter functionality
- bedc95c use static_cast to avoid the warnings
- e6a089e Fix build when Z3_API macro is non-empty (#7553)
- d10efa6 stub for treesitter
- 5c18ce8 genai testing
- 4e51af1 update instructions
- 94d3c59 make sure ackermann works with arrays that have more than one argument
- a3739aa add mycop in addition to code complete
- 9ea921b update spacer projection for arrays to allow ackerman reduction for non-integer arrays
- e920291 fixing the default parameters of dio and rename m_gomory_cuts to m_cuts
- 957b177 set arith.lp.dio_cuts_enable_gomory to False by default
- 5ec10e0 address the review
- 8a9edd1 fix the test build
- 79e3f8a disabling dio handler by default, and fix a print out
- 2131e9b more accurate work with Markovich number
- bdb8f54 Revert "revert the term sorting"
- 5ebee24 revert the term sorting
- f2c1fd4 try markovich number
- cec8dc2 try markovich number
- 3f2d2e8 test
- b6701d5 try another sort in tightening
- 5b0b224 try sorting terms before tightening
- dcd5783 remove the fresh definition when removing its column
- 17d68c1 comment change
- d90b94d stricter is_in_sync paying attenion to m_row2fresh_defs
- 134bed8 throttle the branching in dio
- bd8cf29 ignore large changed_columns
- 3ac11cd fix assert
- cf4e402 avoid usisg indexed_vector for term operations
- 440d78f disallow duplicates in a queue
- 7e02dfe add stats on m_dio_branching_conflicts
- 0bf3ca8 call normalize_e_by_gcd() only when moving an entry from F to S
- 9953856 rebase with master
- a19e109 make dio less aggressive, allow other cuts
- fee7078 register m_added_terms in m_changed_terms
- 21f67ef out of bounds fixes
- 3b3d8ce use m_chandedNterms to tighten terms
- 65bdd58 remove struct entry
- a9098a5 optimise l terms addition
- 3e7e903 use the trail to undo add_term
- 9c51001 fix the debug build
- 058b9e4 optimise rewrite_eqs to avoid fresh variables
- ed3df33 make rewrite_eq boolean, and relax an ASSERT
- ca7c128 clean up fresh definitions on a pop
- b027761 debug dio
- bb869fd don't store fresh definitions in m_e_matrix
- e5ffc3c cleanup
- d7de7eb remove recalculated entries from S
- ef55de1 fix out of bounds bug
- 3990df6 substitute variables with a queue on the recalculated entries
- 78d91f3 simplify dio handler by using bijection m_k2s
- 33f5e30 use entry_status for FRESH entries
- 0e71adf fix some warnings
- 7bba8bc fix some warnings
- abac52e remove var_register_dio.h
- 89eec4c test dio
- 5a72117 debug dio
- 0027ae2 bug fixes
- 5158797 refine trail iterations with lar.m_terms
- 9a9ccf1 introdure lar_term.ext_coeffs(), dio passes some tests
- 083926c debug dio
- a0ece6d cleanup
- ceeece6 debug dio
- ac5c50f fix ubuntu build in dio
- c1ece49 track changed columns in dio\
- 008e922 use std_vector more and getting NOT_IMPLEMENTING in C:\dev\z3\src\math\lp\dioph_eq.cpp
- 57b665d work on incremental dio
- 28556ce cleanup
- 862dc91 work on incremental dio
- fd3bd08 remove some warnings
- 9a96aa9 test
- bef313f test
- 7ecac27 fix a bug in dio
- b0383da fix a bug in dio
- 7fe703e simplify column
- 8d74786 cosmetics
- deac00a persist dio handler
- 2c8a6f8 change int_solver to call find_cube and hnf_cut, conditionally
- 39da4f6 remove an assert
- 28d4178 fix the build
- 397fdf6 fix the build
- 63980f3 fixes in dio branching
- 6bc7662 passes z3test
- 1741855 collect the explanation correctly
- bc0fdfe remove dead code
- c300843 cancel bugs fixes
- e4f3b57 solving regressions/smt2/b1.smt2
- 71c4339 work on incremental version
- d68ebee use var_register in dioph_eq
- 480c48f document dioph_eq
- 02a509b remove a global debug variable
- acc2149 remove redundant m_row_index from entry
- d439073 take dependencies from open_ml
- 3fcc5a2 fixes in tigthening
- 9164672 check feasibility immediately after tightening a bound
- 58e5735 implement explain()
- b30272f add missing explanations
- e0a08f1 fix the build
- 30f5599 use fixed vars to explain tightening
- 36293ac test that pivoting is correct in dioph_eq.cpp
- 0db0efc print output file name
- 8904a50 fix the build
- 5f5f1d4 init m_e_matrix on terms instead of the tableau
- 392c24a throttle dioph equalities
- 128d5b4 change type of m_e_matrix
- a63e0d8 add a template instantiotion
- 0f03e75 handle empty rows in m_e_matrix
- ba7268c vector access bugs
- 66f8820 bug fixes with tableau
- 62ea6fb bug fixes
- ac49198 bug fixes
- 536c51f debug dio with static matrix
- 28fbc81 unifying vectors into eprime_entry
- 42bdc89 dio with static_matrix initial setup
- 9e8b17b do not use conf 8000 licts with fresh vars to create branches
- eaf2f7f...
z3-4.13.4
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
- 750 10000 dd68 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...
z3-4.13.3
4.13.3 release
Changes:
- 54d30f2 add _0 to platform tag for pypi
- 6e3b99f downgrade to macos13 in builds until fully supported by pypi
- b268b56 update release notes
- 00f1f1b fix typo in setup.py
- fe71b75 remove : from setup.py
- 5dc1b1a remove hard-wired osx=11.0
- 48aa2f6 setup python dist to remove internal build suffix for macos
- da614c6 remove m_level attribute, use s->get_scope_level directly
- 6bd46b0 fix #7363. Replay relevancy on unit literals that are re-asserted during backtracking.
- cfd00ad add slice solver option to command context
See More
- 8a95dd4 A slice solver option for interactive use case
- 0fec7ef micro-tuning
- c6cd25c mico-tuning
- 24d7b05 refactor and optimize git operations for commit messages and failure analysis (#7412)
- 2ae4ac8 fix build
- b60e1a2 fixup variables
- 969511a fixup std-order / inv-order
- 66bb310 reset before manager is deallocated
- a98c925 optimize var_subst
- f5db6bf install Julia for macos build
- e58eb9f fix indentation for mbp
- 3586b61 remove default destructors
- b170f10 reorder template definition
- 6dec943 Bump docker/build-push-action from 6.7.0 to 6.9.0 (#7408)
- d686e92 disambiguate
- 93ff89b add == for const_ref and ref to disambiguate equality.
- c7af973 fixes for #7402
- 328616b fix build warnings
- 8c39863 fix typo in arch for setup.py
- 4cefc51 add sequoia to os versions #7407
- 19f63cd add sequoia to os versions #7407
- 86b9718 fix build warnings
- 551cc53 fix un-intialized variable warnings
- 2c94a3a fix build warnings
- 7da58b9 fix build warnings
- 30b4fe6 2nd attempt to use uniform java library location under bin #7406
- b65afd4 attempt to use uniform java library location under bin #7406
- 5413018 Update euf_ac_plugin.cpp
- 826835f fixes to build warnings
- 2ac6f8b increment minor revision number
- c2b2626 remove --java option
- 2123d38 Update nightly.yaml for Azure Pipelines
- fc1c6b4 try to build java on linux/arm nightly
This list of changes was auto generated.
z3-4.13.2
4.13.2 release
Changes:
- 9a8ff74 update version number and release notes
- 11bb19d make default tactic cases lazy
- 40b0210 fixes to lazy tactic uses
- 01cf042 fix #7404, relates to #7400.
- d047b86 pypi publish
- f4452a0 pypi publish
- 3df7299 update signature of operator==
- 649c36a align nightly and release yamls
- 8d831a1 set to macos latest
- b39bcd6 remove ubuntu20
See More
- ebdb037 fix indent
- c690279 skip pypi publish during dry run
- 77aa528 wasm: increase timeout in tests (#7401)
- 103c5ad wasm: attempt to GC in tests (#7400)
- 82eb186 remove ubuntu build 20 from nightly
- eb5d036 fix #7392
- 2655301 comment out simple proofs unit test
- 8b81bda Julia now used the C API. (#7388)
- 994056f C API now used by Julia. (#7387)
- 716a815 update lock file
- a831fe9 fix some build warnings
- afaa48d sample fix script
- fa1a2cd disable simple check in nlsat
- c34c847 Add .gitattributes for genaiscript and update git commit flow script. (#7396)
- ec14ef7 Update Ubuntu job name in Azure pipeline and add string variable creation in C API example
- 95d2e00 Update OCaml jobs to use Ubuntu-latest in Azure Pipelines configuration
- 0604d23 Check if model_converter is non-null before initializing values in sat_tactic
- 5a6dc18 Override convert_initialize_value method in bit_blaster_model_converter.cpp
- 5c58329 Remove unnecessary const qualifiers from comparison operator overloads in z3++.h
- ee34773 remove junk
- eb8c630 Refactor and fix uninitialized variables and improve function consistency across multiple modules
- 499ed5d remove unneeded iterator functions
- 737c220 delete more default constructors
- 4b4a282 Add const qualifiers to comparison operators and update iterator equality checks in various classes
- a62fede remove a few default constructors
- 22d9bfa fix warning with iterators due to non-const comparator
- 1121815 Standardize C++20 flag across different platforms in build script
- 1e580a7 update to c++20, remove debug output
- 96c1375 #7391
- a9f8ec1 updated handling of value initialization for bit-vectors
- ba5cec7 additional rewrites for bv2int
- fa7fc8e Refactor bv_rewriter functions using unified variable assignment and early break logic
- d66609e fix #7389
- 0c48a50 Add support for initializing variable values in solver and optimize contexts in Z3
- 342dccd correctly process cancellation in gomory cuts
- b99c4a4 Add override specifiers to methods in set_initial_value_cmd class for clarity and consistency
- 8349ee0 Add support for const array in all logics as per issue #7383
- 4896edf Add tracking of values size in scoped_state push method in opt_context
- a3f35b6 Add command to set initial value hints for solver in various components
- 1c163db remove output
- 0f89650 Add initial value setting API for solver and optimize contexts and update related function signatures
- 48712b4 Add initial value setting for variables in Z3 API, solver, and optimize modules
- 0ba306e y
- 99a9a4a fix #7372
- 1ace3d0 fix #7372
- 8061765 remove default destructors & some default constructors
- 0837e3b Fix nightly (#7365)
- 5237e7d Adjust memory reallocation to consider SIZE_T_ALIGN in memory_manager
- 6086a30 Add reference URL to GenAI script file for auto Git commit guide
- db4176a #6902
- ef58376 replace a few old-school constructors for a 0.5% reduction in code size
- a3eb2ff revert update to vector for testing #6902
- a1bcf13 fix build
- 01a4195 #7362
- 9a87bb1 #7362
- 46d602e update gitignore to prepare for genaiscript
- 84b2c21 Update nightly.yaml for Azure Pipelines
- dcdb7c4 wheelhouse
- 96417d4 Update nightly.yaml
- 59853d0 Update nightly.yaml
- c79477a update nightly
- ea93f07 Update azure-pipelines.yml
- cd89867 add back auditwheel
- ea417bb Update README.md
- 954dddb retain pip install build, remove audit
- 5360656 fix expected
- 0bf3eeb Bump docker/build-push-action from 6.6.1 to 6.7.0 (#7350)
- f6dbaee adding to nightly
- e1f1d67 New python packaging and tests (#7356)
- 349ebd0 #7344
- 84da614 make gcc linting happy
- b84b4e7 fix attribute order
- 49ba3bc address compiler warnings gcc-13
- cff1e92 Avoid broken stack at few places (#7353)
- 6a68cc5 #7353 - clear pointer when existing stack
- c1454dc Fix building with Windows SDK and Clang-CL (#7337)
- 0612a0b Bump docker/build-push-action from 6.5.0 to 6.6.1 (#7338)
- 6565455 fix #7343
- ed17de5 fix #7343
- 83f47bd wasm build problem
- bf34600 add release nodes and add the author reference in qfnra_tactic
- f2d35dd more cleanup
- 8999e1a use standard name conventions and add file headers
- 33f0256 cleanup
- 752c999 cleanup
- f81303f delete unused nlsat_symmetry_checker
- f7905a5 remove printouts
- 518a8b2 fix the build
- 4b3a06a port hybridSMT
- 1a5bddb port more from hybridSMT
- 209366b cleanup porting comments
- 839594a remove option look_for_0_witness
- 0306eff port look for 0 witness
- a09e412 cleaning up
- 6ce0fcd port sample cell projection
- 3e518b9 fix #7331
- 26b8d63 add max conflict throttle to SAT based QFNIA tactic #7329
- 52f8eb2 #7255 #7328
- bc8fa67 #7255 #7328
- d6040ee do not copy artifacts from CI pipeline
- 51fcb10 shave some overhead from fingerprint hash function #7281
- 7c30cbf add scoped_vector invariants and unit tests (#7327)
- d2fc085 update heap unit tests (#7324)
- fce4b36 add apply_permutation tests (#7322)
- ea9fa17 add static
- 23e7dc0 assert -> SASSERT
- fe59461 fix dlist tests (#7323)
- 6ba25b8 add permutation unit tests (#7300)
- e7382d6 Added "λ" pretty printing to python (#7320)
- 0c16d34 fix #7292 (#7316)
- 5fcc50f Revert "add scoped vector unit test (#7307)" (#7317)
- 2ae3d87 add scoped vector unit test (#7307)
- 2ce89e5 Gcc 15 two phase (#7313)
- 25e683e fix finalize method
- ac7014a expose pu...
z3-4.13.0
4.13.0 release
Changes:
- 3049f57 add download of Arm64 to python packaging
- f9ce332 update release notes
- 6254844 update release notes
- 7b7084d Add LinuxBuildsArm64 to python wheels in release (#7155)
- e873664 Downgrade arm cross compile toolchain to glibc 2.34 (#7153)
- 364da19 remove test
- 620efbb add aacrhc
- aad8cbd Add LinuxBuildsArm64 ci azure-pipelines for testing (#7152)
- 017367d Handle cross compile within manylinux (#7150)
- e8c8d8a Put in workaround to rename manylinux_arm64 to manylinux_aarch64 (#7149)
See More
- d6f522e na
- 531bda3 fix alias bug
- 657aaf9 na
- 8679c08 fix test
- 22616da updates
- 5be8872 na
- dfd5c27 na
- 803f0f0 na
- 5455603 na
- 9888d87 na
- f46c378 bugfixes
- d774f07 add eval field to sls-valuation to track temporary values.
- 8f139e8 updates to multiplication
- 2590d67 na
- 58474df na
- 0e5b504 remove bw setting
- a328366 move to single path mode for search
- 8f85df0 fb
- c451e4e na
- 63804c5 na
- 74e73f2 reorg to use datatypes
- 48026ed move to hide bits
- acc9c21 move to hide bits
- cfa6bd4 update python build dependencies
- 5379fab include thread
- b14499f prepare for sls experiment
- cf72a91 bugfixes, adding plugin solver
- 659e384 bugfixes
- cd6382f fix alias bug
- 9cde4f7 bugfixes
- d7e419b fixes and checks
- ab0459e bugfixes
- 7dc4ce8 use tuned gcd to compute mult inverse
- 4391c90 na
- 9915378 fixes based on unit tests
- 046db66 na
- 388b2f5 n/a
- ddf2d28 add tests for evaluation
- 1cf008d updates
- bd323d6 save
- f39756c initial stab at new bv-sls based on repair actions
- 1068708 Revert "For many linux build, use aarch64 instead of arm64 (#7147)" (#7148)
- 7694bca For many linux build, use aarch64 instead of arm64 (#7147)
- 77a07bb detect arm64 for manylinux setup
- 4050a43 Add arm64 for linux python wheels to nightly (#7145)
- 57c20be fix #7143: type punning in test
- 91886da some code cleaning and complexity improvements (#7133)
- 2880ea3 convert formatting tabs to spaces (#7140)
- c67200e update versions
This list of changes was auto generated.
z3-4.12.6
4.12.6 release
Changes:
- fa2c0e0 enable release publish
- 85425a6 Update nightly.yaml for Azure Pipelines (#7139)
- 19f5e7f ci: Really fix set-output. (#7138) [ #7136 ]
- 019c064 Update coverage.yml
- c0621cb ci: Stop using deprecated
::set-output. (#7136) - 143a35d Fix typos. (#7137)
- 785f71b prepare for 12.6
- 79b7d8a throttle squash-store #7134
- a3d00ce Improved Java phantom references (#7131)
- f7691d3 fix generic example
See More
- 199ef30 conditionally depend on importlib_resources (#7116)
- 84d592c fix #7121
- 2b14793 #7117
- 155dfb1 Fix some typos in identifiers. (#7118)
- dba2f78 ci: Update
microsoft/setup-msbuildtov2fromv1.3. (#7119) - 4d06c39 replace DEBUG_CODE by #ifdef Z3DEBUG in nlsat
- f1d97c7 allow callbacks to be nested
- 53f89a8 Fix some typos. (#7115)
- 937d4aa move files from lib and java directory to bin
- c40e72a include debug output
- f4eaa6f improve logging
- 683070a finish encoding of n'th root
- 8555f25 add todo note, and log more lemmas
- f4474a3 typo
- 446a9de distinguish vs-arch from arch identifier
- d743e1b add note that the encoding is a first approximation
- b9528b1 update self-validator to handle root expressions
- 548b9d0 move libz3.so from lib to bin, remove lib from distribution
- 7970e4f add clause persistence to sat/smt solver
- 3cec3fc bypass replaying new clause within propagation
- 3b90816 add option to persist clauses #7109
- a2fa4ff update assembly names
- c926705 update assembly names
- b9bec18 copy over dotnet files
- bc70282 mute some compiler warnings
- 9425c41 port remaining egraph update
- a5a819c port updates to egraph from poly
- 24ffef8 fix typo
- e295ac9 update build-win-signed-cmake
- e398f84 update build-win-signed-cmake
- bd082ab update mk-win-dist-cmake
- 14fb235 update mk-win-dist-cmake
- 736d634 move windows builds to use mk_win_dist_cmake in nightly
- cfc8774 move windows builds to use mk_win_dist_cmake in nightly
- 05d625b fixing paths and re-add arm64
- 485a018 add back legacy build-win-signed
- 9db834c add back legacy build-win-signed
- 2280e95 Improve instructions for working with the Julia API (#7108)
- 0d24ec3 add 'dist' to folder path
- 4260206 include variable ReleaseVersion in Nightly
- 30c14f5 include variable ReleaseVersion in Nightly
- d231913 remove period
- 93cbcd0 rename
- 77b98d5 update folder names to align with mk_win_dist_cmake
- bd2d96e update folder names to align with mk_win_dist_cmake
- 06466be disable arm64 nightly
- 28d62bf move to use release.yml version for windows build
- 5cac9b8 fix build warnings
- ca0e9a1 remove explicit option for shared build, set to Release mode. .so artifacts take 800MB in distribution
- ec6640d Update nightly.yaml
- 8507297 update ubuntu builds
- 432432b update ubuntu builds
- d624eec Update nightly.yaml
- 0a1a57c Update nightly.yaml for Azure Pipelines
- f16afe5 Update nightly.yaml for Azure Pipelines
- 9a095cc Update nightly.yaml for Azure Pipelines
- e820701 fix #7107
- e26344e update nightly
- 5551f1e update nightly
- 5c4ad4f cd to dist in nightly.yaml
- d3fbb9d add line continuations to nightly.yaml
- 4b4e057 install ninja
- ac1f971 move nightly builds of Unixes to use cmake
- 738c5b6 add warning messages for #7100
- 50deece fix #7098
- 99ebbd6 porting unix distribution script to cmake
- 28c44a6 fix #7105
- 67e5ba9 update release scripts
- f811801 remove optional Julia build
- 5d4303f build Julia for x64
- e0bed3b build Julia for x64
- 680b0f5 add download stage for arm64
- b3b95db move installation directories to under bin
- 9bd8e35 adapt paths to new distribution
- f7ed4ad update path for win distributions
- bef67f8 special purpose dotnet copy
- 4be8b7d update win-dist
- 908aaa0 fix #7101
- 2b68394 fix #7103
- f8a3b6f fix #7102
- 2af1cff updating java cmake scrip
- 527f824 update java install/build
- c8c2e3a update java install/build
- 637ffcd Update mk_win_dist_cmake.py
- dec5715 Expose forall and exists to Julia (#7099)
- 9d59d86 update cmake build
- ee2be7d attempting to build ARM
- bdb9106 Api (#7097)
- 1335466 update minor version number
- 1b94d43 fix build
- fad4283 prepare for integer intervals
- 98c9fa7 prepare for handling integer intervals
- 36453c5 use while (true) in do loops with continue
- be7856c fix #7027
- 125a82b improved diagnostics
- 8d4e7fa add diagnostics option to new arithmetic solver
- 839b710 add ability to multiply term
- 0ebd8d6 prepare for printing more cases of root objects in SMT
- 69f118e use assignment
- 414c33f Bump mymindstorm/setup-emsdk from 13 to 14 (#7095)
This list of changes was auto generated.
z3-4.12.5
4.12.5 release
Changes:
- a7b564c update release scripts and notes
- 7486e87 track quantifier instantiation method in proof hint #7080
- 302ebff prepare for release
- e722dc7 add status badge for windows build, remove windows build from Azure pipelines
- 2dd45f8 add Windows build
- 910b302 free memory the clean way
- d32dcfc free memory the clean way
- 1754523 encapsulate anum functionality
- 548be4c add explicit move constructor to deal with unit test regression test-z3 algebraic on Windows/debug -
- a2993f7 encapsulate mpz a bit more
See More
- d2706ba Fixes in Java's User Propagator (#7088)
- 2c55aa5 remove unused code
- d084a19 take care of strategy undecided, Nikolaj's comments
- 6e9a938 Merge branch 'master' of https://github.com/z3prover/z3
- c591a7a force int bound on int columns, call term_is_int() after subst
- fef1596 pin expression passed to validate_eq
- 4f75153 Update z3_api.h
- c340233 fix #7081
- afba43a fix #7085
- 4ff352f fix #7084
- 91ca55e change the definition of Gomory row
- d8df203 remove an unused declaration
- e2fb4fb fix dependencies for Gomory polarity
- 2eadcf0 avoid duplicate explanations
- 7d7fef0 add explanations and fix polarity
- ddf2eb5 deleted parameter
- 3381fd2 spell check from microsoft/z3guide#165
- 2717159 Update sat_params.pyg
- 59b18d4 create as_bin as_hex wrappers for display
- 999e67d address Nikolaj's comments in Gomory cut
- 2d24436 remove a blank line
- 2b974a0 do not delay update for the polar case
- 2ac866a take the coefficient from cut_result, not lia
- 1b39290 try to remove version spec
- b239371 try to remove version spec
- aa4e1b3 update Julia versions
- 955c80e import updates from poly branch
- 2ca1187 fix a bug in polarity
- 75005d9 add validation option for debugging regressions
- 2934618 remove simplify_inequality from gomory.cpp
- 696b70f fix
- 239d68e return conflict on an empty term in Gomory cuts
- b75367f port improvements to arith rewriter
- a7bfdcd readd big cuts
- 84997f8 move a TRACE statement
- fd2b6c6 bug fix in gomory polarity
- d66df26 Fix some typos. (#7075)
- ec2b8eb Merge shared parts from polysat branch (#7063)
- 53c95e3 cleanup
- 0728b81 add parameter lp_settings.m_gomory_simplify
- 5796e88 use vector instead of unordered_map in gomory
- a3529a0 create bounds for gomory cuts with big numbers
- af76912 adding the polarity bound
- d7931b9 Bump microsoft/setup-msbuild from 1.1 to 1.3 (#7071)
- ebe5ebf Add branch and bound solver, for fun
- ad07e0e add sub and super-slice functionality directory to euf-bv-plugin
- cd331b8 remove reference to tactic.h
- 7adb402 add missing dependencies
- 5f45118 missing cmake list
- e321643 move sls core functionality to be independent of tactic
- 606a9a7 fix test build
- cab3c45 remove unnecessary parameter copies
- ab22e76 some code simplifications in mpn
- 4fe4234 bugfix on slack
- 766f5f0 reduce memory allocs in params
- ae1d927 improve add bin/item functions
- b09c237 rudimentary bin cover solver using the user propagator
- 68a2c08 Add Z3_get_estimated_alloc_size to OCaml API (#7068)
- 19f3ad4 fix the build
- e9fa7db revert smt_enode
- a00eb08 Merge branch 'master' of https://github.com/z3prover/z3
- 4317d13 refactor: move gomory functionaly from int_solver to gomory
- c4fa719 revert last two commits; MSVC doesn't like to statically allocate flexible arrays
- 6246c65 fix debug build
- c9c53b7 tmp_enode: don't heap allocate an app. store it inline instead.
- 4898a15 shrink ast's app by 8 bytes on 64-bit platforms when number of args > 0
- b2d5c24 remove a few string copies
- e28b644 remove an empty line
- d636561 change some TRACE statements
- db5a1a7 Bump actions/upload-artifact from 3 to 4 (#7065)
- 97d4508 Vector updates from polysat branch (#7066)
- 4c9f705 tptr: add pointer tagging templates (#7067)
- fcc7b25 remove a few string copies
- e5f52e2 Update Windows.yml
- d088fe9 Merge branch 'master' of https://github.com/z3prover/z3
- 9a18628 remove unnecessary assignments
- 5cafda1 remove reference to matrix bindings to see if it works
- 2602fc2 remove reference to matrix bindings to see if it works
- 1b75504 add path n prefix
- 00965cb fix string
- 394a355 fix string
- 9469f75 Update Windows.yml
- ea03b55 Update Windows.yml
- bb8ed43 Update Windows.yml
- ea44c11 gc expressions in the scope of updates, not old expressions
- 842385a Update Windows.yml
- 62ae9a0 Update Windows.yml
- 91ba893 Update Windows.yml
- ee073be Update Windows.yml
- c7c007c Update Windows.yml
- 9e3a489 Update Windows.yml
- 0dc8511 Create Windows.yml
- 13be3c3 reset model converter between rounds to elim-unconstrained.
- 0daa05a add ability to log selected bv rewrites
- dff419a pin expressions to fix unsound behavior
- 5d4c18d fixes
- 6d23847 fix typos
- d008dbe port Jakob's update to bv_internalize
- 085b5e2 port Jakob's update to union_find from polysat branch
- 2f2bf74 fixes to intblast encoding and more arithmetic rewriters
- bb99f44 fix bugs in elim-unconstr2 and fix bugs in intblast_solver
- 4867073 remove windowsArm64 from nightly
- d0a59f3 intblast with lazy expansion of shl, ashr, lshr
- 50e0fd3 Use
noexceptmore. (#7058) - b44ab2f add rewriters for and
- 4778f27 revert to standard solver
- 9293923 Add intblast solver
- 0520558 port updated pdd from polysat
- 2e83352 Fix bug in fp.round_to_integral (#7060)
- e90a844 Use
overridemore. (#7059) - f6e69d4 Merge branch 'master' of https://github.com/z3prover/z3
- a2b490b Disable Python compilation cache during build (#7057)
- 7c2e4f2 fiddle with what gets added to win-arm64
- f7d9a5b Revert "Disable Python compilation cache during build (#7052)" (#7054)
- b40e301 fix #7053
- c20b8cb nightly
- 995b40...
z3-4.12.4
4.12.4 release
Changes:
- dce2f3d add release notes
- b3ef74c remove readme for dist
- fc3a765 try to put readme in root
- 2c8d338 add README path to mk_nuget_task
- 8111d87 add README path to mk_nuget_task
- 1fde3e9 update release
- 1d6616a make var-queue a template
- 156426a use / for package path
- 111ce01 update path reference to readme
- d566eb3 include readme in package
See More
- 76c05f1 specify a readme file with the nuget package
- 426d7f5 remove reference to readme in nuget task
- a9513c1 Improve BoolRef addition (#7045)
- 7c81ee0 fix case of README.md in nuget
- 669f665 update release pipeline
- aa2e54c update release pipeline
- 23fcb43 readme
- f5ae8c3 make a readme file
- 9ad4d50 Use built-in
importlib.resourceson Python 3.9+ (#7042) - 764f0d5 Overload xor operator for BoolRef (#7043)
- 4d4359f fix shebang syntax issue (#7044)
- 389aea3 update release notes, update version number
This list of changes was auto generated.