4.14.0 release
Changes:
- 3c47fd9 bump timeout for jobs
- 2e008a9 Update release.yml for Azure Pipelines
- d1575af Update nightly.yaml for Azure Pipelines
- 96e3233 Update azure-pipelines.yml for Azure Pipelines
- 813da35 fix unit test
- f8f2678 convert def into expression tree
- f977b48 adjust solve_for to handle rationals
- 528efbb fixes to failure conditions for unification
- fe27ca1 remove verbose output
- 50f9fdd Add unification based projection function
See More
- b27a2aa remove calls to removed def constructor
- a703cf8 replace model_ref by model* in tg_project,
- eee96ec bug fixes and cleanup in projection functions
- 0cf2b5f add retry, rename to optibot
- 6b9ce86 fixes to opt-tool
- 719ea6a added ai scripts
- 9fad15e adding mergeopt
- 01ba749 focused query to optimize
- a003139 update description
- 45f3ea3 add treesitter functionality
- bedc95c use static_cast to avoid the warnings
- e6a089e Fix build when Z3_API macro is non-empty (#7553)
- d10efa6 stub for treesitter
- 5c18ce8 genai testing
- 4e51af1 update instructions
- 94d3c59 make sure ackermann works with arrays that have more than one argument
- a3739aa add mycop in addition to code complete
- 9ea921b update spacer projection for arrays to allow ackerman reduction for non-integer arrays
- e920291 fixing the default parameters of dio and rename m_gomory_cuts to m_cuts
- 957b177 set arith.lp.dio_cuts_enable_gomory to False by default
- 5ec10e0 address the review
- 8a9edd1 fix the test build
- 79e3f8a disabling dio handler by default, and fix a print out
- 2131e9b more accurate work with Markovich number
- bdb8f54 Revert "revert the term sorting"
- 5ebee24 revert the term sorting
- f2c1fd4 try markovich number
- cec8dc2 try markovich number
- 3f2d2e8 test
- b6701d5 try another sort in tightening
- 5b0b224 try sorting terms before tightening
- dcd5783 remove the fresh definition when removing its column
- 17d68c1 comment change
- d90b94d stricter is_in_sync paying attenion to m_row2fresh_defs
- 134bed8 throttle the branching in dio
- bd8cf29 ignore large changed_columns
- 3ac11cd fix assert
- cf4e402 avoid usisg indexed_vector for term operations
- 440d78f disallow duplicates in a queue
- 7e02dfe add stats on m_dio_branching_conflicts
- 0bf3ca8 call normalize_e_by_gcd() only when moving an entry from F to S
- 9953856 rebase with master
- a19e109 make dio less aggressive, allow other cuts
- fee7078 register m_added_terms in m_changed_terms
- 21f67ef out of bounds fixes
- 3b3d8ce use m_chandedNterms to tighten terms
- 65bdd58 remove struct entry
- a9098a5 optimise l terms addition
- 3e7e903 use the trail to undo add_term
- 9c51001 fix the debug build
- 058b9e4 optimise rewrite_eqs to avoid fresh variables
- ed3df33 make rewrite_eq boolean, and relax an ASSERT
- ca7c128 clean up fresh definitions on a pop
- b027761 debug dio
- bb869fd don't store fresh definitions in m_e_matrix
- e5ffc3c cleanup
- d7de7eb remove recalculated entries from S
- ef55de1 fix out of bounds bug
- 3990df6 substitute variables with a queue on the recalculated entries
- 78d91f3 simplify dio handler by using bijection m_k2s
- 33f5e30 use entry_status for FRESH entries
- 0e71adf fix some warnings
- 7bba8bc fix some warnings
- abac52e remove var_register_dio.h
- 89eec4c test dio
- 5a72117 debug dio
- 0027ae2 bug fixes
- 5158797 refine trail iterations with lar.m_terms
- 9a9ccf1 introdure lar_term.ext_coeffs(), dio passes some tests
- 083926c debug dio
- a0ece6d cleanup
- ceeece6 debug dio
- ac5c50f fix ubuntu build in dio
- c1ece49 track changed columns in dio\
- 008e922 use std_vector more and getting NOT_IMPLEMENTING in C:\dev\z3\src\math\lp\dioph_eq.cpp
- 57b665d work on incremental dio
- 28556ce cleanup
- 862dc91 work on incremental dio
- fd3bd08 remove some warnings
- 9a96aa9 test
- bef313f test
- 7ecac27 fix a bug in dio
- b0383da fix a bug in dio
- 7fe703e simplify column
- 8d74786 cosmetics
- deac00a persist dio handler
- 2c8a6f8 change int_solver to call find_cube and hnf_cut, conditionally
- 39da4f6 remove an assert
- 28d4178 fix the build
- 397fdf6 fix the build
- 63980f3 fixes in dio branching
- 6bc7662 passes z3test
- 1741855 collect the explanation correctly
- bc0fdfe remove dead code
- c300843 cancel bugs fixes
- e4f3b57 solving regressions/smt2/b1.smt2
- 71c4339 work on incremental version
- d68ebee use var_register in dioph_eq
- 480c48f document dioph_eq
- 02a509b remove a global debug variable
- acc2149 remove redundant m_row_index from entry
- d439073 take dependencies from open_ml
- 3fcc5a2 fixes in tigthening
- 9164672 check feasibility immediately after tightening a bound
- 58e5735 implement explain()
- b30272f add missing explanations
- e0a08f1 fix the build
- 30f5599 use fixed vars to explain tightening
- 36293ac test that pivoting is correct in dioph_eq.cpp
- 0db0efc print output file name
- 8904a50 fix the build
- 5f5f1d4 init m_e_matrix on terms instead of the tableau
- 392c24a throttle dioph equalities
- 128d5b4 change type of m_e_matrix
- a63e0d8 add a template instantiotion
- 0f03e75 handle empty rows in m_e_matrix
- ba7268c vector access bugs
- 66f8820 bug fixes with tableau
- 62ea6fb bug fixes
- ac49198 bug fixes
- 536c51f debug dio with static matrix
- 28fbc81 unifying vectors into eprime_entry
- 42bdc89 dio with static_matrix initial setup
- 9e8b17b do not use conflicts with fresh vars to create branches
- eaf2f7f remove disabling return
- 8aeba62 remove more warnings
- 552a504 remove a warning
- 4bd8158 fix ubuntu's build
- ea50208 prepare using fresh vars in cuts
- 06faf03 use cuts from proofs, remove gcc warnings
- 2ebb957 enable cuts from proofs
- 44fd0e4 fixes in dio
- a8e667c do not eliminate fresh variables when tightening
- 52b0b8d fixed dio
- 5ac428f comment out global_max_change
- 89e4f59 debug dio
- 798f0e2 test tightening with S
- 193116b handle sat with tightening
- b1be8c0 cosmetics
- 5db46c1 use u_dependency in eprime_pair
- 1408fe6 work on tighten_with_S
- f0b5cd1 remove a throw
- be8f3e9 bug fix
- 0b1e923 small optimization
- 66c6bad optimize dio changes
- 18c75e6 less eager dio
- bbeecc6 fix the build
- 3d5ee82 handle zero rows correctly
- 78a58b0 dio passes regression\smt2 tests with limited functionality
- 245d448 fix term_o init
- a796d48 debug dio
- df18885 debug dio
- cd13890 fix in substitution of fresh variables, clean column.h
- f5e646c bug fix in init and getting explanations
- 59e2dab create a conflict explanation
- 52653e6 a version with less pointers: got a conflict
- 5a36e02 in the middle
- 122e013 use std::list
- 3b22d3b fix the crash
- abf29b5 crash
- a5dd59f fix the build
- a1a01b9 move some functionality from int_solver to int_solver::imp
- 8892924 fix the build
- 3d6cc64 prepare for calling diophantine equations
- 097a25e add parameter to control calling diophantine equations
- acd48b6 Fixing #7465 (#7551)
- c2b7b58 #7468 - add option (get-info :parameters) to display solver parameters that were updated globally and distinct from defaults
- 62126fd fix build warnings
- af270da Fix complete_partial_func for finite domains (#7547)
- 0919844 Fixed bug in UP (#7545)
- 17d47ca fix #7493
- 99cbfa7 Add a sharp throttle to lia2card tactic to control overhead in default tactic mode
- fd2a8a5 disable small clause generation for propagation
- 0ef2698 release
- aea4490 throttle overhead with lia2card
- d465bdb include extensionality constraints for arrays
- d6dcc51 rehearse release
- edc5679 updated release notes
- 8ae24e2 update release version
- 1d622a6 Bump docker/build-push-action from 6.12.0 to 6.13.0 (#7535)
- 9557e7c Minor (#7540)
- 1ce6e66 generalize logic detection to use sub-string matching
- eb82585 increase the log level on callbacks with bit-indices that get set
- c9ac4d6 pre-flatten use list before iterating over m_unsat
- e356628 fixes based on benchmarking UFDTLIA/NIA/BV
- f1e0950 fix several crashes exposed by QF_UFDTNIA benchmark sets
- bfe4673 this check is not an invariant in the first place
- 51357f6 Add selective filter on Ackerman axioms
- c2a0919 Removed no progress case in seq-sls (#7537)
- 6d3cfb6 add eval1 functionality for replace_all
- ab43d2d fix semantics of check-int64 div operation to align with smtlib semantics
- 30d72f7 remove verbose output of overflow
- 3379155 add check for root literal assignment
- fe5d17d handle exception internally, avoid passing rationals to integer operations
- 5b175c1 fix crashes in sls_datatype
- fe713eb disable quadratic moves for non-integers as sqrt isn't currently defined for rationals
- d843081 fix mixup between sync and sls managed variables
- fa60545 fix crash reported by Nikhil on F* due to unhandled exception while using the rewriter during search
- 5c2a9d9 fix pickup of new constraints
- 1676378 skip last power
- 8a7d971 Update sls_bv_lookahead.h
- 2ebc647 skip update stack items that are not Bool/bv
- 632e2b5 fix initialization of mod terms
- fd5f5fe add cmake option to turn on asan
- a8279dd reset kv map consistently with egraph
- 57a5474 revert flat default
- 72ae161 compress store array before model-eval rewriter sees it
- fe1622b sls fixes for ABV. Axiomatization required as saturation can produce conflicts by congruence closure
- 2050fc3 Preserve fingerprint in trace (#7534)
- 2d8f024 Mark fixed_eq literals as relevant (#7533)
- 63f9fda fix build
- 15ee879 fix #7532
- b6e7b80 updates to handle bugs exposed by qf-abv for local search
- 7ffed86 fix bug with handling theory symbols of bit-vector type. Happens for data-type accessors. Reported by Clemens Eisenhofer
- 09e84e0 fix crash when accessing bool-info vars, reported by Clemens Eisenhofer
- f574950 fix #7521 (#7531)
- 5634dc5 fix model construction bug: ignore non-relevant expressions when building model
- d3bf25c throttle value smt -> sls
- d4100fc fixes to update propagation.
- 04d0e94 set log level of revert repair down to 3
- 55fc57b relax out of range restrictions to handle large intervals
- 4f2272d increase log level for 'set value failed'
- 7fb6497 fix return value when in external mode bool-flip
- d4f2de7 add smt_params dependency to sls in cmakelists
- 12e8082 consolidate functionality
- a701057 align use_list with number of variables during flatten, push clause and bool_vars_of addition into clause and atom creation time.
- 7fc59b6 add recursive updates to lookahead
- 57cb988 fix gcc build
- 60fb53a fix debug build
- ecc302b fix trace build
- d805322 create separate file for expression based lookahead solver
- f6e7dcf Fix crash exposed in QF_UFNIA
- 9e8dd68 disable lookahead on compound values (fixes bug reported by Clemens), bail to rationals when there are reals.
- 053349c remove incorrect calls to VERIFY in array solver
- 0e8969c deal with compiler warnings and include value exchange prior to final check.
- ce615ee avoid repeated clauses during scoring function
- b149d1f count every lookahead as activity
- 4d33f44 enable value import in parallel mode
- e32f685 disable backoff on smt->sls value export
- beb9d2e update restart next
This list of changes was auto generated.