mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-24 09:11:17 +00:00
Code Activity
21725 commits 74 branches 58 tags 181 MiB
Commit graph

21725 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
8fbc4ed26d
Merge pull request #8727 from Z3Prover/copilot/expose-max-bv-sharing-simplifier 
Expose max-bv-sharing as a registered simplifier
 2026-02-22 19:40:35 -08:00
Nikolaj Bjorner
0b5480b6c3
Merge pull request #8729 from Z3Prover/copilot/convert-bvarray2uf-to-simplifier 
Convert `bvarray2uf` tactic to a dependent_expr_simplifier
 2026-02-22 19:39:19 -08:00
Nikolaj Bjorner
69eab28550
Merge pull request #8730 from Z3Prover/copilot/convert-der-tactic-to-simplifier 
Convert `der` tactic to a `dependent_expr_simplifier`
 2026-02-22 14:04:04 -08:00
copilot-swe-agent[bot]
1d2a76d27b Delete bvarray2uf_tactic.cpp (removed from CMakeLists.txt) 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-22 08:57:39 +00:00
copilot-swe-agent[bot]
57d1667d28 Remove der_tactic.cpp from CMakeLists.txt (file was deleted) 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-22 08:47:14 +00:00
Nikolaj Bjorner
b149f27e82
Delete src/tactic/core/der_tactic.cpp 2026-02-22 00:25:24 -08:00
copilot-swe-agent[bot]
d9d712f1d0 Remove old bvarray2uf_tactic implementation; use simplifier as basis 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-22 00:43:36 +00:00
copilot-swe-agent[bot]
7c4a3b2c1b Remove old der_tactic implementation; rename mk_der2_tactic to mk_der_tactic 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-22 00:40:49 +00:00
Nikolaj Bjorner
0d553f2ce9
Merge pull request #8712 from Z3Prover/copilot/fix-soundness-issue-conversion 
Fix FPA soundness issue in incremental (push/pop) solving
 2026-02-21 16:26:23 -08:00
Nikolaj Bjorner
919cd5c86c
Merge pull request #8722 from Toby-Shi-cloud/master 
Add `parser_context` in C++ API
 2026-02-21 16:26:00 -08:00
copilot-swe-agent[bot]
0cc4afa097 Add bvarray2uf_simplifier: convert tactic to simplifier 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-21 23:50:32 +00:00
copilot-swe-agent[bot]
c78b3d872d Convert der tactic to simplifier: add der_simplifier.h and update der_tactic.h 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-21 23:49:05 +00:00
copilot-swe-agent[bot]
ce905f91c3 Register max_bv_sharing simplifier via ADD_SIMPLIFIER 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-21 23:26:47 +00:00
copilot-swe-agent[bot]
30784ecaa9 Initial plan 2026-02-21 23:26:04 +00:00
copilot-swe-agent[bot]
6bd009ed6a Initial plan 2026-02-21 23:25:53 +00:00
copilot-swe-agent[bot]
db533abed5 Initial plan 2026-02-21 23:25:31 +00:00
Toby Shi
f5fba112bc
add parser_context in c++ api 2026-02-21 17:59:44 +08:00
copilot-swe-agent[bot]
46daa160ed Fix FPA soundness issue: reset rewriter cache in pop_scope_eh (issue #8345) 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-21 03:35:47 +00:00
Nikolaj Bjorner
2382cd4e9d
Merge pull request #8715 from Z3Prover/copilot/update-workflow-schedule 
Change workflow suggestion agent from daily to weekly schedule
 2026-02-20 19:25:34 -08:00
Nikolaj Bjorner
14b88cc583
Merge pull request #8714 from Z3Prover/copilot/update-release-notes 
Add release notes for Version 4.17.0 (Python API, perf, bug fixes)
 2026-02-20 19:24:35 -08:00
copilot-swe-agent[bot]
920428f293 Change workflow suggestion agent schedule from daily to weekly 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-21 03:24:07 +00:00
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]
611cd12faa Add recommended release notes to RELEASE_NOTES.md for Version 4.17.0 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-21 03:22:07 +00:00
copilot-swe-agent[bot]
d929f85719 Initial plan 2026-02-21 03:21:27 +00:00
copilot-swe-agent[bot]
335e6f78e9 Initial plan 2026-02-21 03:20:33 +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]
b16e142127 Initial plan 2026-02-21 02:45:20 +00: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