z3-4.12.0

4.12.0 release

Changes:

• feda706 Update release.yml for Azure Pipelines
• 5dbd0bb add sign
• 54524de Update release.yml for Azure Pipelines
• c33b1e3 fixup manylinux reference in release script
• 234ff28 prepare release script
• f180513 missing code signing
• 60fef92 missing code signing
• 42fbf23 update code signing
• d289434 fix #6535
• 0d46787 update readme

See More

• d204413 remove update
• 85abbb8 include apt-get update for doc build
• e4bd406 update version of manylinux
• 25b0b14 move bound_manager to simplifiers, add bound manager to extract_eqs for solve-eqs #6532
• e5e1626 Initialize m_istamp_id in lookahead::init (#6533)
• 8970a54 expose parameters to control behavior for #5660
• 1c7ff72 add tactic doc
• d415f07 memory leak on proof justifications
• b700dbf fix #6528
• 2bd933d Fix hwf.cpp for MinGW-w64 32-bit clang (#6529)
• c3e3114 fix #6530
• a4d4e2e track assertions
• 64ec8ac fix model reconstruction ordering for elim_unconstrained
• 30e0f78 remove exit
• a4f2a1b Bump json5 from 2.2.1 to 2.2.3 in /src/api/js (#6527)
• 49ee570 split into separate function
• 5899fe3 Add rewrite for array selects of chain of stores of a same value (#6526)
• 1ddef11 several fixes to proof logging in legacy solver
• 61b90e6 disable new simplifcation for multiplier until really understood
• fcea323 add missing tactic descriptions, add rewrite for tamagochi
• 95cb06d add quasi macro detection
• 25112e4 bugfix to flatten-clases simplifier
• c07b6ab more tactic descriptions
• 0d8a472 pass sign into literal definition for pbge
• 81ce57b #6429
• e009915 #6429
• 380c701 restore debug clang/gcc build
• 21362c0 make case-def and recfun-num-rounds re-parsable for logging
• ef10119 #6429 fixes
• aa080a6 update ignore-int handling #6429
• 8d0d6d8 Merge branch 'master' of https://github.com/z3prover/z3
• 6f95c77 fix bugs in flatten_clauses simplifier, switch proof/fml
• e448191 array rewriter: expand select of store with const array into an ite
• e508ef1 fix Alive bug #875: bit blaster not respecting soft memory limit
• a2cc504 remove a couple more std::endl
• d30cb55 don't flush stream when printing param vals
• d449073 Merge branch 'master' of https://github.com/z3prover/z3
• ea0d09b add pointer to build parameters to README #6518
• dbf93c5 Fixing array select for lambda expressions in Python API (#6516)
• f6d411d experimental feature to access congruence closure of SimpleSolver
• c0f1f33 dampen second setup of theory_bv
• 5f6f2fc rename bit_blaster class to bit_blaster_simplifier to avoid name clash
• 0d05e06 initialization order
• 2c3ecce fix build
• 8002a51 tiny fix to qprofdiff (#6497)
• 293627c fix #6513
• 07ab4d3 fix #6513
• 47324af be nicer when memout is reached in SMT internalize: return undef rather than crashing
• 7cc58c9 Merge branch 'master' of https://github.com/z3prover/z3
• ec74a87 fix #6510
• 3e8cbb6 #5884
• abef260 Merge branch 'master' of https://github.com/z3prover/z3
• bc19992 add doc for ackermannize
• 8d332cc #6508 (#6509)
• 6fab4fe #6508
• b9c4f5d #6506
• 8efaaaf Fix #6503
• fe80347 fix #6501
• f961300 Merge branch 'master' of https://github.com/z3prover/z3
• 603597a deal with cancellation in qe for #6500
• e423fab tactic
• 0768a2e updated doc
• ecf25a4 outline scheme
• 13920c4 more doc
• d5316e0 add tactic descriptions
• f01d9d2 Merge branch 'master' of https://github.com/z3prover/z3
• aed3d76 add doc
• d47dd15 set encoding into gparams because this is the only entry point in zstring #6490
• c4b2aca add missing error checking #6492
• dbb4bbe remove debug out
• 9054e72 fix #6467
• cd3d38c sort out terminology/add explanations, add shortcut to C++, fix #6491
• 2d7a38e fix #6488
• 7afcaa5 update doc
• e648e68 add doc
• e82c8e7 Fix a compilation error with clang-cl (VS2022) (#6489)
• aded8e5 fix #6488
• 4598af7 fix #6488
• a3e6885 fix #6488
• 039de6a build issues
• cb86031 fix build
• d308b8f simplify code + remove unused file
• 6b60a3d fix syntax
• 2520dcb merge
• 2d43ccc Revert "fix crashes in elim-uncnstr2"
• 6a1b3f7 move debug output to before state update
• f7269bb update doc
• a9f52b0 doc fixes
• 527fb18 add doc for card2bv
• a302c2f fix crashes in elim-uncnstr2
• ee307dd Merge branch 'master' of https://github.com/z3prover/z3
• 1434c7d #6059
• 9ebacd8 fix buggy mask (typo in my last commit..)
• 96a2c04 fix bug reported by Nuno
• a96f5a9 fix overflow in mpz::bitwise_not
• c6f9c09 cleanup more in dependent_expr_state_tactic to reduce mem consumption
• ca6fed8 minor code simplification
• 8981d32 #6481
• 4a451b1 add custom coercion for floats. fix #6482
• c45c40e doc
• 7e69dab distribute forall cpp code
• c33e58e update distribute forall
• 80033e8 cave in to supporting proofs (partially) in simplifiers, updated doc
• aaabbfb remove comment that does not align with result
• d125d87 typo
• 1e06c74 add doc
• 7df4e04 add der description
• 90ba225 add more doc
• 5a5758b add documentation to initial selection of tactics
• f1a65d9 add documentation notes
• a2f5a5b remove memory alloc from statistics_report
• eb8c53c simplify factory of dependent_expr_state_tactic
• de916f5 add demodulator tactic based on demodulator-simplifier
• 8709595 fix #6477
• ead2a46 build
• b76ed6a proper fix to #6476
• 9b58135 try to fix linux builds
• 0f7bebc try big M for linux build
• 1974c22 add demodulator simplifier
• 9acbfa3 move it into substitution to handle dependencies
• 3d7bd40 a round of cleanup
• d218083 The demodulator doesn't produce proofs so remove code path that depends it does.
• 7fe6787 ufbv-rewriter is really a demodulator rewriter and does not reference ufbv
• e455897 fix #6476
• 79e6d4e tune and debug elim-unconstrained (v2 - for simplifiers infrastructure)
• 59fa896 minor code cleanup
• 3ebbb84 fix perf bugs in new value propagation
• 758c3b2 fix filtering for recursive functions
• cf7bba6 use ast_manager as an attribute
• 5073959 add macro attribute
• 54a8d65 move flushes in display_statistics (#6472)
• a96b7d2 remove incorrect check for quantifier
• e5984dd add cnf/nnf simplifier
• e3e2c21 Create cnf_nnf.h
• 847aec1 update dependencies
• 529f116 disable new code until pre-condition gets fixed
• 147fb0d fix tptp5 build
• 30c9cda increment generation for literals created during E-matching
• f24ecde wip - fixes to simplifiers
• cfc8e19 add more simplifiers, fix model reconstruction order for elim_unconstrained
• edb0fc3 rewrite some simplifiers
• 23c53c6 fix build
• c1ff3d3 wip - adding quasi macro detection
• 7b9dfb8 update dependencies for python build
• b084821 wip - dependent expr simpliifer
• bec3acd consolidate freeze functionality into dependent_expr_state
• 73a652c some fixes to backtracking restore points in new solver
• dd1ca8f move qhead to attribute on the state instead of the simplifier,
• ac02393 introduce sat-smt-solver
• 82d9e4a update goal2sat interface to use explicit initialization
• 500626e add sat-smt-preprocess module
• 85f9c7e replace restore_size_trail by more generic restore_vector
• 6454014 enable incrementality for model reconstruction
• 4e9f21c add rewriter and seq simplifiers
• a152f9c port bit-blaster to simplifiers
• f0570fb remove tactic exception dependency
• e95b0bd remove include of tactical
• 8184e7f keep track of qhead
• 5af6e1a make max_bv_sharing a simplifier
• db74e23 make card2bv a simplifier
• cb789f6 add arithmetical macros
• eb812e4 cleanup
• b0247d8 add exception handling for rewriter exceptions
• 1815812 fix typo in name of tactic
• a64c7c5 add incremental version of value propagate
• decb3d3 stashed header file
• 3479129 remove unused structs
• caf204a hoist macro-replacer as shared utility, update eliminate-predicates and model reconstruction
• 5fe2ff8 change functionality to not track ite terms for congruence closure
• 15dc7b7 Move merge_tf handling to euf_internalize
• eceeb29 fix #6457
• 4ac5e51 #6429
• f87e187 #6429
• 0a671f2 fix #6464
• 0a28bac remove debug out
• 9a2693b tune euf-completion
• 22353c2 new core perf - add merge_tf and enable_cgc distinction
• 11b712f switch to new configuration convention in solver object
• 6188c53 add logging of propagations to smt core
• 5374142 continue updates for adding proof-log to smt core
• c7781f3 move parameter sat.smt.proof to solver.proof.log
• cd0d52a using C++11 features to simplify for-loops
• 5c5673b make sure parser context within solver object has its parameters updated
• 477b902 fix #6460: crash in mk_to_ieee_bv_i
• 0445d6f FPA->BV fix unused vars
• b9f3428 generalize macro head detection and elaboration
• fcaa85d #6456 - elaborate on error message
• 86f3702 prevent re-declaration of enumeration sort names
• c3c45f4 add some comments to elim_predicates
• 251d49d remove outdated comment
• 3f10933 remove VERBOSE 0
• 7711576 new simplifier/tactic
• d735faa add isolated hide/add model converter functions
• a81a5ec add virtual function requirement to dependent_expr_state
• dcc995f code simplification
• 41b40c3 remove dead code
• c2e9016 display model-add parameters in correct order
• ba68652 add destructive equality resolution to existentials
• 7da91f4 allow printing declarations with reverse variable order
• 59b7845 reset visited (fast mark) to not clash with occurs
• 6662afd perf improvements to solve-eqs and euf-completion
• 2c77999 wip - tuning and fixes to euf-completion
• 98fc8c9 add shortcut to equality mk utility
• 55ab777 fix perf bug in new solve_eqs.
• d70dbda wip euf-completion - debugging
• 255414f fix regression crash
• 9845c33 add shortcuts in rewriter, eliminate redundancies in dependent_expr tactic
• bfae8b2 set flat_and_or to false in bv rewriter
• 041b5f9 rename away solve_eqs2 to solve_eqs
• 48c0f86 euf-completion bug fix, streamline name to solve_eqs
• 3eeb59d fix #6451 missing occurrence marking when there is an unsafe equality already
• 95e07ff disable unsound context equality solving
• 6297c00 remove legacy solve_eqs_tactic entirely
• 3f2bbe5 harness del_object #6452
• 3d2bf13 streamline statistics, fix bug in updating goals
• ce6cfea fix bug in euf-completion relating to missed normalization
• 3fa81d6 bug fixes to elim-uncnstr2 tactic
• 38cde14 wip missing updates
• 196788a bug fix for equality solving
• ce76e31 streamlining expr-inverter code
• 3d570aa add missing process_eq
• 0b83732 missing override specifier
• 343603f fix build
• e33e662 propagate values should not flatten and/or
• f4e17ec add logging and diagnostics
• 9d09064 add comments to elim_unconstrained and remove unused function
• efbe0a6 wip - updated version of elim_uncstr_tactic
• 689af3b add comments to elim_unconstr_tactic
• 15be80c remove dependency on hash_compare
• 8da13ae add statistics to verbose output of asserted formulas
• 9a65677 fix #6446
• 4d86d73 disable also tests for Windows x86, does not work with CI pipeline
• ff68df3 update output of z3 doc
• 254f7b9 cleanup state to clear model trail during calls.
• 823cd23 building x64 windows tests during ci is too slow, skipping tests
• 3faca52 re-enable new solve_eqs with bug fixes
• 9ef78fc revert new solve-eqs
• 3a37cfc switch to solve_eqs2 tactic
• f769e2f have bool rewriter use flat_and_or, and integrate hoist rewriter
• 238ea0a add shorthands for concatentation

This list of changes was auto generated.