z3-4.12.3
4.12.3 release
Changes:
- 5e3f1d9 update release notes
- 4a9b38e clean up nla_grobner
- 84a7a79 fix #7037
- f98b42a install importlib-resources for ubuntu doc
- de75692 install importlib-resources for ubuntu doc
- f7415bb install importlib-resources for ubuntu doc
- 17913f3 remove braces
- 18f1492 Clarify optimizer guarantees (#7030)
- 6910a4e Fix to_fp_signed (#7034)
- ea3628e remove hoist functionality
See More
- bd8bed1 handle ac-op in legacy special relations procedure by adding warning
- 1b1ebaa minor simplification during internalization
- 3672538 minor simplification of terms during internalization.
- f06e07a fix cone of influence computation for terms with nested variables [ #7027 ]
- 25dd299 refine no-effect predicate to include value of ret
- 9cc2ce4 #7027
- a8f3396 #7033
- 965bee5 fix build
- 1de25ed pending files
- b22daa9 missing header
- 362d299 #7027
- ba8d8f0 Disable hoist entirely, it is bad on QF_LIA and does not help on other observed cases
- 585d027 remove assert #7032
- 331507c #7027
- 7eab26e try with missed bounds
- 5c1e7f7 fix #7029
- ed5ab54 CMake: Improve handling of git hash/describe (#7028)
- a15a7ce touch
- faf1401 Regressions reported by Guido
- 99e2794 update output
- 8a0dec1 fix build
- b52fd8d add EUF plugin framework.
- 5784c2d remove an unnecessary if
- d540d88 Add enter and exit methods to Solver class (#7025)
- 26440ed deal with ubuntu/clang warnings
- e9abdbb fix #7011
- 9efe6f6 fix regression in fix for #7006
- faa2d8a re-enable delayed literal propagation
- 2f01b5b re-enable delayed literal propagation
- 4289cfa revert some fixes to euf
- 41a3196 fix #7024
- d469c10 remove separate to_add_literal queue
- e972eb3 #6523 - contains_ptr bug regarding etable reinserts
- 1d4644f fix typos in script
- 79bbbf7 fix #7006
- 8179f8b fix #7017
- f36f21f add comments for API versions of bit-vector overflow/underflow checks for #7011
- f90b10a fix #7012
- 69f9640 fix #7018
- 3422f44 Fix syntax warning when using Python 3.12. (#7022)
- 8192b32 Bump mymindstorm/setup-emsdk from 12 to 13 (#7021)
- 9d1ceab cmake: Use
FindPython3
. (#7019) - b5e8f59 mbp: term: Fix reorder ctor warning. (#7016)
- 9d3fef3 cmake: Require cmake 3.16 or later. (#7015)
- 2354998 z3.h: Don't include
stdio.h
(#7014) - a10c93e Bump docker/build-push-action from 5.0.0 to 5.1.0 (#7008)
- 16753e4 Add accessors for RCF numeral internals (#7013)
- 9382b96 add API to access symbols associated with quantifiers
- d272acc fix crash when api_solver sets reset_tracked_assertions
- ac105b7 remove unused code
- 4350bd7 check cancel flag to avoid unsound conflicts
- 32f8705 #7001 - align is_numeral without to behavior if is_numeral with return numeral.
- 35bc522 #7003
- 924c296 add logging
- 5bec982 chores in theory_lra
- e40b8a2 household chores in legacy arithmetic solver
- 5ab1afe expose enode pp convenciences
- 1710fe4 use iterator shortcut
- a9f9d3d build fixes
- b9455c3 #6999 deal with implicit assumptions, more robust pattern matching
- 6d6d6b8 build issue
- f94a475 Qel fixes (#6999) [ #6950, #6991, #6889 ]
- 1b6c7d6 fix #6996
- 36382cc Fix memory and concurrency issues in OCaml API (#6992)
- 5b9fdcf fix #6997
- f1a39b8 add comment regarding usage model for flush_objects() to relate with pr #6992
- 3baaba5 Revert unsound NaN constraints in theory_fpa (#6993)
- c0ee4e9 pip install importlib resources
- 1ce95d3 pip install importlib resources
- 37b283f use python3 in nightly
- 7ed27a1 prepare release script
- ad2107f fix #6978
- 4406011 fix #6984
- 3c2e97d fix #6988
- c2610cb #6523
- 8a4e857 #6523
- 3de5af3 fix bug in bound simplification in Gomory for mixed integer linear cuts, enable fixed variable redution after bugfix, add notes that rewriting bounds does not work
- aa9c791 fixed possible undefined variable assigment (#6985)
- 0556059 change to expr_ref to allow trying simplification
- bd4d580 fix #6986
- e6385f8 disable bound validation in debug mode
- 3d99ed9 Gomory cut / branch and bound improvements
- 9f0b3cd Add utility to expand sub-terms
- fb95760 remove template
- 77dab53 track number of Gomory cuts
- 2d1f4d5 remove verbose logging
- e86eae2 #6523 and other heap-use-after-free error
- eed02b6 improved logging, use C++11 for loops instead of iterators
- 14312ef remove some warnings with clang
- 08d3a82 simplify the jump on entering
- bdf1fcf remove an assert
- ca6cb0a add changes in lp with validate_bound and maximize_term
- ebd4d1a WARNINGS_AS_ERRORS is ON/OFF, not TRUE/FALSE (#6979)
- 49a0719 remove temporary algebraic numbers from upper layers, move to owner module
- ea915e5 #6971
- 3af2b36 Add Z3_solver_interrupt to OCaml API (#6976)
- 91c2139 just use std::string
- fe6f38a #6951, fix build
- c82b7dd Merge branch 'master' of https://github.com/z3prover/z3
- f97dd34 tests
- 996b844 Fixed parsing of | and \ (#6975)
- 938a89e prepare for local version of Gomory cuts
- 160971d fix #6969, again
- a957a56 remove experiment with theory lemmas
- 3726960 fix #6969
- 589024a fix #6969
- 9d57bdd Assorted fixes for floats (#6968)
- bd8e5ee add simplification experiment (disabled) for tracking, some reshuffling of equation/fixed_equation structs
- e7c17e6 Fixed next_split call in pop (#6966)
- 52d16a1 deal with non-termination in new arithmetic solver
- f6c9ead #6964
- 93427f1 regression test 2447
- 0b8d7b7 useful string rewrites
- 5622fd1 initialize delay bound
- 76f9e1d fix build
- 702744f fix build
- 4434cee merge
- 20c5404 use cone of influence reduction before calling nlsat.
- e2db2b8 add hook for in-processing simplification for NLA
- 6ba1515 Merge branch 'master' of https://github.com/z3prover/z3
- 55775bd incremnet log level for debug output on cancelation
- 236afeb docs: More intra-doc linking, bit of formatting. (#6963)
- 7b49054 add missing simplification; handle nit #6952
- 0859be5 #6953
- d5fe4b0 Update script to use importlib_resources (#6949)
- f07c46a Bump actions/setup-node from 3 to 4 (#6961)
- 8b04049 Bump @babel/traverse from 7.19.4 to 7.23.2 in /src/api/js (#6954)
- aa70316 Update README.md (#6960)
- 8fac89c enable more simplification in case inequality triggers a change.
- 4e21e12 update add_lemmas to use check-feasible
- c9d298e enable propagate-linear-equations and extend to monomials
- 53ce18e update backoff for bounded_nla
- 97058b0 allow for propagations the trigger make-feasible check
- 8c00181 fix #6955
- 11ab583 fix #6956
- 37fe9cc add Horner saturation to Grobner conflict detection
- 0a1cc4c fix exception safety in pdd-solver
- 3fa6777 fix exception safety in pdd-solver
- c9c5dbc #6523
- f678861 fix #6947
- ba881d9 add facility to experiment with nla justified conflicts from Grobner equations
- 18fc691 add facility to experiment with nla justified conflicts from Grobner equations
- bdac865 add facility to check for missing propagations
- cafe3ac delay detach
- 891ab8b #6523
- 6553382 remove extra assume-eqs
- b2efa59 #6523
- 41b1f47 #6523
- 5942dc2 #6523
- 5619ed0 resurrect old bounds propagation
- a39d4ad build fixes
- 47f1c86 fix regression
- d44d78f remove temporary configuration parameter used for testing
- 08af965 updates to monomial bounds
- ba6c23b bug fix #6934 (#6940)
- fcb03aa minor code simplification
- 0118846 build
- 960a024 fix build
- 6445d01 normalize newlines for if
- d04807e merge
- 338d7b3 remove unused variables
- f3e9712 formatting
- e8e636c fix #6936
- 7afa4d0 Merge pull request #6938 from Z3Prover/uprop
- 180ab72 fix a bug in unit nl prop
- adbee0c fix #6937
- 267e9e8 #6935
- 4a87096 add code to enable unit propagation of bounds
- 1bdf66b move initialization to header file
- 75e29b2 Merge pull request #6905 from Z3Prover/unit_prop_on_monomials
- 1ba0f5a cosmetic changes
- 3aac528 add a comment
- 54f7aac column value is not necessarily at bounds
- 4c228fb Merge branch 'master' into unit_prop_on_monomials
- a94a754 fixin nla_solver_test.cpp
- f847d03 use the simple version of move_non_basic_column_to_bounds
- 19e9212 increase wasm stack size (#6931)
- 23de805 Add RCF functions to OCaml API (#6932)
- bf3817e restore move_non_basic_to_bounds
- b61f4ac merge changes from master
- b0df74c #6930
- 45c0ed1 remove unnecessery call
- edd1761 restore the scheme of m_columns_with_changed_bounds
- a88aa7f debug new propagation scheme
- 00ba064 ensure bounds propagation on changed columns after nla propagation
- 4133a1c Fix UP registration in final callback (#6929)
- 7de06c4 merging master to unit_prop_on_monomials
- a297a2b fixes in lar_solver around nl unit propagation
- ab8fe19 fix case for 0 multiplier in monomial_bounds
- 50654f1 add theory propagation to linear monomial propagation
- 702322a change the order of lp and nlp propagation
- b64fdef better tracking changinc rows and monomials
- f30a2c1 propagate only one non-fixed monomial intrernally
- ddcd1ee non-fixed term should have bound 0
- 65e59e3 sketch of internal propagation
- 7207f0f sketch of internal propagation
- 29b5c47 track changed monics efficiently
- 9033b82 debug output with the variable that is fixed and its value
- 42767b9 Merge branch 'master' into unit_prop_on_monomials
- 2297b03 re-introduce simple implementation of linear monomial propagation for evaluation
- 6559e5f port over std_vector and std-allocator functionality from monomial propagation branch
- aaa5873 add propagation flag to monic and method for updating it to emonics. This replaces the bool-vector tracking for propagation and internalizes it to the emonics class
- 4b85a10 Merge branch 'master' into unit_prop_on_monomials
- 9c63ea3 port over cosmetics from unit_prop_on_monomials branch
- 94eb101 Merge branch 'master' into unit_prop_on_monomials
- 36566d6 port over moving m_nla_lemmas into nla_core from the linear monomial propagation branch
- ac6310d Merge branch 'master' into unit_prop_on_monomials
- e4e1d61 port over moving m_nla_lemmas into nla_core from the linear monomial propagation branch
- e8fcc87 Merge branch 'master' into unit_prop_on_monomials
- ec2937e port over moving m_nla_lemmas into nla_core from the linear monomial propagation branch
- 8d2b65b add options to allow testing the effect of non-linear hammers
- 368fe80 fix the build
- 6ff4856 throttle monomial unit prop and and nl params
- 896aba3 move monomial propagation from theory_lra to nla_solver
- d2c0f7d fix test build
- 0a1ade6 move m_nla_lemma_vector to be internal to nla_core
- 26a9b77 clean m_nla_lemma_vector in nla_solver
- 029d726 minor code simplification
- 87a839c fixup unit test for added argument to constructor of nla_solver
- 010a994 Merge branch 'master' of https://github.com/z3prover/z3 into unit_prop_on_monomials
- db097ba use format from unit_prop_on_monomials branch
- 3433366 Merge branch 'unit_prop_on_monomials' of https://github.com/z3prover/z3 into unit_prop_on_monomials
- 85eacf9 merge with master
- 61319ff cache is_shared information in the enode
- a3e2e68 Update theory_lra.cpp
- acad9fa Update smt_context.cpp
- eea9c0b fix #6914
- 30d1800 #6916
- 421fe94 rmove debug out
- 886d3f4 indentation
- eac54ba indentation
- 940775d indentation
- caa929f do not use lemmase in monomial propagation
- 5d8779b Merge branch 'master' into unit_prop_on_monomials
- eff3f5f port bug fixes from unit prop branch
- 576309a Revert "reject rows with columns with big numbers for lp bound propagation"
- c0b55d1 reject rows with columns with big numbers for lp bound propagation
- f423642 try the lemma scheme
- e31cecf transfer propagate monomial bounds to nla_solver
- 536930b make m_ibounds inside of lp_bound_propagator
This list of changes was auto generated.