1 /*++ 2 Copyright (c) 2015 Microsoft Corporation 3 4 Module Name: 5 6 mbp_arrays.cpp 7 8 Abstract: 9 10 Model based projection for arrays 11 12 Author: 13 14 Nikolaj Bjorner (nbjorner) 2015-06-13 15 16 Revision History: 17 18 --*/ 19 20 21 #include "util/lbool.h" 22 #include "ast/rewriter/rewriter_def.h" 23 #include "ast/expr_functors.h" 24 #include "ast/for_each_expr.h" 25 #include "ast/rewriter/expr_safe_replace.h" 26 #include "ast/rewriter/th_rewriter.h" 27 #include "ast/ast_util.h" 28 #include "ast/ast_pp.h" 29 #include "model/model_evaluator.h" 30 #include "qe/mbp/mbp_arrays.h" 31 #include "qe/mbp/mbp_term_graph.h" 32 33 34 namespace { 35 bool is_partial_eq (app* a); 36 37 /** 38 * \brief utility class for partial equalities 39 * 40 * A partial equality (a ==I b), for two arrays a,b and a finite set of indices I holds 41 * iff (Forall i. i \not\in I => a[i] == b[i]); in other words, it is a 42 * restricted form of the extensionality axiom 43 * 44 * using this class, we denote (a =I b) as f(a,b,i0,i1,...) 45 * where f is an uninterpreted predicate with name PARTIAL_EQ and 46 * I = {i0,i1,...} 47 */ 48 49 // TBD: make work for arrays with multiple arguments. 50 class peq { 51 ast_manager& m; 52 expr_ref m_lhs; 53 expr_ref m_rhs; 54 vector<expr_ref_vector> m_diff_indices; 55 func_decl_ref m_decl; // the partial equality declaration 56 app_ref m_peq; // partial equality application 57 app_ref m_eq; // equivalent std equality using def. of partial eq 58 array_util m_arr_u; 59 60 public: 61 static const char* PARTIAL_EQ; 62 peq(app * p,ast_manager & m)63 peq (app* p, ast_manager& m): 64 m (m), 65 m_lhs (p->get_arg (0), m), 66 m_rhs (p->get_arg (1), m), 67 m_decl (p->get_decl (), m), 68 m_peq (p, m), 69 m_eq (m), 70 m_arr_u (m) 71 { 72 VERIFY (is_partial_eq (p)); 73 SASSERT (m_arr_u.is_array (m_lhs) && 74 m_arr_u.is_array (m_rhs) && 75 m.get_sort(m_lhs) == m.get_sort(m_rhs)); 76 unsigned arity = get_array_arity(m.get_sort(m_lhs)); 77 for (unsigned i = 2; i < p->get_num_args (); i += arity) { 78 SASSERT(arity + i <= p->get_num_args()); 79 expr_ref_vector vec(m); 80 vec.append(arity, p->get_args() + i); 81 m_diff_indices.push_back (vec); 82 } 83 } 84 peq(expr * lhs,expr * rhs,vector<expr_ref_vector> const & diff_indices,ast_manager & m)85 peq (expr* lhs, expr* rhs, vector<expr_ref_vector> const& diff_indices, ast_manager& m): 86 m (m), 87 m_lhs (lhs, m), 88 m_rhs (rhs, m), 89 m_diff_indices (diff_indices), 90 m_decl (m), 91 m_peq (m), 92 m_eq (m), 93 m_arr_u (m) { 94 SASSERT (m_arr_u.is_array (lhs) && 95 m_arr_u.is_array (rhs) && 96 m.get_sort(lhs) == m.get_sort(rhs)); 97 ptr_vector<sort> sorts; 98 sorts.push_back (m.get_sort (m_lhs)); 99 sorts.push_back (m.get_sort (m_rhs)); 100 for (auto const& v : diff_indices) { 101 SASSERT(v.size() == get_array_arity(m.get_sort(m_lhs))); 102 for (expr* e : v) 103 sorts.push_back (m.get_sort(e)); 104 } 105 m_decl = m.mk_func_decl (symbol (PARTIAL_EQ), sorts.size (), sorts.c_ptr (), m.mk_bool_sort ()); 106 } 107 lhs()108 expr_ref lhs () { return m_lhs; } 109 rhs()110 expr_ref rhs () { return m_rhs; } 111 get_diff_indices(vector<expr_ref_vector> & result)112 void get_diff_indices (vector<expr_ref_vector>& result) { result.append(m_diff_indices); } 113 mk_peq()114 app_ref mk_peq () { 115 if (!m_peq) { 116 ptr_vector<expr> args; 117 args.push_back (m_lhs); 118 args.push_back (m_rhs); 119 for (auto const& v : m_diff_indices) { 120 args.append (v.size(), v.c_ptr()); 121 } 122 m_peq = m.mk_app (m_decl, args.size (), args.c_ptr ()); 123 } 124 return m_peq; 125 } 126 mk_eq(app_ref_vector & aux_consts,bool stores_on_rhs=true)127 app_ref mk_eq (app_ref_vector& aux_consts, bool stores_on_rhs = true) { 128 if (!m_eq) { 129 expr_ref lhs (m_lhs, m), rhs (m_rhs, m); 130 if (!stores_on_rhs) { 131 std::swap (lhs, rhs); 132 } 133 // lhs = (...(store (store rhs i0 v0) i1 v1)...) 134 sort* val_sort = get_array_range (m.get_sort (lhs)); 135 for (expr_ref_vector const& diff : m_diff_indices) { 136 ptr_vector<expr> store_args; 137 store_args.push_back (rhs); 138 store_args.append (diff.size(), diff.c_ptr()); 139 app_ref val(m.mk_fresh_const ("diff", val_sort), m); 140 store_args.push_back (val); 141 aux_consts.push_back (val); 142 rhs = m_arr_u.mk_store (store_args); 143 } 144 m_eq = m.mk_eq (lhs, rhs); 145 } 146 return m_eq; 147 } 148 }; 149 150 const char* peq::PARTIAL_EQ = "!partial_eq"; 151 is_partial_eq(app * a)152 bool is_partial_eq (app* a) { 153 return a->get_decl ()->get_name () == peq::PARTIAL_EQ; 154 } 155 } 156 157 namespace mbp { 158 159 is_eq(expr_ref_vector const & xs,expr_ref_vector const & ys)160 static bool is_eq(expr_ref_vector const& xs, expr_ref_vector const& ys) { 161 for (unsigned i = 0; i < xs.size(); ++i) if (xs[i] != ys[i]) return false; 162 return true; 163 } 164 mk_eq(expr_ref_vector const & xs,expr_ref_vector const & ys)165 static expr_ref mk_eq(expr_ref_vector const& xs, expr_ref_vector const& ys) { 166 ast_manager& m = xs.get_manager(); 167 expr_ref_vector eqs(m); 168 for (unsigned i = 0; i < xs.size(); ++i) eqs.push_back(m.mk_eq(xs[i], ys[i])); 169 return mk_and(eqs); 170 } 171 172 /** 173 * 1. Extract all equalities (store (store .. (store x i1 v1) i2 v2) .. ) = ... 174 * where x appears and the equalities do not evaluate to false in the current model. 175 * 2. Track them as partial equivalence relations. 176 * 3. Sort them according to nesting depth. 177 * 4. Solve for x by potentially introducing fresh variables. 178 * Thus, (store x i v) = y, then 179 * x = (store y i w), (select y i) = v, where w is fresh and evaluates to (select x i). 180 * Generally, equalities are tracked as x =_idxs y, where x, y are equal up to idxs. 181 */ 182 183 class array_project_eqs_util { 184 ast_manager& m; 185 array_util m_arr_u; 186 model_ref M; 187 model_evaluator* m_mev; 188 app_ref m_v; // array var to eliminate 189 ast_mark m_has_stores_v; // has stores for m_v 190 expr_ref m_subst_term_v; // subst term for m_v 191 expr_safe_replace m_true_sub_v; // subst for true equalities 192 expr_safe_replace m_false_sub_v; // subst for false equalities 193 expr_ref_vector m_aux_lits_v; 194 expr_ref_vector m_idx_lits_v; 195 app_ref_vector m_aux_vars; 196 reset_v()197 void reset_v () { 198 m_v = nullptr; 199 m_has_stores_v.reset (); 200 m_subst_term_v = nullptr; 201 m_true_sub_v.reset (); 202 m_false_sub_v.reset (); 203 m_aux_lits_v.reset (); 204 m_idx_lits_v.reset (); 205 } 206 reset()207 void reset () { 208 M = nullptr; 209 m_mev = nullptr; 210 reset_v (); 211 m_aux_vars.reset (); 212 } 213 214 /** 215 * find all array equalities on m_v or containing stores on/of m_v 216 * 217 * also mark terms containing stores on/of m_v 218 */ find_arr_eqs(expr_ref const & fml,app_ref_vector & eqs)219 void find_arr_eqs (expr_ref const& fml, app_ref_vector& eqs) { 220 if (!is_app (fml)) return; 221 ast_mark done; 222 ptr_vector<app> todo; 223 todo.push_back (to_app (fml)); 224 while (!todo.empty ()) { 225 app* a = todo.back (); 226 if (done.is_marked (a)) { 227 todo.pop_back (); 228 continue; 229 } 230 bool all_done = true; 231 bool args_have_stores = false; 232 for (expr * arg : *a) { 233 if (!is_app (arg)) continue; 234 if (!done.is_marked (arg)) { 235 all_done = false; 236 todo.push_back (to_app (arg)); 237 } 238 else if (!args_have_stores && m_has_stores_v.is_marked (arg)) { 239 args_have_stores = true; 240 } 241 } 242 if (!all_done) continue; 243 todo.pop_back (); 244 245 // mark if a has stores 246 if ((!m_arr_u.is_select (a) && args_have_stores) || 247 (m_arr_u.is_store (a) && (a->get_arg (0) == m_v))) { 248 m_has_stores_v.mark (a, true); 249 250 TRACE ("qe", 251 tout << "has stores:\n"; 252 tout << mk_pp (a, m) << "\n"; 253 ); 254 } 255 256 // check if a is a relevant array equality 257 expr * a0 = nullptr, *a1 = nullptr; 258 if (m.is_eq (a, a0, a1)) { 259 if (a0 == m_v || a1 == m_v || 260 (m_arr_u.is_array (a0) && m_has_stores_v.is_marked (a))) { 261 eqs.push_back (a); 262 } 263 } 264 // else, we can check for disequalities and handle them using extensionality, 265 // but it's not necessary 266 267 done.mark (a, true); 268 } 269 } 270 271 /** 272 * factor out select terms on m_v using fresh consts 273 */ factor_selects(app_ref & fml)274 void factor_selects (app_ref& fml) { 275 expr_map sel_cache (m); 276 ast_mark done; 277 ptr_vector<app> todo; 278 expr_ref_vector pinned (m); // to ensure a reference 279 280 todo.push_back (fml); 281 while (!todo.empty ()) { 282 app* a = todo.back (); 283 if (done.is_marked (a)) { 284 todo.pop_back (); 285 continue; 286 } 287 expr_ref_vector args (m); 288 bool all_done = true; 289 for (expr * arg : *a) { 290 if (!is_app (arg)) { 291 args.push_back(arg); 292 } 293 else if (!done.is_marked (arg)) { 294 all_done = false; 295 todo.push_back (to_app (arg)); 296 } 297 else if (all_done) { // all done so far.. 298 expr* arg_new = nullptr; proof* pr; 299 sel_cache.get (arg, arg_new, pr); 300 if (!arg_new) { 301 arg_new = arg; 302 } 303 args.push_back (arg_new); 304 } 305 } 306 if (!all_done) continue; 307 todo.pop_back (); 308 309 expr_ref a_new (m.mk_app (a->get_decl (), args.size (), args.c_ptr ()), m); 310 311 // if a_new is select on m_v, introduce new constant 312 if (m_arr_u.is_select (a) && 313 (args.get (0) == m_v || m_has_stores_v.is_marked (args.get (0)))) { 314 sort* val_sort = get_array_range (m.get_sort (m_v)); 315 app_ref val_const (m.mk_fresh_const ("sel", val_sort), m); 316 m_aux_vars.push_back (val_const); 317 // extend M to include val_const 318 expr_ref val = (*m_mev)(a_new); 319 M->register_decl (val_const->get_decl (), val); 320 // add equality 321 m_aux_lits_v.push_back (m.mk_eq (val_const, a_new)); 322 // replace select by const 323 a_new = val_const; 324 } 325 326 if (a != a_new) { 327 sel_cache.insert (a, a_new, nullptr); 328 pinned.push_back (a_new); 329 } 330 done.mark (a, true); 331 } 332 expr* res = nullptr; proof* pr; 333 sel_cache.get (fml, res, pr); 334 if (res) { 335 fml = to_app (res); 336 } 337 } 338 339 /** 340 * convert partial equality expression p_exp to an equality by 341 * recursively adding stores on diff indices 342 * 343 * add stores on lhs or rhs depending on whether stores_on_rhs is false/true 344 */ convert_peq_to_eq(expr * p_exp,app_ref & eq,bool stores_on_rhs=true)345 void convert_peq_to_eq (expr* p_exp, app_ref& eq, bool stores_on_rhs = true) { 346 peq p (to_app (p_exp), m); 347 app_ref_vector diff_val_consts (m); 348 eq = p.mk_eq (diff_val_consts, stores_on_rhs); 349 m_aux_vars.append (diff_val_consts); 350 // extend M to include diff_val_consts 351 vector<expr_ref_vector> I; 352 expr_ref arr = p.lhs (); 353 p.get_diff_indices (I); 354 expr_ref val (m); 355 unsigned num_diff = diff_val_consts.size (); 356 SASSERT (num_diff == I.size ()); 357 for (unsigned i = 0; i < num_diff; i++) { 358 // mk val term 359 ptr_vector<expr> sel_args; 360 sel_args.push_back (arr); 361 sel_args.append(I[i].size(), I[i].c_ptr()); 362 expr_ref val_term (m_arr_u.mk_select (sel_args), m); 363 // evaluate and assign to ith diff_val_const 364 val = (*m_mev)(val_term); 365 M->register_decl (diff_val_consts.get (i)->get_decl (), val); 366 } 367 } 368 369 /** 370 * mk (e0 ==indices e1) 371 * 372 * result has stores if either e0 or e1 or an index term has stores 373 */ mk_peq(expr * e0,expr * e1,vector<expr_ref_vector> const & indices)374 app_ref mk_peq (expr* e0, expr* e1, vector<expr_ref_vector> const& indices) { 375 peq p (e0, e1, indices, m); 376 return p.mk_peq (); 377 } 378 find_subst_term(app * eq)379 void find_subst_term (app* eq) { 380 SASSERT(m.is_eq(eq)); 381 vector<expr_ref_vector> empty; 382 app_ref p_exp = mk_peq (eq->get_arg (0), eq->get_arg (1), empty); 383 bool subst_eq_found = false; 384 while (true) { 385 TRACE ("qe", tout << "processing peq:\n" << p_exp << "\n";); 386 387 peq p (p_exp, m); 388 expr_ref lhs = p.lhs(), rhs = p.rhs(); 389 if (!m_has_stores_v.is_marked (lhs)) { 390 std::swap (lhs, rhs); 391 } 392 if (m_has_stores_v.is_marked (lhs) && m_arr_u.is_store(lhs)) { 393 /** project using the equivalence: 394 * 395 * (store(arr0,idx,x) ==I arr1) <-> 396 * 397 * (idx \in I => (arr0 ==I arr1)) /\ 398 * (idx \not\in I => (arr0 ==I+idx arr1) /\ (arr1[idx] == x))) 399 */ 400 vector<expr_ref_vector> I; 401 expr_ref_vector idxs (m); 402 p.get_diff_indices (I); 403 app* a_lhs = to_app (lhs); 404 expr* arr0 = a_lhs->get_arg (0); 405 idxs.append(a_lhs->get_num_args() - 2, a_lhs->get_args() + 1); 406 expr* x = a_lhs->get_arg (2); 407 expr* arr1 = rhs; 408 // check if (idx \in I) in M 409 bool idx_in_I = false; 410 expr_ref_vector idx_diseq (m); 411 if (!I.empty ()) { 412 expr_ref_vector vals = (*m_mev)(idxs); 413 for (unsigned i = 0; i < I.size () && !idx_in_I; i++) { 414 if (is_eq(idxs, I.get(i))) { 415 idx_in_I = true; 416 } 417 else { 418 expr_ref idx_eq = mk_eq(idxs, I[i]); 419 expr_ref_vector vals1 = (*m_mev)(I[i]); 420 if (is_eq(vals, vals1)) { 421 idx_in_I = true; 422 m_idx_lits_v.push_back (idx_eq); 423 } 424 else { 425 idx_diseq.push_back (m.mk_not (idx_eq)); 426 } 427 } 428 } 429 } 430 if (idx_in_I) { 431 TRACE ("qe", 432 tout << "store index in diff indices:\n"; 433 tout << mk_pp (m_idx_lits_v.back (), m) << "\n"; 434 ); 435 436 // arr0 ==I arr1 437 p_exp = mk_peq (arr0, arr1, I); 438 439 TRACE ("qe", 440 tout << "new peq:\n"; 441 tout << mk_pp (p_exp, m) << "\n"; 442 ); 443 } 444 else { 445 m_idx_lits_v.append (idx_diseq); 446 // arr0 ==I+idx arr1 447 I.push_back (idxs); 448 p_exp = mk_peq (arr0, arr1, I); 449 450 TRACE ("qe", tout << "new peq:\n" << p_exp << "\n"; ); 451 452 // arr1[idx] == x 453 ptr_vector<expr> sel_args; 454 sel_args.push_back (arr1); 455 sel_args.append(idxs.size(), idxs.c_ptr()); 456 expr_ref arr1_idx (m_arr_u.mk_select (sel_args), m); 457 expr_ref eq (m.mk_eq (arr1_idx, x), m); 458 m_aux_lits_v.push_back (eq); 459 460 TRACE ("qe", 461 tout << "new eq:\n"; 462 tout << mk_pp (eq, m) << "\n"; 463 ); 464 } 465 } 466 else if (lhs == rhs) { // trivial peq (a ==I a) 467 break; 468 } 469 else if (lhs == m_v || rhs == m_v) { 470 subst_eq_found = true; 471 TRACE ("qe", 472 tout << "subst eq found!\n"; 473 ); 474 break; 475 } 476 else { 477 UNREACHABLE (); 478 } 479 } 480 481 // factor out select terms on m_v from p_exp using fresh constants 482 if (subst_eq_found) { 483 factor_selects (p_exp); 484 485 TRACE ("qe", 486 tout << "after factoring selects:\n"; 487 tout << mk_pp (p_exp, m) << "\n"; 488 for (unsigned i = m_aux_lits_v.size () - m_aux_vars.size (); i < m_aux_lits_v.size (); i++) { 489 tout << mk_pp (m_aux_lits_v.get (i), m) << "\n"; 490 } 491 ); 492 493 // find subst_term 494 bool stores_on_rhs = true; 495 app* a = to_app (p_exp); 496 if (a->get_arg (1) == m_v) { 497 stores_on_rhs = false; 498 } 499 app_ref eq (m); 500 convert_peq_to_eq (p_exp, eq, stores_on_rhs); 501 m_subst_term_v = eq->get_arg (1); 502 503 TRACE ("qe", 504 tout << "subst term found:\n"; 505 tout << mk_pp (m_subst_term_v, m) << "\n"; 506 ); 507 } 508 } 509 510 /** 511 * compute nesting depths of stores on m_v in true_eqs, as follows: 512 * 0 if m_v appears on both sides of equality 513 * 1 if equality is (m_v=t) 514 * 2 if equality is (store(m_v,i,v)=t) 515 * ... 516 */ get_nesting_depth(app * eq)517 unsigned get_nesting_depth(app* eq) { 518 expr* lhs = nullptr, *rhs = nullptr; 519 VERIFY(m.is_eq(eq, lhs, rhs)); 520 bool lhs_has_v = (lhs == m_v || m_has_stores_v.is_marked (lhs)); 521 bool rhs_has_v = (rhs == m_v || m_has_stores_v.is_marked (rhs)); 522 app* store = nullptr; 523 524 SASSERT (lhs_has_v || rhs_has_v); 525 526 if (!lhs_has_v && is_app(rhs)) { 527 store = to_app (rhs); 528 } 529 else if (!rhs_has_v && is_app(lhs)) { 530 store = to_app (lhs); 531 } 532 else { 533 // v appears on both sides -- trivial equality 534 // put it in the beginning to simplify it away 535 return 0; 536 } 537 538 unsigned nd = 0; // nesting depth 539 for (nd = 1; m_arr_u.is_store (store); nd++, store = to_app (store->get_arg (0))) { 540 /* empty */ ; 541 } 542 if (store != m_v) { 543 TRACE("qe", tout << "not a store " << mk_pp(eq, m) << " " << lhs_has_v << " " << rhs_has_v << " " << mk_pp(m_v, m) << "\n";); 544 return UINT_MAX; 545 } 546 return nd; 547 } 548 549 struct compare_nd { operator ()mbp::array_project_eqs_util::compare_nd550 bool operator()(std::pair<unsigned, app*> const& x, std::pair<unsigned, app*> const& y) const { 551 return x < y; 552 } 553 }; 554 555 /** 556 * try to substitute for m_v, using array equalities 557 * 558 * compute substitution term and aux lits 559 */ project(expr_ref const & fml)560 bool project (expr_ref const& fml) { 561 app_ref_vector eqs (m); 562 svector<std::pair<unsigned, app*> > true_eqs; 563 564 find_arr_eqs (fml, eqs); 565 TRACE ("qe", tout << "array equalities:\n" << eqs << "\n";); 566 567 // evaluate eqs in M 568 for (app * eq : eqs) { 569 TRACE ("qe", tout << "array equality:\n" << mk_pp (eq, m) << "\n"; ); 570 571 if (m_mev->is_false(eq)) { 572 m_false_sub_v.insert (eq, m.mk_false()); 573 } 574 else { 575 true_eqs.push_back (std::make_pair(get_nesting_depth(eq), eq)); 576 } 577 } 578 std::sort(true_eqs.begin(), true_eqs.end(), compare_nd()); 579 DEBUG_CODE(for (unsigned i = 0; i + 1 < true_eqs.size(); ++i) SASSERT(true_eqs[i].first <= true_eqs[i+1].first);); 580 581 // search for subst term 582 for (unsigned i = 0; !m_subst_term_v && i < true_eqs.size(); i++) { 583 app* eq = true_eqs[i].second; 584 m_true_sub_v.insert (eq, m.mk_true ()); 585 // try to find subst term 586 find_subst_term (eq); 587 } 588 589 return true; 590 } 591 mk_result(expr_ref & fml)592 void mk_result (expr_ref& fml) { 593 th_rewriter rw(m); 594 rw (fml); 595 // add in aux_lits and idx_lits 596 expr_ref_vector lits (m); 597 // TODO: eliminate possible duplicates, especially in idx_lits 598 // theory rewriting is a possibility, but not sure if it 599 // introduces unwanted terms such as ite's 600 lits.append (m_idx_lits_v); 601 lits.append (m_aux_lits_v); 602 lits.push_back (fml); 603 fml = mk_and(lits); 604 605 if (m_subst_term_v) { 606 m_true_sub_v.insert (m_v, m_subst_term_v); 607 m_true_sub_v (fml); 608 } 609 else { 610 m_true_sub_v (fml); 611 m_false_sub_v (fml); 612 } 613 rw(fml); 614 SASSERT (!m.is_false (fml)); 615 } 616 617 public: 618 array_project_eqs_util(ast_manager & m)619 array_project_eqs_util (ast_manager& m): 620 m (m), 621 m_arr_u (m), 622 m_v (m), 623 m_subst_term_v (m), 624 m_true_sub_v (m), 625 m_false_sub_v (m), 626 m_aux_lits_v (m), 627 m_idx_lits_v (m), 628 m_aux_vars (m) 629 {} 630 operator ()(model & mdl,app_ref_vector & arr_vars,expr_ref & fml,app_ref_vector & aux_vars)631 void operator () (model& mdl, app_ref_vector& arr_vars, expr_ref& fml, app_ref_vector& aux_vars) { 632 reset (); 633 model_evaluator mev(mdl); 634 mev.set_model_completion(true); 635 M = &mdl; 636 m_mev = &mev; 637 638 unsigned j = 0; 639 for (unsigned i = 0; i < arr_vars.size (); i++) { 640 reset_v (); 641 m_v = arr_vars.get (i); 642 if (!m_arr_u.is_array (m_v)) { 643 TRACE ("qe", 644 tout << "not an array variable: " << m_v << "\n"; 645 ); 646 aux_vars.push_back (m_v); 647 continue; 648 } 649 TRACE ("qe", tout << "projecting equalities on variable: " << m_v << "\n"; ); 650 651 if (project (fml)) { 652 mk_result (fml); 653 654 contains_app contains_v (m, m_v); 655 if (!m_subst_term_v || contains_v (m_subst_term_v)) { 656 arr_vars[j++] = m_v; 657 } 658 TRACE ("qe", tout << "after projection: \n" << fml << "\n";); 659 } 660 else { 661 IF_VERBOSE(2, verbose_stream() << "can't project:" << m_v << "\n";); 662 TRACE ("qe", tout << "Failed to project: " << m_v << "\n";); 663 arr_vars[j++] = m_v; 664 } 665 } 666 arr_vars.shrink(j); 667 aux_vars.append (m_aux_vars); 668 } 669 }; 670 671 /** 672 * Eliminate (select (store ..) ..) redexes by evaluating indices under model M. 673 * This does not eliminate variables, but introduces additional constraints on index equalities. 674 */ 675 676 class array_select_reducer { 677 ast_manager& m; 678 array_util m_arr_u; 679 obj_map<expr, expr*> m_cache; 680 expr_ref_vector m_pinned; // to ensure a reference 681 expr_ref_vector m_idx_lits; 682 model_ref M; 683 model_evaluator* m_mev; 684 th_rewriter m_rw; 685 ast_mark m_arr_test; 686 ast_mark m_has_stores; 687 bool m_reduce_all_selects; 688 reset()689 void reset () { 690 m_cache.reset (); 691 m_pinned.reset (); 692 m_idx_lits.reset (); 693 M = nullptr; 694 m_mev = nullptr; 695 m_arr_test.reset (); 696 m_has_stores.reset (); 697 m_reduce_all_selects = false; 698 } 699 is_equals(expr * e1,expr * e2)700 bool is_equals (expr *e1, expr *e2) { 701 return e1 == e2 || (*m_mev)(e1) == (*m_mev)(e2); 702 } 703 is_equals(unsigned arity,expr * const * xs,expr * const * ys)704 bool is_equals (unsigned arity, expr * const* xs, expr * const * ys) { 705 for (unsigned i = 0; i < arity; ++i) { 706 if (!is_equals(xs[i], ys[i])) return false; 707 } 708 return true; 709 } 710 mk_eq(unsigned arity,expr * const * xs,expr * const * ys)711 expr_ref mk_eq(unsigned arity, expr * const* xs, expr * const * ys) { 712 expr_ref_vector r(m); 713 for (unsigned i = 0; i < arity; ++i) { 714 r.push_back(m.mk_eq(xs[i], ys[i])); 715 } 716 return mk_and(r); 717 } 718 add_idx_cond(expr_ref & cond)719 void add_idx_cond (expr_ref& cond) { 720 m_rw (cond); 721 if (!m.is_true (cond)) m_idx_lits.push_back (cond); 722 } 723 has_stores(expr * e)724 bool has_stores (expr* e) { 725 if (m_reduce_all_selects) return true; 726 return m_has_stores.is_marked (e); 727 } 728 mark_stores(app * a,bool args_have_stores)729 void mark_stores (app* a, bool args_have_stores) { 730 if (m_reduce_all_selects) return; 731 if (args_have_stores || 732 (m_arr_u.is_store (a) && m_arr_test.is_marked (a->get_arg (0)))) { 733 m_has_stores.mark (a, true); 734 } 735 } 736 reduce(expr_ref & e)737 bool reduce (expr_ref& e) { 738 if (!is_app (e)) return true; 739 740 expr *r = nullptr; 741 if (m_cache.find (e, r)) { 742 e = r; 743 return true; 744 } 745 746 ptr_vector<app> todo; 747 todo.push_back (to_app (e)); 748 expr_ref_vector args (m); 749 750 while (!todo.empty ()) { 751 app *a = todo.back (); 752 unsigned sz = todo.size (); 753 bool dirty = false; 754 bool args_have_stores = false; 755 args.reset(); 756 for (expr * arg : *a) { 757 expr *narg = nullptr; 758 if (!is_app (arg)) { 759 args.push_back (arg); 760 } 761 else if (m_cache.find (arg, narg)) { 762 args.push_back (narg); 763 dirty |= (arg != narg); 764 if (!args_have_stores && has_stores (narg)) { 765 args_have_stores = true; 766 } 767 } 768 else { 769 todo.push_back (to_app (arg)); 770 } 771 } 772 773 if (todo.size () > sz) continue; 774 todo.pop_back (); 775 776 if (dirty) { 777 r = m.mk_app (a->get_decl (), args.size (), args.c_ptr ()); 778 m_pinned.push_back (r); 779 } 780 else { 781 r = a; 782 } 783 784 if (m_arr_u.is_select (r) && has_stores (to_app (r)->get_arg (0))) { 785 r = reduce_core (to_app(r)); 786 } 787 else { 788 mark_stores (to_app (r), args_have_stores); 789 } 790 791 m_cache.insert (a, r); 792 } 793 794 SASSERT (r); 795 e = r; 796 return true; 797 } 798 799 /** 800 * \brief reduce (select (store (store x i1 v1) i2 v2) idx) under model M 801 * such that the result is v2 if idx = i2 under M, it is v1 if idx = i1, idx != i2 under M, 802 * and it is (select x idx) if idx != i1, idx !+ i2 under M. 803 */ reduce_core(app * a)804 expr* reduce_core (app *a) { 805 if (!m_arr_u.is_store (a->get_arg (0))) return a; 806 expr* array = a->get_arg(0); 807 unsigned arity = get_array_arity(m.get_sort(array)); 808 809 expr* const* js = a->get_args() + 1; 810 811 while (m_arr_u.is_store (array)) { 812 a = to_app (array); 813 expr* const* idxs = a->get_args() + 1; 814 expr_ref cond = mk_eq(arity, idxs, js); 815 816 if (is_equals (arity, idxs, js)) { 817 add_idx_cond (cond); 818 return a->get_arg (a->get_num_args() - 1); 819 } 820 else { 821 cond = m.mk_not (cond); 822 add_idx_cond (cond); 823 array = a->get_arg (0); 824 } 825 } 826 ptr_vector<expr> args; 827 args.push_back(array); 828 args.append(arity, js); 829 expr* r = m_arr_u.mk_select (args); 830 m_pinned.push_back (r); 831 return r; 832 } 833 mk_result(expr_ref & fml)834 void mk_result (expr_ref& fml) { 835 // conjoin idx lits 836 expr_ref_vector lits (m); 837 lits.append (m_idx_lits); 838 lits.push_back (fml); 839 fml = mk_and(lits); 840 // simplify all trivial expressions introduced 841 m_rw (fml); 842 TRACE ("qe", tout << "after reducing selects:\n" << fml << "\n";); 843 } 844 845 public: 846 array_select_reducer(ast_manager & m)847 array_select_reducer (ast_manager& m): 848 m (m), 849 m_arr_u (m), 850 m_pinned (m), 851 m_idx_lits (m), 852 m_rw (m), 853 m_reduce_all_selects (false) 854 {} 855 operator ()(model & mdl,app_ref_vector const & arr_vars,expr_ref & fml,bool reduce_all_selects=false)856 void operator () (model& mdl, app_ref_vector const& arr_vars, expr_ref& fml, bool reduce_all_selects = false) { 857 if (!reduce_all_selects && arr_vars.empty ()) return; 858 859 reset (); 860 model_evaluator mev(mdl); 861 mev.set_model_completion(true); 862 M = &mdl; 863 m_mev = &mev; 864 m_reduce_all_selects = reduce_all_selects; 865 866 // mark vars to eliminate 867 for (app* v : arr_vars) { 868 m_arr_test.mark (v, true); 869 } 870 871 // assume all arr_vars are of array sort 872 // and assume no store equalities on arr_vars 873 if (reduce (fml)) { 874 mk_result (fml); 875 } 876 else { 877 IF_VERBOSE(2, verbose_stream() << "can't project arrays:" << "\n";); 878 TRACE ("qe", tout << "Failed to project arrays\n";); 879 } 880 } 881 }; 882 883 /** 884 * Perform Ackerman reduction on arrays. 885 * for occurrences (select a i1), (select a i2), ... assuming these are all occurrences. 886 * - collect i1, i2, i3, into equivalence classes according to M 887 * - for distinct index classes accumulate constraint i1 < i2 < i3 .. (for arithmetic) 888 * and generally distinct(i1, i2, i3) for arbitrary index sorts. 889 * - for equal indices accumulate constraint i1 = i2, i3 = i5, .. 890 * - introduce variables v1, v2, .., for each equivalence class. 891 * - replace occurrences of select by v1, v2, ... 892 * - update M to evaluate v1, v2, the same as (select a i1) (select a i2) 893 */ 894 895 class array_project_selects_util { 896 typedef obj_map<app, ptr_vector<app>*> sel_map; 897 898 struct idx_val { 899 expr_ref_vector idx; 900 expr_ref_vector val; 901 vector<rational> rval; idx_valmbp::array_project_selects_util::idx_val902 idx_val(expr_ref_vector && idx, expr_ref_vector && val, vector<rational> && rval): 903 idx(std::move(idx)), val(std::move(val)), rval(std::move(rval)) {} 904 }; 905 ast_manager& m; 906 array_util m_arr_u; 907 arith_util m_ari_u; 908 bv_util m_bv_u; 909 sel_map m_sel_terms; 910 // representative indices for eliminating selects 911 vector<idx_val> m_idxs; 912 app_ref_vector m_sel_consts; 913 expr_ref_vector m_idx_lits; 914 model_ref M; 915 model_evaluator* m_mev; 916 expr_safe_replace m_sub; 917 ast_mark m_arr_test; 918 reset()919 void reset () { 920 m_sel_terms.reset (); 921 m_idxs.reset(); 922 m_sel_consts.reset (); 923 m_idx_lits.reset (); 924 M = nullptr; 925 m_mev = nullptr; 926 m_sub.reset (); 927 m_arr_test.reset (); 928 } 929 930 /** 931 * collect sel terms on array vars as given by m_arr_test 932 */ collect_selects(expr * fml)933 void collect_selects (expr* fml) { 934 if (!is_app (fml)) return; 935 ast_mark done; 936 ptr_vector<app> todo; 937 todo.push_back (to_app (fml)); 938 for (unsigned i = 0; i < todo.size(); ++i) { 939 app* a = todo[i]; 940 if (done.is_marked (a)) continue; 941 done.mark (a, true); 942 for (expr* arg : *a) { 943 if (!done.is_marked (arg) && is_app (arg)) { 944 todo.push_back (to_app (arg)); 945 } 946 } 947 if (m_arr_u.is_select (a)) { 948 expr* arr = a->get_arg (0); 949 if (m_arr_test.is_marked (arr)) { 950 ptr_vector<app>* lst = m_sel_terms.find (to_app (arr));; 951 lst->push_back (a); 952 } 953 } 954 } 955 } 956 to_num(expr_ref_vector const & vals)957 vector<rational> to_num(expr_ref_vector const& vals) { 958 vector<rational> rs; 959 rational r; 960 for (expr* v : vals) { 961 if (m_bv_u.is_bv(v)) { 962 VERIFY (m_bv_u.is_numeral(v, r)); 963 } 964 else if (m_ari_u.is_real(v) || m_ari_u.is_int(v)) { 965 VERIFY (m_ari_u.is_numeral(v, r)); 966 } 967 else { 968 r.reset(); 969 } 970 rs.push_back(std::move(r)); 971 } 972 return rs; 973 } 974 975 struct compare_idx { 976 array_project_selects_util& u; compare_idxmbp::array_project_selects_util::compare_idx977 compare_idx(array_project_selects_util& u):u(u) {} operator ()mbp::array_project_selects_util::compare_idx978 bool operator()(idx_val const& x, idx_val const& y) { 979 SASSERT(x.rval.size() == y.rval.size()); 980 for (unsigned j = 0; j < x.rval.size(); ++j) { 981 rational const& xv = x.rval[j]; 982 rational const& yv = y.rval[j]; 983 if (xv < yv) return true; 984 if (xv > yv) return false; 985 } 986 return false; 987 } 988 }; 989 mk_lt(expr * x,expr * y)990 expr* mk_lt(expr* x, expr* y) { 991 if (m_bv_u.is_bv(x)) { 992 return m.mk_not(m_bv_u.mk_ule(y, x)); 993 } 994 else { 995 return m_ari_u.mk_lt(x, y); 996 } 997 } 998 mk_lex_lt(expr_ref_vector const & xs,expr_ref_vector const & ys)999 expr_ref mk_lex_lt(expr_ref_vector const& xs, expr_ref_vector const& ys) { 1000 SASSERT(xs.size() == ys.size() && !xs.empty()); 1001 expr_ref result(mk_lt(xs.back(), ys.back()), m); 1002 for (unsigned i = xs.size()-1; i-- > 0; ) { 1003 result = m.mk_or(mk_lt(xs[i], ys[i]), 1004 m.mk_and(m.mk_eq(xs[i], ys[i]), result)); 1005 } 1006 return result; 1007 } 1008 1009 /** 1010 * model based ackermannization for sel terms of some array 1011 * 1012 * update sub with val consts for sel terms 1013 */ ackermann(ptr_vector<app> const & sel_terms)1014 void ackermann (ptr_vector<app> const& sel_terms) { 1015 if (sel_terms.empty ()) return; 1016 1017 expr* v = sel_terms.get (0)->get_arg (0); // array variable 1018 sort* v_sort = m.get_sort (v); 1019 sort* val_sort = get_array_range (v_sort); 1020 unsigned arity = get_array_arity(v_sort); 1021 bool is_numeric = true; 1022 for (unsigned i = 0; i < arity && is_numeric; ++i) { 1023 sort* srt = get_array_domain(v_sort, i); 1024 if (!m_ari_u.is_real(srt) && !m_ari_u.is_int(srt) && !m_bv_u.is_bv_sort(srt)) { 1025 TRACE("qe", tout << "non-numeric index sort for Ackerman" << mk_pp(srt, m) << "\n";); 1026 is_numeric = false; 1027 } 1028 } 1029 1030 unsigned start = m_idxs.size (); // append at the end 1031 for (app * a : sel_terms) { 1032 expr_ref_vector idxs(m, arity, a->get_args() + 1); 1033 expr_ref_vector vals = (*m_mev)(idxs); 1034 bool is_new = true; 1035 for (unsigned j = start; j < m_idxs.size (); j++) { 1036 if (!is_eq(m_idxs[j].val, vals)) continue; 1037 // idx belongs to the jth equivalence class; 1038 // substitute sel term with ith sel const 1039 expr* c = m_sel_consts.get (j); 1040 m_sub.insert (a, c); 1041 // add equality (idx == repr) 1042 m_idx_lits.push_back (mk_eq (idxs, m_idxs[j].idx)); 1043 is_new = false; 1044 break; 1045 } 1046 if (is_new) { 1047 // new repr, val, and sel const 1048 m_idxs.push_back(idx_val(std::move(idxs), std::move(vals), to_num(vals))); 1049 app_ref c (m.mk_fresh_const ("sel", val_sort), m); 1050 m_sel_consts.push_back (c); 1051 // substitute sel term with new const 1052 m_sub.insert (a, c); 1053 // extend M to include c 1054 expr_ref val = (*m_mev)(a); 1055 M->register_decl (c->get_decl (), val); 1056 } 1057 } 1058 1059 if (start + 1 == m_idxs.size()) { 1060 // nothing to differentiate. 1061 } 1062 else if (is_numeric) { 1063 // sort reprs by their value and add a chain of strict inequalities 1064 compare_idx cmp(*this); 1065 std::sort(m_idxs.begin() + start, m_idxs.end(), cmp); 1066 for (unsigned i = start; i + 1 < m_idxs.size(); ++i) { 1067 m_idx_lits.push_back (mk_lex_lt(m_idxs[i].idx, m_idxs[i+1].idx)); 1068 } 1069 } 1070 else if (arity == 1) { 1071 // create distinct constraint. 1072 expr_ref_vector xs(m); 1073 for (unsigned i = start; i < m_idxs.size(); ++i) { 1074 xs.append(m_idxs[i].idx); 1075 } 1076 m_idx_lits.push_back(m.mk_distinct(xs.size(), xs.c_ptr())); 1077 } 1078 else { 1079 datatype::util dt(m); 1080 sort_ref_vector srts(m); 1081 ptr_vector<accessor_decl> acc; 1082 unsigned i = 0; 1083 for (expr * x : m_idxs[0].idx) { 1084 std::stringstream name; 1085 name << "get" << (i++); 1086 acc.push_back(mk_accessor_decl(m, symbol(name.str()), type_ref(m.get_sort(x)))); 1087 } 1088 constructor_decl* constrs[1] = { mk_constructor_decl(symbol("tuple"), symbol("is-tuple"), acc.size(), acc.c_ptr()) }; 1089 datatype::def* dts = mk_datatype_decl(dt, symbol("tuple"), 0, nullptr, 1, constrs); 1090 VERIFY(dt.plugin().mk_datatypes(1, &dts, 0, nullptr, srts)); 1091 del_datatype_decl(dts); 1092 sort* tuple = srts.get(0); 1093 ptr_vector<func_decl> const & decls = *dt.get_datatype_constructors(tuple); 1094 expr_ref_vector xs(m); 1095 for (unsigned i = start; i < m_idxs.size(); ++i) { 1096 xs.push_back(m.mk_app(decls[0], m_idxs[i].idx.size(), m_idxs[i].idx.c_ptr())); 1097 } 1098 m_idx_lits.push_back(m.mk_distinct(xs.size(), xs.c_ptr())); 1099 } 1100 } 1101 mk_result(expr_ref & fml)1102 void mk_result (expr_ref& fml) { 1103 // conjoin idx lits 1104 m_idx_lits.push_back(fml); 1105 fml = mk_and (m_idx_lits); 1106 1107 // substitute for sel terms 1108 m_sub (fml); 1109 1110 TRACE ("qe", tout << "after projection of selects:\n" << fml << "\n";); 1111 } 1112 1113 /** 1114 * project selects 1115 * populates idx lits and obtains substitution for sel terms 1116 */ project(expr * fml)1117 bool project (expr* fml) { 1118 // collect sel terms -- populate the map m_sel_terms 1119 collect_selects (fml); 1120 // model based ackermannization 1121 for (auto & kv : m_sel_terms) { 1122 TRACE ("qe",tout << "ackermann for var: " << mk_pp (kv.m_key, m) << "\n";); 1123 ackermann (*(kv.m_value)); 1124 } 1125 TRACE ("qe", tout << "idx lits:\n" << m_idx_lits; ); 1126 return true; 1127 } 1128 1129 public: 1130 array_project_selects_util(ast_manager & m)1131 array_project_selects_util (ast_manager& m): 1132 m (m), 1133 m_arr_u (m), 1134 m_ari_u (m), 1135 m_bv_u (m), 1136 m_sel_consts (m), 1137 m_idx_lits (m), 1138 m_sub (m) 1139 {} 1140 operator ()(model & mdl,app_ref_vector & arr_vars,expr_ref & fml,app_ref_vector & aux_vars)1141 void operator () (model& mdl, app_ref_vector& arr_vars, expr_ref& fml, app_ref_vector& aux_vars) { 1142 if (arr_vars.empty()) return; 1143 reset (); 1144 model_evaluator mev(mdl); 1145 mev.set_model_completion(true); 1146 M = &mdl; 1147 m_mev = &mev; 1148 1149 // mark vars to eliminate 1150 // alloc empty map from array var to sel terms over it 1151 for (app* v : arr_vars) { 1152 m_arr_test.mark(v, true); 1153 m_sel_terms.insert(v, alloc (ptr_vector<app>)); 1154 } 1155 1156 // assume all arr_vars are of array sort 1157 // and they only appear in select terms 1158 if (project (fml)) { 1159 mk_result (fml); 1160 aux_vars.append (m_sel_consts); 1161 arr_vars.reset (); 1162 } 1163 else { 1164 IF_VERBOSE(2, verbose_stream() << "can't project arrays:" << "\n";); 1165 TRACE ("qe", tout << "Failed to project arrays\n";); 1166 } 1167 1168 // dealloc 1169 for (auto & kv : m_sel_terms) dealloc(kv.m_value); 1170 m_sel_terms.reset (); 1171 } 1172 }; 1173 1174 1175 struct array_project_plugin::imp { 1176 1177 struct indices { 1178 expr_ref_vector m_values; 1179 expr* const* m_vars; 1180 indicesmbp::array_project_plugin::imp::indices1181 indices(ast_manager& m, model& model, unsigned n, expr* const* vars): 1182 m_values(m), m_vars(vars) { 1183 expr_ref val(m); 1184 for (unsigned i = 0; i < n; ++i) { 1185 m_values.push_back(model(vars[i])); 1186 } 1187 } 1188 }; 1189 1190 ast_manager& m; 1191 array_util a; 1192 scoped_ptr<contains_app> m_var; 1193 impmbp::array_project_plugin::imp1194 imp(ast_manager& m): m(m), a(m), m_stores(m) {} ~impmbp::array_project_plugin::imp1195 ~imp() {} 1196 solvembp::array_project_plugin::imp1197 bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) { 1198 return false; 1199 } 1200 remove_truembp::array_project_plugin::imp1201 void remove_true(expr_ref_vector& lits) { 1202 for (unsigned i = 0; i < lits.size(); ++i) { 1203 if (m.is_true(lits[i].get())) { 1204 project_plugin::erase(lits, i); 1205 } 1206 } 1207 } 1208 contains_xmbp::array_project_plugin::imp1209 bool contains_x(expr* e) { 1210 return (*m_var)(e); 1211 } 1212 mk_eqmbp::array_project_plugin::imp1213 void mk_eq(indices const& x, indices const& y, expr_ref_vector& lits) { 1214 SASSERT(x.m_values.size() == y.m_values.size()); 1215 unsigned n = x.m_values.size(); 1216 for (unsigned j = 0; j < n; ++j) { 1217 lits.push_back(m.mk_eq(x.m_vars[j], y.m_vars[j])); 1218 } 1219 } 1220 solve_eqmbp::array_project_plugin::imp1221 bool solve_eq(model& model, app_ref_vector& vars, expr_ref_vector& lits) { 1222 // find an equality to solve for. 1223 expr* s, *t; 1224 for (unsigned i = 0; i < lits.size(); ++i) { 1225 if (m.is_eq(lits[i].get(), s, t)) { 1226 vector<indices> idxs; 1227 expr_ref save(m), back(m); 1228 save = lits[i].get(); 1229 back = lits.back(); 1230 lits[i] = back; 1231 lits.pop_back(); 1232 unsigned sz = lits.size(); 1233 if (contains_x(s) && !contains_x(t) && is_app(s)) { 1234 if (solve(model, to_app(s), t, idxs, vars, lits)) { 1235 return true; 1236 } 1237 } 1238 else if (contains_x(t) && !contains_x(s) && is_app(t)) { 1239 if (solve(model, to_app(t), s, idxs, vars, lits)) { 1240 return true; 1241 } 1242 } 1243 // put back the equality literal. 1244 lits.resize(sz); 1245 lits.push_back(back); 1246 lits[i] = save; 1247 } 1248 // TBD: not distinct? 1249 } 1250 return false; 1251 } 1252 solvembp::array_project_plugin::imp1253 bool solve(model& model, app* s, expr* t, vector<indices>& idxs, app_ref_vector& vars, expr_ref_vector& lits) { 1254 SASSERT(contains_x(s)); 1255 SASSERT(!contains_x(t)); 1256 1257 if (s == m_var->x()) { 1258 expr_ref result(t, m); 1259 expr_ref_vector args(m); 1260 sort* range = get_array_range(m.get_sort(s)); 1261 for (unsigned i = 0; i < idxs.size(); ++i) { 1262 app_ref var(m), sel(m); 1263 expr_ref val(m); 1264 var = m.mk_fresh_const("value", range); 1265 vars.push_back(var); 1266 args.reset(); 1267 1268 args.push_back (s); 1269 args.append(idxs[i].m_values.size(), idxs[i].m_vars); 1270 sel = a.mk_select (args); 1271 val = model(sel); 1272 model.register_decl (var->get_decl (), val); 1273 1274 args[0] = result; 1275 args.push_back(var); 1276 result = a.mk_store(args.size(), args.c_ptr()); 1277 } 1278 expr_safe_replace sub(m); 1279 sub.insert(s, result); 1280 for (unsigned i = 0; i < lits.size(); ++i) { 1281 sub(lits[i].get(), result); 1282 lits[i] = result; 1283 } 1284 return true; 1285 } 1286 1287 if (a.is_store(s)) { 1288 unsigned n = s->get_num_args()-2; 1289 indices idx(m, model, n, s->get_args()+1); 1290 for (unsigned i = 1; i < n; ++i) { 1291 if (contains_x(s->get_arg(i))) { 1292 return false; 1293 } 1294 } 1295 unsigned i; 1296 expr_ref_vector args(m); 1297 switch (contains(idx, idxs, i)) { 1298 case l_true: 1299 mk_eq(idx, idxs[i], lits); 1300 return solve(model, to_app(s->get_arg(0)), t, idxs, vars, lits); 1301 case l_false: 1302 for (unsigned i = 0; i < idxs.size(); ++i) { 1303 expr_ref_vector eqs(m); 1304 mk_eq(idx, idxs[i], eqs); 1305 lits.push_back(m.mk_not(mk_and(eqs))); // TBD: extract single index of difference based on model. 1306 } 1307 args.push_back(t); 1308 args.append(n, s->get_args()+1); 1309 lits.push_back(m.mk_eq(a.mk_select(args), s->get_arg(n+1))); 1310 idxs.push_back(idx); 1311 return solve(model, to_app(s->get_arg(0)), t, idxs, vars, lits); 1312 case l_undef: 1313 return false; 1314 } 1315 } 1316 return false; 1317 } 1318 containsmbp::array_project_plugin::imp1319 lbool contains(indices const& idx, vector<indices> const& idxs, unsigned& j) { 1320 for (unsigned i = 0; i < idxs.size(); ++i) { 1321 switch (compare(idx, idxs[i])) { 1322 case l_true: 1323 j = i; 1324 return l_true; 1325 case l_false: 1326 break; 1327 case l_undef: 1328 return l_undef; 1329 } 1330 } 1331 return l_false; 1332 } 1333 comparembp::array_project_plugin::imp1334 lbool compare(indices const& idx1, indices const& idx2) { 1335 unsigned n = idx1.m_values.size(); 1336 for (unsigned i = 0; i < n; ++i) { 1337 switch (compare(idx1.m_values[i], idx2.m_values[i])) { 1338 case l_true: 1339 break; 1340 case l_false: 1341 return l_false; 1342 case l_undef: 1343 return l_undef; 1344 } 1345 } 1346 return l_true; 1347 } 1348 comparembp::array_project_plugin::imp1349 lbool compare(expr* val1, expr* val2) { 1350 if (m.are_equal (val1, val2)) return l_true; 1351 if (m.are_distinct (val1, val2)) return l_false; 1352 1353 if (is_uninterp(val1) || 1354 is_uninterp(val2)) { 1355 // TBD chase definition of nested array. 1356 return l_undef; 1357 } 1358 return l_undef; 1359 } 1360 saturatembp::array_project_plugin::imp1361 void saturate(model& model, func_decl_ref_vector const& shared, expr_ref_vector& lits) { 1362 term_graph tg(m); 1363 tg.set_vars(shared, false); 1364 tg.add_model_based_terms(model, lits); 1365 1366 // need tg to take term and map it to optional rep over the 1367 // shared vocabulary if it exists. 1368 1369 // . collect shared store expressions, index sorts 1370 // . collect shared index expressions 1371 // . assert extensionality (add shared index expressions) 1372 // . assert store axioms for collected expressions 1373 1374 collect_store_expressions(tg, lits); 1375 collect_index_expressions(tg, lits); 1376 1377 TRACE("qe", 1378 tout << "indices\n"; 1379 for (auto& kv : m_indices) { 1380 tout << sort_ref(kv.m_key, m) << " |-> " << *kv.m_value << "\n"; 1381 } 1382 tout << "stores " << m_stores << "\n"; 1383 tout << "arrays\n"; 1384 for (auto& kv : m_arrays) { 1385 tout << sort_ref(kv.m_key, m) << " |-> " << *kv.m_value << "\n"; 1386 }); 1387 1388 assert_extensionality(model, tg, lits); 1389 assert_store_select(model, tg, lits); 1390 1391 TRACE("qe", tout << lits << "\n";); 1392 1393 for (auto& kv : m_indices) { 1394 dealloc(kv.m_value); 1395 } 1396 for (auto& kv : m_arrays) { 1397 dealloc(kv.m_value); 1398 } 1399 m_stores.reset(); 1400 m_indices.reset(); 1401 m_arrays.reset(); 1402 1403 TRACE("qe", tout << "done: " << lits << "\n";); 1404 1405 } 1406 1407 app_ref_vector m_stores; 1408 obj_map<sort, app_ref_vector*> m_indices; 1409 obj_map<sort, app_ref_vector*> m_arrays; 1410 add_index_sortmbp::array_project_plugin::imp1411 void add_index_sort(expr* n) { 1412 sort* s = m.get_sort(n); 1413 if (!m_indices.contains(s)) { 1414 m_indices.insert(s, alloc(app_ref_vector, m)); 1415 } 1416 } 1417 add_arraymbp::array_project_plugin::imp1418 void add_array(app* n) { 1419 sort* s = m.get_sort(n); 1420 app_ref_vector* vs = nullptr; 1421 if (!m_arrays.find(s, vs)) { 1422 vs = alloc(app_ref_vector, m); 1423 m_arrays.insert(s, vs); 1424 } 1425 vs->push_back(n); 1426 } 1427 is_indexmbp::array_project_plugin::imp1428 app_ref_vector* is_index(expr* n) { 1429 app_ref_vector* result = nullptr; 1430 m_indices.find(m.get_sort(n), result); 1431 return result; 1432 } 1433 1434 struct for_each_store_proc { 1435 imp& m_imp; 1436 term_graph& tg; for_each_store_procmbp::array_project_plugin::imp::for_each_store_proc1437 for_each_store_proc(imp& i, term_graph& tg) : m_imp(i), tg(tg) {} 1438 operator ()mbp::array_project_plugin::imp::for_each_store_proc1439 void operator()(app* n) { 1440 if (m_imp.a.is_array(n) && tg.rep_of(n)) { 1441 m_imp.add_array(n); 1442 } 1443 1444 if (m_imp.a.is_store(n) && 1445 (tg.rep_of(n->get_arg(0)) || 1446 tg.rep_of(n->get_arg(n->get_num_args() - 1)))) { 1447 m_imp.m_stores.push_back(n); 1448 for (unsigned i = 1; i + 1 < n->get_num_args(); ++i) { 1449 m_imp.add_index_sort(n->get_arg(i)); 1450 } 1451 } 1452 } 1453 operator ()mbp::array_project_plugin::imp::for_each_store_proc1454 void operator()(expr* e) {} 1455 }; 1456 1457 struct for_each_index_proc { 1458 imp& m_imp; 1459 term_graph& tg; for_each_index_procmbp::array_project_plugin::imp::for_each_index_proc1460 for_each_index_proc(imp& i, term_graph& tg) : m_imp(i), tg(tg) {} 1461 operator ()mbp::array_project_plugin::imp::for_each_index_proc1462 void operator()(app* n) { 1463 auto* v = m_imp.is_index(n); 1464 if (v && tg.rep_of(n)) { 1465 v->push_back(n); 1466 } 1467 } 1468 operator ()mbp::array_project_plugin::imp::for_each_index_proc1469 void operator()(expr* e) {} 1470 1471 }; 1472 collect_store_expressionsmbp::array_project_plugin::imp1473 void collect_store_expressions(term_graph& tg, expr_ref_vector const& terms) { 1474 for_each_store_proc proc(*this, tg); 1475 for_each_expr<for_each_store_proc>(proc, terms); 1476 } 1477 collect_index_expressionsmbp::array_project_plugin::imp1478 void collect_index_expressions(term_graph& tg, expr_ref_vector const& terms) { 1479 for_each_index_proc proc(*this, tg); 1480 for_each_expr<for_each_index_proc>(proc, terms); 1481 } 1482 are_equalmbp::array_project_plugin::imp1483 bool are_equal(model& mdl, expr* s, expr* t) { 1484 return mdl.are_equal(s, t); 1485 } 1486 assert_extensionalitymbp::array_project_plugin::imp1487 void assert_extensionality(model & mdl, term_graph& tg, expr_ref_vector& lits) { 1488 for (auto& kv : m_arrays) { 1489 app_ref_vector const& vs = *kv.m_value; 1490 if (vs.size() <= 1) continue; 1491 func_decl_ref_vector ext(m); 1492 sort* s = kv.m_key; 1493 unsigned arity = get_array_arity(s); 1494 for (unsigned i = 0; i < arity; ++i) { 1495 ext.push_back(a.mk_array_ext(s, i)); 1496 } 1497 expr_ref_vector args(m); 1498 args.resize(arity + 1); 1499 for (unsigned i = 0; i < vs.size(); ++i) { 1500 expr* s = vs[i]; 1501 for (unsigned j = i + 1; j < vs.size(); ++j) { 1502 expr* t = vs[j]; 1503 if (are_equal(mdl, s, t)) { 1504 lits.push_back(m.mk_eq(s, t)); 1505 } 1506 else { 1507 for (unsigned k = 0; k < arity; ++k) { 1508 args[k+1] = m.mk_app(ext.get(k), s, t); 1509 } 1510 args[0] = t; 1511 expr* t1 = a.mk_select(args); 1512 args[0] = s; 1513 expr* s1 = a.mk_select(args); 1514 lits.push_back(m.mk_not(m.mk_eq(t1, s1))); 1515 } 1516 } 1517 } 1518 } 1519 } 1520 assert_store_selectmbp::array_project_plugin::imp1521 void assert_store_select(model & mdl, term_graph& tg, expr_ref_vector& lits) { 1522 for (auto& store : m_stores) { 1523 assert_store_select(store, mdl, tg, lits); 1524 } 1525 } 1526 assert_store_selectmbp::array_project_plugin::imp1527 void assert_store_select(app* store, model & mdl, term_graph& tg, expr_ref_vector& lits) { 1528 SASSERT(a.is_store(store)); 1529 ptr_vector<app> indices; 1530 for (unsigned i = 1; i + 1 < store->get_num_args(); ++i) { 1531 SASSERT(indices.empty()); 1532 assert_store_select(indices, store, mdl, tg, lits); 1533 } 1534 } 1535 assert_store_selectmbp::array_project_plugin::imp1536 void assert_store_select(ptr_vector<app>& indices, app* store, model & mdl, term_graph& tg, expr_ref_vector& lits) { 1537 unsigned sz = store->get_num_args(); 1538 if (indices.size() + 2 == sz) { 1539 ptr_vector<expr> args; 1540 args.push_back(store); 1541 for (expr* idx : indices) args.push_back(idx); 1542 for (unsigned i = 1; i + 1 < sz; ++i) { 1543 expr* idx1 = store->get_arg(i); 1544 expr* idx2 = indices[i - 1]; 1545 if (!are_equal(mdl, idx1, idx2)) { 1546 lits.push_back(m.mk_not(m.mk_eq(idx1, idx2))); 1547 lits.push_back(m.mk_eq(store->get_arg(sz-1), a.mk_select(args))); 1548 return; 1549 } 1550 } 1551 for (unsigned i = 1; i + 1 < sz; ++i) { 1552 expr* idx1 = store->get_arg(i); 1553 expr* idx2 = indices[i - 1]; 1554 lits.push_back(m.mk_eq(idx1, idx2)); 1555 } 1556 expr* a1 = a.mk_select(args); 1557 args[0] = store->get_arg(0); 1558 expr* a2 = a.mk_select(args); 1559 lits.push_back(m.mk_eq(a1, a2)); 1560 } 1561 else { 1562 sort* s = m.get_sort(store->get_arg(indices.size() + 1)); 1563 for (app* idx : *m_indices[s]) { 1564 indices.push_back(idx); 1565 assert_store_select(indices, store, mdl, tg, lits); 1566 indices.pop_back(); 1567 } 1568 } 1569 } 1570 1571 }; 1572 1573 array_project_plugin(ast_manager & m)1574 array_project_plugin::array_project_plugin(ast_manager& m):project_plugin(m) { 1575 m_imp = alloc(imp, m); 1576 } 1577 ~array_project_plugin()1578 array_project_plugin::~array_project_plugin() { 1579 dealloc(m_imp); 1580 } 1581 operator ()(model & model,app * var,app_ref_vector & vars,expr_ref_vector & lits)1582 bool array_project_plugin::operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) { 1583 ast_manager& m = vars.get_manager(); 1584 app_ref_vector vvars(m, 1, &var); 1585 expr_ref fml = mk_and(lits); 1586 (*this)(model, vvars, fml, vars, false); 1587 lits.reset(); 1588 flatten_and(fml, lits); 1589 return true; 1590 } 1591 solve(model & model,app_ref_vector & vars,expr_ref_vector & lits)1592 bool array_project_plugin::solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) { 1593 return m_imp->solve(model, vars, lits); 1594 } 1595 get_family_id()1596 family_id array_project_plugin::get_family_id() { 1597 return m_imp->a.get_family_id(); 1598 } 1599 operator ()(model & mdl,app_ref_vector & arr_vars,expr_ref & fml,app_ref_vector & aux_vars,bool reduce_all_selects)1600 void array_project_plugin::operator()(model& mdl, app_ref_vector& arr_vars, expr_ref& fml, app_ref_vector& aux_vars, bool reduce_all_selects) { 1601 // 1. project array equalities 1602 ast_manager& m = fml.get_manager(); 1603 array_project_eqs_util pe (m); 1604 pe (mdl, arr_vars, fml, aux_vars); 1605 TRACE ("qe", 1606 tout << "Projected array eqs: " << fml << "\n"; 1607 tout << "Remaining array vars: " << arr_vars << "\n"; 1608 tout << "Aux vars: " << aux_vars << "\n"; 1609 ); 1610 1611 // 2. reduce selects 1612 array_select_reducer rs (m); 1613 rs (mdl, arr_vars, fml, reduce_all_selects); 1614 1615 TRACE ("qe", tout << "Reduced selects:\n" << fml << "\n"; ); 1616 1617 // 3. project selects using model based ackermannization 1618 array_project_selects_util ps (m); 1619 ps (mdl, arr_vars, fml, aux_vars); 1620 1621 TRACE ("qe", 1622 tout << "Projected array selects: " << fml << "\n"; 1623 tout << "All aux vars: " << aux_vars << "\n"; 1624 ); 1625 } 1626 project(model & model,app_ref_vector & vars,expr_ref_vector & lits)1627 vector<def> array_project_plugin::project(model& model, app_ref_vector& vars, expr_ref_vector& lits) { 1628 return vector<def>(); 1629 } 1630 saturate(model & model,func_decl_ref_vector const & shared,expr_ref_vector & lits)1631 void array_project_plugin::saturate(model& model, func_decl_ref_vector const& shared, expr_ref_vector& lits) { 1632 m_imp->saturate(model, shared, lits); 1633 } 1634 1635 1636 }; 1637