Z3Prover/z3 z3-4.15.3

on GitHub

• 57a60c8 add > operator as shorthand for Array
• 3abb091 fix #7776
• c8e866f Parallel solving (#7775) [ #7741, #7752, #7743, #7745, #7739, #7748, #7750, #7756, #7758, #7734, #7759, #7769, #7771, #7603, #7755, #7774 ]
• d375d97 Bump actions/checkout from 4 to 5 (#7773)
• 6486d92 Add .github/copilot-instructions.md with comprehensive Z3 development guide (#7766)
• cf8a17a restore the square-free check
• e33dc47 remove unused square-free check
• b7d5add Update RELEASE_NOTES.md
• 8598a74 rename add_lcs to add_lc
• 88293bf get the finest factorizations before project
• efb0bda remove ref to theory_str
• baa0588 remove automata from python build
• fcd3a70 remove theory_str and classes that are only used by it
• 2ac1b24 avoid interferring side-effects in function calls
• 7ba967e fix java build for java bindings
• 0cefc92 register on_binding attribute
• d57dd6e use jboolean in Native interface
• fa3d341 add on_binding callbacks across APIs
• 30830aa rename a Python file
• f5016b4 remove a printout
• 3eda386 precalc parameters to define the eval order
• eeb1c18 more untangle params
• efa63db debug under defined calls
• d218e87 add python file
• 31a3037 add Z3_solver_propagate_on_binding to ml callback declarations
• aad511d missing new closure
• b33f444 add an option to register callback on quantifier instantiation
• d4a4dd6 add arithemtic saturation
• b1ab695 fix #7603: race condition in Ctrl-C handling (#7755)
• 7a8ba4b Add support for Algebraic Datatypes in JavaScript/TypeScript bindings (#7734)
• d66fabe Update smt_parallel.cpp
• b9b3e0d Update euf_completion.cpp
• d8fafd8 Update euf_ac_plugin.cpp
• f23b053 remove a bunch of string copies
• 97aa46a remove default constructor
• 89cc9bd disable pre-processing during cubing
• 2d876d5 allow for internalize implies
• f77123c enable passive, add check for bloom up-to-date
• 67695b4 updates to ac-plugin
• 0761394 Add parameter validation for selected API functions
• e3139d4 #7750
• eb24488 FreshConst is_sort (#7748)
• ad2934f fix unsound len(substr) axiom
• 1f8b081 #7739 optimization
• 8e1a528 ensure atomic constraints are processed by arithmetic solver
• 0528c86 fix #7745
• 95be0cf remove verbose output
• e549286 add option to selectively disable variable solving for only ground expressions
• 1a488bb indentation
• 01633f7 respect smt configuration parameter in elim_unconstrained simplifier
• a6c51df ensure solve_eqs is fully disabled when smt.solve_eqs=false, #7743
• a2f1742 moving to active/passive division
• 44cd38c Update msvc-static-build.yml
• fc51067 compile warnings
• 1d1a01c update logging
• dbcbc6c revamp ac plugin and plugin propagation
• b983524 add diagnostics instrumentation to mam
• 383f4db update pretty printer to show lambdas
• 47a2376 bugfix to ac-plugin
• fd54554 fix #7725 - proofs are only possible if context was created with proofs enabled
• e575919 debug : Add support for selecting LLDB via invoke on macOS (#7726)
• 0995928 wip - throttle AC completion, enable congruences over bound bodies
• 35b1d09 working on ho-matcher
• 195f3c9 update build dependencies
• 0c5b0c3 turn on ho-matcher for completion
• 1b3c3c2 initial pattern abstraction and move matching to src
• 2d1a42d fixes to ho-matcher
• 3ccf7a6 make concurrent collect_statistics in a timeout thread safe
• 951554e ho matcher draft
• 0ee1ee5 Update azure-pipelines.yml for Azure Pipelines
• d2990e2 use usize to suppress the data loss warnings
• f544dd4 deal with warnings
• bb100a4 c is non-null
• 75678fc Fix O(n²) performance issue in CLI datatype declaration processing (#7712)
• 53c48f7 trace : Sort and reorder trace tags by tag_class and tag_name (#7714)
• 0218fb7 fixup pipleline to support testing packaging
• 0928a1f trace : Classify tag_names unique to smt_internalize.cpp (#7713)
• 8de80e6 #7710
• 97193b4 call into collect_statistics in case of -T interrupt
• a28f55a log scope level of lemma
• bfed237 expose scope level
• bc96e9e Add python packaging to main pipeline to check updates to sdist
• 725c093 use usize to work around mess with static_cast insertions when looping over small vectors
• a73e244 nits
• 661ccb3 Revert "Fix source installation to create dist-info directory for package dis…" (#7704)
• b1259fb Update nightly.yaml for Azure Pipelines
• ad0afbb Fix source installation to create dist-info directory for package discovery (#7695)
• 28d0b47 following the review comments
• 84a6e4d Fix pydoc doctest failures by updating expected output format for string operations (#7703)
• c2efd3d Update on building OCaml binding with CMake (#7698)
• 2de40ff Improve Extract function documentation to clarify bit-vector vs sequence usage (#7701)
• d717dae remove the parameter for throttling nla lemmas
• 2b6c73a add stats for throttling
• 899677e fix a warning
• 9e52a38 add throttling to generate_plane1/2
• ac34dbd consolidate throttling
• 727dfd2 use the new throttle in order lemmas
• 832cfb3 consolidate throttling
• f320667 remove debug_location parameter
• 5caa7f1 throttle lemmas in nla_solver untested
• 4631915 a version of key
• 20fb830 filter out empty lemmas from nla_solver on consumption
• 4e33b44 add lemma.is_empty()
• 5bda42e rename new_lemma to lemma_builder
• 2f2289e update minor version number

This list of changes was auto generated.