mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-20 11:55:49 +00:00
Code Activity
21994 commits 67 branches 58 tags 205 MiB
Commit graph

31 commits

Author SHA1 Message Date
Copilot
fbeb4b22eb
Add missing Go Goal/FuncEntry/Model APIs and TypeScript Seq higher-order operations (#9006) 
* Initial plan

* fix: add missing API bindings from discussion #8992 for Go and TypeScript

- Go tactic.go: add Goal.Depth(), Goal.Precision(), Goal.Translate(), Goal.ConvertModel()
- Go solver.go: add FuncEntry struct, FuncInterp.GetEntry/SetElse/AddEntry, Model.HasInterp
- TypeScript types.ts + high-level.ts: add Seq.map/mapi/foldl/foldli

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-15 12:57:44 -07:00
Copilot
6893674392
fix: correct misleading API comments in fp.go and JavaExample.java (#9003) 
* Initial plan

* fix: correct misleading API comments in fp.go and JavaExample.java

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-15 12:08:59 -07:00
Copilot
21bfb115ea
Fix high and medium priority API coherence issues (Go, Java, C++, TypeScript) (#8983) 
* Initial plan

* Add missing API functions to Go, Java, C++, and TypeScript bindings

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-14 10:46:03 -07:00
copilot-swe-agent[bot]
47e9c37fbb Go: Add MkBVRotateLeft, MkBVRotateRight, MkRepeat to bitvec.go 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-09 16:20:13 +00:00
copilot-swe-agent[bot]
28fbe33114 Add missing API bindings: Python BvNand/BvNor/BvXnor, Go MkAsArray/MkRecFuncDecl/AddRecDef/Model.Translate, TS Array.fromFunc/Model.translate, OCaml Model.translate 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-02 00:21:57 +00:00
copilot-swe-agent[bot]
a15c659e81 Add Python Optimize.translate() and missing Go tactic/simplifier functions 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-01 02:14:16 +00:00
copilot-swe-agent[bot]
2b8615f4fc Add 8 missing BV overflow/underflow check functions to Go bindings 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-01 01:51:27 +00:00
copilot-swe-agent[bot]
282db840de Add missing API functions to Go, OCaml, and TypeScript bindings 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-27 02:55:37 +00:00
Nikolaj Bjorner
23d8bdd47c
Merge pull request #8758 from Z3Prover/copilot/fix-issues-except-rust 
Add missing solver/optimize API methods across Java, .NET, OCaml, Go, and TypeScript bindings
 2026-02-24 11:47:09 -08:00
copilot-swe-agent[bot]
9802b32a3e Add missing API methods: dimacs, translate, proof, addSimplifier, getLower/getUpper, etc. 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-24 17:22:17 +00:00
copilot-swe-agent[bot]
575f4a8911 Simplify Go user propagator callbacks with withCallback helper 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-24 16:48:05 +00:00
copilot-swe-agent[bot]
3feac95119 Simplify boolean return in goOnBindingCb 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-24 04:42:49 +00:00
copilot-swe-agent[bot]
d5030dfe30 Fix unsafe.Pointer usage in Go propagator - use uintptr_t for cgo.Handle 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-23 01:09:07 +00:00
copilot-swe-agent[bot]
0de7af9112 Add missing API bindings: importModelConverter, OnClause, and user propagator 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-23 01:01:26 +00: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
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]
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]
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]
5a9f416837 Simplify Go bindings: refactor GetLowerAsVector and GetUpperAsVector to use astVectorToExprs helper 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-17 03:46:58 +00:00
copilot-swe-agent[bot]
96d9c66aff Fix formatting of z3.go using gofmt 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-16 22:00:07 +00:00
Nikolaj Bjorner
1fb405cf44
Merge pull request #8655 from Z3Prover/copilot/fix-go-bindings-reference-count 
[WIP] Fix reference counting for Z3_ast_vector in go bindings
 2026-02-16 13:58:03 -08:00
copilot-swe-agent[bot]
ea1f5a333a Fix Go bindings reference counting for Z3_ast_vector objects 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-16 21:48:49 +00:00
copilot-swe-agent[bot]
188880a20c Add missing high-priority Go bindings to Solver 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-16 21:28:24 +00:00
copilot-swe-agent[bot]
d33c0e5601 Fix trailing whitespace in Go source files 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-16 06:06:48 +00:00
copilot-swe-agent[bot]
3f4bd11f00 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-16 06:05:58 +00:00
copilot-swe-agent[bot]
bbc1e501ab 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-16 05:58:20 +00:00
Nikolaj Bjorner
66d0fb5477 git bindings v1.0 2026-02-15 21:24:40 -08:00