best effort evaluator of extensional array equality. */
| 534 | best effort evaluator of extensional array equality. |
| 535 | */ |
| 536 | void model_implicant::eval_array_eq(app* e, expr* arg1, expr* arg2) { |
| 537 | TRACE(pdr, tout << "array equality: " << mk_pp(e, m) << "\n";); |
| 538 | expr_ref v1 = (*m_model)(arg1); |
| 539 | expr_ref v2 = (*m_model)(arg2); |
| 540 | if (v1 == v2) { |
| 541 | set_true(e); |
| 542 | return; |
| 543 | } |
| 544 | sort* s = arg1->get_sort(); |
| 545 | sort* r = get_array_range(s); |
| 546 | // give up evaluating finite domain/range arrays |
| 547 | if (!r->is_infinite() && !r->is_very_big() && !s->is_infinite() && !s->is_very_big()) { |
| 548 | TRACE(pdr, tout << "equality is unknown: " << mk_pp(e, m) << "\n";); |
| 549 | set_x(e); |
| 550 | return; |
| 551 | } |
| 552 | vector<expr_ref_vector> store; |
| 553 | expr_ref else1(m), else2(m); |
| 554 | if (!extract_array_func_interp(v1, store, else1) || |
| 555 | !extract_array_func_interp(v2, store, else2)) { |
| 556 | TRACE(pdr, tout << "equality is unknown: " << mk_pp(e, m) << "\n";); |
| 557 | set_x(e); |
| 558 | return; |
| 559 | } |
| 560 | |
| 561 | if (else1 != else2) { |
| 562 | if (m.is_value(else1) && m.is_value(else2)) { |
| 563 | TRACE(pdr, tout |
| 564 | << "defaults are different: " << mk_pp(e, m) << " " |
| 565 | << mk_pp(else1, m) << " " << mk_pp(else2, m) << "\n";); |
| 566 | set_false(e); |
| 567 | } |
| 568 | else if (m_array.is_array(else1)) { |
| 569 | eval_array_eq(e, else1, else2); |
| 570 | } |
| 571 | else { |
| 572 | TRACE(pdr, tout << "equality is unknown: " << mk_pp(e, m) << "\n";); |
| 573 | set_x(e); |
| 574 | } |
| 575 | return; |
| 576 | } |
| 577 | |
| 578 | expr_ref s1(m), s2(m), w1(m), w2(m); |
| 579 | expr_ref_vector args1(m), args2(m); |
| 580 | args1.push_back(v1); |
| 581 | args2.push_back(v2); |
| 582 | for (unsigned i = 0; i < store.size(); ++i) { |
| 583 | args1.resize(1); |
| 584 | args2.resize(1); |
| 585 | args1.append(store[i].size()-1, store[i].data()); |
| 586 | args2.append(store[i].size()-1, store[i].data()); |
| 587 | s1 = m_array.mk_select(args1.size(), args1.data()); |
| 588 | s2 = m_array.mk_select(args2.size(), args2.data()); |
| 589 | w1 = (*m_model)(s1); |
| 590 | w2 = (*m_model)(s2); |
| 591 | if (w1 == w2) { |
| 592 | continue; |
| 593 | } |
nothing calls this directly
no test coverage detected