mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity
20096 commits 49 branches 53 tags 182 MiB
Commit graph

20096 commits

This branch
This branch
All branches
Author SHA1 Message Date
Don Syme
2d0b9e6972 recompile improvers 2025-09-17 15:50:33 +01:00
Don Syme
aabdb407d1 latest improvers 2025-09-17 13:49:00 +01:00
Don Syme
2364ea42ba update improvers 2025-09-17 13:19:24 +01:00
Don Syme
7268136bb6 update workflows 2025-09-17 11:33:24 +01:00
Don Syme
db8206d265 improve improvers 2025-09-17 11:03:23 +01:00
Don Syme
5b70f75d89 allow burner to create PRs 2025-09-17 02:41:38 +01:00
Don Syme
81da4be228 backlog burner 2025-09-17 02:20:48 +01:00
Don Syme
ba4c9238c0 add daily backlog burner 2025-09-17 02:03:48 +01:00
Don Syme
ee083a2e6c
Daily Test Coverage Improver: Add comprehensive API AST map tests (#7890) 
* Add comprehensive tests for AST map API functions

Improved test coverage from 0% to 84% for src/api/api_ast_map.cpp by adding comprehensive tests for:
- Basic map operations (creation, insertion, lookup, size)
- Map manipulation (overwrite values, erase entries, reset)
- Reference counting (inc_ref/dec_ref)
- String representation (to_string function)

This contributes 94 newly covered lines to overall project test coverage.

🤖 Generated with [Claude Code](https://claude.ai/code)

Co-Authored-By: Claude <noreply@anthropic.com>

* staged files

* Delete coverage-steps.log

* Delete coverage-summary.txt

* Delete coverage.html

* Delete z3.log

---------

Co-authored-by: Daily Test Coverage Improver <github-actions[bot]@users.noreply.github.com>
Co-authored-by: Claude <noreply@anthropic.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-16 17:26:07 -07:00
Lev Nachmanson
9b88aaf134 determine parameter evaluation order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-09-16 16:32:46 -07:00
Don Syme
05ba67f432 Merge branch 'master' of https://github.com/Z3Prover/z3 2025-09-17 00:04:31 +01:00
Don Syme
647c8cc6c1 add roles 2025-09-17 00:04:24 +01:00
Don Syme
44d2bba3e5
Add comprehensive tests for API algebraic number functions (#7888) 
- Created new test file api_algebraic.cpp with tests for all algebraic API functions
- Tests cover basic operations (add, sub, mul, div, power, root)
- Tests cover comparison operations (lt, le, gt, ge, eq, neq)
- Tests cover sign detection (is_zero, is_pos, is_neg, sign)
- Tests cover algebraic value detection (is_value)
- Added comprehensive test cases for rational numbers and fractions
- Updated main.cpp and CMakeLists.txt to include the new test module

Coverage improvements:
- src/api/api_algebraic.cpp: 0% -> 52% (136/258 lines covered)
- Overall project coverage: ~47% (gained 71 covered lines)

Co-authored-by: Daily Test Coverage Improver <github-actions[bot]@users.noreply.github.com>
 2025-09-16 15:32:23 -07:00
Don Syme
6d3daa5338 add ask and pr-fix 2025-09-16 23:31:01 +01:00
Don Syme
75a6e7a379 update improvers 2025-09-16 23:27:26 +01:00
Don Syme
ce81aa9078
Merge pull request #7886 from Z3Prover/fix-coverage-merge-mode-3c3ea7b0579fb998 
Daily Test Coverage Improver: Fix coverage report generation
 2025-09-16 18:07:10 +01:00
Nikolaj Bjorner
9069a35b69
Update wip.yml 2025-09-16 09:57:37 -07:00
Daily Test Coverage Improver
6926a4e2ca Fix coverage report generation with merge-mode-functions=separate 
- Add --merge-mode-functions=separate flag to all gcovr commands
- Resolves AssertionError with C++ template destructors on multiple lines
- Fixes coverage HTML and text report generation
- Coverage reports now generate successfully without merge conflicts
 2025-09-16 16:03:11 +00:00
Don Syme
40a60f10ce update token 2025-09-16 16:25:14 +01:00
Don Syme
1aeef3bf81 update agentics 2025-09-16 13:10:58 +01:00
dependabot[bot]
96996bf9ec
Bump actions/github-script from 7 to 8 (#7882) 
Bumps [actions/github-script](https://github.com/actions/github-script) from 7 to 8.
- [Release notes](https://github.com/actions/github-script/releases)
- [Commits](https://github.com/actions/github-script/compare/v7...v8)

---
updated-dependencies:
- dependency-name: actions/github-script
  dependency-version: '8'
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
 2025-09-15 16:40:27 -07:00
dependabot[bot]
7d6ff3fae4
Bump anthropics/claude-code-base-action from 0.0.56 to 0.0.63 (#7881) 
Bumps [anthropics/claude-code-base-action](https://github.com/anthropics/claude-code-base-action) from 0.0.56 to 0.0.63.
- [Release notes](https://github.com/anthropics/claude-code-base-action/releases)
- [Commits](https://github.com/anthropics/claude-code-base-action/compare/v0.0.56...v0.0.63)

---
updated-dependencies:
- dependency-name: anthropics/claude-code-base-action
  dependency-version: 0.0.63
  dependency-type: direct:production
  update-type: version-update:semver-patch
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
 2025-09-15 16:40:18 -07:00
dependabot[bot]
c4675cb463
Bump actions/checkout from 3 to 5 (#7880) 
Bumps [actions/checkout](https://github.com/actions/checkout) from 3 to 5.
- [Release notes](https://github.com/actions/checkout/releases)
- [Changelog](https://github.com/actions/checkout/blob/main/CHANGELOG.md)
- [Commits](https://github.com/actions/checkout/compare/v3...v5)

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

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
 2025-09-15 16:40:07 -07:00
Nikolaj Bjorner
6752be7263
Remove unused variable in polynomial.cpp 
Removed unused variable 'sz2' in polynomial multiplication.
 2025-09-15 10:43:09 -07:00
Nikolaj Bjorner
b0bc41457f
Update polynomial.cpp 2025-09-15 10:41:56 -07:00
Nikolaj Bjorner
58bab093d1
Change MSVC build trigger to scheduled cron job 
Updated workflow to schedule builds every two days.
 2025-09-15 10:36:58 -07:00
Nikolaj Bjorner
9a91ba1955
Change MSVC Clang-CL build trigger to scheduled 
Updated workflow to trigger on a schedule instead of push and pull_request events.
 2025-09-15 10:36:42 -07:00
Nikolaj Bjorner
01da267988
Update Pyodide workflow to use scheduled builds 2025-09-15 10:35:44 -07:00
Nikolaj Bjorner
93333eca66
Change GitHub Actions trigger to scheduled 2025-09-15 10:35:14 -07:00
Nikolaj Bjorner
c496787923
Change coverage schedule to run every two days 2025-09-15 10:34:59 -07:00
Nikolaj Bjorner
ff6a4f9b12
Add scheduled trigger for Android build workflow 2025-09-15 10:34:32 -07:00
Nikolaj Bjorner
7efcda2674 Update polynomial.cpp 2025-09-15 09:46:29 -07:00
Nikolaj Bjorner
f4a87d4f61 shelve experiment with a variant of geobuckets 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-15 09:46:29 -07:00
Don Syme
7b4194994a
Merge pull request #7878 from Z3Prover/perf/daily-perf-improver-build-steps-8936dfa90701cfcd 
Daily Perf Improver: Updates to complete configuration
 2025-09-15 15:12:45 +01:00
Daily Perf Improver
a31656a705 Daily Perf Improver: Add build steps configuration 
This commit adds the GitHub Action configuration file for setting up
the Z3 build environment for performance development work.

The action includes:
- Installing build dependencies (cmake, ninja, python3, etc.)
- Cleaning any polluted source tree from previous Python builds
- Configuring CMake with RelWithDebInfo for performance work
- Building Z3 and test executables
- Cloning z3test repository for benchmarks
- Setting up performance measurement tools
- Creating micro-benchmark infrastructure

This configuration is based on the research and plan outlined in
issue #7872 and follows the standard CMake build process documented
in README-CMake.md.

> AI-generated content by [Daily Perf Improver](https://github.com/Z3Prover/z3/actions/runs/17735701277) may contain mistakes.
 2025-09-15 14:05:21 +00:00
Don Syme
25a79d73b1 update workflows and use token for safe outputs 2025-09-15 15:00:15 +01:00
Copilot
41491d79be
Add comprehensive test coverage for math/lp and math/polynomial modules (#7877) 
* Initial plan

* Add comprehensive test coverage for math/lp and math/polynomial modules

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Finalize test coverage improvements with corrected implementations

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix compilation errors in test files

- Fix algebraic_numbers.cpp: Simplified tests to use basic algebraic operations without polynomial manager dependencies
- Fix polynomial_factorization.cpp: Corrected upolynomial::factors usage and API calls
- Fix nla_intervals.cpp: Changed 'solver' to 'nla::core' and fixed lar_solver constructor
- Fix monomial_bounds.cpp: Updated class names and method calls to match current NLA API

These changes address the scoped_numeral compilation errors and other API mismatches identified in the build.

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix monomial bounds test assertions to use consistent values

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2025-09-14 14:57:21 -07:00
Nikolaj Bjorner
6e767795db set status to unknown 2025-09-14 13:43:10 -07:00
Nikolaj Bjorner
928a2e7cf2 update python doc tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-14 10:56:26 -07:00
Nikolaj Bjorner
0d0dd0315a evaluate unhandled arithmetic operators based on an initialized model #7876 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-14 06:45:36 -07:00
Nikolaj Bjorner
3c897b450f add rewrite rules for update-field under accessors and recognizers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-14 06:14:42 -07:00
Nikolaj Bjorner
6afa1c5be8 add back coverage module 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-14 05:16:54 -07:00
Nikolaj Bjorner
84bf34266b put back shortcut for square test. Remove assumption in unit test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-14 05:00:47 -07:00
Nikolaj Bjorner
8158a500d4 remove shortcut as it breaks current contract 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-14 04:49:27 -07:00
Nikolaj Bjorner
573c2cb8f7 micro tuning perfect square test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-13 20:10:43 -07:00
Nuno Lopes
c350ddf990 remove a few useless dynamic casts 2025-09-13 21:06:55 +01:00
Don Syme
f0c788581a
Merge pull request #7871 from Z3Prover/add-workflow-githubnext-agentics-daily-perf-improver-9993 
Add workflow: githubnext/agentics/daily-perf-improver
 2025-09-12 23:47:59 +01:00
Don Syme
095e0f5db8 Add workflow: githubnext/agentics/daily-perf-improver 2025-09-12 23:47:24 +01:00
Don Syme
66acd4aa7b
Merge pull request #7870 from Z3Prover/daily-test-coverage-improver-config-6b08d6955c91424a 
Daily test coverage improver config
 2025-09-12 23:45:56 +01:00
Don Syme
93b00d9fcb
Delete coverage-steps.log 2025-09-12 23:45:41 +01:00