mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-27 02:25:38 +00:00
Code Activity
21771 commits 35 branches 58 tags 183 MiB
Commit graph

2806 commits

Author SHA1 Message Date
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
Nikolaj Bjorner
cfb3a01756
Update Solver.cs 2026-02-24 09:58:12 -08:00
copilot-swe-agent[bot]
ce04a24348 Improve TypeScript Optimize documentation for handle index clarity 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-24 17:28:45 +00: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
Toby Shi
f5fba112bc
add parser_context in c++ api 2026-02-21 17:59:44 +08:00
copilot-swe-agent[bot]
a3ea31cb42 Fix congruence closure API naming in Python and Java bindings 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-21 02:04:31 +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
Nikolaj Bjorner
20c446cede
Merge pull request #8703 from Z3Prover/copilot/fix-finite-set-apis 
Add FiniteSet API support to Go, OCaml, and JavaScript/TypeScript bindings
 2026-02-20 08:40:07 -08:00
copilot-swe-agent[bot]
ce0fb1bd24 Fix OCaml build error: use status instead of solver_result in z3.mli 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-20 04:32:56 +00:00
copilot-swe-agent[bot]
5253f9af9d Fix TypeScript type error: explicitly type consVec as AstVectorImpl<Bool<Name>> 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-20 04:31:18 +00:00
copilot-swe-agent[bot]
60f5a76516 Add tests and documentation for addAndTrack in TypeScript bindings (fix discussion #8705) 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-20 04:28:10 +00: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
Nikolaj Bjorner
5bd7d93b55 add parameter validation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-19 14:02:59 -08:00
Nikolaj Bjorner
ee03533c3a update examples to use arrays 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-19 13:57:43 -08:00
Nikolaj Bjorner
c94eb5dc88 fixup API functions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-19 13:33:25 -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]
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]
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]
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]
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]
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]
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]
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]
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
Nikolaj Bjorner
709d1b0182 remove brittle pydoc example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 21:02:27 -08:00
Daniel Tang
c17e8f990e Document example for Solver.sexpr() 2026-02-18 21:02:26 -08:00
Daniel Tang
c281e9dace Add Solver.solutions(t) 
For parity with
[z3.rs](https://docs.rs/z3/latest/z3/struct.Solver.html#method.solutions)
.

Having a way to find all solutions is frequently requested:
* https://stackoverflow.com/q/63231398/10477326
* https://stackoverflow.com/q/11867611/10477326

In accordance with the Rust, I did not
[guess `t`](https://stackoverflow.com/a/11869410/10477326).
 2026-02-18 21:02:25 -08:00
Daniel Tang
5b349f8f9a Suggest eval in ModelRef.__getitem__ error 
This improves the previously cryptic error message. I searched multiple
websites before Google AI suggested using model.eval(arr[0]) for getting
solutions out of arrays.
 2026-02-18 21:02:25 -08:00
Daniel Tang
380a8ee20f Alias ArithRef.__abs__ to Abs 
This integrates with the `abs(Int('x'))` Python builtin.
 2026-02-18 21:02:25 -08:00
Nikolaj Bjorner
a03500a194 git bindings v1.0 2026-02-18 21:02:25 -08:00
Nikolaj Bjorner
487db1a658 Modify behavior for division by zero 
Allow division by zero in z3 expressions without raising an error.
 2026-02-18 21:02:23 -08:00
Nikolaj Bjorner
bcc87975e5 Delete src/api/python/test_critical_fixes.py 2026-02-18 21:02:23 -08:00
copilot-swe-agent[bot]
25c2b7e4c1 Fix error message capitalization for Python conventions 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:23 -08:00
copilot-swe-agent[bot]
0ee04d25c8 Add comprehensive tests for Python API bug fixes 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:23 -08:00
copilot-swe-agent[bot]
28db5e2440 Fix 9 critical assert statements and RatVal division by zero (Priority 1) 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:23 -08:00
copilot-swe-agent[bot]
c946207e23 Fix BOUNDS and ASSERT_FAIL issues in Python API 
- Add negative index support to AstVector.__setitem__, ModelRef.__getitem__, ApplyResult.__getitem__
- Replace bare assertions with proper Z3Exception in z3num.Numeral methods
- All changes tested and validated with comprehensive test suite

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:23 -08:00
copilot-swe-agent[bot]
51fd4b2806 Fix OCaml linker flag and align validation runners with build runners 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:15 -08:00
copilot-swe-agent[bot]
3ae8d7026a Apply headerpad fix to build systems (Python and CMake) and fix validation test paths 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:10 -08:00
copilot-swe-agent[bot]
d3c388a489 Add -headerpad_max_install_names flag for macOS dylib builds 
This fixes the install_name_tool issue on macOS where the tool fails
with "larger updated load commands do not fit". The linker flag
-Wl,-headerpad_max_install_names ensures sufficient header padding
in the Mach-O binary for install_name_tool to modify install names.

Changes made:
- CMake: Added flag to libz3, z3java, z3jl shared libraries on Darwin
- Python build: Changed flag from ML-only to all macOS builds
- OCaml CMake: Added flag to OCaml stublib build on APPLE

Fixes #7623 (regression in 4.15.5)

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 20:58:07 -08:00