Daily Test Coverage Improver: Add comprehensive API Datalog tests

[dsyme]

Summary

This PR adds comprehensive test coverage for Z3's Datalog/fixedpoint API functions, improving coverage from 0% to 17% (84/486 lines) in src/api/api_datalog.cpp.

Problem Found

The Datalog API functions had zero test coverage despite being important functionality for logic programming and fixedpoint computation:

• src/api/api_datalog.cpp: 0% coverage (0/486 lines covered)
• No existing tests exercised the Datalog/fixedpoint API layer
• Important functionality like finite domain sorts, fixedpoint creation, and basic operations was untested

Actions Taken

• Created comprehensive test suite in src/test/api_datalog.cpp
• Added test registration in src/test/main.cpp and src/test/CMakeLists.txt
• Implemented tests for core API functions:
  • Z3_mk_finite_domain_sort - Create finite domain sorts with specified size
  • Z3_get_finite_domain_sort_size - Retrieve size of finite domain sorts
  • Z3_mk_fixedpoint - Create fixedpoint context
  • Z3_fixedpoint_inc_ref/Z3_fixedpoint_dec_ref - Reference counting
  • Z3_fixedpoint_to_string - String conversion for debugging
  • Z3_fixedpoint_get_statistics - Statistics retrieval
  • Z3_fixedpoint_get_reason_unknown - Reason for unknown results
• Comprehensive test cases covering:
  • Basic functionality with valid inputs
  • Error conditions and edge cases (non-finite domain sorts)
  • Reference counting and memory management
  • Empty fixedpoint contexts
  • String operations for debugging output

Test Coverage Results

Before:

• src/api/api_datalog.cpp: 0% coverage (0/486 lines)
• Overall project coverage: 46% (estimated from previous reports)

After:

• src/api/api_datalog.cpp: 17% coverage (84/486 lines) - +84 lines covered
• Overall project coverage improvement: Significant increase in API datalog functions

Coverage improvement breakdown:

• 84 new lines covered in Datalog API functions
• Major functions now tested: Finite domain sorts, fixedpoint creation, reference counting, string operations, statistics
• Remaining uncovered areas: Query operations, rule addition, parsing, complex fixedpoint manipulations

Replicating the Test Coverage Measurements

Build and run the new test:

# Build test executable
ninja test-z3

# Run the specific API datalog test
./test-z3 api_datalog

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

Expected Output:

PASS
src/api/api_datalog.cpp                      486      84    17%   [detailed line coverage]

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_datalog

# 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 uncovered areas in api_datalog.cpp (17% → 100% potential):

• Query Operations - Z3_fixedpoint_query, Z3_fixedpoint_query_relations for executing datalog queries
• Rule Management - Z3_fixedpoint_add_rule for adding inference rules
• Fact Management - Z3_fixedpoint_add_fact for adding base facts
• Parsing Functions - Z3_fixedpoint_from_string, Z3_fixedpoint_from_file for loading datalog programs
• Answer Extraction - Z3_fixedpoint_get_answer for retrieving query results
• Predicate Registration - Z3_fixedpoint_set_predicate_representation for configuring predicates
• Relation Properties - Z3_get_relation_arity, Z3_get_relation_column for introspection

Other high-impact areas for future coverage improvements:

• 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

Workflow Details

Bash Commands Run

• git checkout -b daily-test-improver-api-datalog-tests
• ninja test-z3
• ./test-z3 api_datalog
• gcovr --merge-mode-functions=separate --gcov-ignore-parse-errors --gcov-executable "llvm-cov gcov" --filter ".*api_datalog.*" .
• git add src/test/api_datalog.cpp src/test/main.cpp src/test/CMakeLists.txt
• git commit --author "Daily Test Coverage Improver <github-actions[bot]@users.noreply.github.com>" -m "..."

Web Searches Performed

None

Web Pages Fetched

None

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

Generated by Agentic Workflow Run