Daily Test Coverage Improver: Add comprehensive API algebraic number tests #7888
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Summary
This PR adds comprehensive test coverage for Z3's algebraic number API functions, significantly improving test coverage from 0% to 52% for the
src/api/api_algebraic.cppmodule.Problem Found
The algebraic number API functions (
Z3_algebraic_*) had zero test coverage despite being a core part of Z3's arithmetic capabilities:src/api/api_algebraic.cpp: 0% coverage (0/258 lines covered)Actions Taken
src/test/api_algebraic.cppsrc/test/main.cppandsrc/test/CMakeLists.txtZ3_algebraic_add,Z3_algebraic_sub,Z3_algebraic_mul,Z3_algebraic_divZ3_algebraic_power,Z3_algebraic_rootZ3_algebraic_lt,Z3_algebraic_le,Z3_algebraic_gt,Z3_algebraic_ge,Z3_algebraic_eq,Z3_algebraic_neqZ3_algebraic_is_zero,Z3_algebraic_is_pos,Z3_algebraic_is_neg,Z3_algebraic_signZ3_algebraic_is_valueChanges in Test Coverage Achieved
Before:
src/api/api_algebraic.cpp: 0% coverage (0/258 lines)After:
src/api/api_algebraic.cpp: 52% coverage (136/258 lines) - +136 lines coveredCoverage improvement breakdown:
Z3_algebraic_is_value, basic arithmetic operations, comparisons, sign detectionZ3_algebraic_roots,Z3_algebraic_eval,Z3_algebraic_get_poly)Validation Commands
To validate the coverage improvements:
Future Improvement Areas
Based on remaining uncovered areas in
api_algebraic.cpp:Z3_algebraic_roots) - requires complex polynomial constructionZ3_algebraic_eval) - needs multivariate polynomial setupZ3_algebraic_get_poly) - requires irrational algebraic numbersOther high-impact areas for future coverage improvements:
src/api/api_commands.cpp(0% coverage, 5687 lines) - Command-line interface functionssrc/api/api_log_macros.cpp(0% coverage, 5333 lines) - API logging infrastructure<details>
<summary>Workflow Details</summary>
Bash Commands Run
git checkout -b daily-test-improver-api-algebraic-testsninja -C build test-z3./build/test-z3 api_algebraicgcovr --merge-mode-functions=separate --gcov-ignore-parse-errors --gcov-executable "llvm-cov gcov" . | grep api_algebraicgit add src/test/api_algebraic.cpp src/test/main.cpp src/test/CMakeLists.txtgit commit --author "Daily Test Coverage Improver <github-actions[bot]@users.noreply.github.com>" -m "..."Web Searches Performed
None
Web Pages Fetched
None
</details>
> AI-generated content by Daily Test Coverage Improver may contain mistakes.