mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-08 06:14:52 +00:00
Code Activity
20790 commits 46 branches 58 tags 222 MiB
Commit graph

17246 commits

Author SHA1 Message Date
Nuno Lopes
8562788ad8 fixes 2026-02-17 09:50:48 +00:00
copilot-swe-agent[bot]
45f5209c23 Add out-of-line definitions for static constexpr members to fix ODR violations 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-17 09:50:48 +00:00
copilot-swe-agent[bot]
227e48c0b1 Fix SMALL_BITS constant reference to use direct calculation instead 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-17 09:50:48 +00:00
copilot-swe-agent[bot]
4941ef138b Fix undefined behavior when negating SMALL_INT_MIN in power_of_two_multiple 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-17 09:50:48 +00:00
copilot-swe-agent[bot]
cd699ca582 Fix remaining int truncation issues in is_power_of_two, power_of_two_multiple, and log2 for 64-bit platforms 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-17 09:50:48 +00:00
copilot-swe-agent[bot]
9bf691f8bd Refactor decompose function and consolidate value()/value64() into single value() returning int64_t 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-17 09:50:48 +00:00
copilot-swe-agent[bot]
10c82a3b84 Fix machine_div2k to not truncate when result doesn't fit in small (add assertion instead) 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-17 09:50:48 +00:00
copilot-swe-agent[bot]
a5e1fa9930 Fix more uses of value() that should use value64() for 64-bit correctness 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-17 09:50:48 +00:00
copilot-swe-agent[bot]
76dde47c4e Fix uses of value() that should be value64() for 64-bit small integers 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-17 09:50:48 +00:00
copilot-swe-agent[bot]
5edef9e9a0 Remove nonsensical assertion and revert to simpler shift for SMALL_INT constants 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-17 09:50:48 +00:00
copilot-swe-agent[bot]
dcfeb559fe Add assertion to set() method and simplify get_sign_cell by removing redundant SMALL_INT_MIN case 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-17 09:50:48 +00:00
copilot-swe-agent[bot]
4dc74e2e30 Fix undefined behavior in SMALL_INT_MAX/MIN constants by using unsigned arithmetic 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-17 09:50:48 +00:00
copilot-swe-agent[bot]
b8ed45bfac Revert deallocation in set methods and restore indentation in gcd function 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-17 09:50:48 +00:00
copilot-swe-agent[bot]
6faaf86dca Implement proper bounds checking for small integers based on platform pointer size 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-17 09:50:47 +00:00
copilot-swe-agent[bot]
cb3b8603eb Fix syntax errors in mpz.h 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-17 09:50:47 +00:00
Nuno Lopes
ac1bef0053 mpz: use pointer tagging to save space (#8447) 
Co-authored-by: Copilot <198982749+Copilot@users.noreply.github.com>
 2026-02-17 09:50:47 +00:00
Nikolaj Bjorner
cff06b528f 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-16 20:57:38 -08:00
copilot-swe-agent[bot]
037a4aa155 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-17 04:44:23 +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
Nikolaj Bjorner
dd10826c99
Merge pull request #8646 from Z3Prover/copilot/build-go-bindings-ci 
Enable Go bindings in ubuntu-cmake CI builds
 2026-02-16 09:45:42 -08:00
Nikolaj Bjorner
e87cf5ad2b remove brittle pydoc example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-16 09:20:57 -08: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
249b59f42c
Merge pull request #8637 from Z3Prover/copilot/refactor-proof-functions-initializer-list 
Modernize mk_unit_resolution and mk_transitivity with std::initializer_list overloads
 2026-02-15 21:33:08 -08:00
Nikolaj Bjorner
a6620765dc
Merge pull request #8638 from Z3Prover/copilot/refactor-update-quantifier-initializer-list 
Modernize update_quantifier with std::initializer_list overloads
 2026-02-15 21:32:38 -08:00
Nikolaj Bjorner
e099c74985 Merge branch 'master' of https://github.com/z2prover/z3 2026-02-15 21:25:04 -08:00
Nikolaj Bjorner
66d0fb5477 git bindings v1.0 2026-02-15 21:24:40 -08:00
Nikolaj Bjorner
b0ebc78217
Merge pull request #8631 from danielzgtg/doc/solverSexpr 
Document example for Solver.sexpr()
 2026-02-15 20:51:54 -08:00
Daniel Tang
114a325cd4
Document example for Solver.sexpr() 2026-02-15 21:38:46 -05:00
copilot-swe-agent[bot]
f3c4c57c58 Improve test validation for mk_transitivity 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-16 01:52:20 +00:00
copilot-swe-agent[bot]
e627e60fe7 Restore defensive SASSERT in smt_conflict_resolution 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-16 01:50:51 +00:00
copilot-swe-agent[bot]
d239e7a19d Add test for initializer_list overloads 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-16 01:48:21 +00:00
copilot-swe-agent[bot]
fb043ac9ee Add std::initializer_list overloads for update_quantifier and update call sites 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-16 01:28:31 +00:00
copilot-swe-agent[bot]
9efb0e0794 Add initializer_list overloads and update all call sites 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-16 01:27:08 +00:00
Nikolaj Bjorner
166a9afab0
Merge pull request #8633 from danielzgtg/feat/solverSolutions 
Add Solver.solutions(t)
 2026-02-15 17:22:03 -08:00
Nikolaj Bjorner
24f3258c49
Merge pull request #8626 from danielzgtg/feat/modelRefGetitemErrorMessageModelRefEval 
Suggest eval in ModelRef.__getitem__ error
 2026-02-15 17:20:11 -08:00
Daniel Tang
32c4c87e22
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-15 01:18:02 -05:00
Daniel Tang
1ada488cb6
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-14 18:16:39 -05:00
Daniel Tang
c172b58268
Alias ArithRef.__abs__ to Abs 
This integrates with the `abs(Int('x'))` Python builtin.
 2026-02-14 01:37:58 -05:00
Copilot
cc7e6cd92d
Eliminate unnecessary copies with std::move for ref-counted types (#8591) 2026-02-13 12:16:47 +00:00
Nikolaj Bjorner
5497de0af7
Merge pull request #8597 from Z3Prover/copilot/fix-high-severity-bugs-python-api 
Fix 13 critical bugs in Python API: assertion removal, division by zero, bounds checking
 2026-02-12 09:40:50 -08:00
Nikolaj Bjorner
8077e3d031
Modify behavior for division by zero 
Allow division by zero in z3 expressions without raising an error.
 2026-02-12 07:10:00 -08:00
Nikolaj Bjorner
dcbafa9442
Delete src/api/python/test_critical_fixes.py 2026-02-12 07:07:15 -08:00
Nikolaj Bjorner
39f5ef5e4e
Remove assertion for number of watches in normalize 2026-02-12 07:03:52 -08:00
copilot-swe-agent[bot]
a8f32ed291 Fix error message capitalization for Python conventions 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-12 05:03:07 +00:00