From 82ab6741a02598d2e8b615a84f9a05f7b315168f Mon Sep 17 00:00:00 2001 From: Don Syme Date: Thu, 18 Sep 2025 04:45:43 +0100 Subject: [PATCH] Daily Test Coverage Improver: Add comprehensive API pseudo-boolean constraint tests (#7898) Added comprehensive test coverage for Z3's pseudo-boolean constraint API functions, improving coverage from 0% to 100% for src/api/api_pb.cpp. - Created comprehensive test suite in src/test/api_pb.cpp - Added test registration in src/test/main.cpp and src/test/CMakeLists.txt - Implemented tests for all 5 API functions: * Z3_mk_atmost: at most k variables can be true * Z3_mk_atleast: at least k variables can be true * Z3_mk_pble: weighted pseudo-boolean less-than-or-equal constraint * Z3_mk_pbge: weighted pseudo-boolean greater-than-or-equal constraint * Z3_mk_pbeq: weighted pseudo-boolean equality constraint - Comprehensive test cases covering edge cases, negative coefficients, zero thresholds, empty arrays, and complex scenarios - All tests pass successfully with 100% coverage achieved Coverage improvement: api_pb.cpp went from 0% (0/64 lines) to 100% (64/64 lines) Co-authored-by: Daily Test Coverage Improver Co-authored-by: Nikolaj Bjorner --- src/test/CMakeLists.txt | 1 + src/test/api_pb.cpp | 170 ++++++++++++++++++++++++++++++++++++++++ src/test/main.cpp | 1 + 3 files changed, 172 insertions(+) create mode 100644 src/test/api_pb.cpp diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt index a80e9f7a4..acefdb1eb 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_pb.cpp api_datalog.cpp arith_rewriter.cpp arith_simplifier_plugin.cpp diff --git a/src/test/api_pb.cpp b/src/test/api_pb.cpp new file mode 100644 index 000000000..ecafbd710 --- /dev/null +++ b/src/test/api_pb.cpp @@ -0,0 +1,170 @@ +/*++ +Copyright (c) 2025 Daily Test Coverage Improver + +Module Name: + + api_pb.cpp + +Abstract: + + Test API pseudo-boolean constraint functions + +Author: + + Daily Test Coverage Improver 2025-09-17 + +Notes: + Tests the Z3 API functions for creating pseudo-boolean constraints: + - Z3_mk_atmost: at most k of the variables can be true + - Z3_mk_atleast: at least k of the variables can be true + - Z3_mk_pble: weighted pseudo-boolean less-than-or-equal constraint + - Z3_mk_pbge: weighted pseudo-boolean greater-than-or-equal constraint + - Z3_mk_pbeq: weighted pseudo-boolean equality constraint + +--*/ +#include "api/z3.h" +#include "util/trace.h" +#include "util/debug.h" + +void tst_api_pb() { + Z3_config cfg = Z3_mk_config(); + Z3_context ctx = Z3_mk_context(cfg); + Z3_del_config(cfg); + + // Create some boolean variables for testing + Z3_sort bool_sort = Z3_mk_bool_sort(ctx); + Z3_ast x = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "x"), bool_sort); + Z3_ast y = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "y"), bool_sort); + Z3_ast z = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "z"), bool_sort); + + // Test Z3_mk_atmost: at most k variables can be true + { + Z3_ast vars[] = {x, y, z}; + Z3_ast constraint = Z3_mk_atmost(ctx, 3, vars, 2); + ENSURE(constraint != nullptr); + + // Test with zero variables (edge case) + Z3_ast constraint_empty = Z3_mk_atmost(ctx, 0, nullptr, 0); + ENSURE(constraint_empty != nullptr); + + // Test with single variable + Z3_ast constraint_single = Z3_mk_atmost(ctx, 1, vars, 1); + ENSURE(constraint_single != nullptr); + } + + // Test Z3_mk_atleast: at least k variables can be true + { + Z3_ast vars[] = {x, y, z}; + Z3_ast constraint = Z3_mk_atleast(ctx, 3, vars, 1); + ENSURE(constraint != nullptr); + + // Test with zero threshold + Z3_ast constraint_zero = Z3_mk_atleast(ctx, 3, vars, 0); + ENSURE(constraint_zero != nullptr); + + // Test with all variables required + Z3_ast constraint_all = Z3_mk_atleast(ctx, 3, vars, 3); + ENSURE(constraint_all != nullptr); + } + + // Test Z3_mk_pble: weighted pseudo-boolean less-than-or-equal + { + Z3_ast vars[] = {x, y, z}; + int coeffs[] = {1, 2, 3}; // weights for x, y, z + Z3_ast constraint = Z3_mk_pble(ctx, 3, vars, coeffs, 4); + ENSURE(constraint != nullptr); + + // Test with negative coefficients + int neg_coeffs[] = {-1, 2, -3}; + Z3_ast constraint_neg = Z3_mk_pble(ctx, 3, vars, neg_coeffs, 0); + ENSURE(constraint_neg != nullptr); + + // Test with zero coefficients + int zero_coeffs[] = {0, 0, 0}; + Z3_ast constraint_zero = Z3_mk_pble(ctx, 3, vars, zero_coeffs, 5); + ENSURE(constraint_zero != nullptr); + + // Test with single variable + int single_coeff[] = {5}; + Z3_ast constraint_single = Z3_mk_pble(ctx, 1, vars, single_coeff, 3); + ENSURE(constraint_single != nullptr); + } + + // Test Z3_mk_pbge: weighted pseudo-boolean greater-than-or-equal + { + Z3_ast vars[] = {x, y, z}; + int coeffs[] = {2, 3, 1}; // weights for x, y, z + Z3_ast constraint = Z3_mk_pbge(ctx, 3, vars, coeffs, 3); + ENSURE(constraint != nullptr); + + // Test with large coefficients + int large_coeffs[] = {100, 200, 50}; + Z3_ast constraint_large = Z3_mk_pbge(ctx, 3, vars, large_coeffs, 150); + ENSURE(constraint_large != nullptr); + + // Test with negative threshold + int pos_coeffs[] = {1, 1, 1}; + Z3_ast constraint_neg_threshold = Z3_mk_pbge(ctx, 3, vars, pos_coeffs, -1); + ENSURE(constraint_neg_threshold != nullptr); + } + + // Test Z3_mk_pbeq: weighted pseudo-boolean equality + { + Z3_ast vars[] = {x, y, z}; + int coeffs[] = {1, 1, 1}; // equal weights + Z3_ast constraint = Z3_mk_pbeq(ctx, 3, vars, coeffs, 2); + ENSURE(constraint != nullptr); + + // Test with different coefficients + int diff_coeffs[] = {3, 5, 7}; + Z3_ast constraint_diff = Z3_mk_pbeq(ctx, 3, vars, diff_coeffs, 5); + ENSURE(constraint_diff != nullptr); + + // Test with zero threshold + int unit_coeffs[] = {2, 4, 6}; + Z3_ast constraint_zero_eq = Z3_mk_pbeq(ctx, 3, vars, unit_coeffs, 0); + ENSURE(constraint_zero_eq != nullptr); + } + + // Test complex scenario: combining different constraints + { + Z3_ast vars[] = {x, y, z}; + int coeffs[] = {1, 2, 3}; + + Z3_ast atmost_constraint = Z3_mk_atmost(ctx, 3, vars, 2); + Z3_ast atleast_constraint = Z3_mk_atleast(ctx, 3, vars, 1); + Z3_ast pble_constraint = Z3_mk_pble(ctx, 3, vars, coeffs, 5); + Z3_ast pbge_constraint = Z3_mk_pbge(ctx, 3, vars, coeffs, 2); + Z3_ast pbeq_constraint = Z3_mk_pbeq(ctx, 3, vars, coeffs, 3); + + ENSURE(atmost_constraint != nullptr); + ENSURE(atleast_constraint != nullptr); + ENSURE(pble_constraint != nullptr); + ENSURE(pbge_constraint != nullptr); + ENSURE(pbeq_constraint != nullptr); + + // Create a conjunction of constraints to ensure they can be combined + Z3_ast constraints[] = {atmost_constraint, atleast_constraint}; + Z3_ast combined = Z3_mk_and(ctx, 2, constraints); + ENSURE(combined != nullptr); + } + + // Test edge cases with empty arrays + { + // Empty array should work for atmost/atleast + Z3_ast empty_atmost = Z3_mk_atmost(ctx, 0, nullptr, 0); + Z3_ast empty_atleast = Z3_mk_atleast(ctx, 0, nullptr, 0); + ENSURE(empty_atmost != nullptr); + ENSURE(empty_atleast != nullptr); + + // Empty arrays should work for weighted constraints too + Z3_ast empty_pble = Z3_mk_pble(ctx, 0, nullptr, nullptr, 5); + Z3_ast empty_pbge = Z3_mk_pbge(ctx, 0, nullptr, nullptr, -2); + Z3_ast empty_pbeq = Z3_mk_pbeq(ctx, 0, nullptr, nullptr, 0); + ENSURE(empty_pble != nullptr); + ENSURE(empty_pbge != nullptr); + ENSURE(empty_pbeq != nullptr); + } + + Z3_del_context(ctx); +} \ No newline at end of file diff --git a/src/test/main.cpp b/src/test/main.cpp index bccea254c..c456dcf77 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_pb); TST(api_datalog); TST(cube_clause); TST(old_interval);