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

20827 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
copilot-swe-agent[bot]
b8148b9457 Initial plan 2026-02-18 21:02:29 -08:00
copilot-swe-agent[bot]
3cad025365 Simplify Go bindings: refactor GetLowerAsVector and GetUpperAsVector to use astVectorToExprs helper 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:28 -08:00
copilot-swe-agent[bot]
74ae287f31 Initial plan 2026-02-18 21:02:28 -08:00
dependabot[bot]
9e96ecbf4d Bump githubnext/gh-aw from 0.42.17 to 0.45.1 
Bumps [githubnext/gh-aw](https://github.com/githubnext/gh-aw) from 0.42.17 to 0.45.1.
- [Release notes](https://github.com/githubnext/gh-aw/releases)
- [Changelog](https://github.com/github/gh-aw/blob/main/CHANGELOG.md)
- [Commits](https://github.com/githubnext/gh-aw/compare/v0.42.17...v0.45.1)

---
updated-dependencies:
- dependency-name: githubnext/gh-aw
  dependency-version: 0.45.1
  dependency-type: direct:production
  update-type: version-update:semver-minor
...

Signed-off-by: dependabot[bot] <support@github.com>
 2026-02-18 21:02:28 -08:00
dependabot[bot]
68e4a2a52b Bump actions/download-artifact from 6.0.0 to 7.0.0 
Bumps [actions/download-artifact](https://github.com/actions/download-artifact) from 6.0.0 to 7.0.0.
- [Release notes](https://github.com/actions/download-artifact/releases)
- [Commits](https://github.com/actions/download-artifact/compare/v6...v7)

---
updated-dependencies:
- dependency-name: actions/download-artifact
  dependency-version: 7.0.0
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <support@github.com>
 2026-02-18 21:02:28 -08:00
dependabot[bot]
0cb36f99dc Bump actions/checkout from 5.0.1 to 6.0.2 
Bumps [actions/checkout](https://github.com/actions/checkout) from 5.0.1 to 6.0.2.
- [Release notes](https://github.com/actions/checkout/releases)
- [Commits](https://github.com/actions/checkout/compare/v5.0.1...v6.0.2)

---
updated-dependencies:
- dependency-name: actions/checkout
  dependency-version: 6.0.2
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <support@github.com>
 2026-02-18 21:02:28 -08:00
dependabot[bot]
7d58011129 Bump github/gh-aw from 0.43.15 to 0.45.1 
Bumps [github/gh-aw](https://github.com/github/gh-aw) from 0.43.15 to 0.45.1.
- [Release notes](https://github.com/github/gh-aw/releases)
- [Commits](https://github.com/github/gh-aw/compare/v0.43.15...v0.45.1)

---
updated-dependencies:
- dependency-name: github/gh-aw
  dependency-version: 0.45.1
  dependency-type: direct:production
  update-type: version-update:semver-minor
...

Signed-off-by: dependabot[bot] <support@github.com>
 2026-02-18 21:02:28 -08:00
dependabot[bot]
f2a41ca9f0 Bump actions/cache from 4.3.0 to 5.0.3 
Bumps [actions/cache](https://github.com/actions/cache) from 4.3.0 to 5.0.3.
- [Release notes](https://github.com/actions/cache/releases)
- [Commits](https://github.com/actions/cache/compare/v4.3.0...v5.0.3)

---
updated-dependencies:
- dependency-name: actions/cache
  dependency-version: 5.0.3
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <support@github.com>
 2026-02-18 21:02:28 -08:00
copilot-swe-agent[bot]
d56ae1a669 Fix formatting of z3.go using gofmt 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:28 -08:00
copilot-swe-agent[bot]
d43c556a80 Initial plan 2026-02-18 21:02:28 -08:00
copilot-swe-agent[bot]
15365616fb Fix Go bindings reference counting for Z3_ast_vector objects 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:28 -08:00
copilot-swe-agent[bot]
0532efeb26 Initial plan 2026-02-18 21:02:28 -08:00
copilot-swe-agent[bot]
b0702bfa0f Fix variable naming: tmpFile -> tempFile for Go conventions 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:28 -08:00
copilot-swe-agent[bot]
f734ce9ce3 Address code review feedback: use os.CreateTemp and remove unused vars 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:28 -08:00
copilot-swe-agent[bot]
42c783ac98 Fix duplicate example in advanced_example.go and add silent markers for unused vars 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:28 -08:00
copilot-swe-agent[bot]
d1dd539519 Add missing high-priority Go bindings to Solver 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:27 -08:00
copilot-swe-agent[bot]
550b190267 Initial plan 2026-02-18 21:02:27 -08:00
copilot-swe-agent[bot]
0ef12e3468 Fix git sparse-checkout initialization in a3-python workflows 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:27 -08:00
copilot-swe-agent[bot]
beb77566b1 Initial plan 2026-02-18 21:02:27 -08:00
copilot-swe-agent[bot]
436a2f887c Add Go bindings to API coherence checker workflow 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:27 -08:00
copilot-swe-agent[bot]
95c17e5fff Initial plan 2026-02-18 21:02:27 -08:00
Nikolaj Bjorner
fa5f5c5824 update version 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 21:02:27 -08:00
copilot-swe-agent[bot]
dd09b89557 Fix trailing whitespace in Go source files 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:27 -08:00
copilot-swe-agent[bot]
c61ee6b16c Fix Go bindings and enable in CI 
- Fix all compilation errors in Go bindings
- Add missing type definitions (Pattern, ASTVector, ParamDescrs)
- Fix boolean comparisons to use bool() casts
- Fix Z3_app type casts using unsafe.Pointer
- Fix null symbol handling to use nil
- Fix unused variable in basic_example.go
- Fix CMake test target to run from examples/go directory
- Restore CI steps to build and test Go bindings

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:27 -08:00
copilot-swe-agent[bot]
25a83fc87e Fix Go bindings compilation issues and add to CI 
- Fix malformed z3.go with duplicate function body fragments
- Fix datatype.go to use Z3_del_constructor and Z3_del_constructor_list instead of non-existent inc_ref/dec_ref functions
- Remove non-existent Push/Pop methods from fixedpoint.go
- Fix CMake Go bindings targets quoting for proper LDFLAGS handling
- Add Go bindings support to ubuntu-cmake CI jobs

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:27 -08:00
copilot-swe-agent[bot]
e9fcdd46c6 Add Go bindings support to ubuntu-cmake CI builds 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:27 -08:00
copilot-swe-agent[bot]
eed75bba5e Initial plan 2026-02-18 21:02:27 -08:00
Nikolaj Bjorner
2da80914cc revert to last working flows 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 21:02:27 -08:00
Nikolaj Bjorner
709d1b0182 remove brittle pydoc example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 21:02:27 -08:00
copilot-swe-agent[bot]
388f893d2e Improve test validation for mk_transitivity 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:26 -08:00
copilot-swe-agent[bot]
eedade141c Restore defensive SASSERT in smt_conflict_resolution 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:26 -08:00