1 /*++
2 Copyright (c) 2016 Microsoft Corporation
3
4 Module Name:
5
6 pb2bv_rewriter.cpp
7
8 Abstract:
9
10 Conversion from pseudo-booleans to bit-vectors.
11
12 Author:
13
14 Nikolaj Bjorner (nbjorner) 2016-10-23
15
16 Notes:
17
18 --*/
19
20 #include "util/statistics.h"
21 #include "util/lbool.h"
22 #include "util/uint_set.h"
23 #include "util/gparams.h"
24 #include "util/debug.h"
25
26 #include "ast/rewriter/rewriter.h"
27 #include "ast/rewriter/rewriter_def.h"
28 #include "ast/rewriter/pb2bv_rewriter.h"
29 #include "ast/ast_util.h"
30 #include "ast/ast_pp.h"
31 #include "util/sorting_network.h"
32
33
34 static const unsigned g_primes[7] = { 2, 3, 5, 7, 11, 13, 17};
35
36
37 struct pb2bv_rewriter::imp {
38
39 ast_manager& m;
40 params_ref m_params;
41 expr_ref_vector m_lemmas;
42 func_decl_ref_vector m_fresh; // all fresh variables
43 unsigned_vector m_fresh_lim;
44 unsigned m_num_translated;
45 unsigned m_compile_bv;
46 unsigned m_compile_card;
47
48 struct card2bv_rewriter {
49 typedef expr* pliteral;
50 typedef ptr_vector<expr> pliteral_vector;
51 psort_nw<card2bv_rewriter> m_sort;
52 ast_manager& m;
53 imp& m_imp;
54 arith_util au;
55 pb_util pb;
56 bv_util bv;
57 expr_ref_vector m_trail;
58 expr_ref_vector m_args;
59 rational m_k;
60 vector<rational> m_coeffs;
61 bool m_keep_cardinality_constraints;
62 symbol m_pb_solver;
63 unsigned m_min_arity;
64
65 template<lbool is_le>
mk_le_gepb2bv_rewriter::imp::card2bv_rewriter66 expr_ref mk_le_ge(expr_ref_vector& fmls, expr* a, expr* b, expr* bound) {
67 expr_ref x(m), y(m), result(m);
68 unsigned nb = bv.get_bv_size(a);
69 x = bv.mk_zero_extend(1, a);
70 y = bv.mk_zero_extend(1, b);
71 result = bv.mk_bv_add(x, y);
72 x = bv.mk_extract(nb, nb, result);
73 result = bv.mk_extract(nb-1, 0, result);
74 if (is_le != l_false) {
75 fmls.push_back(m.mk_eq(x, bv.mk_numeral(rational::zero(), 1)));
76 fmls.push_back(bv.mk_ule(result, bound));
77 }
78 else {
79 fmls.push_back(m.mk_eq(x, bv.mk_numeral(rational::one(), 1)));
80 fmls.push_back(bv.mk_ule(bound, result));
81 }
82 return result;
83 }
84
85 typedef std::pair<rational, expr_ref> ca;
86
87 struct compare_coeffs {
operator ()pb2bv_rewriter::imp::card2bv_rewriter::compare_coeffs88 bool operator()(ca const& x, ca const& y) const {
89 return x.first > y.first;
90 }
91 };
92
sort_argspb2bv_rewriter::imp::card2bv_rewriter93 void sort_args() {
94 vector<ca> cas;
95 for (unsigned i = 0; i < m_args.size(); ++i) {
96 cas.push_back(std::make_pair(m_coeffs[i], expr_ref(m_args.get(i), m)));
97 }
98 std::sort(cas.begin(), cas.end(), compare_coeffs());
99 m_coeffs.reset();
100 m_args.reset();
101 for (ca const& ca : cas) {
102 m_coeffs.push_back(ca.first);
103 m_args.push_back(ca.second);
104 }
105 }
106
107 template <lbool is_le>
gcd_reducepb2bv_rewriter::imp::card2bv_rewriter108 void gcd_reduce(vector<rational>& coeffs, rational & k) {
109 rational g(0);
110 for (rational const& c : coeffs) {
111 if (!c.is_int())
112 return;
113 g = gcd(g, c);
114 if (g.is_one())
115 return;
116 }
117 if (g.is_zero())
118 return;
119 switch (is_le) {
120 case l_undef:
121 if (!k.is_int())
122 return;
123 g = gcd(k, g);
124 if (g.is_one() || g.is_zero())
125 return;
126 k /= g;
127 break;
128 case l_true:
129 k /= g;
130 k = floor(k);
131 break;
132 case l_false:
133 k /= g;
134 k = ceil(k);
135 break;
136 }
137 for (rational& c : coeffs)
138 c /= g;
139 }
140
141 //
142 // create a circuit of size sz*log(k)
143 // by forming a binary tree adding pairs of values that are assumed <= k,
144 // and in each step we check that the result is <= k by checking the overflow
145 // bit and that the non-overflow bits are <= k.
146 // The procedure for checking >= k is symmetric and checking for = k is
147 // achieved by checking <= k on intermediary addends and the resulting sum is = k.
148 //
149 // is_le = l_true - <=
150 // is_le = l_undef - =
151 // is_le = l_false - >=
152 //
153 template<lbool is_le>
mk_le_gepb2bv_rewriter::imp::card2bv_rewriter154 expr_ref mk_le_ge(rational const & _k) {
155 rational k(_k);
156 //sort_args();
157 gcd_reduce<is_le>(m_coeffs, k);
158 unsigned sz = m_args.size();
159 expr * const* args = m_args.data();
160 TRACE("pb",
161 for (unsigned i = 0; i < sz; ++i) {
162 tout << m_coeffs[i] << "*" << mk_pp(args[i], m) << " ";
163 if (i + 1 < sz && !m_coeffs[i+1].is_neg()) tout << "+ ";
164 }
165 switch (is_le) {
166 case l_true: tout << "<= "; break;
167 case l_undef: tout << "= "; break;
168 case l_false: tout << ">= "; break;
169 }
170 tout << k << "\n";);
171
172 if (k.is_zero()) {
173 if (is_le != l_false) {
174 return expr_ref(m.mk_not(::mk_or(m_args)), m);
175 }
176 else {
177 return expr_ref(m.mk_true(), m);
178 }
179 }
180 if (k.is_neg()) {
181 return expr_ref((is_le == l_false)?m.mk_true():m.mk_false(), m);
182 }
183
184 if (m_pb_solver == "totalizer") {
185 expr_ref result(m);
186 switch (is_le) {
187 case l_true: if (mk_le_tot(sz, args, k, result)) return result; else break;
188 case l_false: if (mk_ge_tot(sz, args, k, result)) return result; else break;
189 case l_undef: break;
190 }
191 }
192
193 if (m_pb_solver == "sorting") {
194 expr_ref result(m);
195 switch (is_le) {
196 case l_true: if (mk_le(sz, args, k, result)) return result; else break;
197 case l_false: if (mk_ge(sz, args, k, result)) return result; else break;
198 case l_undef: if (mk_eq(sz, args, k, result)) return result; else break;
199 }
200 }
201
202 if (m_pb_solver == "segmented") {
203 throw default_exception("segmented encoding is disabled, use a different value for pb.solver");
204 switch (is_le) {
205 case l_true: return mk_seg_le(k);
206 case l_false: return mk_seg_ge(k);
207 case l_undef: break;
208 }
209 }
210
211 if (m_pb_solver == "binary_merge") {
212 expr_ref result = binary_merge(is_le, k);
213 if (result) return result;
214 }
215
216 // fall back to divide and conquer encoding.
217 SASSERT(k.is_pos());
218 expr_ref zero(m), bound(m);
219 expr_ref_vector es(m), fmls(m);
220 unsigned nb = k.get_num_bits();
221 zero = bv.mk_numeral(rational(0), nb);
222 bound = bv.mk_numeral(k, nb);
223 for (unsigned i = 0; i < sz; ++i) {
224 SASSERT(!m_coeffs[i].is_neg());
225 if (m_coeffs[i] > k) {
226 if (is_le != l_false) {
227 fmls.push_back(m.mk_not(args[i]));
228 }
229 else {
230 fmls.push_back(args[i]);
231 }
232 }
233 else {
234 es.push_back(mk_ite(args[i], bv.mk_numeral(m_coeffs[i], nb), zero));
235 }
236 }
237 while (es.size() > 1) {
238 for (unsigned i = 0; i + 1 < es.size(); i += 2) {
239 es[i/2] = mk_le_ge<is_le>(fmls, es[i].get(), es[i+1].get(), bound);
240 }
241 if ((es.size() % 2) == 1) {
242 es[es.size()/2] = es.back();
243 }
244 es.shrink((1 + es.size())/2);
245 }
246 switch (is_le) {
247 case l_true:
248 return ::mk_and(fmls);
249 case l_false:
250 if (!es.empty()) {
251 fmls.push_back(bv.mk_ule(bound, es.back()));
252 }
253 return ::mk_or(fmls);
254 case l_undef:
255 if (es.empty()) {
256 fmls.push_back(m.mk_bool_val(k.is_zero()));
257 }
258 else {
259 fmls.push_back(m.mk_eq(bound, es.back()));
260 }
261 return ::mk_and(fmls);
262 default:
263 UNREACHABLE();
264 return expr_ref(m.mk_true(), m);
265 }
266 }
267
268 /**
269 \brief Totalizer encoding. Based on a version by Miguel.
270 */
271
mk_le_totpb2bv_rewriter::imp::card2bv_rewriter272 bool mk_le_tot(unsigned sz, expr * const * args, rational const& _k, expr_ref& result) {
273 SASSERT(sz == m_coeffs.size());
274 if (!_k.is_unsigned() || sz == 0) return false;
275 unsigned k = _k.get_unsigned();
276 expr_ref_vector args1(m);
277 rational bound;
278 flip(sz, args, args1, _k, bound);
279 if (bound.get_unsigned() < k) {
280 return mk_ge_tot(sz, args1.data(), bound, result);
281 }
282 if (k > 20) {
283 return false;
284 }
285 result = m.mk_not(bounded_addition(sz, args, k + 1));
286 TRACE("pb", tout << result << "\n";);
287 return true;
288 }
289
mk_ge_totpb2bv_rewriter::imp::card2bv_rewriter290 bool mk_ge_tot(unsigned sz, expr * const * args, rational const& _k, expr_ref& result) {
291 SASSERT(sz == m_coeffs.size());
292 if (!_k.is_unsigned() || sz == 0) return false;
293 unsigned k = _k.get_unsigned();
294 expr_ref_vector args1(m);
295 rational bound;
296 flip(sz, args, args1, _k, bound);
297 if (bound.get_unsigned() < k) {
298 return mk_le_tot(sz, args1.data(), bound, result);
299 }
300 if (k > 20) {
301 return false;
302 }
303 result = bounded_addition(sz, args, k);
304 TRACE("pb", tout << result << "\n";);
305 return true;
306 }
307
flippb2bv_rewriter::imp::card2bv_rewriter308 void flip(unsigned sz, expr* const* args, expr_ref_vector& args1, rational const& k, rational& bound) {
309 bound = -k;
310 for (unsigned i = 0; i < sz; ++i) {
311 args1.push_back(mk_not(args[i]));
312 bound += m_coeffs[i];
313 }
314 }
315
bounded_additionpb2bv_rewriter::imp::card2bv_rewriter316 expr_ref bounded_addition(unsigned sz, expr * const * args, unsigned k) {
317 SASSERT(sz > 0);
318 expr_ref result(m);
319 vector<expr_ref_vector> es;
320 vector<unsigned_vector> coeffs;
321 for (unsigned i = 0; i < m_coeffs.size(); ++i) {
322 unsigned_vector v;
323 expr_ref_vector e(m);
324 unsigned c = m_coeffs[i].get_unsigned();
325 v.push_back(c >= k ? k : c);
326 e.push_back(args[i]);
327 es.push_back(e);
328 coeffs.push_back(v);
329 }
330 while (es.size() > 1) {
331 for (unsigned i = 0; i + 1 < es.size(); i += 2) {
332 expr_ref_vector o(m);
333 unsigned_vector oc;
334 tot_adder(es[i], coeffs[i], es[i + 1], coeffs[i + 1], k, o, oc);
335 es[i / 2].set(o);
336 coeffs[i / 2] = oc;
337 }
338 if ((es.size() % 2) == 1) {
339 es[es.size() / 2].set(es.back());
340 coeffs[es.size() / 2] = coeffs.back();
341 }
342 es.shrink((1 + es.size())/2);
343 coeffs.shrink((1 + coeffs.size())/2);
344 }
345 SASSERT(coeffs.size() == 1);
346 SASSERT(coeffs[0].back() <= k);
347 if (coeffs[0].back() == k) {
348 result = es[0].back();
349 }
350 else {
351 result = m.mk_false();
352 }
353 return result;
354 }
355
tot_adderpb2bv_rewriter::imp::card2bv_rewriter356 void tot_adder(expr_ref_vector const& l, unsigned_vector const& lc,
357 expr_ref_vector const& r, unsigned_vector const& rc,
358 unsigned k,
359 expr_ref_vector& o, unsigned_vector & oc) {
360 SASSERT(l.size() == lc.size());
361 SASSERT(r.size() == rc.size());
362 uint_set sums;
363 vector<expr_ref_vector> trail;
364 u_map<unsigned> sum2def;
365 for (unsigned i = 0; i <= l.size(); ++i) {
366 for (unsigned j = (i == 0) ? 1 : 0; j <= r.size(); ++j) {
367 unsigned sum = std::min(k, ((i == 0) ? 0 : lc[i - 1]) + ((j == 0) ? 0 : rc[j - 1]));
368 sums.insert(sum);
369 }
370 }
371 for (unsigned u : sums) {
372 oc.push_back(u);
373 }
374 std::sort(oc.begin(), oc.end());
375 DEBUG_CODE(
376 for (unsigned i = 0; i + 1 < oc.size(); ++i) {
377 SASSERT(oc[i] < oc[i+1]);
378 });
379 for (unsigned i = 0; i < oc.size(); ++i) {
380 sum2def.insert(oc[i], i);
381 trail.push_back(expr_ref_vector(m));
382 }
383 for (unsigned i = 0; i <= l.size(); ++i) {
384 for (unsigned j = (i == 0) ? 1 : 0; j <= r.size(); ++j) {
385 if (i != 0 && j != 0 && (lc[i - 1] >= k || rc[j - 1] >= k)) continue;
386 unsigned sum = std::min(k, ((i == 0) ? 0 : lc[i - 1]) + ((j == 0) ? 0 : rc[j - 1]));
387 expr_ref_vector ands(m);
388 if (i != 0) {
389 ands.push_back(l[i - 1]);
390 }
391 if (j != 0) {
392 ands.push_back(r[j - 1]);
393 }
394 trail[sum2def.find(sum)].push_back(::mk_and(ands));
395 }
396 }
397 for (unsigned i = 0; i < oc.size(); ++i) {
398 o.push_back(::mk_or(trail[sum2def.find(oc[i])]));
399 }
400 }
401
402 /**
403 \brief MiniSat+ based encoding of PB constraints.
404 Translating Pseudo-Boolean Constraints into SAT,
405 Niklas Een, Niklas Soerensson, JSAT 2006.
406 */
407
408
409 vector<rational> m_min_base;
410 rational m_min_cost;
411 vector<rational> m_base;
412
create_basispb2bv_rewriter::imp::card2bv_rewriter413 void create_basis(vector<rational> const& seq, rational const& carry_in, rational const& cost) {
414 if (cost >= m_min_cost) {
415 return;
416 }
417 rational delta_cost(0);
418 for (unsigned i = 0; i < seq.size(); ++i) {
419 delta_cost += seq[i];
420 }
421 if (cost + delta_cost < m_min_cost) {
422 m_min_cost = cost + delta_cost;
423 m_min_base = m_base;
424 m_min_base.push_back(delta_cost + rational::one());
425 }
426
427 for (unsigned i = 0; i < sizeof(g_primes)/sizeof(*g_primes); ++i) {
428 vector<rational> seq1;
429 rational p(g_primes[i]);
430 rational rest = carry_in;
431 // create seq1
432 for (unsigned j = 0; j < seq.size(); ++j) {
433 rest += seq[j] % p;
434 if (seq[j] >= p) {
435 seq1.push_back(div(seq[j], p));
436 }
437 }
438
439 m_base.push_back(p);
440 create_basis(seq1, div(rest, p), cost + rest);
441 m_base.pop_back();
442 }
443 }
444
create_basispb2bv_rewriter::imp::card2bv_rewriter445 bool create_basis() {
446 m_base.reset();
447 m_min_cost = rational(INT_MAX);
448 m_min_base.reset();
449 rational cost(0);
450 create_basis(m_coeffs, rational::zero(), cost);
451 m_base = m_min_base;
452 TRACE("pb",
453 tout << "Base: ";
454 for (unsigned i = 0; i < m_base.size(); ++i) {
455 tout << m_base[i] << " ";
456 }
457 tout << "\n";);
458 return
459 !m_base.empty() &&
460 m_base.back().is_unsigned() &&
461 m_base.back().get_unsigned() <= 20*m_base.size();
462 }
463
464 /**
465 \brief Check if 'out mod n >= lim'.
466 */
mod_gepb2bv_rewriter::imp::card2bv_rewriter467 expr_ref mod_ge(ptr_vector<expr> const& out, unsigned n, unsigned lim) {
468 TRACE("pb", for (unsigned i = 0; i < out.size(); ++i) tout << mk_pp(out[i], m) << " "; tout << "\n";
469 tout << "n:" << n << " lim: " << lim << "\n";);
470 if (lim == n) {
471 return expr_ref(m.mk_false(), m);
472 }
473 if (lim == 0) {
474 return expr_ref(m.mk_true(), m);
475 }
476 SASSERT(0 < lim && lim < n);
477 expr_ref_vector ors(m);
478 for (unsigned j = 0; j + lim - 1 < out.size(); j += n) {
479 expr_ref tmp(m);
480 tmp = out[j + lim - 1];
481 if (j + n - 1 < out.size()) {
482 tmp = m.mk_and(tmp, m.mk_not(out[j + n - 1]));
483 }
484 ors.push_back(tmp);
485 }
486 return ::mk_or(ors);
487 }
488
489 // x0 + 5x1 + 3x2 >= k
490 // x0 x1 x1 -> s0 s1 s2
491 // s2 x1 x2 -> s3 s4 s5
492 // k = 7: s5 or (s4 & not s2 & s0)
493 // k = 6: s4
494 // k = 5: s4 or (s3 & not s2 & s1)
495 // k = 4: s4 or (s3 & not s2 & s0)
496 // k = 3: s3
497 //
mk_gepb2bv_rewriter::imp::card2bv_rewriter498 bool mk_ge(unsigned sz, expr * const* args, rational bound, expr_ref& result) {
499 if (!create_basis()) return false;
500 if (!bound.is_unsigned()) return false;
501 vector<rational> coeffs(m_coeffs);
502 result = m.mk_true();
503 expr_ref_vector carry(m), new_carry(m);
504 m_base.push_back(bound + rational::one());
505 for (const rational& b_i : m_base) {
506 unsigned B = b_i.get_unsigned();
507 unsigned d_i = (bound % b_i).get_unsigned();
508 bound = div(bound, b_i);
509 for (unsigned j = 0; j < coeffs.size(); ++j) {
510 rational c = coeffs[j] % b_i;
511 SASSERT(c.is_unsigned());
512 for (unsigned k = 0; k < c.get_unsigned(); ++k) {
513 carry.push_back(args[j]);
514 }
515 coeffs[j] = div(coeffs[j], b_i);
516 }
517 TRACE("pb", tout << "Carry: " << carry << "\n";
518 for (auto c : coeffs) tout << c << " ";
519 tout << "\n";
520 );
521 ptr_vector<expr> out;
522 m_sort.sorting(carry.size(), carry.data(), out);
523
524 expr_ref gt = mod_ge(out, B, d_i + 1);
525 expr_ref ge = mod_ge(out, B, d_i);
526 result = mk_and(ge, result);
527 result = mk_or(gt, result);
528 TRACE("pb", tout << "b: " << b_i << " d: " << d_i << " gt: " << gt << " ge: " << ge << " " << result << "\n";);
529
530 new_carry.reset();
531 for (unsigned j = B - 1; j < out.size(); j += B) {
532 new_carry.push_back(out[j]);
533 }
534 carry.reset();
535 carry.append(new_carry);
536 }
537 TRACE("pb", tout << "bound: " << bound << " Carry: " << carry << " result: " << result << "\n";);
538 return true;
539 }
540
541 /**
542 \brief binary merge encoding.
543 */
binary_mergepb2bv_rewriter::imp::card2bv_rewriter544 expr_ref binary_merge(lbool is_le, rational const& k) {
545 expr_ref result(m);
546 unsigned_vector coeffs;
547 for (rational const& c : m_coeffs) {
548 if (c.is_unsigned()) {
549 coeffs.push_back(c.get_unsigned());
550 }
551 else {
552 return result;
553 }
554 }
555 if (!k.is_unsigned()) {
556 return result;
557 }
558 switch (is_le) {
559 case l_true:
560 result = m_sort.le(k.get_unsigned(), coeffs.size(), coeffs.data(), m_args.data());
561 break;
562 case l_false:
563 result = m_sort.ge(k.get_unsigned(), coeffs.size(), coeffs.data(), m_args.data());
564 break;
565 case l_undef:
566 result = m_sort.eq(k.get_unsigned(), coeffs.size(), coeffs.data(), m_args.data());
567 break;
568 }
569 return result;
570 }
571
572 /**
573 \brief Segment based encoding.
574 The PB terms are partitoned into segments, such that each segment contains arguments with the same cofficient.
575 The segments are sorted, such that the segment with highest coefficient is first.
576 Then for each segment create circuits based on sorting networks the arguments of the segment.
577 */
578
mk_seg_gepb2bv_rewriter::imp::card2bv_rewriter579 expr_ref mk_seg_ge(rational const& k) {
580 rational bound(-k);
581 for (unsigned i = 0; i < m_args.size(); ++i) {
582 m_args[i] = mk_not(m_args[i].get());
583 bound += m_coeffs[i];
584 }
585 return mk_seg_le(bound);
586 }
587
mk_seg_lepb2bv_rewriter::imp::card2bv_rewriter588 expr_ref mk_seg_le(rational const& k) {
589 sort_args();
590 unsigned sz = m_args.size();
591 expr* const* args = m_args.data();
592
593 // Create sorted entries.
594 vector<ptr_vector<expr>> outs;
595 vector<rational> coeffs;
596 for (unsigned i = 0, seg_size = 0; i < sz; i += seg_size) {
597 seg_size = segment_size(i);
598 ptr_vector<expr> out;
599 m_sort.sorting(seg_size, args + i, out);
600 out.push_back(m.mk_false());
601 outs.push_back(out);
602 coeffs.push_back(m_coeffs[i]);
603 }
604 return mk_seg_le_rec(outs, coeffs, 0, k);
605 }
606
mk_seg_le_recpb2bv_rewriter::imp::card2bv_rewriter607 expr_ref mk_seg_le_rec(vector<ptr_vector<expr>> const& outs, vector<rational> const& coeffs, unsigned i, rational const& k) {
608 if (k.is_neg()) {
609 return expr_ref(m.mk_false(), m);
610 }
611 if (i == outs.size()) {
612 return expr_ref(m.mk_true(), m);
613 }
614 rational const& c = coeffs[i];
615 ptr_vector<expr> const& out = outs[i];
616
617 if (i + 1 == outs.size() && k >= rational(out.size()-1)*c) {
618 return expr_ref(m.mk_true(), m);
619 }
620 expr_ref_vector fmls(m);
621 fmls.push_back(m.mk_implies(m.mk_not(out[0]), mk_seg_le_rec(outs, coeffs, i + 1, k)));
622 rational k1;
623 for (unsigned j = 0; j + 1 < out.size(); ++j) {
624 k1 = k - rational(j+1)*c;
625 if (k1.is_neg()) {
626 fmls.push_back(m.mk_not(out[j]));
627 break;
628 }
629 fmls.push_back(m.mk_implies(m.mk_and(out[j], m.mk_not(out[j+1])), mk_seg_le_rec(outs, coeffs, i + 1, k1)));
630 }
631 return ::mk_and(fmls);
632 }
633
634 // The number of arguments with the same coefficient.
segment_sizepb2bv_rewriter::imp::card2bv_rewriter635 unsigned segment_size(unsigned start) const {
636 unsigned i = start;
637 while (i < m_args.size() && m_coeffs[i] == m_coeffs[start]) ++i;
638 return i - start;
639 }
640
mk_andpb2bv_rewriter::imp::card2bv_rewriter641 expr_ref mk_and(expr_ref& a, expr_ref& b) {
642 if (m.is_true(a)) return b;
643 if (m.is_true(b)) return a;
644 if (m.is_false(a)) return a;
645 if (m.is_false(b)) return b;
646 return expr_ref(m.mk_and(a, b), m);
647 }
648
mk_orpb2bv_rewriter::imp::card2bv_rewriter649 expr_ref mk_or(expr_ref& a, expr_ref& b) {
650 if (m.is_true(a)) return a;
651 if (m.is_true(b)) return b;
652 if (m.is_false(a)) return b;
653 if (m.is_false(b)) return a;
654 return expr_ref(m.mk_or(a, b), m);
655 }
656
mk_lepb2bv_rewriter::imp::card2bv_rewriter657 bool mk_le(unsigned sz, expr * const* args, rational const& k, expr_ref& result) {
658 expr_ref_vector args1(m);
659 rational bound(-k);
660 for (unsigned i = 0; i < sz; ++i) {
661 args1.push_back(mk_not(args[i]));
662 bound += m_coeffs[i];
663 }
664 return mk_ge(sz, args1.data(), bound, result);
665 }
666
mk_eqpb2bv_rewriter::imp::card2bv_rewriter667 bool mk_eq(unsigned sz, expr * const* args, rational const& k, expr_ref& result) {
668 expr_ref r1(m), r2(m);
669 if (mk_ge(sz, args, k, r1) && mk_le(sz, args, k, r2)) {
670 result = m.mk_and(r1, r2);
671 return true;
672 }
673 else {
674 return false;
675 }
676 }
677
mk_bvpb2bv_rewriter::imp::card2bv_rewriter678 expr_ref mk_bv(func_decl * f, unsigned sz, expr * const* args) {
679 ++m_imp.m_compile_bv;
680 decl_kind kind = f->get_decl_kind();
681 rational k = pb.get_k(f);
682 m_coeffs.reset();
683 m_args.reset();
684 for (unsigned i = 0; i < sz; ++i) {
685 m_coeffs.push_back(pb.get_coeff(f, i));
686 m_args.push_back(args[i]);
687 }
688 CTRACE("pb", k.is_neg(), tout << expr_ref(m.mk_app(f, sz, args), m) << "\n";);
689 SASSERT(!k.is_neg());
690 switch (kind) {
691 case OP_PB_GE:
692 case OP_AT_LEAST_K: {
693 dualize(f, m_args, k);
694 SASSERT(!k.is_neg());
695 return mk_le_ge<l_true>(k);
696 }
697 case OP_PB_LE:
698 case OP_AT_MOST_K:
699 return mk_le_ge<l_true>(k);
700 case OP_PB_EQ:
701 return mk_le_ge<l_undef>(k);
702 default:
703 UNREACHABLE();
704 return expr_ref(m.mk_true(), m);
705 }
706 }
707
dualizepb2bv_rewriter::imp::card2bv_rewriter708 void dualize(func_decl* f, expr_ref_vector & args, rational & k) {
709 k.neg();
710 for (unsigned i = 0; i < args.size(); ++i) {
711 k += pb.get_coeff(f, i);
712 args[i] = ::mk_not(m, args[i].get());
713 }
714 }
715
negatepb2bv_rewriter::imp::card2bv_rewriter716 expr* negate(expr* e) {
717 if (m.is_not(e, e)) return e;
718 return m.mk_not(e);
719 }
mk_itepb2bv_rewriter::imp::card2bv_rewriter720 expr* mk_ite(expr* c, expr* hi, expr* lo) {
721 while (m.is_not(c, c)) {
722 std::swap(hi, lo);
723 }
724 if (hi == lo) return hi;
725 if (m.is_true(hi) && m.is_false(lo)) return c;
726 if (m.is_false(hi) && m.is_true(lo)) return negate(c);
727 if (m.is_true(hi)) return m.mk_or(c, lo);
728 if (m.is_false(lo)) return m.mk_and(c, hi);
729 if (m.is_false(hi)) return m.mk_and(negate(c), lo);
730 if (m.is_true(lo)) return m.mk_implies(c, hi);
731 return m.mk_ite(c, hi, lo);
732 }
733
is_orpb2bv_rewriter::imp::card2bv_rewriter734 bool is_or(func_decl* f) {
735 switch (f->get_decl_kind()) {
736 case OP_AT_MOST_K:
737 case OP_PB_LE:
738 return false;
739 case OP_AT_LEAST_K:
740 case OP_PB_GE:
741 return pb.get_k(f).is_one();
742 case OP_PB_EQ:
743 return false;
744 default:
745 UNREACHABLE();
746 return false;
747 }
748 }
749
750 public:
751
card2bv_rewriterpb2bv_rewriter::imp::card2bv_rewriter752 card2bv_rewriter(imp& i, ast_manager& m):
753 m_sort(*this),
754 m(m),
755 m_imp(i),
756 au(m),
757 pb(m),
758 bv(m),
759 m_trail(m),
760 m_args(m),
761 m_keep_cardinality_constraints(false),
762 m_pb_solver(symbol("solver")),
763 m_min_arity(9)
764 {}
765
set_pb_solverpb2bv_rewriter::imp::card2bv_rewriter766 void set_pb_solver(symbol const& s) { m_pb_solver = s; }
767
mk_apppb2bv_rewriter::imp::card2bv_rewriter768 bool mk_app(bool full, func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
769 if (f->get_family_id() == pb.get_family_id() && mk_pb(full, f, sz, args, result)) {
770 // skip
771 }
772 else if (au.is_le(f) && is_pb(args[0], args[1])) {
773 result = mk_le_ge<l_true>(m_k);
774 }
775 else if (au.is_lt(f) && is_pb(args[0], args[1])) {
776 ++m_k;
777 result = mk_le_ge<l_true>(m_k);
778 }
779 else if (au.is_ge(f) && is_pb(args[1], args[0])) {
780 result = mk_le_ge<l_true>(m_k);
781 }
782 else if (au.is_gt(f) && is_pb(args[1], args[0])) {
783 ++m_k;
784 result = mk_le_ge<l_true>(m_k);
785 }
786 else if (m.is_eq(f) && is_pb(args[0], args[1])) {
787 result = mk_le_ge<l_undef>(m_k);
788 }
789 else {
790 return false;
791 }
792 ++m_imp.m_num_translated;
793 return true;
794 }
795
mk_app_corepb2bv_rewriter::imp::card2bv_rewriter796 br_status mk_app_core(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
797 if (mk_app(true, f, sz, args, result)) {
798 return BR_DONE;
799 }
800 else {
801 return BR_FAILED;
802 }
803 }
804
mk_apppb2bv_rewriter::imp::card2bv_rewriter805 bool mk_app(bool full, expr* e, expr_ref& r) {
806 app* a;
807 return (is_app(e) && (a = to_app(e), mk_app(full, a->get_decl(), a->get_num_args(), a->get_args(), r)));
808 }
809
is_pbpb2bv_rewriter::imp::card2bv_rewriter810 bool is_pb(expr* x, expr* y) {
811 m_args.reset();
812 m_coeffs.reset();
813 m_k.reset();
814 return is_pb(x, rational::one()) && is_pb(y, rational::minus_one());
815 }
816
is_pbpb2bv_rewriter::imp::card2bv_rewriter817 bool is_pb(expr* e, rational const& mul) {
818 if (!is_app(e)) {
819 return false;
820 }
821 app* a = to_app(e);
822 rational r, r1, r2;
823 expr* c, *th, *el;
824 unsigned sz = a->get_num_args();
825 if (a->get_family_id() == au.get_family_id()) {
826 switch (a->get_decl_kind()) {
827 case OP_ADD:
828 for (unsigned i = 0; i < sz; ++i) {
829 if (!is_pb(a->get_arg(i), mul)) return false;
830 }
831 return true;
832 case OP_SUB: {
833 if (!is_pb(a->get_arg(0), mul)) return false;
834 r = -mul;
835 for (unsigned i = 1; i < sz; ++i) {
836 if (!is_pb(a->get_arg(1), r)) return false;
837 }
838 return true;
839 }
840 case OP_UMINUS:
841 return is_pb(a->get_arg(0), -mul);
842 case OP_NUM:
843 VERIFY(au.is_numeral(a, r));
844 m_k -= mul * r;
845 return m_k.is_int();
846 case OP_MUL:
847 if (sz != 2) {
848 return false;
849 }
850 if (au.is_numeral(a->get_arg(0), r)) {
851 r *= mul;
852 return is_pb(a->get_arg(1), r);
853 }
854 if (au.is_numeral(a->get_arg(1), r)) {
855 r *= mul;
856 return is_pb(a->get_arg(0), r);
857 }
858 return false;
859 default:
860 return false;
861 }
862 }
863 if (m.is_ite(a, c, th, el) &&
864 au.is_numeral(th, r1) &&
865 au.is_numeral(el, r2)) {
866 r1 *= mul;
867 r2 *= mul;
868 if (r1 < r2) {
869 m_args.push_back(::mk_not(m, c));
870 m_coeffs.push_back(r2-r1);
871 m_k -= r1;
872 }
873 else {
874 m_args.push_back(c);
875 m_coeffs.push_back(r1-r2);
876 m_k -= r2;
877 }
878 return m_k.is_int() && (r1-r2).is_int();
879 }
880 return false;
881 }
882
mk_pbpb2bv_rewriter::imp::card2bv_rewriter883 bool mk_pb(bool full, func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
884 SASSERT(f->get_family_id() == pb.get_family_id());
885 if (is_or(f)) {
886 result = m.mk_or(sz, args);
887 }
888 else if (pb.is_at_most_k(f) && pb.get_k(f).is_unsigned()) {
889 if (m_keep_cardinality_constraints && f->get_arity() >= m_min_arity) return false;
890 result = m_sort.le(full, pb.get_k(f).get_unsigned(), sz, args);
891 ++m_imp.m_compile_card;
892 }
893 else if (pb.is_at_least_k(f) && pb.get_k(f).is_unsigned()) {
894 if (m_keep_cardinality_constraints && f->get_arity() >= m_min_arity) return false;
895 result = m_sort.ge(full, pb.get_k(f).get_unsigned(), sz, args);
896 ++m_imp.m_compile_card;
897 }
898 else if (pb.is_eq(f) && pb.get_k(f).is_unsigned() && pb.has_unit_coefficients(f)) {
899 if (m_keep_cardinality_constraints && f->get_arity() >= m_min_arity) return false;
900 result = m_sort.eq(full, pb.get_k(f).get_unsigned(), sz, args);
901 ++m_imp.m_compile_card;
902 }
903 else if (pb.is_le(f) && pb.get_k(f).is_unsigned() && pb.has_unit_coefficients(f)) {
904 if (m_keep_cardinality_constraints && f->get_arity() >= m_min_arity) return false;
905 result = m_sort.le(full, pb.get_k(f).get_unsigned(), sz, args);
906 ++m_imp.m_compile_card;
907 }
908 else if (pb.is_ge(f) && pb.get_k(f).is_unsigned() && pb.has_unit_coefficients(f)) {
909 if (m_keep_cardinality_constraints && f->get_arity() >= m_min_arity) return false;
910 result = m_sort.ge(full, pb.get_k(f).get_unsigned(), sz, args);
911 ++m_imp.m_compile_card;
912 }
913 else if (pb.is_eq(f) && pb.get_k(f).is_unsigned() && has_small_coefficients(f) && m_pb_solver == "solver") {
914 return false;
915 }
916 else if (pb.is_le(f) && pb.get_k(f).is_unsigned() && has_small_coefficients(f) && m_pb_solver == "solver") {
917 return false;
918 }
919 else if (pb.is_ge(f) && pb.get_k(f).is_unsigned() && has_small_coefficients(f) && m_pb_solver == "solver") {
920 return false;
921 }
922 else {
923 result = mk_bv(f, sz, args);
924 }
925 TRACE("pb", tout << "full: " << full << " " << expr_ref(m.mk_app(f, sz, args), m) << " " << result << "\n";
926 );
927 return true;
928 }
929
has_small_coefficientspb2bv_rewriter::imp::card2bv_rewriter930 bool has_small_coefficients(func_decl* f) {
931 unsigned sz = f->get_arity();
932 unsigned sum = 0;
933 for (unsigned i = 0; i < sz; ++i) {
934 rational c = pb.get_coeff(f, i);
935 if (!c.is_unsigned()) return false;
936 unsigned sum1 = sum + c.get_unsigned();
937 if (sum1 < sum) return false;
938 sum = sum1;
939 }
940 return true;
941 }
942
943 // definitions used for sorting network
mk_falsepb2bv_rewriter::imp::card2bv_rewriter944 pliteral mk_false() { return m.mk_false(); }
mk_truepb2bv_rewriter::imp::card2bv_rewriter945 pliteral mk_true() { return m.mk_true(); }
mk_maxpb2bv_rewriter::imp::card2bv_rewriter946 pliteral mk_max(unsigned n, pliteral const* lits) { return trail(m.mk_or(n, lits)); }
mk_minpb2bv_rewriter::imp::card2bv_rewriter947 pliteral mk_min(unsigned n, pliteral const* lits) { return trail(m.mk_and(n, lits)); }
mk_notpb2bv_rewriter::imp::card2bv_rewriter948 pliteral mk_not(pliteral a) { if (m.is_not(a,a)) return a; return trail(m.mk_not(a)); }
949
pppb2bv_rewriter::imp::card2bv_rewriter950 std::ostream& pp(std::ostream& out, pliteral lit) { return out << mk_ismt2_pp(lit, m); }
951
trailpb2bv_rewriter::imp::card2bv_rewriter952 pliteral trail(pliteral l) {
953 m_trail.push_back(l);
954 return l;
955 }
freshpb2bv_rewriter::imp::card2bv_rewriter956 pliteral fresh(char const* n) {
957 expr_ref fr(m.mk_fresh_const(n, m.mk_bool_sort()), m);
958 m_imp.m_fresh.push_back(to_app(fr)->get_decl());
959 return trail(fr);
960 }
961
mk_clausepb2bv_rewriter::imp::card2bv_rewriter962 void mk_clause(unsigned n, pliteral const* lits) {
963 m_imp.m_lemmas.push_back(::mk_or(m, n, lits));
964 }
965
keep_cardinality_constraintspb2bv_rewriter::imp::card2bv_rewriter966 void keep_cardinality_constraints(bool f) {
967 m_keep_cardinality_constraints = f;
968 }
969
set_cardinality_encodingpb2bv_rewriter::imp::card2bv_rewriter970 void set_cardinality_encoding(sorting_network_encoding enc) { m_sort.cfg().m_encoding = enc; }
971
set_min_aritypb2bv_rewriter::imp::card2bv_rewriter972 void set_min_arity(unsigned ma) { m_min_arity = ma; }
973
974 };
975
976 struct card2bv_rewriter_cfg : public default_rewriter_cfg {
977 card2bv_rewriter m_r;
rewrite_patternspb2bv_rewriter::imp::card2bv_rewriter_cfg978 bool rewrite_patterns() const { return false; }
flat_assocpb2bv_rewriter::imp::card2bv_rewriter_cfg979 bool flat_assoc(func_decl * f) const { return false; }
reduce_apppb2bv_rewriter::imp::card2bv_rewriter_cfg980 br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
981 result_pr = nullptr;
982 if (m_r.m.proofs_enabled()) {
983 return BR_FAILED;
984 }
985 return m_r.mk_app_core(f, num, args, result);
986 }
card2bv_rewriter_cfgpb2bv_rewriter::imp::card2bv_rewriter_cfg987 card2bv_rewriter_cfg(imp& i, ast_manager & m):m_r(i, m) {}
keep_cardinality_constraintspb2bv_rewriter::imp::card2bv_rewriter_cfg988 void keep_cardinality_constraints(bool f) { m_r.keep_cardinality_constraints(f); }
set_pb_solverpb2bv_rewriter::imp::card2bv_rewriter_cfg989 void set_pb_solver(symbol const& s) { m_r.set_pb_solver(s); }
set_cardinality_encodingpb2bv_rewriter::imp::card2bv_rewriter_cfg990 void set_cardinality_encoding(sorting_network_encoding enc) { m_r.set_cardinality_encoding(enc); }
set_min_aritypb2bv_rewriter::imp::card2bv_rewriter_cfg991 void set_min_arity(unsigned ma) { m_r.set_min_arity(ma); }
992
993 };
994
995 class card_pb_rewriter : public rewriter_tpl<card2bv_rewriter_cfg> {
996 public:
997 card2bv_rewriter_cfg m_cfg;
card_pb_rewriter(imp & i,ast_manager & m)998 card_pb_rewriter(imp& i, ast_manager & m):
999 rewriter_tpl<card2bv_rewriter_cfg>(m, false, m_cfg),
1000 m_cfg(i, m) {}
keep_cardinality_constraints(bool f)1001 void keep_cardinality_constraints(bool f) { m_cfg.keep_cardinality_constraints(f); }
set_pb_solver(symbol const & s)1002 void set_pb_solver(symbol const& s) { m_cfg.set_pb_solver(s); }
set_cardinality_encoding(sorting_network_encoding e)1003 void set_cardinality_encoding(sorting_network_encoding e) { m_cfg.set_cardinality_encoding(e); }
set_min_arity(unsigned ma)1004 void set_min_arity(unsigned ma) { m_cfg.set_min_arity(ma); }
rewrite(bool full,expr * e,expr_ref & r,proof_ref & p)1005 void rewrite(bool full, expr* e, expr_ref& r, proof_ref& p) {
1006 expr_ref ee(e, m());
1007 if (m().proofs_enabled()) {
1008 r = e;
1009 return;
1010 }
1011 if (m_cfg.m_r.mk_app(full, e, r)) {
1012 ee = r;
1013 }
1014 (*this)(ee, r, p);
1015 }
1016 };
1017
1018 card_pb_rewriter m_rw;
1019
keep_cardinalitypb2bv_rewriter::imp1020 bool keep_cardinality() const {
1021 params_ref const& p = m_params;
1022 return
1023 p.get_bool("keep_cardinality_constraints", false) ||
1024 p.get_bool("sat.cardinality.solver", false) ||
1025 p.get_bool("cardinality.solver", false) ||
1026 gparams::get_module("sat").get_bool("cardinality.solver", false);
1027 }
1028
pb_solverpb2bv_rewriter::imp1029 symbol pb_solver() const {
1030 params_ref const& p = m_params;
1031 symbol s = p.get_sym("sat.pb.solver", symbol());
1032 if (s != symbol()) return s;
1033 s = p.get_sym("pb.solver", symbol());
1034 if (s != symbol()) return s;
1035 return gparams::get_module("sat").get_sym("pb.solver", symbol("solver"));
1036 }
1037
min_aritypb2bv_rewriter::imp1038 unsigned min_arity() const {
1039 params_ref const& p = m_params;
1040 unsigned r = p.get_uint("sat.pb.min_arity", UINT_MAX);
1041 if (r != UINT_MAX) return r;
1042 r = p.get_uint("pb.min_arity", UINT_MAX);
1043 if (r != UINT_MAX) return r;
1044 return gparams::get_module("sat").get_uint("pb.min_arity", 9);
1045 }
1046
cardinality_encodingpb2bv_rewriter::imp1047 sorting_network_encoding cardinality_encoding() const {
1048 symbol enc = m_params.get_sym("cardinality.encoding", symbol());
1049 if (enc == symbol()) {
1050 enc = gparams::get_module("sat").get_sym("cardinality.encoding", symbol());
1051 }
1052 if (enc == symbol("grouped")) return sorting_network_encoding::grouped_at_most;
1053 if (enc == symbol("bimander")) return sorting_network_encoding::bimander_at_most;
1054 if (enc == symbol("ordered")) return sorting_network_encoding::ordered_at_most;
1055 if (enc == symbol("unate")) return sorting_network_encoding::unate_at_most;
1056 if (enc == symbol("circuit")) return sorting_network_encoding::circuit_at_most;
1057 return sorting_network_encoding::grouped_at_most;
1058 }
1059
1060
imppb2bv_rewriter::imp1061 imp(ast_manager& m, params_ref const& p):
1062 m(m), m_params(p), m_lemmas(m),
1063 m_fresh(m),
1064 m_num_translated(0),
1065 m_rw(*this, m) {
1066 updt_params(p);
1067 m_compile_bv = 0;
1068 m_compile_card = 0;
1069 }
1070
updt_paramspb2bv_rewriter::imp1071 void updt_params(params_ref const & p) {
1072 m_params.append(p);
1073 m_rw.keep_cardinality_constraints(keep_cardinality());
1074 m_rw.set_pb_solver(pb_solver());
1075 m_rw.set_cardinality_encoding(cardinality_encoding());
1076 m_rw.set_min_arity(min_arity());
1077 }
1078
collect_param_descrspb2bv_rewriter::imp1079 void collect_param_descrs(param_descrs& r) const {
1080 r.insert("keep_cardinality_constraints", CPK_BOOL, "(default: false) retain cardinality constraints (don't bit-blast them) and use built-in cardinality solver");
1081 r.insert("pb.solver", CPK_SYMBOL, "(default: solver) retain pb constraints (don't bit-blast them) and use built-in pb solver");
1082 r.insert("cardinality.encoding", CPK_SYMBOL, "(default: none) grouped, bimander, ordered, unate, circuit");
1083 }
1084
get_num_stepspb2bv_rewriter::imp1085 unsigned get_num_steps() const { return m_rw.get_num_steps(); }
cleanuppb2bv_rewriter::imp1086 void cleanup() { m_rw.cleanup(); }
operator ()pb2bv_rewriter::imp1087 void operator()(bool full, expr * e, expr_ref & result, proof_ref & result_proof) {
1088 // m_rw(e, result, result_proof);
1089 m_rw.rewrite(full, e, result, result_proof);
1090 }
pushpb2bv_rewriter::imp1091 void push() {
1092 m_fresh_lim.push_back(m_fresh.size());
1093 }
poppb2bv_rewriter::imp1094 void pop(unsigned num_scopes) {
1095 SASSERT(m_lemmas.empty()); // lemmas must be flushed before pop.
1096 if (num_scopes > 0) {
1097 SASSERT(num_scopes <= m_fresh_lim.size());
1098 unsigned new_sz = m_fresh_lim.size() - num_scopes;
1099 unsigned lim = m_fresh_lim[new_sz];
1100 m_fresh.resize(lim);
1101 m_fresh_lim.resize(new_sz);
1102 }
1103 m_rw.reset();
1104 }
1105
flush_side_constraintspb2bv_rewriter::imp1106 void flush_side_constraints(expr_ref_vector& side_constraints) {
1107 side_constraints.append(m_lemmas);
1108 m_lemmas.reset();
1109 }
1110
collect_statisticspb2bv_rewriter::imp1111 void collect_statistics(statistics & st) const {
1112 st.update("pb-compile-bv", m_compile_bv);
1113 st.update("pb-compile-card", m_compile_card);
1114 st.update("pb-aux-variables", m_fresh.size());
1115 st.update("pb-aux-clauses", m_rw.m_cfg.m_r.m_sort.m_stats.m_num_compiled_clauses);
1116 }
1117
1118 };
1119
1120
pb2bv_rewriter(ast_manager & m,params_ref const & p)1121 pb2bv_rewriter::pb2bv_rewriter(ast_manager & m, params_ref const& p) { m_imp = alloc(imp, m, p); }
~pb2bv_rewriter()1122 pb2bv_rewriter::~pb2bv_rewriter() { dealloc(m_imp); }
updt_params(params_ref const & p)1123 void pb2bv_rewriter::updt_params(params_ref const & p) { m_imp->updt_params(p); }
collect_param_descrs(param_descrs & r) const1124 void pb2bv_rewriter::collect_param_descrs(param_descrs& r) const { m_imp->collect_param_descrs(r); }
1125
m() const1126 ast_manager & pb2bv_rewriter::m() const { return m_imp->m; }
get_num_steps() const1127 unsigned pb2bv_rewriter::get_num_steps() const { return m_imp->get_num_steps(); }
cleanup()1128 void pb2bv_rewriter::cleanup() { ast_manager& mgr = m(); params_ref p = m_imp->m_params; dealloc(m_imp); m_imp = alloc(imp, mgr, p); }
fresh_constants() const1129 func_decl_ref_vector const& pb2bv_rewriter::fresh_constants() const { return m_imp->m_fresh; }
operator ()(bool full,expr * e,expr_ref & result,proof_ref & result_proof)1130 void pb2bv_rewriter::operator()(bool full, expr * e, expr_ref & result, proof_ref & result_proof) { (*m_imp)(full, e, result, result_proof); }
push()1131 void pb2bv_rewriter::push() { m_imp->push(); }
pop(unsigned num_scopes)1132 void pb2bv_rewriter::pop(unsigned num_scopes) { m_imp->pop(num_scopes); }
flush_side_constraints(expr_ref_vector & side_constraints)1133 void pb2bv_rewriter::flush_side_constraints(expr_ref_vector& side_constraints) { m_imp->flush_side_constraints(side_constraints); }
num_translated() const1134 unsigned pb2bv_rewriter::num_translated() const { return m_imp->m_num_translated; }
1135
1136
collect_statistics(statistics & st) const1137 void pb2bv_rewriter::collect_statistics(statistics & st) const { m_imp->collect_statistics(st); }
1138