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

21632 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
copilot-swe-agent[bot]
ca8f379823 Initial plan 2026-02-19 17:49:39 +00:00
Nikolaj Bjorner
86dc55691d add extra parameter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 21:34:29 -08:00
Nikolaj Bjorner
31a85925ee
Delete FINITE_SET_API.md 2026-02-18 21:14:55 -08:00
Nikolaj Bjorner
a32c9effb2 remove examples 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 21:13:48 -08:00
Nikolaj Bjorner
24f36c2498
Delete examples/SMT-LIB2/finite-sets/cycle.smt2 2026-02-18 21:12:28 -08:00
Nikolaj Bjorner
7fe9b1f873
Merge branch 'master' into finite-sets 2026-02-18 21:11:44 -08:00
Nikolaj Bjorner
07d8971ef9 add sketch for incremental algorithm 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 21:10:17 -08:00
Nikolaj Bjorner
69b73c64cf enable post setup parameter tweaking in theory solvers, update azure-pipeline 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 21:08:24 -08:00
Nikolaj Bjorner
c32b213a20 add finite sets to datatype recursion, delay initialize finite_set plugin, fix bugs in are_distinct and equality simplification 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 21:07:40 -08:00
Nikolaj Bjorner
a1d43f5fb9 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 21:03:19 -08:00
Nikolaj Bjorner
fc792b645c update version 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 21:02:32 -08:00
copilot-swe-agent[bot]
2f33a34692 Fix OCaml build error in solver_get_levels 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:32 -08:00
copilot-swe-agent[bot]
316bc3d821 Initial plan 2026-02-18 21:02:32 -08:00
Nikolaj Bjorner
29e759ac27 Delete examples/go/test_new_api_additions.go 2026-02-18 21:02:32 -08:00
copilot-swe-agent[bot]
c22e20c8a0 Add test for new Go API methods 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:32 -08:00
copilot-swe-agent[bot]
8f4ecc8baa Add missing API methods to Go and OCaml bindings 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:31 -08:00
copilot-swe-agent[bot]
04c1b04c5c Initial plan 2026-02-18 21:02:31 -08:00
Nikolaj Bjorner
3364bf2802 remove deprecated workflows 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 21:02:31 -08:00
copilot-swe-agent[bot]
200cb3d025 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 21:02:31 -08:00
copilot-swe-agent[bot]
f4b5dd8d17 Initial plan 2026-02-18 21:02:31 -08:00
copilot-swe-agent[bot]
bfdcfbe77c Fix indentation in commented-out code section 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:31 -08:00
copilot-swe-agent[bot]
7e71ee9eb6 Improve documentation for RatVal division by zero handling 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:31 -08:00
copilot-swe-agent[bot]
92d684e942 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 21:02:31 -08:00
copilot-swe-agent[bot]
b5b79343e4 Initial plan 2026-02-18 21:02:31 -08:00
Nikolaj Bjorner
5349fad6ed fixup docs.ytml 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 21:02:31 -08:00
Nikolaj Bjorner
05c301a064 update go doc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 21:02:31 -08:00
Nikolaj Bjorner
ac2cbdd24c update a3-python to fix issues 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 21:02:31 -08:00
Nikolaj Bjorner
78a7b17f50 Update documentation generation to include Go 2026-02-18 21:02:31 -08:00
Nikolaj Bjorner
e261bacf8e new repository agnostic workflow 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 21:02:30 -08:00
Nikolaj Bjorner
cc74d55cc8 recompile workflows 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 21:02:30 -08:00
Nikolaj Bjorner
0f890da281 Remove checkout steps from A3 Python workflow 
Removed steps for checking out Python source files.
 2026-02-18 21:02:30 -08:00
Nikolaj Bjorner
7562de2f7a Remove checkout steps from A3 Python workflow 
Removed steps for checking out Python source files.
 2026-02-18 21:02:30 -08:00
copilot-swe-agent[bot]
04b2fb3aaa Document upgrade changes and verify workflow compilation 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:30 -08:00
copilot-swe-agent[bot]
26c9adbe68 Upgrade agentic workflows to gh-aw v0.45.6 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:30 -08:00
copilot-swe-agent[bot]
7680f49aed Initial plan 2026-02-18 21:02:30 -08:00
Lev Nachmanson
f065b843c8 remove irrelevant order-sign invariance tracking from levelwise 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 21:02:30 -08:00
Nuno Lopes
3b89789438 delete dead code 2026-02-18 21:02:30 -08:00
Nikolaj Bjorner
d048eec197 Delete examples/go/test_new_apis.go 2026-02-18 21:02:30 -08:00
copilot-swe-agent[bot]
a04f255379 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-18 21:02:29 -08:00
copilot-swe-agent[bot]
7da235a954 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-18 21:02:29 -08:00
copilot-swe-agent[bot]
20f596768c 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-18 21:02:29 -08:00
copilot-swe-agent[bot]
5ecbb9d655 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-18 21:02:29 -08:00
copilot-swe-agent[bot]
edb35e7332 Initial plan 2026-02-18 21:02:29 -08:00
Nikolaj Bjorner
534361dee4 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-18 21:02:29 -08:00
copilot-swe-agent[bot]
d5ba26e754 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-18 21:02:29 -08:00
copilot-swe-agent[bot]
cf60e7a3f3 Initial plan 2026-02-18 21:02:29 -08:00
copilot-swe-agent[bot]
298803ce44 Fix shell substitution in a3-python-v2 workflow as well 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:29 -08:00
copilot-swe-agent[bot]
2f2c4d99a6 Remove problematic shell substitution from a3-python workflow 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:29 -08:00
copilot-swe-agent[bot]
1163774b12 Initial plan: Fix a3-python.md workflow shell substitution issue 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:29 -08:00