1 /*++ 2 Copyright (c) 2006 Microsoft Corporation 3 4 Module Name: 5 6 theory_array.cpp 7 8 Abstract: 9 10 <abstract> 11 12 Author: 13 14 Leonardo de Moura (leonardo) 2008-06-01. 15 16 Revision History: 17 18 --*/ 19 #include "smt/smt_context.h" 20 #include "smt/theory_array.h" 21 #include "ast/ast_ll_pp.h" 22 #include "ast/ast_pp.h" 23 #include "util/stats.h" 24 25 namespace smt { 26 theory_array(context & ctx)27 theory_array::theory_array(context& ctx): 28 theory_array_base(ctx), 29 m_params(ctx.get_fparams()), 30 m_find(*this), 31 m_trail_stack(), 32 m_final_check_idx(0) { 33 if (!ctx.relevancy()) 34 m_params.m_array_laziness = 0; 35 } 36 ~theory_array()37 theory_array::~theory_array() { 38 std::for_each(m_var_data.begin(), m_var_data.end(), delete_proc<var_data>()); 39 m_var_data.reset(); 40 } 41 merge_eh(theory_var v1,theory_var v2,theory_var,theory_var)42 void theory_array::merge_eh(theory_var v1, theory_var v2, theory_var, theory_var) { 43 // v1 is the new root 44 TRACE("array", 45 tout << "merging v" << v1 << " v" << v2 << "\n"; display_var(tout, v1); 46 tout << mk_pp(get_enode(v1)->get_expr(), m) << " <- " << mk_pp(get_enode(v2)->get_expr(), m) << "\n";); 47 SASSERT(v1 == find(v1)); 48 var_data * d1 = m_var_data[v1]; 49 var_data * d2 = m_var_data[v2]; 50 if (!d1->m_prop_upward && d2->m_prop_upward) 51 set_prop_upward(v1); 52 for (unsigned i = 0; i < d2->m_stores.size(); ++i) 53 add_store(v1, d2->m_stores[i]); 54 for (unsigned i = 0; i < d2->m_parent_stores.size(); ++i) 55 add_parent_store(v1, d2->m_parent_stores[i]); 56 for (unsigned i = 0; i < d2->m_parent_selects.size(); ++i) 57 add_parent_select(v1, d2->m_parent_selects[i]); 58 TRACE("array", tout << "after merge\n"; display_var(tout, v1);); 59 } 60 unmerge_eh(theory_var v1,theory_var v2)61 void theory_array::unmerge_eh(theory_var v1, theory_var v2) { 62 // do nothing 63 } 64 mk_var(enode * n)65 theory_var theory_array::mk_var(enode * n) { 66 theory_var r = theory_array_base::mk_var(n); 67 VERIFY(r == static_cast<theory_var>(m_find.mk_var())); 68 SASSERT(r == static_cast<int>(m_var_data.size())); 69 m_var_data.push_back(alloc(var_data)); 70 var_data * d = m_var_data[r]; 71 TRACE("array", tout << mk_bounded_pp(n->get_expr(), m) << "\nis_array: " << is_array_sort(n) << ", is_select: " << is_select(n) << 72 ", is_store: " << is_store(n) << "\n";); 73 d->m_is_array = is_array_sort(n); 74 if (d->m_is_array) 75 register_sort(n->get_expr()->get_sort()); 76 d->m_is_select = is_select(n); 77 if (is_store(n)) 78 d->m_stores.push_back(n); 79 ctx.attach_th_var(n, this, r); 80 if (m_params.m_array_laziness <= 1 && is_store(n)) 81 instantiate_axiom1(n); 82 return r; 83 } 84 add_parent_select(theory_var v,enode * s)85 void theory_array::add_parent_select(theory_var v, enode * s) { 86 if (m_params.m_array_cg && !s->is_cgr()) 87 return; 88 SASSERT(is_select(s)); 89 v = find(v); 90 var_data * d = m_var_data[v]; 91 d->m_parent_selects.push_back(s); 92 TRACE("array", tout << v << " " << mk_pp(s->get_expr(), m) << " " << mk_pp(get_enode(v)->get_expr(), m) << "\n";); 93 m_trail_stack.push(push_back_trail<enode *, false>(d->m_parent_selects)); 94 for (enode* n : d->m_stores) { 95 instantiate_axiom2a(s, n); 96 } 97 if (!m_params.m_array_delay_exp_axiom && d->m_prop_upward) { 98 for (enode* store : d->m_parent_stores) { 99 SASSERT(is_store(store)); 100 if (!m_params.m_array_cg || store->is_cgr()) { 101 instantiate_axiom2b(s, store); 102 } 103 } 104 } 105 } 106 add_parent_store(theory_var v,enode * s)107 void theory_array::add_parent_store(theory_var v, enode * s) { 108 if (m_params.m_array_cg && !s->is_cgr()) 109 return; 110 SASSERT(is_store(s)); 111 v = find(v); 112 var_data * d = m_var_data[v]; 113 d->m_parent_stores.push_back(s); 114 m_trail_stack.push(push_back_trail<enode *, false>(d->m_parent_stores)); 115 if (d->m_prop_upward && !m_params.m_array_delay_exp_axiom) { 116 for (enode* n : d->m_parent_selects) { 117 if (!m_params.m_array_cg || n->is_cgr()) { 118 instantiate_axiom2b(n, s); 119 } 120 } 121 } 122 } 123 instantiate_axiom2b_for(theory_var v)124 bool theory_array::instantiate_axiom2b_for(theory_var v) { 125 bool result = false; 126 var_data * d = m_var_data[v]; 127 for (enode* n1 : d->m_parent_stores) 128 for (enode * n2 : d->m_parent_selects) 129 if (instantiate_axiom2b(n2, n1)) 130 result = true; 131 return result; 132 } 133 134 /** 135 \brief Mark v for upward propagation. That is, enables the propagation of select(v, i) to store(v,j,k). 136 */ set_prop_upward(theory_var v)137 void theory_array::set_prop_upward(theory_var v) { 138 v = find(v); 139 var_data * d = m_var_data[v]; 140 if (!d->m_prop_upward) { 141 if (m_params.m_array_weak) { 142 add_weak_var(v); 143 return; 144 } 145 TRACE("array", tout << "#" << v << "\n";); 146 m_trail_stack.push(reset_flag_trail(d->m_prop_upward)); 147 d->m_prop_upward = true; 148 if (!m_params.m_array_delay_exp_axiom) 149 instantiate_axiom2b_for(v); 150 for (enode * n : d->m_stores) 151 set_prop_upward(n); 152 } 153 } 154 set_prop_upward(enode * store)155 void theory_array::set_prop_upward(enode * store) { 156 if (is_store(store)) { 157 theory_var st_v = store->get_arg(0)->get_th_var(get_id()); 158 set_prop_upward(st_v); 159 } 160 } 161 set_prop_upward(theory_var v,var_data * d)162 void theory_array::set_prop_upward(theory_var v, var_data* d) { 163 unsigned sz = d->m_stores.size(); 164 for (unsigned i = 0; i < sz; ++i) { 165 set_prop_upward(d->m_stores[i]); 166 } 167 } 168 169 170 /** 171 \brief Return the size of the equivalence class for array terms 172 that can be expressed as \lambda i : Index . [.. (select a i) ..] 173 */ get_lambda_equiv_size(theory_var v,var_data * d)174 unsigned theory_array::get_lambda_equiv_size(theory_var v, var_data* d) { 175 return d->m_stores.size(); 176 } 177 add_store(theory_var v,enode * s)178 void theory_array::add_store(theory_var v, enode * s) { 179 if (m_params.m_array_cg && !s->is_cgr()) 180 return; 181 SASSERT(is_store(s)); 182 v = find(v); 183 var_data * d = m_var_data[v]; 184 unsigned lambda_equiv_class_size = get_lambda_equiv_size(v, d); 185 if (m_params.m_array_always_prop_upward || lambda_equiv_class_size >= 1) { 186 set_prop_upward(v, d); 187 } 188 d->m_stores.push_back(s); 189 m_trail_stack.push(push_back_trail<enode *, false>(d->m_stores)); 190 for (enode * n : d->m_parent_selects) { 191 SASSERT(is_select(n)); 192 instantiate_axiom2a(n, s); 193 } 194 if (m_params.m_array_always_prop_upward || lambda_equiv_class_size >= 1) 195 set_prop_upward(s); 196 } 197 instantiate_axiom1(enode * store)198 void theory_array::instantiate_axiom1(enode * store) { 199 TRACE("array", tout << "axiom 1:\n" << mk_bounded_pp(store->get_expr(), m) << "\n";); 200 SASSERT(is_store(store)); 201 m_stats.m_num_axiom1++; 202 assert_store_axiom1(store); 203 } 204 instantiate_axiom2a(enode * select,enode * store)205 void theory_array::instantiate_axiom2a(enode * select, enode * store) { 206 TRACE("array", tout << "axiom 2a: #" << select->get_owner_id() << " #" << store->get_owner_id() << "\n";); 207 SASSERT(is_select(select)); 208 SASSERT(is_store(store)); 209 if (assert_store_axiom2(store, select)) 210 m_stats.m_num_axiom2a++; 211 } 212 instantiate_axiom2b(enode * select,enode * store)213 bool theory_array::instantiate_axiom2b(enode * select, enode * store) { 214 TRACE("array_axiom2b", tout << "axiom 2b: #" << select->get_owner_id() << " #" << store->get_owner_id() << "\n";); 215 SASSERT(is_select(select)); 216 SASSERT(is_store(store)); 217 if (assert_store_axiom2(store, select)) { 218 m_stats.m_num_axiom2b++; 219 return true; 220 } 221 return false; 222 } 223 instantiate_extensionality(enode * a1,enode * a2)224 void theory_array::instantiate_extensionality(enode * a1, enode * a2) { 225 TRACE("array", tout << "extensionality: #" << a1->get_owner_id() << " #" << a2->get_owner_id() << "\n";); 226 SASSERT(is_array_sort(a1)); 227 SASSERT(is_array_sort(a2)); 228 if (m_params.m_array_extensional && assert_extensionality(a1, a2)) 229 m_stats.m_num_extensionality++; 230 } 231 232 internalize_atom(app * atom,bool)233 bool theory_array::internalize_atom(app * atom, bool) { 234 return internalize_term(atom); 235 } 236 237 // 238 // Internalize the term. If it has already been internalized, return false. 239 // internalize_term_core(app * n)240 bool theory_array::internalize_term_core(app * n) { 241 TRACE("array_bug", tout << mk_bounded_pp(n, m) << "\n";); 242 unsigned num_args = n->get_num_args(); 243 for (unsigned i = 0; i < num_args; i++) 244 ctx.internalize(n->get_arg(i), false); 245 if (ctx.e_internalized(n)) { 246 return false; 247 } 248 enode * e = ctx.mk_enode(n, false, false, true); 249 if (!is_attached_to_var(e)) 250 mk_var(e); 251 252 if (m.is_bool(n)) { 253 bool_var bv = ctx.mk_bool_var(n); 254 ctx.set_var_theory(bv, get_id()); 255 ctx.set_enode_flag(bv, true); 256 } 257 return true; 258 } 259 internalize_term(app * n)260 bool theory_array::internalize_term(app * n) { 261 if (!is_store(n) && !is_select(n)) { 262 if (!is_array_ext(n)) 263 found_unsupported_op(n); 264 return false; 265 } 266 TRACE("array_bug", tout << mk_bounded_pp(n, m) << "\n";); 267 if (!internalize_term_core(n)) { 268 return true; 269 } 270 enode * arg0 = ctx.get_enode(n->get_arg(0)); 271 if (!is_attached_to_var(arg0)) 272 mk_var(arg0); 273 274 275 if (m_params.m_array_laziness == 0) { 276 theory_var v_arg = arg0->get_th_var(get_id()); 277 278 SASSERT(v_arg != null_theory_var); 279 if (is_select(n)) { 280 add_parent_select(v_arg, ctx.get_enode(n)); 281 } 282 else if (is_store(n)) { 283 add_parent_store(v_arg, ctx.get_enode(n)); 284 } 285 } 286 287 return true; 288 } 289 apply_sort_cnstr(enode * n,sort * s)290 void theory_array::apply_sort_cnstr(enode * n, sort * s) { 291 SASSERT(is_array_sort(s)); 292 if (!is_attached_to_var(n)) 293 mk_var(n); 294 } 295 new_eq_eh(theory_var v1,theory_var v2)296 void theory_array::new_eq_eh(theory_var v1, theory_var v2) { 297 m_find.merge(v1, v2); 298 enode* n1 = get_enode(v1), *n2 = get_enode(v2); 299 if (n1->get_expr()->get_decl()->is_lambda() || 300 n2->get_expr()->get_decl()->is_lambda()) { 301 assert_congruent(n1, n2); 302 } 303 } 304 new_diseq_eh(theory_var v1,theory_var v2)305 void theory_array::new_diseq_eh(theory_var v1, theory_var v2) { 306 v1 = find(v1); 307 v2 = find(v2); 308 var_data * d1 = m_var_data[v1]; 309 TRACE("ext", tout << "extensionality: " << d1->m_is_array << "\n" 310 << mk_bounded_pp(get_enode(v1)->get_expr(), m, 5) << "\n" 311 << mk_bounded_pp(get_enode(v2)->get_expr(), m, 5) << "\n";); 312 313 if (d1->m_is_array) { 314 SASSERT(m_var_data[v2]->m_is_array); 315 instantiate_extensionality(get_enode(v1), get_enode(v2)); 316 } 317 } 318 relevant_eh(app * n)319 void theory_array::relevant_eh(app * n) { 320 if (m_params.m_array_laziness == 0) 321 return; 322 if (m.is_ite(n)) { 323 TRACE("array", tout << "relevant ite " << mk_pp(n, m) << "\n";); 324 } 325 if (!is_store(n) && !is_select(n)) 326 return; 327 if (!ctx.e_internalized(n)) ctx.internalize(n, false); 328 enode * arg = ctx.get_enode(n->get_arg(0)); 329 theory_var v_arg = arg->get_th_var(get_id()); 330 SASSERT(v_arg != null_theory_var); 331 332 enode* e = ctx.get_enode(n); 333 if (is_select(n)) { 334 add_parent_select(v_arg, e); 335 } 336 else { 337 SASSERT(is_store(n)); 338 if (m_params.m_array_laziness > 1) 339 instantiate_axiom1(e); 340 add_parent_store(v_arg, e); 341 } 342 } 343 push_scope_eh()344 void theory_array::push_scope_eh() { 345 theory_array_base::push_scope_eh(); 346 m_trail_stack.push_scope(); 347 } 348 pop_scope_eh(unsigned num_scopes)349 void theory_array::pop_scope_eh(unsigned num_scopes) { 350 m_trail_stack.pop_scope(num_scopes); 351 unsigned num_old_vars = get_old_num_vars(num_scopes); 352 std::for_each(m_var_data.begin() + num_old_vars, m_var_data.end(), delete_proc<var_data>()); 353 m_var_data.shrink(num_old_vars); 354 theory_array_base::pop_scope_eh(num_scopes); 355 SASSERT(m_find.get_num_vars() == m_var_data.size()); 356 SASSERT(m_find.get_num_vars() == get_num_vars()); 357 } 358 final_check_eh()359 final_check_status theory_array::final_check_eh() { 360 m_final_check_idx++; 361 final_check_status r = FC_DONE; 362 if (m_params.m_array_lazy_ieq) { 363 // Delay the creation of interface equalities... The 364 // motivation is too give other theories and quantifier 365 // instantiation to do something useful during final 366 // check. 367 if (m_final_check_idx % m_params.m_array_lazy_ieq_delay != 0) { 368 assert_delayed_axioms(); 369 r = FC_CONTINUE; 370 } 371 else { 372 if (mk_interface_eqs_at_final_check() == FC_CONTINUE) 373 r = FC_CONTINUE; 374 else 375 r = assert_delayed_axioms(); 376 } 377 } 378 else { 379 if (m_final_check_idx % 2 == 1) { 380 if (assert_delayed_axioms() == FC_CONTINUE) 381 r = FC_CONTINUE; 382 else 383 r = mk_interface_eqs_at_final_check(); 384 } 385 else { 386 if (mk_interface_eqs_at_final_check() == FC_CONTINUE) 387 r = FC_CONTINUE; 388 else 389 r = assert_delayed_axioms(); 390 } 391 } 392 bool should_giveup = m_found_unsupported_op || has_propagate_up_trail(); 393 if (r == FC_DONE && should_giveup && !ctx.get_fparams().m_array_fake_support) 394 r = FC_GIVEUP; 395 CTRACE("array", r != FC_DONE || m_found_unsupported_op, tout << r << "\n";); 396 return r; 397 } 398 assert_delayed_axioms()399 final_check_status theory_array::assert_delayed_axioms() { 400 if (!m_params.m_array_delay_exp_axiom) 401 return FC_DONE; 402 final_check_status r = FC_DONE; 403 unsigned num_vars = get_num_vars(); 404 for (unsigned v = 0; v < num_vars; v++) { 405 var_data * d = m_var_data[v]; 406 if (d->m_prop_upward && instantiate_axiom2b_for(v)) 407 r = FC_CONTINUE; 408 } 409 return r; 410 } 411 mk_interface_eqs_at_final_check()412 final_check_status theory_array::mk_interface_eqs_at_final_check() { 413 unsigned n = mk_interface_eqs(); 414 m_stats.m_num_eq_splits += n; 415 if (n > 0) 416 return FC_CONTINUE; 417 return FC_DONE; 418 } 419 reset_eh()420 void theory_array::reset_eh() { 421 m_trail_stack.reset(); 422 std::for_each(m_var_data.begin(), m_var_data.end(), delete_proc<var_data>()); 423 m_var_data.reset(); 424 theory_array_base::reset_eh(); 425 } 426 display(std::ostream & out) const427 void theory_array::display(std::ostream & out) const { 428 unsigned num_vars = get_num_vars(); 429 if (num_vars == 0) return; 430 out << "Theory array:\n"; 431 for (unsigned v = 0; v < num_vars; v++) { 432 display_var(out, v); 433 } 434 } 435 436 // TODO: move to another file display_ids(std::ostream & out,unsigned n,enode * const * v)437 void theory_array::display_ids(std::ostream & out, unsigned n, enode * const * v) { 438 for (unsigned i = 0; i < n; i++) { 439 if (i > 0) out << " "; 440 out << "#" << v[i]->get_owner_id(); 441 } 442 } 443 display_var(std::ostream & out,theory_var v) const444 void theory_array::display_var(std::ostream & out, theory_var v) const { 445 var_data const * d = m_var_data[v]; 446 out << "v"; 447 out.width(4); 448 out << std::left << v; 449 out << " #"; 450 out.width(4); 451 out << get_enode(v)->get_owner_id() << " -> #"; 452 out.width(4); 453 out << get_enode(find(v))->get_owner_id(); 454 out << std::right; 455 out << " is_array: " << d->m_is_array << " is_select: " << d->m_is_select << " upward: " << d->m_prop_upward; 456 out << " stores: {"; 457 display_ids(out, d->m_stores.size(), d->m_stores.data()); 458 out << "} p_stores: {"; 459 display_ids(out, d->m_parent_stores.size(), d->m_parent_stores.data()); 460 out << "} p_selects: {"; 461 display_ids(out, d->m_parent_selects.size(), d->m_parent_selects.data()); 462 out << "}"; 463 out << "\n"; 464 } 465 collect_statistics(::statistics & st) const466 void theory_array::collect_statistics(::statistics & st) const { 467 st.update("array ax1", m_stats.m_num_axiom1); 468 st.update("array ax2", m_stats.m_num_axiom2a); 469 st.update("array exp ax2", m_stats.m_num_axiom2b); 470 st.update("array ext ax", m_stats.m_num_extensionality); 471 st.update("array splits", m_stats.m_num_eq_splits); 472 } 473 474 }; 475