z3-src 500.0.0

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

/*++
Copyright (c) 2024 Microsoft Corporation

Module Name:

    monomial_bounds.cpp

Abstract:

    Tests for monomial bounds functionality in math/lp

Author:

    Test Coverage Improvement

Revision History:

--*/

#include "math/lp/monomial_bounds.h"
#include "math/lp/nla_core.h"
#include "math/lp/lar_solver.h"
#include "util/rational.h"
#include "util/rlimit.h"

namespace nla {

void test_monomial_bounds_basic() {
    std::cout << "test_monomial_bounds_basic\n";
    
    lp::lar_solver s;
    reslimit rl;
    params_ref p;
    
    // Create variables x, y, z and their product xyz
    lpvar x = s.add_var(0, true);
    lpvar y = s.add_var(1, true);  
    lpvar z = s.add_var(2, true);
    lpvar xyz = s.add_var(3, true);
    
    // Set up solver with monomial bounds
    nla::core nla_solver(s, p, rl);
    
    // Create monomial xyz = x * y * z
    vector<lpvar> vars;
    vars.push_back(x);
    vars.push_back(y);
    vars.push_back(z);
    nla_solver.add_monic(xyz, vars.size(), vars.begin());
    
    // Set values that are consistent with monomial constraint
    s.set_column_value_test(x, lp::impq(rational(2)));
    s.set_column_value_test(y, lp::impq(rational(3)));
    s.set_column_value_test(z, lp::impq(rational(4)));
    s.set_column_value_test(xyz, lp::impq(rational(24))); // 2*3*4 = 24
    
    // Test that this is consistent
    lbool result = nla_solver.test_check();
    VERIFY(result != l_false); // Should be satisfiable or unknown
}

void test_monomial_bounds_propagation() {
    std::cout << "test_monomial_bounds_propagation\n";
    
    lp::lar_solver s;
    reslimit rl;
    params_ref p;
    
    // Create variables for testing bound propagation
    lpvar x = s.add_var(0, true);
    lpvar y = s.add_var(1, true);
    lpvar xy = s.add_var(2, true);
    
    nla::core nla_solver(s, p, rl);
    
    // Create monomial xy = x * y
    vector<lpvar> vars;
    vars.push_back(x);
    vars.push_back(y);
    nla_solver.add_monic(xy, vars.size(), vars.begin());
    
    // Test case where one variable is zero - should produce xy = 0
    s.set_column_value_test(x, lp::impq(rational(0)));
    s.set_column_value_test(y, lp::impq(rational(5)));
    s.set_column_value_test(xy, lp::impq(rational(0))); // 0 * 5 = 0
    
    lbool result = nla_solver.test_check();
    VERIFY(result != l_false); // Should be consistent
}

void test_monomial_bounds_intervals() {
    std::cout << "test_monomial_bounds_intervals\n";
    
    lp::lar_solver s;
    reslimit rl;
    params_ref p;
    
    // Test interval-based monomial bounds
    lpvar a = s.add_var(0, true);
    lpvar b = s.add_var(1, true);
    lpvar ab = s.add_var(2, true);
    
    nla::core nla_solver(s, p, rl);
    
    vector<lpvar> vars;
    vars.push_back(a);
    vars.push_back(b);
    nla_solver.add_monic(ab, vars.size(), vars.begin());
    
    // Set up consistent bounds on variables
    s.set_column_value_test(a, lp::impq(rational(1), rational(2))); // 0.5
    s.set_column_value_test(b, lp::impq(rational(3), rational(2))); // 1.5
    s.set_column_value_test(ab, lp::impq(rational(3), rational(4))); // 0.5 * 1.5 = 0.75
    
    lbool result = nla_solver.test_check();
    VERIFY(result != l_false); // Should be consistent
}

void test_monomial_bounds_power() {
    std::cout << "test_monomial_bounds_power\n";
    
    lp::lar_solver s;
    reslimit rl;
    params_ref p;
    
    // Test power/repeated variable cases
    lpvar x = s.add_var(0, true);
    lpvar x_squared = s.add_var(1, true);
    
    nla::core nla_solver(s, p, rl);
    
    // Create x^2 = x * x
    vector<lpvar> vars;
    vars.push_back(x);
    vars.push_back(x);
    nla_solver.add_monic(x_squared, vars.size(), vars.begin());
    
    // Test with negative value
    s.set_column_value_test(x, lp::impq(rational(-3)));
    s.set_column_value_test(x_squared, lp::impq(rational(9))); // (-3)^2 = 9
    
    lbool result = nla_solver.test_check();
    VERIFY(result != l_false); // Should be consistent
}

void test_monomial_bounds_linear_case() {
    std::cout << "test_monomial_bounds_linear_case\n";
    
    lp::lar_solver s;
    reslimit rl;
    params_ref p;
    
    // Test linear monomial (degree 1)
    lpvar x = s.add_var(0, true);
    lpvar mx = s.add_var(1, true); // monomial of just x
    
    nla::core nla_solver(s, p, rl);
    
    vector<lpvar> vars;
    vars.push_back(x);
    nla_solver.add_monic(mx, vars.size(), vars.begin());
    
    s.set_column_value_test(x, lp::impq(rational(7)));
    s.set_column_value_test(mx, lp::impq(rational(7))); // mx = x = 7 (linear case)
    
    lbool result = nla_solver.test_check();
    VERIFY(result != l_false); // Should be consistent
}

void test_monomial_bounds() {
    test_monomial_bounds_basic();
    test_monomial_bounds_propagation();
    test_monomial_bounds_intervals();
    test_monomial_bounds_power();
    test_monomial_bounds_linear_case();
}

} // namespace nla

void tst_monomial_bounds() {
    nla::test_monomial_bounds();
}