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

17710 commits

Author SHA1 Message Date
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
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
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
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
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]
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
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
copilot-swe-agent[bot]
6e91f3b321 Add test for initializer_list overloads 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:26 -08:00
copilot-swe-agent[bot]
d958036711 Add initializer_list overloads and update all call sites 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:26 -08:00
copilot-swe-agent[bot]
d414646975 Add std::initializer_list overloads for update_quantifier and update call sites 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:26 -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
Copilot
d9c6da215f Eliminate unnecessary copies with std::move for ref-counted types (#8591) 2026-02-18 21:02:24 -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
Nikolaj Bjorner
49d41272d9 Remove assertion for number of watches in normalize 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
Nikolaj Bjorner
07c639a422 #8552 
make it recompile constraints with duplicates
 2026-02-18 21:02:22 -08:00
Nikolaj Bjorner
c031058978 small update to testing on p.m_sls_worker instead of should_run_sls 2026-02-18 21:02:22 -08:00
Copilot
730a54a767 Eliminate unnecessary copy operations in function parameters and range-based loops (#8589) 2026-02-18 21:02:22 -08:00
Nuno Lopes
f6f8beaf78 Remove copies (#8583) 2026-02-18 21:02:22 -08:00
Nikolaj Bjorner
776976cbd1 fix #8572 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 21:02:20 -08:00
Nikolaj Bjorner
88a2a82898 fix #8552 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 21:02:20 -08:00
Nikolaj Bjorner
05e8e4a37c fix another regression by Nuno's changes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 21:02:19 -08:00