z3-4.9.0

4.9.0 release

Changes:

• 2ae84f8 Update release.yml for Azure Pipelines
• 15391fc remove musll from release.yml
• f1b7ab3 x64
• 7f2ebf8 Remove package sub-directory from release script
• 580ed31 fix types and incompleteness for feature #6104
• bda8672 macarm
• 4f62336 download arm64
• 593d5be bind variables
• 8b35b7b bind variables
• 594b5da remove download of mullinux

See More

• 3ce6663 update release script
• 73f35e0 Update release.yml for Azure Pipelines
• 85c3d87 neatify
• f23dc89 add disabled pass to detect upper bound range constraints
• a374e2c ignore qid if they are both numerical - come from the parser
• 6e53621 #6112
• a251595 Merge branch 'master' of https://github.com/z3prover/z3
• d7472f0 fix #6124
• db09d38 bump emscripten version used to build wasm artifact (#6136)
• f82ca19 #6104 also in the new core
• de41cfd fix #6104
• 282c786 setting version to release
• 2a5d23b rename URL
• cd416ee add note about opt.incremental
• ac822ac add parameter incremental to ensure preprocessing does not interefere with adding constraints during search
• 2cf0c81 Update RELEASE_NOTES.md
• 2990b69 Update RELEASE_NOTES.md
• 605a312 make release notes markdown
• 71fc83c Move out equality use out of the loop
• 0353fc3 fix #6127 again
• 6ed2b44 probably won't fix #6127
• ac8aaed fix #6126
• d61d0f6 prepare release notes
• 02a92fb revert to use GCHandle for UserPropagator
• 1e8f907 fix unsoundness in explanation handling for nested datatypes and sequences
• e6e0c74 Update update_api.py
• bb96677 Update UserPropagator.cs
• d37ed41 Update Expr.cs
• c35d0d1 Update update_api.py
• 54b16f0 Update NativeStatic.txt
• 004139b rewrites for characters
• f20db3e allow for toggling proof and core mode until the first assertion.
• 4d23f28 ml pre
• 815518d add facility for incremental parsing #6123
• 8c2ba3d missing virtual functions
• 06771d1 missing virtual functions
• 4f9ef12 create dummy tactics for single threaded mode
• 3c94083 fix doc errors
• ea2a843 flat only
• b618537 Merge branch 'master' of https://github.com/z3prover/z3
• 94a2477 totalizer
• 959a0ba fix #6121
• e054f16 fixing compiler warn (missing override) (#6125)
• c3d2120 add totalizer version of rc2
• 8ab8b63 fix incorrect mod axiomatization #6116
• f6932f9 Merge branch 'master' of https://github.com/z3prover/z3
• 1a91226 remove unsound axioms, fix #6115
• 03287d6 fixes issue #6119 (#6120)
• ff26523 adjust trace output
• 5afcb48 adding totalizer
• fd8ee34 add logging
• 12e7b4c fix gc'ed callbacks in .NET propagator api (#6118)
• 7977876 add doc string
• 798a4ee use IEnumerator and format
• 556f0d7 use static list to connect managed and unmanaged objects
• 820c782 pinned semantics
• 9836d5e missing public
• b43965b make user propagator work with combined solver
• 4c8f6b6 fix #6107
• 61f5489 fix #6107
• 1fcf7cf add nl div mod axioms
• 30165ed fix #6105
• 56aa426 fix #6082
• 352666b JS api: fix type for from (#6103)
• c15a000 Make high-level JS API more idiomatic/type-safe (#6101)
• 8234eea unbreak
• 3189544 next split
• a7b41c4 fix for spurious wakeups in scoped_timer (#6102)
• 41deed5 fix bug in array rewriter introduced in 202ce1e
• 36a1f75 mask regression
• ab9aee1 perf #6100
• 202ce1e #6100 - two perf fixes
• f24c5ca #6095
• 5ba8231 make it work with old pythons
• d792d30 Update NativeContext.cs
• b254f40 Separate out native static content for Java [ #6097 ]
• 25e915f fix #5990: deadlock in the scoped_timer
• 911134b add new heuristic rc2bin (to be tested) to maxsat
• 940d10a Update coverage CI (#6099)
• 2fa60aa Added function to select the next variable to split on (User-Propagator) (#6096)
• f08e3d7 attempt to fix windows build bot
• f3c00a0 attempt to fix windows build bot
• c3407fc fix build of tests
• fcbbf7b fix build warning+error in c++ example
• d9fcfda fix debug build
• 73a24ca remove '#include ' from headers and from unneeded places
• 70bcf0b reduce sizeof(enode) from 120 to 112 bytes by swapping the order of fields
• 08c44bc remove unused static features
• 477e962 Don't reset the cache between applications of replace
• 99b606b add logging
• 7fdcbba Add high level bindings for js (#6048)
• 3d00d1d prepare for equality propagation from Grobner basis
• 8e20271 fix spacing
• 55421af fix regression in top-sort fix #6060
• 637120c Treat arguments to recursive functions as beta redexes
• 25ad5cb prepare ground for drup trim
• 35d4605 remove spurious output to stdout
• 04f94d8 fix #6091
• 46bc726 Better error message for mismatching sorts in substitutions in z3.substitute (#6093)
• 470bf27 drat
• 9cd3398 for Arie
• 994dab8 add pre-filter for F* use case
• 8efa3c8 introduce notion of beta redex to deal with lambdas in non-extensional positions
• b9b5377 add a way to supress lambdas
• 5db133f add a way to supress lambdas
• 97437bc Update sat_params.pyg
• 828850f prepare for trim
• c584750 contains-partition
• 6a1193e reorg if-then-else structure
• 72a6384 time overflow before stack overflow
• e468386 #5656
• dee6c30 na
• 80604c7 na
• 51ed13f update topological sort to use arrays instead of hash tables, expose Context over Z3Object for programmability
• 0e6c645 display model in add/del format
• a7b6f30 Bump docker/metadata-action from 3 to 4 (#6086)
• 35986f3 fix #6084
• fe08c99 fix #6081
• cc045de again
• bb6c274 fix #6085
• dca1dcc ea
• b629960 proof format
• ea365de add cut
• da93829 use common functionality
• f77608e Add interpreted versions of unspecified cases of fp.to_ieee_bv and fp.to_real (#6077)
• d722c73 Fix corner case in MPF FMA (#6075)
• 6422a6b Fix rounding bug in to_fp (#6074)
• cb67f90 Merge pull request #6072 from wintersteiger/cwinter_warnings
• 4421f7d Merge pull request #6073 from wintersteiger/cwinter_deflt_rm_py
• 3345419 Change FP default rounding mode in the Python API
• ed7db89 Fix a couple compiler warnings
• f652c57 fix proof checker
• 3d1e03e add start of self-contained proof checker for arithmetic
• 93a0322 update distribution scripts
• 366860b change to osx-11.0
• c7560e1 change to osx-11.0
• 4191d84 change to 11.0
• 6327367 Merge branch 'master' of https://github.com/z3prover/z3
• 0b17a56 fixes to script
• c05c75c Bump docker/login-action from 1 to 2 (#6068)
• f54e8e5 Bump docker/build-push-action from 2.7.0 to 3.0.0 (#6069)
• 96e3176 Bump actions/setup-node from 2 to 3 (#6067)
• 05c1d6d Bump actions/upload-artifact from 2 to 3 (#6065)
• b836724 Bump actions/checkout from 2 to 3 (#6066)
• 9190f22 os
• 6396cfd os
• 8384c32 chore: Set permissions for GitHub actions (#6063)
• b81b771 chore: Included githubactions in the dependabot config (#6064)
• 9ed7fd9 Update nightly.yaml for Azure Pipelines
• aa8e89c try macos12 for arm64
• a9d70fc fix #6061
• e9cff33 fix #5068
• 15c4780 #6059
• da3f316 fix proof checking for bounds propagation
• cb279fb fix sign for binary propagation hints
• bffa7ff add hint verification, combine bounds/farkas into one rule
• 36ad377 na
• 63b9c4b for AG
• 9ec34d9 comment out muslinux build
• 6abea2d fix nightly, fix regression identified by Nuno
• b8532be remove pragma from cpp file
• ddc3445 try to add back musllinux
• 35db0ae workaround manylinux build failure (it is advertized as a compiler bug)
• d09d37c wt$
• 6b4bc5b remove broken matrix
• e966001 remove hardwired image name
• 6ce03cd Update nightly.yaml for Azure Pipelines
• 0038817 Update nightly.yaml for Azure Pipelines
• 4870182 indent
• 4953b95 cleanup pre-processor for z3_api.h
• 8d980ea remove internal configuration
• dd46224 use structured proof hints
• 7da9f12 expose description of global parameters #6048
• de892ed fix #6054
• f77037e expand select/store when I/J are values #6053
• 4d8e4b5 fix #6052
• 8c95dff cnf
• c850259 rw
• 386c511 core opt
• 127af83 remove ad-hoc diagnostics
• 40fe472 nit
• 363b69f fix #6034
• f6b2874 update to take effect of def_API for callback functions
• ca2497e na
• 186a3c5 merge
• 1028c80 update pretty printer for recursive function filtering
• 7f62fa2 Sparse matrix kernel (#6035)
• 6f7be77 Buildsystem fixes for FreeBSD. (#6029)
• 7497856 add ignore int to new arithmetic solvers
• b1aa6b2 disable normalize
• 6deb4de disable normalize
• 5aec9b3 check zero
• 860d904 check zero
• 3611556 ensure abs
• cbaa16d lcm normalization
• 5ca3bc3 kernel
• 54648f6 add stats for binary clause creation
• 2928cc2 fix
• 805443c wip
• 0557d72 na
• 6a8ac5f adding K
• ad2445e gauss jordan
• 361888f Generate bdist wheels for musllinux_1_1 (#6025)
• dcc01b8 prep for pragmas
• 6670cf0 na
• fbf5e32 js
• 4549ec7 misc
• da9ed82 add decide callback
• 8218f25 add decide callback
• c8d1297 fixes for fresh
• 506f8f8 add user propagator functionality
• 1e7a9e3 fix #6023
• 97af3a6 fix #6021
• cca4915 fix #6021
• 3b44113 ocaml build
• 7def610 build warnings
• d58de2f java build
• a71ce54 freeze functions with callbacks for ocaml
• cf4149d freeze functions with callbacks for ocaml
• 1ab7be6 java build
• e2625cb safe
• 3bf09b1 safe
• a3b066f ml: VOIDP -> ptr
• 04b0b36 js
• b633947 don't log function pointers
• 6d40e6f java
• 1e58688 patch js for fnptr
• 14214c5 exposing user propagators over .Net
• 3ae7810 inc version number

This list of changes was auto generated.