4.15.0 release
Changes:
- 9232ef5 remove copy of LICENSE.txt - pypi doesn't take it
- 49dffae enable pypi
- b54ed38 enable pypi
- 59a7e00 disable pypi
- d4b622e update version number
- a51239c update namespace, hoist exported functions outside of embedded namespace
- 6441186 list euf dependency in api cmakefile
- eca5cd1 mark virtual methods as override
- 9a299eb move mam to euf
- 0e4c033 fix #7639
See More
- 4bedb5f fix #7638
- dd211ba filter out terms that are not solved
- f89e133 revert the behavior of add_zero_assumption (#7631)
- 6af61fa remove experiment
- b502126 fix #7634
- 24090fc move flush smc to first use
- a626cd0 flush smc before use in model construction
- 71b5e44 #7596 - flush smc before copy
- 7a30223 fix #7630
- d581dc1 #7630 propagate parameters on lazy tactics
- 322e444 Fix conversion of signed 1-bit BV to FP
- 792ffee fix latent sign bug
- fe1fff3 add scaffolding for experiments with slack
- 12ccf59 rename fields to compile on c++ platforms
- e41acd7 convert m_r_upper and m_r_lower bounds to plain vectors
- fae6094 consolidate some bounds references
- f6fbeda fix #7629
- 7641393 use inlined functions
- 5cc57b8 coalesce updates to bounds
- 579ba8b add power axioms to arith_solver
- d73d104 remove overwriting x,y,rval
- ff920ba handle root expressions, and checking exponentiation with nlsat
- 2fe2735 Replace
_DEBUGwithZ3DEBUG(#7628) - a1673f2 fallback to Gomory cuts and gcd conflicts if dio fails
- cc1bb0a remove superfluous makefile
- 17cac7d provide shortcut to command-line version to retrieve parameters
- 6e88d91 add badge for ocaml cmake
- 3761dd8 address build warning with overloaded virtual operators
- f7aec02 WIP: Migrating OCaml binding to CMake (#7254)
- ab9f330 change the default of running dio to true, and running gcd to false, remove branching in dio
- dbde713 remove testing code in is_big_term_on_no_term
- 1131d52 fix a bug in tracking the changes in dio
- d289495 allow gcd when dio ignores some terms
- 17af18f make gcd call in dio optional
- 436eefb always remove the tightened term
- dc7185d change the name of m_changed_columns to m_changed_f_columns
- 32e77d8 typo
- cb1818f reject more terms with big numbers
- 1cde40b dio_calls_period=4
- 87e2ce8 Update lp_settings.h - m_dio_calls_period = 4
- 59edb81 Update lp_settings.cpp
- 8db9f52 add parameter m_dio_calls_period
- ae97ee0 throttle dio
- 972f801 throttle dio for big numbers
- 3e49d9f reuse dio branch
- e31e981 Add an option "ctrl_c" that can be used to disable Ctrl-C signal handling (#7619)
- ed5dd26 remove non-working ts mcp server, settle with python variant
- 741cb5c minimal z3 MCP server
- f63c9e3 disable assignment for param_descrs
- 3f73c8b stab at SMTLIB REL mcp server
- 755f579 fix #7622
- 81f1091 remove unused bdd based variable elimination
- e41090d fix #7602
- 8035edb remove lp_assert
- 1510b31 fix build warnings
- 5ad79f2 Add Iterators as acceptable arguments to functions (#7620)
- 6ecc7a2 Fix a race condition in scoped_timer::finalize (#7618)
- a83efa6 spacing
- 8138829 fix #7616
- d792840 Add Z3_is_recursive_datatype_sort to the API (#7615)
- 14e2aad include LICENSE.txt in wheels (#7614) [ #7604 ]
- 0b7a81b list[ExprRef] doesn't build for python
- 2b60550 update agentz3 sample based on hugging face training/test data
- e7ff600 #7605
- a39efbb fix #7607
- 9d8291a remove type annotation Context | None to ensure Centos ARM Build pass
- f607331 type annotations across Python versions
- bd2c7aa remove downlevel version incompatible elements of typing
- 305f1e8 remove references to TypeGuard
- a5048e4 add initial sample agent use case
- 0a37194 fix #7609
- 5e10fd3 add selected type annotations to python API
- 26ab0de rename function
- eb4e28d [z3.py] Fix incorrect call to _get_ctx in SeqMapI (#7610)
- 8d81a2d Note that Z3_get_numeral_small is essentially redundant (#7599)
- 63ad283 Add Z3_get_array_arity (#7598)
- 934455a Remove vestiges of old ml api (#7597)
- e4897ff replace Exists by ForAll in the mathematica lemmas
- 39df899 enable shorterter mathematica printouts in nlsat
- e86a918 turn on ite simplification by default
- 8368094 fix indentation
- 4fd6ba4 replace costly ite reduction by disjointnes check
- 392bc16 optimize bool rewriter
- 2971250 add option to rewrite ite value trees
- e92ccdd change line breaks
- 17bd02d change a comment
- 8bbe752 remove dead code
- 7e4a1f2 fix crash in elim_constr2
- 93cf989 household chores - move to iterators
- dee3cf8 remove an unused field
- 9302a02 reintroduce m_var_register, and avoid modulo gcd in normalize conflicts
- 9a62ed5 added some comments
- c634701 formatting
- f073da9 cleaning up the inner tightening code
- 8c96178 avoid the variable mapping to m_ematrix and suppressing redundand constraints
- 29c5c20 use more descriptive functions than casting comparisons
- 7fb40e8 tidy
- a41bd38 use pattern of matching with undef instead of matching with conflict to reduce assumptions on procedure contracts
- 676a536 fix a print out
- d507d0f attempt to use the gcd of fixed vars
- f181e3a add comment on derivation of bound
- dd19b38 detect more m_terms_to_tighten
- 307af0f remove an unused field
- fc1c8c4 add public access to bijection key_val iterator
- 8b5510b nit
- 7577f6f neatify loops
- f091b6f remove 'unsat' move, we already have 'conflict'. Add display for cancelled
- 1af2474 code review updates, tidy pretty printer for column info
- 3202808 fix bug introduced while absstracting m_conflict_index
- f3b34fd isolate m_conflict_index functionality
- ff5ae4d add systematic way to combine lia_move results
- 00277ba nits
- 488c74d print also column values
- 22cfab3 remove term sorting by the span
- 12203fc sort terms by weight for tightening
- 0a3c118 more aggressive term tightening
- 50418fa try another sorting of terms to tighten
- ec7c615 separate m_changed_terms and m_terms_to_tighten in indexed_uint_sets
- 7c12a02 detect non integral terms in dio
- a62d664 testing! disable gomory cut in int_solver
- 5e2d000 optimize entrry recalculation
- ecfbdbb allow bounds tightening on fixed columns
- f501aea add comments and renaming
- a522e81 profile and remove dead code from dioph_eq.cpp
- 6f7b749 improved dio handler
- 30021dd fix #7590 logic alphabet soup
- 03f18c1 some more copilot aided updated
- 2ecf6dc add code for free bounds axiom, but keep it disabled
- 99ec42c additional simplifications to seq
- c1719e9 Fix : typo-in-simplify-tactic (#7587)
- 2e2a2e2 use iterators on goal and other refactoring
- eb97fcc mild refactoring
- 0e881e7 fix #7584
- 7c226f4 fix #4117
- 382bd05 gitignore
- 13c098f better equality solving pre-processing with bv
- d980ac9 fix #7582
- fa5a50c fix #7295
- 021e855 update minor version to 14.2
This list of changes was auto generated.