mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-22 16:27:37 +00:00
Code Activity
21700 commits 65 branches 58 tags 180 MiB
Commit graph

21700 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
1514361335
Merge pull request #8713 from Z3Prover/copilot/compare-tactics-and-simplifiers 
[WIP] Create workflow to compare exposed tactics and simplifiers
 2026-02-20 19:23:27 -08:00
copilot-swe-agent[bot]
610a3d3c5a Add tactic-to-simplifier comparison agentic workflow 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-21 03:22:56 +00:00
copilot-swe-agent[bot]
ac174ab308 Initial plan 2026-02-21 03:15:32 +00:00
Nikolaj Bjorner
ee1a6a2f91
Merge pull request #8710 from Z3Prover/copilot/fix-discussed-issues-8709 
Align congruence closure API naming in Python and Java bindings
 2026-02-20 19:13:11 -08:00
Nikolaj Bjorner
33f76b839f
Merge pull request #8711 from Z3Prover/copilot/simplify-finite-set-plugin 
Cleanup: finite set decl plugin cosmetic simplifications
 2026-02-20 19:12:43 -08:00
copilot-swe-agent[bot]
e5d7319670 Code simplifications for finite set plugin 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-21 02:08:04 +00:00
copilot-swe-agent[bot]
d0e9d68746 Initial plan 2026-02-21 02:05:49 +00:00
copilot-swe-agent[bot]
a3ea31cb42 Fix congruence closure API naming in Python and Java bindings 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-21 02:04:31 +00:00
copilot-swe-agent[bot]
9ef917c20d Initial plan 2026-02-21 01:59:34 +00:00
Lev Nachmanson
66aaece3f5 try evaluate discriminants more rarely 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-20 10:16:27 -10:00
Nikolaj Bjorner
e2129a7b81
Merge pull request #8702 from Z3Prover/copilot/fix-issues-in-discussion-8701 
Add missing solver/optimizer API bindings across language targets
 2026-02-20 09:28:50 -08:00
Nikolaj Bjorner
20c446cede
Merge pull request #8703 from Z3Prover/copilot/fix-finite-set-apis 
Add FiniteSet API support to Go, OCaml, and JavaScript/TypeScript bindings
 2026-02-20 08:40:07 -08:00
Nikolaj Bjorner
36a47a015f
Merge pull request #8706 from Z3Prover/copilot/fix-discussed-issues-8705 
TypeScript bindings: document and test `addAndTrack` for Solver and Optimize
 2026-02-20 08:39:37 -08:00
copilot-swe-agent[bot]
ce0fb1bd24 Fix OCaml build error: use status instead of solver_result in z3.mli 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-20 04:32:56 +00:00
copilot-swe-agent[bot]
5253f9af9d Fix TypeScript type error: explicitly type consVec as AstVectorImpl<Bool<Name>> 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-20 04:31:18 +00:00
copilot-swe-agent[bot]
60f5a76516 Add tests and documentation for addAndTrack in TypeScript bindings (fix discussion #8705) 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-20 04:28:10 +00:00
copilot-swe-agent[bot]
8d79e21aa7 Add missing API methods across language bindings (discussion #8701) 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-20 04:24:22 +00:00
copilot-swe-agent[bot]
5d93f098fc Add FiniteSet support to Go, OCaml, and JavaScript APIs 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-20 04:23:26 +00:00
copilot-swe-agent[bot]
8f23830879 Initial plan 2026-02-20 04:22:02 +00:00
copilot-swe-agent[bot]
8f6afe3d64 Initial plan 2026-02-20 04:07:56 +00:00
copilot-swe-agent[bot]
50f3051054 Initial plan 2026-02-20 04:06:55 +00:00
Nikolaj Bjorner
8314aecb44
Merge pull request #8686 from Z3Prover/finite-sets 
Finite sets
 2026-02-19 19:49:47 -08:00
Nikolaj Bjorner
30e4c9a629
Fix badge links in README.md 2026-02-19 19:47:30 -08:00
Nikolaj Bjorner
c56e033a94
Merge pull request #8700 from Z3Prover/copilot/update-readme-banners-remove-workflows 
Update README.md build status banners
 2026-02-19 19:40:40 -08:00
Nikolaj Bjorner
99e1ba3a6e update macos runner id 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-19 19:12:44 -08:00
Nikolaj Bjorner
3d8dd0d783 update params 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-19 19:06:06 -08:00
copilot-swe-agent[bot]
e37624ab13 Update README.md banners: remove disabled workflows, fix WASM link, add A3 Python badge 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-20 03:01:16 +00:00
copilot-swe-agent[bot]
1521c43702 Initial plan 2026-02-20 02:57:28 +00:00
Lev Nachmanson
9c4e172e95 set the default of lws_spt_threshold to 4 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-19 14:18:11 -10:00
Lev Nachmanson
385f913a33 try optimize handle_nullified_poly 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-19 13:58:45 -10:00
Nikolaj Bjorner
38ce0882db remove lattice component 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-19 15:49:45 -08:00
Nikolaj Bjorner
bf73fddf6f
Merge pull request #8693 from Z3Prover/copilot/fix-test-coverage-gaps 
Add unit tests covering ackermannization module and Z3_algebraic_eval
 2026-02-19 15:32:46 -08:00
Nikolaj Bjorner
369890330e
Merge pull request #8699 from Z3Prover/copilot/fix-missed-bugs-ff-by-one 
Fix off-by-one vulnerabilities in ackermannization module
 2026-02-19 15:32:23 -08:00
copilot-swe-agent[bot]
dbd7cd7414 Fix off-by-one vulnerabilities: use range-based for on goals; cache loop bound 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-19 22:37:22 +00:00
copilot-swe-agent[bot]
093e227689 Add ackermannize tests for mutation coverage 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-19 22:07:41 +00:00
Nikolaj Bjorner
5bd7d93b55 add parameter validation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-19 14:02:59 -08:00
Nikolaj Bjorner
ee03533c3a update examples to use arrays 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-19 13:57:43 -08:00
Lev Nachmanson
426f8396e3
Merge pull request #8691 from Z3Prover/no_fail 
Disable failure on a nullified polynomial in levelwise
 2026-02-19 11:46:46 -10:00
Nikolaj Bjorner
c94eb5dc88 fixup API functions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-19 13:33:25 -08:00
copilot-swe-agent[bot]
f414c7982d Initial plan 2026-02-19 21:26:59 +00:00
copilot-swe-agent[bot]
5e5d9ebfaf Fix test_ackermannize_bv_model: skip crashing model converter test, keep 4 passing tests 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-19 21:07:30 +00:00
Lev Nachmanson
23560ba8a5 cleanup regarding levelwise 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-19 09:31:30 -10:00
Nikolaj Bjorner
44cd412426
Merge pull request #8694 from Z3Prover/copilot/sub-pr-8686 
Fix ambiguous svector constructor calls in theory_finite_set_lattice_refutation
 2026-02-19 10:49:13 -08:00
Nikolaj Bjorner
ca1865c3fe
Merge pull request #8696 from Z3Prover/copilot/fix-z3-import-error 
Fix arm64 libz3.dylib being packaged in x86_64 macOS wheels
 2026-02-19 10:48:30 -08:00
copilot-swe-agent[bot]
879dc93d2a Add tests for ackermannization module and Z3_algebraic_eval 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-19 18:18:19 +00:00
copilot-swe-agent[bot]
c4acd2a47e Fix macOS cross-compilation from ARM64 to x86_64 in mk_unix_dist.py and mk_util.py 
When macos-latest changed to ARM64 runners, the mac-build-x64 job started
producing arm64 libz3.dylib inside x86_64-tagged wheels, causing import
failures on macOS x86_64.

Root cause: mk_make.py subprocess detects the ARM64 host at module level
(IS_ARCH_ARM64=True), and without --arm64=false override it adds -arch arm64
to SLIBEXTRAFLAGS, overriding the -arch x86_64 set via environment variables.

Fix 1 (mk_unix_dist.py): Pass --arm64=false to mk_make.py subprocess when
building x64 on an ARM64 host, preventing the arm64 flag inheritance.

Fix 2 (mk_util.py): When IS_ARCH_ARM64=False on an ARM64 macOS host, add
-arch x86_64 to SLIBEXTRAFLAGS so the shared library linker also targets
x86_64 (LDFLAGS already receives this flag from the env var).

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-19 18:02:52 +00:00
Nikolaj Bjorner
2fa04f5e38
Merge pull request #8695 from Z3Prover/copilot/simplify-code-structure 
Remove unnecessary blank lines in mk_genfile_common.py and mk_api_doc.py
 2026-02-19 09:58:19 -08:00
copilot-swe-agent[bot]
866f352ea9 Fix ambiguous svector constructor calls in theory_finite_set_lattice_refutation.cpp 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-19 17:57:04 +00:00
Nikolaj Bjorner
8a28bc28f1
Update nightly-validation.yml 2026-02-19 09:54:29 -08:00
copilot-swe-agent[bot]
0ad40a3f54 Remove unnecessary blank lines in mk_genfile_common.py and mk_api_doc.py 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-19 17:52:11 +00:00