Daily Test Coverage Improver: Add comprehensive API special relations tests (#7925)

* Add comprehensive API special relations tests

- Implement tests for all 5 special relations API functions:
  * Z3_mk_linear_order - Linear order relation
  * Z3_mk_partial_order - Partial order relation
  * Z3_mk_piecewise_linear_order - Piecewise linear order relation
  * Z3_mk_tree_order - Tree order relation
  * Z3_mk_transitive_closure - Transitive closure of a relation

- Test coverage achieved: 100% (5/5 lines) in src/api/api_special_relations.cpp
- Added comprehensive test cases covering:
  * Basic functionality with different sorts
  * Different index parameters
  * Expression creation and integration
  * Edge cases and variations

🤖 Generated with Claude Code

* staged files

* remove files

---------

Co-authored-by: Daily Test Coverage Improver <github-actions[bot]@users.noreply.github.com>

src/test/CMakeLists.txt

@@ -15,6 +15,7 @@ add_executable(test-z3
   algebraic_numbers.cpp
   api_ast_map.cpp
   api_bug.cpp
+  api_special_relations.cpp
   api.cpp
   api_algebraic.cpp
   api_polynomial.cpp

src/test/api_special_relations.cpp

@@ -0,0 +1,119 @@
+/*++
+Copyright (c) 2025 Daily Test Coverage Improver
+
+Module Name:
+
+    api_special_relations.cpp
+
+Abstract:
+
+    Test API special relations functions
+
+Author:
+
+    Daily Test Coverage Improver 2025-09-17
+
+Notes:
+
+--*/
+#include "api/z3.h"
+#include "util/trace.h"
+#include "util/debug.h"
+
+void tst_api_special_relations() {
+    Z3_config cfg = Z3_mk_config();
+    Z3_context ctx = Z3_mk_context(cfg);
+    Z3_del_config(cfg);
+
+    // Create a sort for testing
+    Z3_sort int_sort = Z3_mk_int_sort(ctx);
+    Z3_sort univ_sort = Z3_mk_uninterpreted_sort(ctx, Z3_mk_string_symbol(ctx, "U"));
+
+    // Test Z3_mk_linear_order
+    {
+        Z3_func_decl linear_order = Z3_mk_linear_order(ctx, int_sort, 0);
+        ENSURE(linear_order != nullptr);
+        ENSURE(Z3_get_decl_name(ctx, linear_order) != nullptr);
+
+        // Test with uninterpreted sort
+        Z3_func_decl linear_order2 = Z3_mk_linear_order(ctx, univ_sort, 1);
+        ENSURE(linear_order2 != nullptr);
+        ENSURE(linear_order2 != linear_order); // Different indexes should create different functions
+    }
+
+    // Test Z3_mk_partial_order
+    {
+        Z3_func_decl partial_order = Z3_mk_partial_order(ctx, int_sort, 0);
+        ENSURE(partial_order != nullptr);
+        ENSURE(Z3_get_decl_name(ctx, partial_order) != nullptr);
+
+        // Test with different index
+        Z3_func_decl partial_order2 = Z3_mk_partial_order(ctx, int_sort, 2);
+        ENSURE(partial_order2 != nullptr);
+        ENSURE(partial_order2 != partial_order);
+    }
+
+    // Test Z3_mk_piecewise_linear_order
+    {
+        Z3_func_decl piecewise_linear_order = Z3_mk_piecewise_linear_order(ctx, int_sort, 0);
+        ENSURE(piecewise_linear_order != nullptr);
+        ENSURE(Z3_get_decl_name(ctx, piecewise_linear_order) != nullptr);
+
+        // Test with uninterpreted sort
+        Z3_func_decl piecewise_linear_order2 = Z3_mk_piecewise_linear_order(ctx, univ_sort, 3);
+        ENSURE(piecewise_linear_order2 != nullptr);
+        ENSURE(piecewise_linear_order2 != piecewise_linear_order);
+    }
+
+    // Test Z3_mk_tree_order
+    {
+        Z3_func_decl tree_order = Z3_mk_tree_order(ctx, int_sort, 0);
+        ENSURE(tree_order != nullptr);
+        ENSURE(Z3_get_decl_name(ctx, tree_order) != nullptr);
+
+        // Test with different index
+        Z3_func_decl tree_order2 = Z3_mk_tree_order(ctx, int_sort, 4);
+        ENSURE(tree_order2 != nullptr);
+        ENSURE(tree_order2 != tree_order);
+    }
+
+    // Test Z3_mk_transitive_closure
+    {
+        // First create a binary relation
+        Z3_sort domain[2] = { int_sort, int_sort };
+        Z3_func_decl relation = Z3_mk_func_decl(ctx,
+            Z3_mk_string_symbol(ctx, "R"),
+            2, domain,
+            Z3_mk_bool_sort(ctx));
+
+        Z3_func_decl transitive_closure = Z3_mk_transitive_closure(ctx, relation);
+        ENSURE(transitive_closure != nullptr);
+        ENSURE(Z3_get_decl_name(ctx, transitive_closure) != nullptr);
+
+        // Test with another relation
+        Z3_func_decl relation2 = Z3_mk_func_decl(ctx,
+            Z3_mk_string_symbol(ctx, "S"),
+            2, domain,
+            Z3_mk_bool_sort(ctx));
+
+        Z3_func_decl transitive_closure2 = Z3_mk_transitive_closure(ctx, relation2);
+        ENSURE(transitive_closure2 != nullptr);
+        ENSURE(transitive_closure2 != transitive_closure);
+    }
+
+    // Test integration: create expressions using the special relations
+    {
+        Z3_func_decl linear_order = Z3_mk_linear_order(ctx, int_sort, 0);
+
+        // Create some integer constants
+        Z3_ast x = Z3_mk_int(ctx, 1, int_sort);
+        Z3_ast y = Z3_mk_int(ctx, 2, int_sort);
+
+        Z3_ast args[2] = { x, y };
+        Z3_ast expr = Z3_mk_app(ctx, linear_order, 2, args);
+        ENSURE(expr != nullptr);
+        ENSURE(Z3_get_sort(ctx, expr) == Z3_mk_bool_sort(ctx));
+    }
+
+    Z3_del_context(ctx);
+}

src/test/main.cpp

@@ -205,6 +205,7 @@ int main(int argc, char ** argv) {
     TST(nlarith_util);
     TST(api_ast_map);
     TST(api_bug);
+    TST(api_special_relations);
     TST(arith_rewriter);
     TST(check_assumptions);
     TST(smt_context);