diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt index 66de23e1f..a80e9f7a4 100644 --- a/src/test/CMakeLists.txt +++ b/src/test/CMakeLists.txt @@ -17,6 +17,7 @@ add_executable(test-z3 api_bug.cpp api.cpp api_algebraic.cpp + api_datalog.cpp arith_rewriter.cpp arith_simplifier_plugin.cpp ast.cpp diff --git a/src/test/api_datalog.cpp b/src/test/api_datalog.cpp new file mode 100644 index 000000000..40252514d --- /dev/null +++ b/src/test/api_datalog.cpp @@ -0,0 +1,71 @@ +/*++ +Copyright (c) 2025 Daily Test Coverage Improver + +Module Name: + + api_datalog.cpp + +Abstract: + + Test API datalog/fixedpoint 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_datalog() { + Z3_config cfg = Z3_mk_config(); + Z3_context ctx = Z3_mk_context(cfg); + Z3_del_config(cfg); + + // Test 1: Z3_mk_finite_domain_sort and size functions + { + Z3_symbol name = Z3_mk_string_symbol(ctx, "Domain"); + Z3_sort finite_sort = Z3_mk_finite_domain_sort(ctx, name, 5); + ENSURE(finite_sort != nullptr); + + uint64_t size; + bool success = Z3_get_finite_domain_sort_size(ctx, finite_sort, &size); + ENSURE(success); + ENSURE(size == 5); + + // Test with non-finite domain sort (should fail) + Z3_sort int_sort = Z3_mk_int_sort(ctx); + uint64_t wrong_size; + bool wrong_success = Z3_get_finite_domain_sort_size(ctx, int_sort, &wrong_size); + ENSURE(!wrong_success); + } + + // Test 2: Z3_mk_fixedpoint basic operations + { + Z3_fixedpoint fp = Z3_mk_fixedpoint(ctx); + ENSURE(fp != nullptr); + + // Test reference counting + Z3_fixedpoint_inc_ref(ctx, fp); + Z3_fixedpoint_dec_ref(ctx, fp); + + // Test string conversion (empty fixedpoint) + Z3_string fp_str = Z3_fixedpoint_to_string(ctx, fp, 0, nullptr); + ENSURE(fp_str != nullptr); + + // Test statistics + Z3_stats stats = Z3_fixedpoint_get_statistics(ctx, fp); + ENSURE(stats != nullptr); + + // Test reason unknown + Z3_string reason = Z3_fixedpoint_get_reason_unknown(ctx, fp); + (void)reason; // May be null + + Z3_fixedpoint_dec_ref(ctx, fp); + } + + Z3_del_context(ctx); +} \ No newline at end of file diff --git a/src/test/main.cpp b/src/test/main.cpp index a4f23e92e..bccea254c 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -176,6 +176,7 @@ int main(int argc, char ** argv) { TST(simple_parser); TST(api); TST(api_algebraic); + TST(api_datalog); TST(cube_clause); TST(old_interval); TST(get_implied_equalities);