z3-4.12.2

4.12.2 release

Changes:

• e417f7d updated release notes for 12.2
• ba91100 disable publish
• 046b80f remove output
• f6ab5a6 reformat code to remove brackets
• 12e45c9 Implement proposed smtlib2 bitvector overflow predicates (#6715)
• 62e1ec0 Merge branch 'master' of https://github.com/z3prover/z3
• 2e441e3 fix #6713 fix #6714
• 0c9a5f6 JS/TS: add Optimize class (#6712)
• 6c24a70 remove debug output
• f176917 make default argument to ensure_def and mk_def explicit

See More

• c64d61b formatting updates
• 392266c fix processing of else expression for model table
• d5231f8 fix regressions #6703
• c48dc69 adding stubs to find fixed variables
• ef94334 ensure assume-eqs is invoked after check-lia statically
• d2e3e48 add instrumentation to theory_lra for shuffling final check
• 3029fb2 remove references to validating
• 50c855e count gcd conflicts, log row id in rows
• 59bc070 count gcd conflicts
• ace6e8e add gcd-conflicts stats, formatting updates
• 8fb4515 remove redundant function, add checker function to test missed propagations
• e689dea basic formatting updates
• d4fa990 return diagnostics
• d8156ae weird latent bug in wmax: init() succeeds and it returns undef
• fdd5c92 use only maxres if there is a lexicographic objective, fix #6697
• 7a689c3 disable destructive equality resolution simplification if there are patterns
• a2bac11 differentiate fixed from offset-eq in statistics
• ec1480b fix #6693
• cb041c1 fix #6689
• 1319b64 fix #6692
• 97b66d1 fix soundness bug in disabled code
• b75d81f fix #6690
• 6249078 add tests for distribution utility and fix loose ends
• 1a70ac7 fix #6687
• b783879 #6687
• 7cd8edc perf and memory smash fixes to internal node count routine
• f0afbcb fix #6686
• eba0732 fix #6675
• e822243 count internal nodes, use to block expanding use of hoist, #6683
• 444238b formatting updates
• f61168c module for maintaining probability distributions
• 0b5c38d fix #6676 get rid of rem0 declare it to be mod0 semantics to simplify code paths
• 58a2a9c fix #6680
• ccc4f2d fix #6682
• 368d60f add branch / cut selection heuristic from solver=2
• bb44b91 fix #6677
• 98d3fab Bugfix relevancy propagation + UP (old core) (#6678)
• 4a142b0 fix #6623
• e6ea815 fix #6662
• af9c760 fix #6670
• ccb250c fix #6671
• 7b513b4 Some UP bugfixes in the new core (#6673)
• 84b9204 inherit and reset rlimit counter on children limits
• f8242c5 fix regression from Grobner port
• 479f844 fix #6661
• def83ed fix #6661
• 5b385bd fix #6665
• 6324db2 Only print func-decl names for indexed parameters (#6663)
• e0a066e #6654
• 7664429 remove cast expression
• a62e4b2 extract multi-patterns when pattern can be decomposed
• a849a29 fix #6659
• 6aaaa3b fix #6660
• 996e5b1 fix #6655
• b386b84 #6658
• 6670807 update ocaml binding to support more string apis (#6656)
• 130400d Remove non feasible costs (#6653)
• fe348b8 fix #6652
• adec937 fix #6650
• f366772 use field 'm' for streamlined representation
• 0a59617 Fix Ocaml bindings FuncEntry to_string (#6639)
• ce09c2e fix build
• b4ad747 fix #6644
• 8a3a3dc fix #6648
• ce501e0 #6646
• cd2ea6b add parameter access to C++ API
• 9ca0faa enable interactive example
• 50bd6ef fix #6624
• 03a4480 fix #6635
• 2683a2d fix #6637
• 53ca65a fix unsound rewrite
• f075dc2 remove experimental files
• 48de7c2 missing updates
• c6e3fb4 print lemmas2console faster
• a9e6e56 make generation of "some" Boolean value fair
• d1c7ff1 add unconstrained elimination for sequences
• a0f3727 BV: add missing neg internalizer
• cf4df08 fix typo (#6628)
• 1612b57 Make all methods show in java API (#6626)
• 4b34086 use uintptr_t instead of size_t (tptr) for portability (#6627)
• 8b0aa22 replace lp_assert(false) with UNREACHABLE
• 3efe91c more dead code
• 1fb24eb fix lp_tst
• 11eab94 more dead code
• 13549af rm dead code
• c6be67b more dead code
• c8c0a00 remove more dead code
• 748c752 more dead code removal
• e430f28 remove dead code
• f644589 rm lu related fields from lp_core_solver_base.h
• f351eb3 remove many methods dealing with double
• 9ec8263 rp precise
• 569f5be rm dead code
• f33f8c2 more cleanup
• 0fb65de rm square_sparse_matrix
• 1781354 rm scaler
• 6eedbd4 rm lu
• e04e726 rm lu
• 2e9dc3d rm lu
• d00fcc8 Revert "rm dealing with doubles"
• a418918 rm dealing with doubles
• 6201eda rm breakpoints
• 73224ad cleanup
• 377ceba rm lu
• 6132bf9 rm lu
• bfe73c0 rm lu
• 1da4c01 rm lu
• 62bd3bd rm lu
• 5f03c93 rm lu
• 9a7c99d rm lu
• c251151 rm_lu
• 25f103d rm_lp
• 527f0d1 rm lu
• a38be43 rm lu
• 97c1ba4 rm get_column_in_lu_mode
• ea16f66 before rm lu
• f7c9c9e fix unsound slice criteria (#6625) [ #6617 ]
• 42076a3 bug fixes to new core, elim_predicates and elim_unconstrained
• b9a87e4 minor code simplifications
• 92fe8c5 restore the previous state
• ff1dc04 rm lp_solver
• 5e4bca3 small removals
• 2dd30fa rm lp_primal_simplex
• 8989e10 rm lp_dual_simplex
• d2e8297 remove includes of lp_dual_simplex
• 2ec0994 removals
• a447724 more removals
• 8db2f14 lp_dual_simplex.cpp removed from CMakeLists.txt
• cd24c99 remove a lp_primal_simplex.cpp from CMakeLists
• f986ac6 remove mps_reader
• 55d45e0 bug fix. Prevent resetting gg stats #6062 (#6618)
• b82d177 fix build
• aa75ba8 remove parenthesis
• fd97be0 move sat.smt.proof.check_rup into solver.proof.check_rup #6616
• 94b79ee add back max_occs parameter dependency to solve-eqs
• acd2eaa add (disabled) code path to enable nested conjunctions
• 46d37b6 fix #6615
• 0277709 fix bug in quasi macro identification: require quantifiers
• 25d45a3 fixes and tests for arith-sls
• e87fa1c remove stale file
• 79d47eb add preprocessor parameter whether to use bound simplifier
• 76aad68 Update smt_context_pp.cpp
• 5974a2d remove m_b from lar_core_solver
• 1a9990a Use sys.getdefaultencoding() instead of sys.stdout.encoding (#6612)
• 6e7d806 Documentation on how to add z3 to CMake project using FetchContent and documentation to recdef function. (#6613)
• 358caa8 Merge pull request #6608 from hgvk94/bugfix [ #6543 ]
• 828fff9 fix #6543. don't assume order on bindings
• 146f0ea wip - arith local search
• 4aa05b2 remove limiting error mode #6600
• 755b517 fix #6600
• 0758c93 fix #6591
• 6454e7f apply rewriting if result of destructive equality resolution is simplified
• bc60374 clean up build warnings
• 9b6ac45 compile warnings
• 6352340 update do logging
• a6eed9f Update api.cpp
• cb81473 add destructive equality resolution to the main simplifier.
• c0f80f9 deal with compiler warnings (unused variables etc)
• 6092bf5 fix #6599
• daeaed1 revert debug only changes to sat-solver
• c5e33b7 wip - arith sls
• f66a082 fix #6595
• 828ff98 fix tpl instantiation issue for mingw (#6597)
• bd10ddf wip - local search - use dispatch model from bool local search instead of separate phases.
• ac06888 add trichotomy for sequence comparison. #6586
• 554a9e8 fix #6346
• 7c08e53 fixes for #6590
• c1ecc49 wip - local search - move to plugin model
• a1f73d3 wip - local search - fix build
• 4f20b8e wip - local search
• 8ce0c56 fix #6590
• c2fe765 remove dependency on bool-rewriter in hoist rewriter
• a976b78 fix #6585
• 44fcf60 wip experiments with sls
• 9ce5fe7 track assumptions when parsing into a solver. This enables solver.from_file/solver.from_string to support assumptions/cores #6587
• 3dc91de fix #6582
• 2b77012 fix build
• 52804b5 save on dtt
• 7956cf1 annotate arith_sls
• bb81bc5 fix #6580
• 102eee7 patch regressions
• cac5052 fixes related to #6577
• ede9e5f [WIP] More TS Binding Features (#6412)
• 5e30323 wip - bounded local search for arithmetic
• 4b2c166 fixes to build
• 7bef2f3 wip - local search for euf/arithmetic
• 46c8d78 fixes for #6577
• d22e4aa wip - integrating arithmetic local search
• 1b0c76e fixes to mbqi in the new core based on #6575
• d52e893 Added overloaded versions of context::recfun in the c++ api that allow for the declaration of recursive functions where the domain is given by a z3::sort_vector instead of an arity and sort* (#6576)
• 02d48ad fix #6573
• a8335f2 use phase
• b3ebce3 fix compilation
• 96d815b adding arith sls
• 6a2d60a fix #6571
• 601e506 remove debug out
• a150e58 update release script
• 90a7586 elaborating on local-search rephase strategy
• f3ae769 update stage name
• c1cadd3 update stage name
• a723102 try side-by-side nightly
• c1c26f0 restart after sat solution
• 03a4920 fix build
• 75c5738 updates to ddfw, initial local search phase option
• 992793b update nuget packaging targets #6570
• 3712cbd fix #6559
• d69155b Shared features from polysat branch (#6567)
• be44ace fix typo (#6569)
• cb72b96 Merge branch 'master' of https://github.com/z3prover/z3
• 839f87a don't apply tactics in parse mode
• 39d2818 compiler warnings/bugs
• 0d05104 remove unused field
• 741634b compiler warning fix
• efbecb1 compiler warning
• ed4a84e compiler warning
• 4143c54 add simplifier to java API
• 2e068e3 add simplifiers to .net API
• 72e7a8a fix incremental pre-processing to work with consequences/cubes
• 6c7dd4a fix incremental pre-processing to work with assumptions/cores and consequences
• 7767144 fix test
• 30fa37e fix warnings
• 38d526e fix warning
• 682e868 initialize field
• 0f86a00 use setter method to easier track updates to settings.
• 19fed09 protecting add_simplifier API against mis-use
• 151a623 Bump docker/build-push-action from 3.3.0 to 4.0.0 (#6562)
• 63c0f35 update ml api
• d51d518 update ml api
• 1289937 update ml api
• 9a94a9a update ml api
• 17bae9b update ml api
• 162fa3d disambiguate overloaded with for Julia bindings
• 4c6d44f add ocaml signature for simplifier
• 550619b add API for creating and attaching simplifiers
• ebc2cd5 fix build
• 88bf3c6 check if trail is empty to avoid collecting variables
• 8495be1 add shortcut filter to avoid traversing model reconstruction trail if there are no intersections with model
• 6d8d8f1 fix release message
• e6f8fe3 remove empty file
• d263b37 update release notes

This list of changes was auto generated.