mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-01 11:16:54 +00:00
Code Activity
21828 commits 43 branches 58 tags 185 MiB
Commit graph

21828 commits

This branch
This branch
All branches
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
Ruijie Fang
4f4e657449
Merge branch 'Z3Prover:master' into master 2026-02-24 13:39:36 -06:00
copilot-swe-agent[bot]
cdd5582a5b Add Clang Static Analyzer (CSA) agentic workflow with Discussion reporting 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-24 19:30:15 +00:00
copilot-swe-agent[bot]
6fe956c2f6 Initial plan 2026-02-24 19:25:21 +00:00
Lev Nachmanson
0074de0fce improve non-zero witness substitution logic 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-24 09:19:13 -10: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
Nikolaj Bjorner
8e5f1840a9
Merge pull request #8755 from Z3Prover/copilot/simplify-go-propagator-callbacks 
Simplify Go user propagator callbacks with `withCallback` helper
 2026-02-24 09:10:21 -08:00
Nikolaj Bjorner
819144f374
Merge pull request #8756 from Z3Prover/copilot/create-agentic-workflow-backlog 
Add issue backlog processor agentic workflow
 2026-02-24 09:08:28 -08:00
copilot-swe-agent[bot]
08addfa654 Initial plan 2026-02-24 17:03:50 +00:00
copilot-swe-agent[bot]
4ebf453365 Add issue-backlog-processor agentic workflow 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-24 16:54:49 +00:00
copilot-swe-agent[bot]
d2f6dd0d5a Initial plan 2026-02-24 16:49:41 +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]
023b29ff0e Initial plan 2026-02-24 16:44:52 +00:00
Nikolaj Bjorner
e0161b2e2e
Merge pull request #8746 from Z3Prover/copilot/simplify-go-return-logic 
Simplify boolean return in goOnBindingCb
 2026-02-24 08:44:24 -08:00
Nikolaj Bjorner
13cf90ea09
Merge pull request #8753 from Z3Prover/copilot/update-api-coherence-checker-workflow 
Add Rust bindings (prove-rs/z3.rs) to API coherence checker workflow
 2026-02-24 08:43:14 -08:00
Nikolaj Bjorner
aaa62efc90
Merge pull request #8725 from Z3Prover/copilot/convert-factor-to-simplifier 
Convert `factor` tactic to a `dependent_expr_simplifier`
 2026-02-24 08:42:30 -08:00
copilot-swe-agent[bot]
1f5bc9ba0c Add Rust bindings (prove-rs/z3.rs) to API coherence checker workflow 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-24 16:36:54 +00:00
copilot-swe-agent[bot]
cac5e83948 Initial plan 2026-02-24 16:30:20 +00:00
copilot-swe-agent[bot]
de3cf18899 Fix fp.to_real encoding for denormal floating-point values 
The mk_to_real function in fpa2bv_converter.cpp was missing the
normalization shift adjustment (lz) when computing the real-valued
exponent for denormal floating-point numbers.

When unpack(x, sgn, sig, exp, lz, normalize=true) normalizes a denormal
by shifting the significand left by lz positions, the returned exp does
not account for this shift. All other callers (mk_mul, mk_div, mk_fma)
correctly subtract lz from the exponent, but mk_to_real was missing this.

The fix subtracts zero-extended lz from the sign-extended exp to get the
true exponent, matching the convention used by other FP operations.

Fixes incorrect model with (_ FloatingPoint 2 24) and fp.to_real.

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-24 05:22:54 +00:00
copilot-swe-agent[bot]
243275c638 Initial plan 2026-02-24 04:44:27 +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]
f8e97957f8 Initial plan 2026-02-24 04:41:56 +00:00
Nikolaj Bjorner
8ec15639e0
Merge pull request #8726 from Z3Prover/copilot/convert-cofactor-term-ite-to-simplifier 
Convert `cofactor-term-ite` tactic to a simplifier
 2026-02-23 20:40:23 -08:00
Nikolaj Bjorner
441fbe25fa
Merge pull request #8742 from Z3Prover/dependabot/github_actions/actions/setup-go-6 
Bump actions/setup-go from 5 to 6
 2026-02-23 20:33:03 -08:00
Nikolaj Bjorner
fe5c15e1fc
Merge pull request #8743 from Z3Prover/dependabot/github_actions/github/gh-aw-0.49.5 
Bump github/gh-aw from 0.45.6 to 0.49.5
 2026-02-23 20:32:37 -08:00
Nikolaj Bjorner
87a8ccfa0e
Merge pull request #8744 from Z3Prover/dependabot/github_actions/actions/upload-artifact-6 
Bump actions/upload-artifact from 4 to 6
 2026-02-23 20:32:11 -08:00
Nikolaj Bjorner
55753ba36f
Merge pull request #8745 from Z3Prover/dependabot/github_actions/actions/download-artifact-7 
Bump actions/download-artifact from 4 to 7
 2026-02-23 20:31:58 -08:00
Nikolaj Bjorner
6df2aeedb9
Merge pull request #8741 from Z3Prover/dependabot/github_actions/actions/checkout-6.0.2 
Bump actions/checkout from 5.0.1 to 6.0.2
 2026-02-23 20:30:33 -08:00
dependabot[bot]
a61de6023a
Bump actions/download-artifact from 4 to 7 
Bumps [actions/download-artifact](https://github.com/actions/download-artifact) from 4 to 7.
- [Release notes](https://github.com/actions/download-artifact/releases)
- [Commits](https://github.com/actions/download-artifact/compare/v4...v7)

---
updated-dependencies:
- dependency-name: actions/download-artifact
  dependency-version: '7'
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <support@github.com>
 2026-02-23 23:24:27 +00:00
dependabot[bot]
2fed3b67ba
Bump actions/upload-artifact from 4 to 6 
Bumps [actions/upload-artifact](https://github.com/actions/upload-artifact) from 4 to 6.
- [Release notes](https://github.com/actions/upload-artifact/releases)
- [Commits](https://github.com/actions/upload-artifact/compare/v4...v6)

---
updated-dependencies:
- dependency-name: actions/upload-artifact
  dependency-version: '6'
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <support@github.com>
 2026-02-23 23:24:03 +00:00
dependabot[bot]
c3a97b5a03
Bump github/gh-aw from 0.45.6 to 0.49.5 
Bumps [github/gh-aw](https://github.com/github/gh-aw) from 0.45.6 to 0.49.5.
- [Release notes](https://github.com/github/gh-aw/releases)
- [Commits](https://github.com/github/gh-aw/compare/v0.45.6...v0.49.5)

---
updated-dependencies:
- dependency-name: github/gh-aw
  dependency-version: 0.49.5
  dependency-type: direct:production
  update-type: version-update:semver-minor
...

Signed-off-by: dependabot[bot] <support@github.com>
 2026-02-23 23:23:44 +00:00
dependabot[bot]
2aa3ec1dda
Bump actions/setup-go from 5 to 6 
Bumps [actions/setup-go](https://github.com/actions/setup-go) from 5 to 6.
- [Release notes](https://github.com/actions/setup-go/releases)
- [Commits](https://github.com/actions/setup-go/compare/v5...v6)

---
updated-dependencies:
- dependency-name: actions/setup-go
  dependency-version: '6'
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <support@github.com>
 2026-02-23 23:22:25 +00:00
dependabot[bot]
51e53b547a
Bump actions/checkout from 5.0.1 to 6.0.2 
Bumps [actions/checkout](https://github.com/actions/checkout) from 5.0.1 to 6.0.2.
- [Release notes](https://github.com/actions/checkout/releases)
- [Commits](https://github.com/actions/checkout/compare/v5.0.1...v6.0.2)

---
updated-dependencies:
- dependency-name: actions/checkout
  dependency-version: 6.0.2
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <support@github.com>
 2026-02-23 23:22:21 +00:00
Lev Nachmanson
cf3552c029 suppress witness subs optimization 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-23 09:59:08 -10:00
copilot-swe-agent[bot]
c0fd3513a2 Fix RNE/RNA overflow-to-infinity in Real-to-FP conversion (soundness bug) 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-23 04:34:58 +00:00
copilot-swe-agent[bot]
1c6f251062 Initial plan 2026-02-23 04:11:40 +00:00
copilot-swe-agent[bot]
fd424c7afd Delete factor_tactic.cpp (implementation moved to factor_simplifier.cpp) 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-23 04:01:34 +00:00
copilot-swe-agent[bot]
afbd038924 Delete cofactor_term_ite_tactic.cpp 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-23 03:57:37 +00:00
Nikolaj Bjorner
2ea86d94dc
Merge pull request #8735 from Z3Prover/copilot/fix-discussed-issues 
Add missing API bindings: importModelConverter, OnClause, and user propagator (Go/Java)
 2026-02-22 19:46:11 -08:00
Nikolaj Bjorner
8fbc4ed26d
Merge pull request #8727 from Z3Prover/copilot/expose-max-bv-sharing-simplifier 
Expose max-bv-sharing as a registered simplifier
 2026-02-22 19:40:35 -08:00
Nikolaj Bjorner
0b5480b6c3
Merge pull request #8729 from Z3Prover/copilot/convert-bvarray2uf-to-simplifier 
Convert `bvarray2uf` tactic to a dependent_expr_simplifier
 2026-02-22 19:39:19 -08: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
copilot-swe-agent[bot]
43dee82caa Initial plan 2026-02-23 00:19:28 +00:00
Nikolaj Bjorner
69eab28550
Merge pull request #8730 from Z3Prover/copilot/convert-der-tactic-to-simplifier 
Convert `der` tactic to a `dependent_expr_simplifier`
 2026-02-22 14:04:04 -08:00
copilot-swe-agent[bot]
1d2a76d27b Delete bvarray2uf_tactic.cpp (removed from CMakeLists.txt) 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-22 08:57:39 +00:00
copilot-swe-agent[bot]
57d1667d28 Remove der_tactic.cpp from CMakeLists.txt (file was deleted) 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-22 08:47:14 +00:00
Nikolaj Bjorner
b149f27e82
Delete src/tactic/core/der_tactic.cpp 2026-02-22 00:25:24 -08:00