Summary

This PR adds comprehensive test coverage for Z3's special relations API functions, achieving 100% coverage for the src/api/api_special_relations.cpp module, which previously had 0% test coverage.

Problem Found

The special relations API functions had zero test coverage despite being important functionality for creating mathematical order relations:

• src/api/api_special_relations.cpp: 0% coverage (0/5 lines covered)
• No existing tests exercised the special relations API layer
• Important functionality like linear orders, partial orders, tree orders, and transitive closures was untested

Actions Taken

• Created comprehensive test suite in src/test/api_special_relations.cpp
• Added test registration in src/test/main.cpp and src/test/CMakeLists.txt
• Implemented tests for all 5 API functions:
  • Z3_mk_linear_order - Create linear order relations with specified indices
  • Z3_mk_partial_order - Create partial order relations
  • Z3_mk_piecewise_linear_order - Create piecewise linear order relations
  • Z3_mk_tree_order - Create tree order relations
  • Z3_mk_transitive_closure - Create transitive closure of binary relations
• Comprehensive test cases covering:
  • Basic functionality with integer and uninterpreted sorts
  • Different index parameters creating distinct functions
  • Integration with existing binary relation functions
  • Expression creation and type checking
  • Edge cases and parameter variations

Test Coverage Results

Before:

• src/api/api_special_relations.cpp: 0% coverage (0/5 lines)
• Overall project coverage: 47% (estimated from previous reports)

After:

• src/api/api_special_relations.cpp: 100% coverage (5/5 lines) - +5 lines covered
• Overall project coverage improvement: Small but complete coverage of special relations API

Coverage improvement achieved: Complete coverage of all special relations API functions with comprehensive testing of functionality and integration.

Replicating the Test Coverage Measurements

Build and run the new test:

# Build test executable
ninja test-z3

# Run the specific API special relations test
./test-z3 api_special_relations

# Generate coverage report to verify improvements  
gcovr --merge-mode-functions=separate --gcov-ignore-parse-errors --gcov-executable "llvm-cov gcov" --filter ".*api_special_relations.*" .

Expected Output:

PASS
src/api/api_special_relations.cpp             5       5   100%

Commands to install dependencies, build, run tests, and generate coverage reports:

# Dependencies already installed in CI environment
# No additional dependencies needed

# Build configuration (already done)
CXXFLAGS="--coverage" CFLAGS="--coverage" LDFLAGS="-lgcov" CC=clang CXX=clang++ \
  cmake -B build -DCMAKE_BUILD_TYPE=Debug -DCMAKE_INSTALL_PREFIX=./build/install -G "Ninja"

# Build and test
ninja test-z3
./test-z3 api_special_relations

# Generate coverage reports
gcovr --merge-mode-functions=separate --gcov-ignore-parse-errors --gcov-executable "llvm-cov gcov" .
gcovr --html coverage.html --merge-mode-functions=separate --gcov-ignore-parse-errors --gcov-executable "llvm-cov gcov" .

Future Improvement Areas

Based on remaining high-impact areas with 0% coverage for other API modules:

• src/api/api_fpa.cpp (0% coverage, 1090 lines) - Floating-point arithmetic API
• src/api/api_commands.cpp (0% coverage, 5687 lines) - Command interface functions

Other areas with partial coverage that could be improved:

• src/api/api_model.cpp (30% coverage, 330 lines) - Model manipulation functions
• src/api/api_numeral.cpp (20% coverage, 329 lines) - Numeral conversion functions
• src/api/api_goal.cpp (50% coverage, 150 lines) - Goal manipulation functions

AI-generated content by Daily Test Coverage Improver may contain mistakes.

Generated by Agentic Workflow Run