mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-18 16:09:30 +00:00
Code Activity
22189 commits 86 branches 58 tags 206 MiB
Commit graph

22189 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Lev Nachmanson
7aa1ba1905 a bug fix in levelwise with the section case, where a discriminant was not added, and adding new tests for levelwise 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-17 20:00:53 -10:00
Nikolaj Bjorner
136bf0b5eb
Update documentation generation to include Go 2026-02-17 18:36:04 -08:00
Lev Nachmanson
af6d461b5e add tests for levelwise 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-17 14:46:21 -10: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
Lev Nachmanson
269dba0525 add all coeffs ot a nullified polynomial to the projection 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-17 14:20:58 -10:00
Lev Nachmanson
a781f9c0a0 remove an obsolete m_fail and related from levelwise 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-17 14:11:16 -10: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
2d8e866e19 try replace fail with a adding partial derivatives 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-17 13:20:50 -10: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
Nuno Lopes
e6607df831 fixes 2026-02-17 15:41:07 +00:00
Nuno Lopes
fdc5793509 fixes 2026-02-17 14:20:12 +00:00
Nuno Lopes
6db067ca67 fixes 2026-02-17 14:11:41 +00:00
Nuno Lopes
4a8aeb0050 fixes 2026-02-17 09:50:48 +00:00
copilot-swe-agent[bot]
c01062e93b Revert "Fix set_big_i64/set_big_ui64 zero handling: zero is always represented as small" 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-17 09:50:48 +00:00
copilot-swe-agent[bot]
cc7902ac50 Fix set_big_i64/set_big_ui64 zero handling: zero is always represented as small 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-17 09:50:48 +00:00
copilot-swe-agent[bot]
957ba91fa6 Revert "Fix invalid zero representation in set_big_i64 and set_big_ui64" 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-17 09:50:48 +00:00
copilot-swe-agent[bot]
04f07fe1d5 Fix invalid zero representation in set_big_i64 and set_big_ui64 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-17 09:50:48 +00:00
Nuno Lopes
fa73827d98 fixes 2026-02-17 09:50:48 +00:00
Nuno Lopes
1a189ebdd7 fix 2026-02-17 09:50:48 +00:00
Nuno Lopes
ac748d973c fix 2026-02-17 09:50:48 +00:00
Nuno Lopes
bd993ca963 fix 2026-02-17 09:50:48 +00:00
Nuno Lopes
0a22332196 fix 2026-02-17 09:50:48 +00:00
Nuno Lopes
dad012ad5d fix 2026-02-17 09:50:48 +00:00
Nuno Lopes
4cdbe221cf fix 2026-02-17 09:50:48 +00:00
Nuno Lopes
92158ac607 fix 2026-02-17 09:50:48 +00:00
Nuno Lopes
e9556c498b fix 2026-02-17 09:50:48 +00:00
Nuno Lopes
8ce362abda fix 2026-02-17 09:50:48 +00:00
Nuno Lopes
5f429d1223 fix 2026-02-17 09:50:48 +00:00
Nuno Lopes
88242fb4ce fix 2026-02-17 09:50:48 +00:00
Nuno Lopes
9448f67d21 fix 2026-02-17 09:50:48 +00:00