1 /*++
2 Copyright (c) 2013 Microsoft Corporation
3
4 Module Name:
5
6 pb_rewriter_def.h
7
8 Abstract:
9
10 Basic rewriting rules for PB constraints.
11
12 Author:
13
14 Nikolaj Bjorner (nbjorner) 2013-14-12
15
16 Notes:
17
18 --*/
19 #pragma once
20
21 #include "ast/rewriter/pb_rewriter.h"
22
23
24 template<typename PBU>
display(std::ostream & out,typename PBU::args_t & args,typename PBU::numeral & k,bool is_eq)25 void pb_rewriter_util<PBU>::display(std::ostream& out, typename PBU::args_t& args, typename PBU::numeral& k, bool is_eq) {
26 for (unsigned i = 0; i < args.size(); ++i) {
27 out << args[i].second << " * ";
28 m_util.display(out, args[i].first);
29 out << " ";
30 if (i+1 < args.size()) out << "+ ";
31 }
32 out << (is_eq?" = ":" >= ") << k << "\n";
33 }
34
35 template<typename PBU>
unique(typename PBU::args_t & args,typename PBU::numeral & k,bool is_eq)36 void pb_rewriter_util<PBU>::unique(typename PBU::args_t& args, typename PBU::numeral& k, bool is_eq) {
37
38 TRACE("pb_verbose", display(tout << "pre-unique:", args, k, is_eq););
39 for (unsigned i = 0; i < args.size(); ++i) {
40 if (m_util.is_negated(args[i].first)) {
41 args[i].first = m_util.negate(args[i].first);
42 k -= args[i].second;
43 args[i].second = -args[i].second;
44 }
45 }
46 // remove constants
47 unsigned j = 0, sz = args.size();
48 for (unsigned i = 0; i < sz; ++i) {
49 if (m_util.is_true(args[i].first)) {
50 k -= args[i].second;
51 }
52 else if (m_util.is_false(args[i].first)) {
53 // no-op
54 }
55 else {
56 args[j++] = args[i];
57 }
58 }
59 args.shrink(j);
60 // sort and coalesce arguments:
61 typename PBU::compare cmp;
62 std::sort(args.begin(), args.end(), cmp);
63
64 // coallesce
65 unsigned i;
66 for (i = 0, j = 1; j < args.size(); ++j) {
67 if (args[i].first == args[j].first) {
68 args[i].second += args[j].second;
69 }
70 else {
71 ++i;
72 args[i] = args[j];
73 }
74 }
75 args.resize(i+1);
76
77 // remove 0s.
78 for (i = 0, j = 0; j < args.size(); ++j) {
79 if (!args[j].second.is_zero()) {
80 if (i != j) {
81 args[i] = args[j];
82 }
83 ++i;
84 }
85 }
86 args.resize(i);
87 TRACE("pb_verbose", display(tout << "post-unique:", args, k, is_eq););
88 }
89
90 template<typename PBU>
normalize(typename PBU::args_t & args,typename PBU::numeral & k,bool is_eq)91 lbool pb_rewriter_util<PBU>::normalize(typename PBU::args_t& args, typename PBU::numeral& k, bool is_eq) {
92 TRACE("pb_verbose", display(tout << "pre-normalize:", args, k, is_eq););
93
94 DEBUG_CODE(
95 bool found = false;
96 for (unsigned i = 0; !found && i < args.size(); ++i) {
97 found = args[i].second.is_zero();
98 }
99 if (found) display(verbose_stream(), args, k, is_eq);
100 SASSERT(!found););
101
102 //
103 // Ensure all coefficients are positive:
104 // c*l + y >= k
105 // <=>
106 // c*(1-~l) + y >= k
107 // <=>
108 // c - c*~l + y >= k
109 // <=>
110 // -c*~l + y >= k - c
111 //
112 typename PBU::numeral sum(0);
113 for (unsigned i = 0; i < args.size(); ++i) {
114 typename PBU::numeral c = args[i].second;
115 if (c.is_neg()) {
116 args[i].second = -c;
117 args[i].first = m_util.negate(args[i].first);
118 k -= c;
119 }
120 sum += args[i].second;
121 }
122 // detect tautologies:
123 if (!is_eq && k <= PBU::numeral::zero()) {
124 args.reset();
125 k = PBU::numeral::zero();
126 return l_true;
127 }
128 if (is_eq && k.is_zero() && args.empty()) {
129 return l_true;
130 }
131
132 // detect infeasible constraints:
133 if (sum < k) {
134 args.reset();
135 k = PBU::numeral::one();
136 return l_false;
137 }
138
139 if (is_eq && k == sum) {
140 for (unsigned i = 0; i < args.size(); ++i) {
141 args[i].second = PBU::numeral::one();
142 }
143 typename PBU::numeral num(args.size());
144 k = num;
145 return l_undef;
146 }
147
148 bool all_int = true;
149 for (unsigned i = 0; all_int && i < args.size(); ++i) {
150 all_int = args[i].second.is_int();
151 }
152
153 if (!all_int) {
154 // normalize to integers.
155 typename PBU::numeral d(denominator(k));
156 for (unsigned i = 0; i < args.size(); ++i) {
157 d = lcm(d, denominator(args[i].second));
158 }
159 SASSERT(!d.is_one());
160 k *= d;
161 for (unsigned i = 0; i < args.size(); ++i) {
162 args[i].second *= d;
163 }
164 }
165
166 if (is_eq && k.is_neg()) {
167 return l_false;
168 }
169 if (is_eq) {
170 TRACE("pb_verbose", display(tout << "post-normalize:", args, k, is_eq););
171 return l_undef;
172 }
173
174 // Ensure the largest coefficient is not larger than k:
175 sum = PBU::numeral::zero();
176 for (unsigned i = 0; i < args.size(); ++i) {
177 typename PBU::numeral c = args[i].second;
178 if (c > k) {
179 args[i].second = k;
180 }
181 sum += args[i].second;
182 }
183 SASSERT(!args.empty());
184
185 // normalize tight inequalities to unit coefficients.
186 if (sum == k) {
187 for (unsigned i = 0; i < args.size(); ++i) {
188 args[i].second = PBU::numeral::one();
189 }
190 typename PBU::numeral num(args.size());
191 k = num;
192 }
193
194 // apply cutting plane reduction:
195 typename PBU::numeral g(0);
196 for (unsigned i = 0; !g.is_one() && i < args.size(); ++i) {
197 typename PBU::numeral c = args[i].second;
198 if (c != k) {
199 if (g.is_zero()) {
200 g = c;
201 }
202 else {
203 g = gcd(g, c);
204 }
205 }
206 }
207 if (g.is_zero()) {
208 // all coefficients are equal to k.
209 for (unsigned i = 0; i < args.size(); ++i) {
210 SASSERT(args[i].second == k);
211 args[i].second = PBU::numeral::one();
212 }
213 k = PBU::numeral::one();
214 }
215 else if (g > PBU::numeral::one()) {
216
217 //
218 // Example 5x + 5y + 2z + 2u >= 5
219 // becomes 3x + 3y + z + u >= 3
220 //
221 typename PBU::numeral k_new = div(k, g);
222 if (!(k % g).is_zero()) { // k_new is the ceiling of k / g.
223 k_new++;
224 }
225 for (unsigned i = 0; i < args.size(); ++i) {
226 SASSERT(args[i].second.is_pos());
227 typename PBU::numeral c = args[i].second;
228 if (c == k) {
229 c = k_new;
230 }
231 else {
232 c = div(c, g);
233 }
234 args[i].second = c;
235 SASSERT(args[i].second.is_pos());
236 }
237 k = k_new;
238 }
239 //
240 // normalize coefficients that fall within a range
241 // k/n <= ... < k/(n-1) for some n = 1,2,...
242 //
243 // e.g, k/n <= min <= max < k/(n-1)
244 // k/min <= n, n-1 < k/max
245 // . floor(k/max) = ceil(k/min) - 1
246 // . floor(k/max) < k/max
247 //
248 // example: k = 5, min = 3, max = 4: 5/3 -> 2 5/4 -> 1, n = 2
249 // replace all coefficients by 1, and k by 2.
250 //
251 if (!k.is_one()) {
252 typename PBU::numeral min = args[0].second, max = args[0].second;
253 for (unsigned i = 1; i < args.size(); ++i) {
254 if (args[i].second < min) min = args[i].second;
255 if (args[i].second > max) max = args[i].second;
256 }
257 SASSERT(min.is_pos());
258 typename PBU::numeral n0 = k/max;
259 typename PBU::numeral n1 = floor(n0);
260 typename PBU::numeral n2 = ceil(k/min) - PBU::numeral::one();
261 if (n1 == n2 && !n0.is_int()) {
262 for (unsigned i = 0; i < args.size(); ++i) {
263 args[i].second = PBU::numeral::one();
264 }
265 k = n1 + PBU::numeral::one();
266 }
267 }
268 TRACE("pb_verbose", display(tout << "post-normalize:", args, k, is_eq););
269 return l_undef;
270 }
271
272 template<typename PBU>
prune(typename PBU::args_t & args,typename PBU::numeral & k,bool is_eq)273 void pb_rewriter_util<PBU>::prune(typename PBU::args_t& args, typename PBU::numeral& k, bool is_eq) {
274 if (is_eq) {
275 return;
276 }
277 typename PBU::numeral nlt(0);
278 unsigned occ = 0;
279 for (unsigned i = 0; nlt < k && i < args.size(); ++i) {
280 if (args[i].second < k) {
281 nlt += args[i].second;
282 ++occ;
283 }
284 }
285 if (0 < occ && nlt < k) {
286 for (unsigned i = 0; i < args.size(); ++i) {
287 if (args[i].second < k) {
288 args[i] = args.back();
289 args.pop_back();
290 --i;
291 }
292 }
293 unique(args, k, is_eq);
294 normalize(args, k, is_eq);
295 }
296 }
297
298