1 /*++
2 Copyright (c) 2014 Microsoft Corporation
3
4 Module Name:
5
6 doc.cpp
7
8 Abstract:
9
10 difference of cubes.
11
12 Author:
13
14 Nuno Lopes (a-nlopes) 2013-03-01
15 Nikolaj Bjorner (nbjorner) 2014-09-15
16
17 Revision History:
18
19 Based on ternary_diff_bitvector by Nuno Lopes.
20
21 --*/
22
23 #include "muz/rel/doc.h"
24 #include "smt/smt_kernel.h"
25 #include "ast/rewriter/expr_safe_replace.h"
26 #include "smt/params/smt_params.h"
27 #include "ast/ast_util.h"
28 #include "ast/ast_pp.h"
29
doc_manager(unsigned n)30 doc_manager::doc_manager(unsigned n): m(n), m_alloc("doc") {
31 m_full = m.allocateX();
32 }
33
~doc_manager()34 doc_manager::~doc_manager() {
35 m.deallocate(m_full);
36 }
37
allocate()38 doc* doc_manager::allocate() {
39 return allocate(m.allocate());
40 }
allocate1()41 doc* doc_manager::allocate1() {
42 return allocate(m.allocate1());
43 }
allocate0()44 doc* doc_manager::allocate0() {
45 return allocate(m.allocate0());
46 }
allocateX()47 doc* doc_manager::allocateX() {
48 return allocate(m.allocateX());
49 }
allocate(doc const & src)50 doc* doc_manager::allocate(doc const& src) {
51 doc* r = allocate(m.allocate(src.pos()));
52 for (unsigned i = 0; i < src.neg().size(); ++i) {
53 r->neg().push_back(m.allocate(src.neg()[i]));
54 }
55 return r;
56 }
allocate(tbv * t)57 doc* doc_manager::allocate(tbv* t) {
58 SASSERT(t);
59 void* mm = m_alloc.allocate(sizeof(doc));
60 return new (mm) doc(t);
61 }
allocate(tbv const & src)62 doc* doc_manager::allocate(tbv const& src) {
63 return allocate(m.allocate(src));
64 }
allocate(uint64_t n)65 doc* doc_manager::allocate(uint64_t n) {
66 return allocate(m.allocate(n));
67 }
allocate(rational const & r)68 doc* doc_manager::allocate(rational const& r) {
69 return allocate(m.allocate(r));
70 }
allocate(uint64_t n,unsigned hi,unsigned lo)71 doc* doc_manager::allocate(uint64_t n, unsigned hi, unsigned lo) {
72 return allocate(m.allocate(n, hi, lo));
73 }
allocate(doc const & src,unsigned const * permutation)74 doc* doc_manager::allocate(doc const& src, unsigned const* permutation) {
75 doc* r = allocate(m.allocate(src.pos(), permutation));
76 for (unsigned i = 0; i < src.neg().size(); ++i) {
77 r->neg().push_back(m.allocate(src.neg()[i], permutation));
78 }
79 return r;
80 }
deallocate(doc * src)81 void doc_manager::deallocate(doc* src) {
82 if (!src) return;
83 m.deallocate(&src->pos());
84 src->neg().reset(m);
85 src->~doc();
86 m_alloc.deallocate(sizeof(doc), src);
87 }
copy(doc & dst,doc const & src)88 void doc_manager::copy(doc& dst, doc const& src) {
89 m.copy(dst.pos(), src.pos());
90 dst.neg().reset(m);
91 for (unsigned i = 0; i < src.neg().size(); ++i) {
92 dst.neg().push_back(m.allocate(src.neg()[i]));
93 }
94 }
fill0(doc & src)95 doc& doc_manager::fill0(doc& src) {
96 src.neg().reset(m);
97 m.fill0(src.pos());
98 return src;
99 }
fill1(doc & src)100 doc& doc_manager::fill1(doc& src) {
101 src.neg().reset(m);
102 m.fill1(src.pos());
103 return src;
104 }
fillX(doc & src)105 doc& doc_manager::fillX(doc& src) {
106 src.neg().reset(m);
107 m.fillX(src.pos());
108 return src;
109 }
110
get_size_estimate_bytes(const doc & d) const111 unsigned doc_manager::get_size_estimate_bytes(const doc& d) const {
112 return m.get_size_estimate_bytes(d.pos())
113 + d.neg().get_size_estimate_bytes(m)
114 + sizeof(doc);
115 }
116
set_and(doc & dst,doc const & src)117 bool doc_manager::set_and(doc& dst, doc const& src) {
118 // (A \ B) & (C \ D) = (A & C) \ (B u D)
119 if (!m.set_and(dst.pos(), src.pos())) return false;
120 dst.neg().intersect(m, dst.pos());
121 tbv_ref t(m);
122 for (unsigned i = 0; i < src.neg().size(); ++i) {
123 t = m.allocate(src.neg()[i]);
124 if (m.set_and(*t, dst.pos())) {
125 dst.neg().insert(m, t.detach());
126 }
127 }
128 return fold_neg(dst);
129 }
set_and(doc & dst,tbv const & src)130 bool doc_manager::set_and(doc& dst, tbv const& src) {
131 // (A \ B) & C = (A & C) \ (B & C)
132 if (!m.set_and(dst.pos(), src)) return false;
133 dst.neg().intersect(m, src);
134 return fold_neg(dst);
135 }
136
well_formed(doc const & d) const137 bool doc_manager::well_formed(doc const& d) const {
138 if (!m.is_well_formed(d.pos())) return false;
139 for (unsigned i = 0; i < d.neg().size(); ++i) {
140 if (!m.is_well_formed(d.neg()[i])) return false;
141 if (!m.contains(d.pos(), d.neg()[i])) return false;
142 }
143 return true;
144 }
145
fold_neg(doc & dst)146 bool doc_manager::fold_neg(doc& dst) {
147 start_over:
148 for (unsigned i = 0; i < dst.neg().size(); ++i) {
149 if (m.contains(dst.neg()[i], dst.pos()))
150 return false;
151
152 unsigned index;
153 unsigned count = diff_by_012(dst.pos(), dst.neg()[i], index);
154 if (count != 2) {
155 if (count == 0) {
156 return false;
157 }
158 else if (count == 3) {
159 dst.neg().erase(tbvm(), i);
160 --i;
161 }
162 else { // count == 1:
163 m.set(dst.pos(), index, neg(dst.neg()[i][index]));
164 dst.neg().intersect(tbvm(), dst.pos());
165 goto start_over;
166 }
167 }
168 }
169 SASSERT(well_formed(dst));
170 return true;
171 }
172
diff_by_012(tbv const & pos,tbv const & neg,unsigned & index)173 unsigned doc_manager::diff_by_012(tbv const& pos, tbv const& neg, unsigned& index) {
174 unsigned n = num_tbits();
175 unsigned count = 0;
176 for (unsigned i = 0; i < n; ++i) {
177 tbit b1 = pos[i];
178 tbit b2 = neg[i];
179 SASSERT(b1 != BIT_z && b2 != BIT_z);
180 if (b1 != b2) {
181 if (count == 1) return 2;
182 if (b1 == BIT_x) {
183 index = i;
184 count = 1;
185 }
186 else if (b2 != BIT_x) {
187 return 3;
188 }
189 }
190 }
191 return count;
192 }
193
set(doc & d,unsigned idx,tbit value)194 void doc_manager::set(doc& d, unsigned idx, tbit value) {
195 m.set(d.pos(), idx, value);
196 for (unsigned i = 0; i < d.neg().size(); ++i) {
197 tbit b = d.neg()[i][idx];
198 if (b != BIT_x && value != BIT_x && value != b) {
199 d.neg().erase(tbvm(), i);
200 --i;
201 }
202 else {
203 m.set(d.neg()[i], idx, value);
204 }
205 }
206 }
207
208 //
209 // merge range from [lo:lo+length-1] with each index in equivalence class.
210 // under assumption of equalities and columns that are discarded.
211 //
merge(doc & d,unsigned lo,unsigned length,subset_ints const & equalities,bit_vector const & discard_cols)212 bool doc_manager::merge(
213 doc& d, unsigned lo, unsigned length,
214 subset_ints const& equalities, bit_vector const& discard_cols) {
215 for (unsigned i = 0; i < length; ++i) {
216 unsigned idx = lo + i;
217 if (!merge(d, idx, equalities, discard_cols)) return false;
218 }
219 return true;
220 }
merge(doc & d,unsigned idx,subset_ints const & equalities,bit_vector const & discard_cols)221 bool doc_manager::merge(doc& d, unsigned idx, subset_ints const& equalities,
222 bit_vector const& discard_cols) {
223 unsigned root = equalities.find(idx);
224 idx = root;
225 unsigned num_x = 0;
226 unsigned root1 = root;
227 tbit value = BIT_x;
228 do {
229 switch (d[idx]) {
230 case BIT_0:
231 if (value == BIT_1) return false;
232 value = BIT_0;
233 break;
234 case BIT_1:
235 if (value == BIT_0) return false;
236 value = BIT_1;
237 break;
238 case BIT_x:
239 ++num_x;
240 if (!discard_cols.get(idx)) {
241 root1 = idx;
242 }
243 break;
244 default:
245 UNREACHABLE();
246 break;
247 }
248 idx = equalities.next(idx);
249 }
250 while (idx != root);
251
252 TRACE("doc", tout << "num_x: " << num_x << " value: " << value << "\n";);
253 if (num_x == 0) {
254 // nothing to do.
255 }
256 else if (value != BIT_x) {
257 do {
258 if (d[idx] == BIT_x) {
259 set(d, idx, value);
260 }
261 idx = equalities.next(idx);
262 }
263 while (idx != root);
264 }
265 else {
266 bool all_x = true;
267 if (!d.neg().is_empty()) {
268 idx = root;
269 do {
270 for (unsigned i = 0; all_x && i < d.neg().size(); ++i) {
271 all_x = (BIT_x == d.neg()[i][idx]);
272 }
273 idx = equalities.next(idx);
274 }
275 while (idx != root && all_x);
276 }
277 idx = root;
278 do {
279 if ((!discard_cols.get(idx) || !all_x) && idx != root1) {
280 tbv* t = m.allocate(d.pos());
281 m.set(*t, idx, BIT_0);
282 m.set(*t, root1, BIT_1);
283 d.neg().insert(tbvm(), t);
284 t = m.allocate(d.pos());
285 m.set(*t, idx, BIT_1);
286 m.set(*t, root1, BIT_0);
287 d.neg().insert(tbvm(), t);
288 }
289 idx = equalities.next(idx);
290 }
291 while (idx != root);
292 }
293 return true;
294 }
295
intersect(doc const & A,doc const & B,doc & result)296 bool doc_manager::intersect(doc const& A, doc const& B, doc& result) {
297 copy(result, A);
298 return set_and(result, B);
299 }
300
301 //
302 // 1. If n = 0,1: can project directly.
303 // 2. If tbv_i uses X in all positions with vars or constant where tbv is constant: can project directly.
304 // 3. Perform resolution on remaining tbv_i
305 //
306 // tbv & ~tbv1 & ~tbv2 & .. & ~tbv_n
307 // Semantics of ~tbv1 is that it is a clause of literals.
308 // indices where BIT_1 is set are negative.
309 // indices where BIT_0 is set are positive.
310 //
311
project(doc_manager & dstm,bit_vector const & to_delete,doc const & src)312 doc* doc_manager::project(doc_manager& dstm, bit_vector const& to_delete, doc const& src) {
313 tbv_manager& dstt = dstm.m;
314 tbv_ref t(dstt);
315 t = dstt.project(to_delete, src.pos());
316 doc* r = dstm.allocate(t.detach());
317 SASSERT(r);
318
319 if (src.neg().is_empty()) {
320 return r;
321 }
322
323 //
324 // A negation can be projected directly if it does not constrain
325 // deleted variables.
326 //
327 tbv_vector todo, new_todo;
328 for (unsigned i = 0; i < src.neg().size(); ++i) {
329 todo.push_back(tbvm().allocate(src.neg()[i]));
330 }
331 unsigned idx;
332 bool done = false;
333 while (!todo.empty() && !done) {
334 switch(pick_resolvent(src.pos(), todo, to_delete, idx)) {
335 case project_is_empty:
336 t = dstt.allocate(r->pos());
337 r->neg().push_back(t.detach());
338 done = true;
339 break;
340 case project_monolithic:
341 done = true;
342 break;
343 case project_neg:
344 case project_pos:
345 for (unsigned i = 0; i < todo.size(); ++i) {
346 tbv& tx = *todo[i];
347 if (tx[idx] == BIT_x) {
348 new_todo.push_back(&tx);
349 }
350 else {
351 m.deallocate(&tx);
352 }
353 }
354 std::swap(new_todo, todo);
355 new_todo.reset();
356 break;
357 case project_resolve: {
358 utbv pos, neg;
359 for (unsigned i = 0; i < todo.size(); ++i) {
360 tbv& tx = *todo[i];
361 switch(tx[idx]) {
362 case BIT_x: new_todo.push_back(&tx); break;
363 case BIT_0: neg.push_back(&tx); break;
364 case BIT_1: pos.push_back(&tx); break;
365 default: UNREACHABLE(); break;
366 }
367 }
368 TRACE("doc",
369 tout << "pos: ";
370 for (unsigned i = 0; i < pos.size(); ++i) {
371 tbvm().display(tout, pos[i]) << " ";
372 }
373 tout << "\nneg: ";
374 for (unsigned i = 0; i < neg.size(); ++i) {
375 tbvm().display(tout, neg[i]) << " ";
376 }
377 tout << "\n";
378 );
379 SASSERT(pos.size() > 0 && neg.size() > 0);
380 tbv_ref t1(m);
381 for (unsigned j = 0; j < pos.size(); ++j) {
382 for (unsigned k = 0; k < neg.size(); ++k) {
383 t1 = m.allocate(pos[j]);
384 m.set(*t1, idx, BIT_x);
385 if (tbvm().set_and(*t1, neg[k])) {
386 m.set(*t1, idx, BIT_x);
387 new_todo.push_back(t1.detach());
388 }
389 }
390 }
391 pos.reset(m);
392 neg.reset(m);
393 std::swap(todo, new_todo);
394 new_todo.reset();
395 break;
396 }
397 case project_done: {
398 for (unsigned i = 0; i < todo.size(); ++i) {
399 t = dstt.project(to_delete, *todo[i]);
400 if (dstt.equals(r->pos(), *t)) {
401 r->neg().reset(dstt);
402 r->neg().push_back(t.detach());
403 break;
404 }
405 if (r->neg().size() > 0 && dstt.equals(r->neg()[0], *t)) {
406 continue;
407 }
408 r->neg().push_back(t.detach());
409 }
410 done = true;
411 break;
412 }
413 }
414 }
415 for (unsigned i = 0; i < todo.size(); ++i) {
416 m.deallocate(todo[i]);
417 }
418 return r;
419 }
420
join(const doc & d1,const doc & d2,doc_manager & dm1,const unsigned_vector & cols1,const unsigned_vector & cols2)421 doc* doc_manager::join(const doc& d1, const doc& d2, doc_manager& dm1,
422 const unsigned_vector& cols1,
423 const unsigned_vector& cols2) {
424 doc_ref d(*this, allocateX());
425 tbv_ref t(m);
426 tbv& pos = d->pos();
427 utbv& neg = d->neg();
428 unsigned mid = dm1.num_tbits();
429 unsigned hi = num_tbits();
430 m.set(pos, d1.pos(), mid - 1, 0);
431 m.set(pos, d2.pos(), hi - 1, mid);
432 SASSERT(well_formed(*d));
433
434 // first fix bits
435 for (unsigned i = 0; i < cols1.size(); ++i) {
436 unsigned idx1 = cols1[i];
437 unsigned idx2 = mid + cols2[i];
438 tbit v1 = pos[idx1];
439 tbit v2 = pos[idx2];
440
441 if (v1 == BIT_x) {
442 if (v2 != BIT_x)
443 m.set(pos, idx1, v2);
444 }
445 else if (v2 == BIT_x) {
446 m.set(pos, idx2, v1);
447 }
448 else if (v1 != v2) {
449 // columns don't match
450 return nullptr;
451 }
452 SASSERT(well_formed(*d));
453 }
454
455 // fix equality of don't care columns
456 for (unsigned i = 0; i < cols1.size(); ++i) {
457 unsigned idx1 = cols1[i];
458 unsigned idx2 = mid + cols2[i];
459 unsigned v1 = pos[idx1];
460 unsigned v2 = pos[idx2];
461
462 if (v1 == BIT_x && v2 == BIT_x) {
463 // add to subtracted TBVs: 1xx0 and 0xx1
464 t = m.allocate(pos);
465 m.set(*t, idx1, BIT_0);
466 m.set(*t, idx2, BIT_1);
467 neg.push_back(t.detach());
468 t = m.allocate(pos);
469 m.set(*t, idx1, BIT_1);
470 m.set(*t, idx2, BIT_0);
471 neg.push_back(t.detach());
472 }
473 SASSERT(well_formed(*d));
474 }
475
476 // handle subtracted TBVs: 1010 -> 1010xxx
477 for (unsigned i = 0; i < d1.neg().size(); ++i) {
478 t = m.allocateX();
479 m.set(*t, d1.neg()[i], mid - 1, 0);
480 if (m.set_and(*t, pos))
481 neg.push_back(t.detach());
482 SASSERT(well_formed(*d));
483 }
484 for (unsigned i = 0; i < d2.neg().size(); ++i) {
485 t = m.allocateX();
486 m.set(*t, d2.neg()[i], hi - 1, mid);
487 if (m.set_and(*t, pos))
488 neg.push_back(t.detach());
489 SASSERT(well_formed(*d));
490 }
491 SASSERT(well_formed(*d));
492
493 return d.detach();
494 }
495
496 doc_manager::project_action_t
pick_resolvent(tbv const & pos,tbv_vector const & neg,bit_vector const & to_delete,unsigned & idx)497 doc_manager::pick_resolvent(
498 tbv const& pos, tbv_vector const& neg, bit_vector const& to_delete, unsigned& idx) {
499 if (neg.empty()) return project_done;
500 for (unsigned j = 0; j < neg.size(); ++j) {
501 if (m.equals(pos, *neg[j])) return project_is_empty;
502 }
503
504 unsigned best_pos = UINT_MAX;
505 unsigned best_neg = UINT_MAX;
506 unsigned best_idx = UINT_MAX;
507 for (unsigned i = 0; i < num_tbits(); ++i) {
508 if (!to_delete.get(i)) continue;
509 if (pos[i] != BIT_x) continue;
510 unsigned num_pos = 0, num_neg = 0;
511 tbit b1 = (*neg[0])[i];
512 if (b1 == BIT_0) num_neg++;
513 if (b1 == BIT_1) num_pos++;
514 bool monolithic = true;
515 for (unsigned j = 1; j < neg.size(); ++j) {
516 tbit b2 = (*neg[j])[i];
517 if (b1 != b2) {
518 monolithic = false;
519 }
520 if (b2 == BIT_0) num_neg++;
521 if (b2 == BIT_1) num_pos++;
522 }
523 if (monolithic && b1 != BIT_x) {
524 idx = i;
525 return project_monolithic;
526 }
527 if (monolithic && b1 == BIT_x) {
528 continue;
529 }
530 SASSERT(!monolithic);
531 if (num_pos == 0) {
532 SASSERT(num_neg > 0);
533 idx = i;
534 return project_neg;
535 }
536 if (num_neg == 0) {
537 SASSERT(num_pos > 0);
538 idx = i;
539 return project_pos;
540 }
541 if ((best_pos >= num_pos && best_neg >= num_neg) ||
542 num_neg == 1 || num_pos == 1) {
543 best_pos = num_pos;
544 best_neg = num_neg;
545 best_idx = i;
546 }
547 }
548 if (best_idx != UINT_MAX) {
549 idx = best_idx;
550 return project_resolve;
551 }
552 else {
553 return project_done;
554 }
555 }
556
557
558
complement(doc const & src,doc_vector & result)559 void doc_manager::complement(doc const& src, doc_vector& result) {
560 result.reset();
561 if (is_full(src)) {
562 return;
563 }
564 doc* r = allocateX();
565 r->neg().push_back(m.allocate(src.pos()));
566 result.push_back(r);
567 for (unsigned i = 0; i < src.neg().size(); ++i) {
568 result.push_back(allocate(src.neg()[i]));
569 }
570 }
571 // (A \ {A1}) \ (B \ {B1})
572 // (A & !A1 & & !B) | (A & B1 & !A1)
573 // A \ {A1 u B} u (A & B1) \ {A1}
subtract(doc const & A,doc const & B,doc_vector & result)574 void doc_manager::subtract(doc const& A, doc const& B, doc_vector& result) {
575 doc_ref r(*this);
576 tbv_ref t(m);
577 r = allocate(A);
578 t = m.allocate(B.pos());
579 if (m.set_and(*t, A.pos())) {
580 r->neg().insert(m, t.detach());
581 }
582 if (fold_neg(*r))
583 result.push_back(r.detach());
584
585 for (unsigned i = 0; i < B.neg().size(); ++i) {
586 r = allocate(A);
587 if (set_and(*r, B.neg()[i])) {
588 result.push_back(r.detach());
589 }
590 }
591 }
equals(doc const & a,doc const & b) const592 bool doc_manager::equals(doc const& a, doc const& b) const {
593 if (!m.equals(a.pos(), b.pos())) return false;
594 if (a.neg().size() != b.neg().size()) return false;
595 for (unsigned i = 0; i < a.neg().size(); ++i) {
596 if (!m.equals(a.neg()[i], b.neg()[i])) return false;
597 }
598 return true;
599 }
is_full(doc const & src) const600 bool doc_manager::is_full(doc const& src) const {
601 return src.neg().is_empty() && m.equals(src.pos(), *m_full);
602 }
is_empty_complete(ast_manager & m,doc const & src)603 bool doc_manager::is_empty_complete(ast_manager& m, doc const& src) {
604 if (src.neg().size() == 0) return false;
605
606 smt_params fp;
607 smt::kernel s(m, fp);
608 expr_ref fml = to_formula(m, src);
609 s.assert_expr(fml);
610 lbool res = s.check();
611 if (res == l_true) {
612 return false;
613 }
614 SASSERT(res == l_false);
615 return true;
616 }
617
hash(doc const & src) const618 unsigned doc_manager::hash(doc const& src) const {
619 unsigned r = 0;
620 for (unsigned i = 0; i < src.neg().size(); ++i) {
621 r = 2*r + m.hash(src.neg()[i]);
622 }
623 return r + m.hash(src.pos());
624 }
625 // approximation
626 // A \ (A1 u A2) contains B \ (B1 u B2)
627 // if
628 // A contains B
629 // B1 contains A1 or B2 contains A1
630 // B1 contains A2 or B2 contains A2
contains(doc const & a,doc const & b) const631 bool doc_manager::contains(doc const& a, doc const& b) const {
632 if (!m.contains(a.pos(), b.pos())) return false;
633 for (unsigned i = 0; i < a.neg().size(); ++i) {
634 bool found = false;
635 for (unsigned j = 0; !found && j < b.neg().size(); ++j) {
636 found = m.contains(b.neg()[j],a.neg()[i]);
637 }
638 if (!found) return false;
639 }
640 return true;
641 }
642
contains(doc const & a,unsigned_vector const & colsa,doc const & b,unsigned_vector const & colsb) const643 bool doc_manager::contains(doc const& a, unsigned_vector const& colsa,
644 doc const& b, unsigned_vector const& colsb) const {
645 if (!m.contains(a.pos(), colsa, b.pos(), colsb))
646 return false;
647
648 for (unsigned i = 0; i < a.neg().size(); ++i) {
649 bool found = false;
650 for (unsigned j = 0; !found && j < b.neg().size(); ++j) {
651 found = m.contains(b.neg()[j], colsb, a.neg()[i], colsa);
652 }
653 if (!found) return false;
654 }
655 return true;
656 }
657
display(std::ostream & out,doc const & b) const658 std::ostream& doc_manager::display(std::ostream& out, doc const& b) const {
659 if (num_tbits() == 0) return out << "[]";
660 return display(out, b, num_tbits()-1, 0);
661 }
662
display(std::ostream & out,doc const & b,unsigned hi,unsigned lo) const663 std::ostream& doc_manager::display(std::ostream& out, doc const& b, unsigned hi, unsigned lo) const {
664 m.display(out, b.pos(), hi, lo);
665 if (b.neg().is_empty()) return out;
666 out << " \\ ";
667 b.neg().display(m, out, hi, lo);
668 return out;
669 }
670
671
verify_project(ast_manager & m,doc_manager & dstm,bit_vector const & to_delete,doc const & src,doc const & dst)672 void doc_manager::verify_project(ast_manager& m, doc_manager& dstm, bit_vector const& to_delete, doc const& src, doc const& dst) {
673 expr_ref fml1 = to_formula(m, src);
674 expr_ref fml2 = dstm.to_formula(m, dst);
675 project_rename(fml2, to_delete);
676 project_expand(fml1, to_delete);
677 check_equiv(m, fml1, fml2);
678 }
679
check_equiv(ast_manager & m,expr * fml1,expr * fml2)680 void doc_manager::check_equiv(ast_manager& m, expr* fml1, expr* fml2) {
681 smt_params fp;
682 smt::kernel solver(m, fp);
683 expr_ref fml(m);
684 fml = m.mk_not(m.mk_eq(fml1, fml2));
685 solver.assert_expr(fml);
686 lbool res = solver.check();
687 if (res != l_false) {
688 TRACE("doc",
689 tout << mk_pp(fml1, m) << "\n";
690 tout << mk_pp(fml2, m) << "\n";
691 );
692 UNREACHABLE();
693 throw 0;
694 }
695 SASSERT(res == l_false);
696 }
697
to_formula(ast_manager & m,doc const & src)698 expr_ref doc_manager::to_formula(ast_manager& m, doc const& src) {
699 expr_ref result(m);
700 expr_ref_vector conj(m);
701 conj.push_back(tbvm().to_formula(m, src.pos()));
702 for (unsigned i = 0; i < src.neg().size(); ++i) {
703 conj.push_back(m.mk_not(tbvm().to_formula(m, src.neg()[i])));
704 }
705 result = mk_and(m, conj.size(), conj.c_ptr());
706 return result;
707 }
708
project_expand(expr_ref & fml,bit_vector const & to_delete)709 void doc_manager::project_expand(expr_ref& fml, bit_vector const& to_delete) {
710 ast_manager& m = fml.get_manager();
711 expr_ref tmp1(m), tmp2(m);
712 for (unsigned i = 0; i < num_tbits(); ++i) {
713 if (to_delete.get(i)) {
714 expr_safe_replace rep1(m), rep2(m);
715 rep1.insert(tbvm().mk_var(m, i), m.mk_true());
716 rep1(fml, tmp1);
717 rep2.insert(tbvm().mk_var(m, i), m.mk_false());
718 rep2(fml, tmp2);
719 if (tmp1 == tmp2) {
720 fml = tmp1;
721 }
722 else {
723 fml = m.mk_or(tmp1, tmp2);
724 }
725 }
726 }
727 }
728
project_rename(expr_ref & fml,bit_vector const & to_delete)729 void doc_manager::project_rename(expr_ref& fml, bit_vector const& to_delete) {
730 ast_manager& m = fml.get_manager();
731 expr_safe_replace rep(m);
732 for (unsigned i = 0, j = 0; i < num_tbits(); ++i) {
733 if (!to_delete.get(i)) {
734 rep.insert(tbvm().mk_var(m, j), tbvm().mk_var(m, i));
735 ++j;
736 }
737 }
738 rep(fml);
739 }
740