mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-17 06:11:44 +00:00
Code Activity
20735 commits 69 branches 57 tags 175 MiB
Commit graph

20735 commits

This branch
This branch
All branches
Author SHA1 Message Date
copilot-swe-agent[bot]
479a6d3d3b Add Go bindings to API coherence checker workflow 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-16 17:50:48 +00:00
copilot-swe-agent[bot]
47469a3876 Initial plan 2026-02-16 17:48:18 +00:00
Nikolaj Bjorner
1924066ff0 update version 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-16 09:47:37 -08: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
e553ee2110 revert to last working flows 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-16 09:29:10 -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
copilot-swe-agent[bot]
c454b14c24 Add Go bindings support to ubuntu-cmake CI builds 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-16 05:34:36 +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
copilot-swe-agent[bot]
ccb9de7201 Initial plan 2026-02-16 05:31:53 +00: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
015891aff9
Merge pull request #8645 from Z3Prover/copilot/debug-agentic-workflow-failure 
Fix template interpolation failure in agentic workflow markdown files
 2026-02-15 20:57:44 -08:00
copilot-swe-agent[bot]
15c9455c7d Fix template interpolation failure in agentic workflows 
Remove shell command substitution syntax $(date +%Y-%m-%d) from workflow
markdown files that was causing template interpolation to fail. The shell
syntax is not valid in the context/frontmatter section that gets processed
by the template engine.

Fixed files:
- .github/workflows/a3-python-v2.md
- .github/workflows/a3-python.md
- .github/workflows/code-simplifier.md

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-16 04:54:37 +00: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
copilot-swe-agent[bot]
fe4f70e07d Initial plan 2026-02-16 04:51:01 +00:00
Nikolaj Bjorner
a0d232fc2a
Merge pull request #8642 from Z3Prover/copilot/debug-agentic-workflow-a3-python-v2 
Fix a3-python-v2 workflow compilation failure
 2026-02-15 20:46:41 -08:00
Daniel Tang
114a325cd4
Document example for Solver.sexpr() 2026-02-15 21:38:46 -05:00
Nikolaj Bjorner
a96a4f5447 remove junk 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-15 18:00:42 -08: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]
d6300b995c Fix a3-python-v2 workflow compilation error 
- Remove invalid source reference to non-existent commit
- Fix network domains: 'default' → 'defaults'
- Remove serena tools configuration
- Recompile workflow with gh-aw v0.45.0

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-16 01:33:43 +00:00
copilot-swe-agent[bot]
573e53adfa Initial plan 2026-02-16 01:29:46 +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
copilot-swe-agent[bot]
66c8b0c874 Initial plan 2026-02-16 01:24:26 +00:00
copilot-swe-agent[bot]
e57e0df29c Initial plan 2026-02-16 01:24:01 +00:00
Nikolaj Bjorner
1463b1ef08
Merge pull request #8611 from Z3Prover/copilot/fix-action-run-error 
Fix sparse-checkout initialization in a3-python workflows
 2026-02-15 17:23:06 -08: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
Nikolaj Bjorner
e58c689d42
Merge pull request #8623 from danielzgtg/feat/__abs__ 
Alias ArithRef.__abs__ to Abs
 2026-02-15 17:17:21 -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
Nikolaj Bjorner
e2486eff77 upgrade workflows 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-13 08:57:00 -08:00
Copilot
cc7e6cd92d
Eliminate unnecessary copies with std::move for ref-counted types (#8591) 2026-02-13 12:16:47 +00:00
copilot-swe-agent[bot]
8a49ca490f Fix git sparse-checkout error in a3-python workflows 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-13 03:54:06 +00:00
copilot-swe-agent[bot]
34038e2b6d Initial plan 2026-02-13 03:51:36 +00:00
Nikolaj Bjorner
83b60990b1 add tool 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-12 19:40:19 -08:00
Nikolaj Bjorner
3f15666441
Merge pull request #8603 from Z3Prover/copilot/fix-github-actions-job 
Fix macOS NuGet validation: remove RuntimeIdentifier to match package structure
 2026-02-12 19:25:17 -08:00
Nikolaj Bjorner
a81f691899 increment minor version 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-12 17:31:50 -08:00
copilot-swe-agent[bot]
fc6140e489 Remove RuntimeIdentifier to fix assembly loading on macOS 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-12 21:24:22 +00:00
copilot-swe-agent[bot]
1ea2b0865a Fix test-nuget on macOS by rewriting csproj with proper configuration 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-12 21:22:30 +00:00
copilot-swe-agent[bot]
c392c460ad Initial plan 2026-02-12 21:19:19 +00:00
Nikolaj Bjorner
f80414f4bb update release to dedup and include manylinux 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-12 11:38:41 -08:00
Nikolaj Bjorner
b381de4f3f
Merge pull request #8602 from Z3Prover/copilot/fix-nightly-build-job 
Fix nightly workflow: remove unsupported --clobber flag and add artifact deduplication
 2026-02-12 10:23:19 -08:00