z3-src 501.0.1

Source distribution of the Z3 SMT solver, for use as a build dependency
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199

/*++
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);
    }

    // Test thresholds that exceed the number of arguments.
    // The conversion to cardinality constraints in the sat solver used to
    // underflow on these, turning satisfiable constraints into unsatisfiable ones.
    {
        Z3_ast vars[] = {x, y, z};
        Z3_tactic sat_tactic = Z3_mk_tactic(ctx, "sat");
        Z3_tactic_inc_ref(ctx, sat_tactic);
        Z3_solver s = Z3_mk_solver_from_tactic(ctx, sat_tactic);
        Z3_solver_inc_ref(ctx, s);

        Z3_solver_assert(ctx, s, Z3_mk_atmost(ctx, 3, vars, 5));
        ENSURE(Z3_solver_check(ctx, s) == Z3_L_TRUE);

        Z3_solver_reset(ctx, s);
        Z3_solver_assert(ctx, s, Z3_mk_not(ctx, Z3_mk_atleast(ctx, 3, vars, 5)));
        ENSURE(Z3_solver_check(ctx, s) == Z3_L_TRUE);

        Z3_solver_reset(ctx, s);
        Z3_solver_assert(ctx, s, Z3_mk_atleast(ctx, 3, vars, 5));
        ENSURE(Z3_solver_check(ctx, s) == Z3_L_FALSE);

        Z3_solver_reset(ctx, s);
        Z3_solver_assert(ctx, s, Z3_mk_not(ctx, Z3_mk_atmost(ctx, 3, vars, 5)));
        ENSURE(Z3_solver_check(ctx, s) == Z3_L_FALSE);

        Z3_solver_dec_ref(ctx, s);
        Z3_tactic_dec_ref(ctx, sat_tactic);
    }

    Z3_del_context(ctx);
}