Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Update Z3 to 4.13.4 #205

Merged
merged 415 commits into from
Jan 1, 2025
Merged

Update Z3 to 4.13.4 #205

merged 415 commits into from
Jan 1, 2025

Conversation

jurajsic
Copy link
Member

Needed mostly for javascript bindings, see Z3Prover#7473

NikolajBjorner and others added 30 commits August 28, 2024 10:32
@NikolajBjorner
Update README.md
ea417bb
@NikolajBjorner
add back auditwheel
cd89867 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
Update azure-pipelines.yml
ea93f07
@NikolajBjorner
update nightly
c79477a 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
Update nightly.yaml
59853d0 
create build artifacts
@NikolajBjorner
Update nightly.yaml
96417d4 
disable signing options
@NikolajBjorner
wheelhouse
dcdb7c4 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
Update nightly.yaml for Azure Pipelines
84b2c21
@NikolajBjorner
update gitignore to prepare for genaiscript
46d602e 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
Z3Prover#7362
9a87bb1 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
Z3Prover#7362
01a4195 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
fix build
a1bcf13 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
revert update to vector for testing Z3Prover#6902
a3eb2ff 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@nunoplopes
replace a few old-school constructors for a 0.5% reduction in code size
ef58376 
don't waste those 128 KB!
@NikolajBjorner
Z3Prover#6902
db4176a 
See discussion under Z3Prover#6902.
Add genaiscript for commit messages for future use.
@NikolajBjorner
Add reference URL to GenAI script file for auto Git commit guide
6086a30
@NikolajBjorner
Adjust memory reallocation to consider SIZE_T_ALIGN in memory_manager
5237e7d
@rhelmot
Fix nightly (Z3Prover#7365)
0837e3b 
- add some logic to setup.py to handle cross platform tagging correctly
  this adds a dependency on setuptools>=70
- rearrange the nightly CI to use these new builds correctly
@nunoplopes
remove default destructors & some default constructors
8061765 
Another ~700 KB reduction in binary size
@NikolajBjorner
fix Z3Prover#7372
1ace3d0 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
fix Z3Prover#7372
99a9a4a 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
y
0ba306e
@NikolajBjorner
Add initial value setting for variables in Z3 API, solver, and optimi…
48712b4 
…ze modules
@NikolajBjorner
Add initial value setting API for solver and optimize contexts and up…
0f89650 
…date related function signatures
@NikolajBjorner
remove output
1c163db 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
Add command to set initial value hints for solver in various components
a3f35b6
@NikolajBjorner
Add tracking of values size in scoped_state push method in opt_context
4896edf
@NikolajBjorner
Add support for const array in all logics as per issue Z3Prover#7383
8349ee0
@NikolajBjorner
Add override specifiers to methods in set_initial_value_cmd class for…
b99c4a4 
… clarity and consistency
@levnach
correctly process cancellation in gomory cuts
342dccd 
Signed-off-by: Lev Nachmanson <[email protected]>
dependabot bot and others added 22 commits December 2, 2024 15:39
@dependabot
Bump docker/build-push-action from 6.9.0 to 6.10.0 (Z3Prover#7469)
6ea4110 
Bumps [docker/build-push-action](https://github.com/docker/build-push-action) from 6.9.0 to 6.10.0.
- [Release notes](https://github.com/docker/build-push-action/releases)
- [Commits](docker/build-push-action@v6.9.0...v6.10.0)

---
updated-dependencies:
- dependency-name: docker/build-push-action
  dependency-type: direct:production
  update-type: version-update:semver-minor
...

Signed-off-by: dependabot[bot] <[email protected]>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
@NikolajBjorner
bugfix to elim_uncnstr to ensure nodes are created. Prepare smt_inter…
a17d4e6 
…nalizer to replay unit literals

Signed-off-by: Nikolaj Bjorner <[email protected]>
@YuantianDing
Typescript high-level api for Sets (Z3Prover#7471)
4be4067
@NikolajBjorner
v0 of edit distance repair
bcb61ee
@NikolajBjorner
partial fix to make computed term integer well-formed for solve_for f…
1ab0962 
…unctionality
@NikolajBjorner
fixes to regex membership and edit updates
4fbf54a 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@bakkot
Update emscripten (Z3Prover#7473)
e5f8327 
* fixes for newer emscripten thread handling behavior

* fix return type for async wrapper functions

* update prettier

* update typescript and fix errors

* update emscripten version in CI

* update js readme about tests
@NikolajBjorner
add another baseline heuristic for string equalities, add cases for a…
8f5658b 
…rray axioms.

Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
fix Z3Prover#7461
e8c2360 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
add repair step for str.replace
1e5c59a
@BarrensZeppelin
Add __enter__ and __exit__ methods on Optimize class (Z3Prover#7477)
b429562 
This enables the use of the with statement for the Optimize class to
concisely call push() and pop(). This works similarly to the Solver
class.
@NikolajBjorner
extract stats with finalize for parallel mode
538f74d
@NikolajBjorner
wip - incremental edit distance algorithm
31ee56c
@NikolajBjorner
add unit test for incremental equation edit distance with repair
b529a58
@NikolajBjorner
Update release.yml
e40972b 
disable publish to pypi during release dry-runs
@NikolajBjorner
Update RELEASE_NOTES.md
200ef23
@NikolajBjorner
publish pypi
a97ad76 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@NikolajBjorner
fix build flags for release.yaml
a6e59ea 
Signed-off-by: Nikolaj Bjorner <[email protected]>
@nunoplopes
reduce hash table lookups in expr_abstract in half
6f24123
@jurajsic
Merge branch 'master' into new_z3_4.13.4
d935db5
@jurajsic
turn off new rewriter rule which makes noodler not work correctly
983a432
@jurajsic
remove the file that was supposed to be removed
de1d253
@jurajsic
Copy link
Member Author

jurajsic commented Jan 1, 2025

Results:

# of formulae: 103405
--------------------------------------------------
tool                            ✅    ❌      time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ------  ----  --------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-983a432-56780ef  102585   820   8384.26   0.08   0.01   1.30  63076    39509        548   195        77        0
z3-noodler-6470df8-56780ef  102593   812   9600.06   0.09   0.01   1.48  63082    39511        548   189        75        0
cvc5-1.2.0                   99841  3564  73861.19   0.74   0.01   6.42  60931    38910          2  3553         9        0
--------------------------------------------------

image

@jurajsic jurajsic marked this pull request as ready for review January 1, 2025 16:29
@jurajsic jurajsic requested a review from vhavlena January 1, 2025 16:29
vhavlena
vhavlena approved these changes Jan 1, 2025
View reviewed changes
Copy link
Collaborator

@vhavlena vhavlena left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Great. Could you update the README file as well?

@jurajsic
Copy link
Member Author

jurajsic commented Jan 1, 2025

Great. Could you update the README file as well?

Good catch, updated.

@jurajsic jurajsic merged commit cae2540 into devel Jan 1, 2025
2 checks passed
@jurajsic jurajsic deleted the new_z3_4.13.4 branch January 1, 2025 16:43
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@vhavlena vhavlena vhavlena approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.