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

20815 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
copilot-swe-agent[bot]
d7aa454760 Initial plan 2026-02-19 17:50:23 +00:00
Nikolaj Bjorner
9f91380b7d next release notes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 21:30:08 -08:00
Nikolaj Bjorner
33d4d38dee update version 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:37:48 -08:00
Nikolaj Bjorner
ddb49568d3
Merge pull request #8683 from Z3Prover/copilot/fix-build-error-z3 
Fix OCaml binding call to solver_get_levels
 2026-02-18 14:57:51 -08:00
copilot-swe-agent[bot]
366b197c2b Fix OCaml build error in solver_get_levels 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 22:21:58 +00:00
copilot-swe-agent[bot]
b384f74574 Initial plan 2026-02-18 22:12:24 +00:00
Nikolaj Bjorner
02b6aeb097
Merge pull request #8681 from Z3Prover/copilot/fix-discussion-issues-8680 
Add missing solver and model APIs to Go and OCaml bindings
 2026-02-18 13:26:42 -08:00
Nikolaj Bjorner
6c02a3b6bb
Delete examples/go/test_new_api_additions.go 2026-02-18 13:25:52 -08:00
Nikolaj Bjorner
9d3cc4afc9 remove deprecated workflows 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 12:00:18 -08:00
Nikolaj Bjorner
672d243f0f
Merge pull request #8682 from Z3Prover/copilot/fix-docs-and-update-script 
Add Go API link to documentation index and prevent content overwrite
 2026-02-18 11:56:18 -08:00
copilot-swe-agent[bot]
9499b1089c Add --go flag to mk_api_doc.py calls and remove go directory overwrite code 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 19:30:07 +00:00
copilot-swe-agent[bot]
4335b9f545 Initial plan 2026-02-18 19:27:55 +00:00
copilot-swe-agent[bot]
c74acb59a9 Add test for new Go API methods 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 17:45:38 +00:00
copilot-swe-agent[bot]
ac10af417a Add missing API methods to Go and OCaml bindings 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 17:28:12 +00:00
copilot-swe-agent[bot]
f4606b1f2d Initial plan 2026-02-18 17:23:26 +00:00
Nikolaj Bjorner
fa8d60c94f
Merge pull request #8677 from Z3Prover/copilot/fix-code-quality-issues 
Fix A3 static analysis findings: replace assertions with proper error handling
 2026-02-18 08:44:29 -08:00
Nikolaj Bjorner
c9720aa330 fixup docs.ytml 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 08:36:03 -08:00
Nikolaj Bjorner
a077371520 update go doc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 08:27:47 -08:00
Nikolaj Bjorner
82b34e319b update a3-python to fix issues 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 08:16:56 -08:00
Nikolaj Bjorner
136bf0b5eb
Update documentation generation to include Go 2026-02-17 18:36:04 -08:00
copilot-swe-agent[bot]
7e8fc4fdff Fix indentation in commented-out code section 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 00:46:01 +00:00
copilot-swe-agent[bot]
064122a123 Improve documentation for RatVal division by zero handling 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 00:44:40 +00:00
copilot-swe-agent[bot]
ae328dc006 Fix Priority 1 ASSERT_FAIL bugs - replace assertions with proper error handling 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 00:42:55 +00:00
copilot-swe-agent[bot]
ac19bdb9a7 Initial plan 2026-02-18 00:39:14 +00:00
Nikolaj Bjorner
abb83018df new repository agnostic workflow 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-17 16:27:08 -08:00
Nikolaj Bjorner
5a91b0e6e9 recompile workflows 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-17 15:45:34 -08:00
Nikolaj Bjorner
6ef869bf8b
Remove checkout steps from A3 Python workflow 
Removed steps for checking out Python source files.
 2026-02-17 15:39:23 -08:00
Nikolaj Bjorner
ad5e805ec9
Remove checkout steps from A3 Python workflow 
Removed steps for checking out Python source files.
 2026-02-17 15:39:01 -08:00
Nikolaj Bjorner
f561b5a68d
Merge pull request #8673 from Z3Prover/copilot/upgrade-agentic-workflows 
Upgrade agentic workflows to gh-aw v0.45.6
 2026-02-17 15:38:15 -08:00
copilot-swe-agent[bot]
5a0ed8e0f7 Document upgrade changes and verify workflow compilation 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-17 23:34:37 +00:00
copilot-swe-agent[bot]
e6b58ac7dc Upgrade agentic workflows to gh-aw v0.45.6 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-17 23:33:27 +00:00
copilot-swe-agent[bot]
3cd384316c Initial plan 2026-02-17 23:31:54 +00:00
Lev Nachmanson
9ef99f57e8 remove irrelevant order-sign invariance tracking from levelwise 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-17 11:28:26 -10:00
Nuno Lopes
282834f90f delete dead code 2026-02-17 21:18:48 +00:00
Nikolaj Bjorner
8931f61a76
Merge pull request #8671 from Z3Prover/copilot/add-missing-api-functions 
Add missing solver diagnostic and congruence closure APIs to Go bindings
 2026-02-17 13:11:46 -08:00
Nikolaj Bjorner
15e133c7b8
Delete examples/go/test_new_apis.go 2026-02-17 13:11:33 -08:00
copilot-swe-agent[bot]
87812a99c0 Add safety comment and improve test documentation 
- Add comment about safety of &levels[0] after n > 0 check
- Improve test documentation about SimpleSolver limitations
- Clarify that Units/NonUnits are more reliable for general use

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-17 16:43:12 +00:00
copilot-swe-agent[bot]
b799238fe8 Improve documentation clarity for new APIs 
- Add notes to Trail/TrailLevels about SimpleSolver requirement
- Clarify congruence closure API documentation
- Update test example with more detailed comments
- Make it clear when these functions may not work

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-17 16:41:44 +00:00
copilot-swe-agent[bot]
4ccc28cc71 Optimize TrailLevels and improve documentation 
- Fix NonUnits documentation for clarity
- Optimize TrailLevels to avoid double trail retrieval
- Use trail vector directly instead of rebuilding it
- Reduces memory allocations and reference counting overhead

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-17 16:40:09 +00:00
copilot-swe-agent[bot]
1bae5a847c Add missing solver API functions to Go bindings 
- Add Units() - get unit clauses learned by solver
- Add NonUnits() - get non-unit clauses
- Add Trail() - get decision trail
- Add TrailLevels() - get trail decision levels
- Add CongruenceRoot() - get congruence class representative
- Add CongruenceNext() - get next element in congruence class
- Add CongruenceExplain() - explain why two terms are congruent
- Add test example demonstrating new APIs

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-17 16:38:39 +00:00
copilot-swe-agent[bot]
e479c6690f Initial plan 2026-02-17 16:18:34 +00:00
Nikolaj Bjorner
cff06b528f fix #8563 - align indices for flat quantifiers with sks vector layout, and also guard creating instantiation equalities with sort checks 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-16 20:57:38 -08:00
Nikolaj Bjorner
c0e8698bae
Merge pull request #8668 from Z3Prover/copilot/fix-build-warnings 
Fix C4267 warnings in ast.h initializer_list overloads
 2026-02-16 20:50:47 -08:00
copilot-swe-agent[bot]
037a4aa155 Fix C4267 build warnings in ast.h by adding static_cast for size_t to unsigned conversions 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-17 04:44:23 +00:00
Nikolaj Bjorner
6884ffdd07
Merge pull request #8667 from Z3Prover/copilot/fix-a3-python-workflow-error 
Fix shell substitution breaking agentic workflow template interpolation
 2026-02-16 20:28:05 -08:00
copilot-swe-agent[bot]
9d8f736270 Initial plan 2026-02-17 04:27:04 +00:00
copilot-swe-agent[bot]
23d6262f7d Fix shell substitution in a3-python-v2 workflow as well 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-17 04:16:11 +00:00
copilot-swe-agent[bot]
f28b7ce440 Remove problematic shell substitution from a3-python workflow 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-17 04:15:41 +00:00
copilot-swe-agent[bot]
a467a49453 Initial plan: Fix a3-python.md workflow shell substitution issue 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-17 04:15:08 +00:00