1 /*++ 2 Copyright (c) 2006 Microsoft Corporation 3 4 Module Name: 5 6 theory_array_base.cpp 7 8 Abstract: 9 10 <abstract> 11 12 Author: 13 14 Leonardo de Moura (leonardo) 2008-06-02. 15 16 Revision History: 17 18 --*/ 19 #include "smt/smt_context.h" 20 #include "smt/theory_array_base.h" 21 #include "ast/ast_ll_pp.h" 22 #include "ast/ast_pp.h" 23 #include "smt/smt_model_generator.h" 24 #include "model/func_interp.h" 25 #include "ast/ast_smt2_pp.h" 26 27 namespace smt { 28 theory_array_base(context & ctx)29 theory_array_base::theory_array_base(context& ctx): 30 theory(ctx, ctx.get_manager().mk_family_id("array")), 31 m_found_unsupported_op(false), 32 m_array_weak_head(0) 33 { 34 } 35 add_weak_var(theory_var v)36 void theory_array_base::add_weak_var(theory_var v) { 37 ctx.push_trail(push_back_vector<context, svector<theory_var>>(m_array_weak_trail)); 38 m_array_weak_trail.push_back(v); 39 } 40 found_unsupported_op(expr * n)41 void theory_array_base::found_unsupported_op(expr * n) { 42 if (!ctx.get_fparams().m_array_fake_support && !m_found_unsupported_op) { 43 TRACE("array", tout << mk_ll_pp(n, m) << "\n";); 44 ctx.push_trail(value_trail<context, bool>(m_found_unsupported_op)); 45 m_found_unsupported_op = true; 46 } 47 } 48 mk_select(unsigned num_args,expr * const * args)49 app * theory_array_base::mk_select(unsigned num_args, expr * const * args) { 50 app * r = m.mk_app(get_family_id(), OP_SELECT, 0, nullptr, num_args, args); 51 TRACE("mk_var_bug", tout << "mk_select: " << r->get_id() << " num_args: " << num_args; 52 for (unsigned i = 0; i < num_args; i++) tout << " " << args[i]->get_id(); 53 tout << "\n";); 54 return r; 55 } 56 mk_store(unsigned num_args,expr * const * args)57 app * theory_array_base::mk_store(unsigned num_args, expr * const * args) { 58 return m.mk_app(get_family_id(), OP_STORE, 0, nullptr, num_args, args); 59 } 60 mk_default(expr * a)61 app * theory_array_base::mk_default(expr * a) { 62 sort * s = m.get_sort(a); 63 unsigned num_params = get_dimension(s); 64 parameter const* params = s->get_info()->get_parameters(); 65 return m.mk_app(get_family_id(), OP_ARRAY_DEFAULT, num_params, params, 1, & a); 66 } 67 get_dimension(sort * s) const68 unsigned theory_array_base::get_dimension(sort * s) const { 69 SASSERT(s->is_sort_of(get_family_id(), ARRAY_SORT)); 70 SASSERT(s->get_info()->get_num_parameters() >= 2); 71 return s->get_info()->get_num_parameters()-1; 72 } 73 assert_axiom(unsigned num_lits,literal * lits)74 void theory_array_base::assert_axiom(unsigned num_lits, literal * lits) { 75 TRACE("array_axiom", 76 tout << "literals:\n"; 77 for (unsigned i = 0; i < num_lits; ++i) { 78 expr * e = ctx.bool_var2expr(lits[i].var()); 79 if (lits[i].sign()) 80 tout << "not "; 81 tout << mk_pp(e, m) << " "; 82 tout << "\n"; 83 }); 84 ctx.mk_th_axiom(get_id(), num_lits, lits); 85 } 86 assert_axiom(literal l1,literal l2)87 void theory_array_base::assert_axiom(literal l1, literal l2) { 88 literal ls[2] = { l1, l2 }; 89 assert_axiom(2, ls); 90 } 91 assert_axiom(literal l)92 void theory_array_base::assert_axiom(literal l) { 93 assert_axiom(1, &l); 94 } 95 assert_store_axiom1_core(enode * e)96 void theory_array_base::assert_store_axiom1_core(enode * e) { 97 app * n = e->get_owner(); 98 SASSERT(is_store(n)); 99 ptr_buffer<expr> sel_args; 100 unsigned num_args = n->get_num_args(); 101 SASSERT(num_args >= 3); 102 sel_args.push_back(n); 103 for (unsigned i = 1; i < num_args - 1; ++i) { 104 sel_args.push_back(to_app(n->get_arg(i))); 105 } 106 expr_ref sel(m); 107 sel = mk_select(sel_args.size(), sel_args.c_ptr()); 108 expr * val = n->get_arg(num_args - 1); 109 TRACE("array", tout << mk_bounded_pp(sel, m) << " = " << mk_bounded_pp(val, m) << "\n";); 110 if (m.proofs_enabled()) { 111 literal l(mk_eq(sel, val, true)); 112 ctx.mark_as_relevant(l); 113 if (m.has_trace_stream()) log_axiom_instantiation(ctx.bool_var2expr(l.var())); 114 assert_axiom(l); 115 if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; 116 } 117 else { 118 TRACE("mk_var_bug", tout << "mk_sel: " << sel->get_id() << "\n";); 119 ctx.internalize(sel, false); 120 ctx.assign_eq(ctx.get_enode(sel), ctx.get_enode(val), eq_justification::mk_axiom()); 121 ctx.mark_as_relevant(sel.get()); 122 } 123 } 124 125 /** 126 \brief Assert axiom 2: 127 128 FORALL a, i_i, ..., i_n, j_1, ..., j_n 129 i_1 /= j_1 => select(store(a, i_1, ..., i_n, v), j_1, ..., j_n) = select(a, j_1, ..., j_n) 130 and 131 ... 132 and 133 i_n /= j_n => select(store(a, i_1, ..., i_n, v), j_1, ..., j_n) = select(a, j_1, ..., j_n) 134 */ assert_store_axiom2_core(enode * store,enode * select)135 void theory_array_base::assert_store_axiom2_core(enode * store, enode * select) { 136 TRACE("array", tout << "generating axiom2: #" << store->get_owner_id() << " #" << select->get_owner_id() << "\n"; 137 tout << mk_bounded_pp(store->get_owner(), m) << "\n" << mk_bounded_pp(select->get_owner(), m) << "\n";); 138 SASSERT(is_store(store)); 139 SASSERT(is_select(select)); 140 SASSERT(store->get_num_args() == 1 + select->get_num_args()); 141 142 ptr_buffer<expr> sel1_args, sel2_args; 143 enode * a = store->get_arg(0); 144 enode * const * is = select->get_args() + 1; 145 enode * const * js = store->get_args() + 1; 146 unsigned num_args = select->get_num_args() - 1; 147 sel1_args.push_back(store->get_owner()); 148 sel2_args.push_back(a->get_owner()); 149 150 for (unsigned i = 0; i < num_args; i++) { 151 sel1_args.push_back(is[i]->get_owner()); 152 sel2_args.push_back(is[i]->get_owner()); 153 } 154 155 expr_ref sel1(m), sel2(m); 156 bool init = false; 157 literal conseq = null_literal; 158 expr * conseq_expr = nullptr; 159 160 for (unsigned i = 0; i < num_args; i++) { 161 enode * idx1 = js[i]; 162 enode * idx2 = is[i]; 163 164 if (idx1->get_root() == idx2->get_root()) { 165 TRACE("array_bug", tout << "indexes are equal... skipping...\n";); 166 continue; 167 } 168 169 if (!init) { 170 sel1 = mk_select(sel1_args.size(), sel1_args.c_ptr()); 171 sel2 = mk_select(sel2_args.size(), sel2_args.c_ptr()); 172 if (sel1 == sel2) { 173 TRACE("array_bug", tout << "sel1 and sel2 are equal:\n";); 174 break; 175 } 176 init = true; 177 TRACE("array", tout << mk_bounded_pp(sel1, m) << " " << mk_bounded_pp(sel2, m) << "\n";); 178 conseq = mk_eq(sel1, sel2, true); 179 conseq_expr = ctx.bool_var2expr(conseq.var()); 180 } 181 182 literal ante = mk_eq(idx1->get_owner(), idx2->get_owner(), true); 183 ctx.mark_as_relevant(ante); 184 // ctx.force_phase(ante); 185 ctx.add_rel_watch(~ante, conseq_expr); 186 // ctx.mark_as_relevant(conseq_expr); 187 TRACE("array", tout << "asserting axiom2: " << ante << "\n";); 188 TRACE("array_map_bug", tout << "axiom2:\n"; 189 tout << mk_ismt2_pp(idx1->get_owner(), m) << "\n=\n" << mk_ismt2_pp(idx2->get_owner(), m); 190 tout << "\nimplies\n" << mk_ismt2_pp(conseq_expr, m) << "\n";); 191 if (m.has_trace_stream()) { 192 app_ref body(m); 193 body = m.mk_or(ctx.bool_var2expr(ante.var()), conseq_expr); 194 log_axiom_instantiation(body); 195 } 196 assert_axiom(ante, conseq); 197 if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; 198 } 199 } 200 assert_store_axiom2(enode * store,enode * select)201 bool theory_array_base::assert_store_axiom2(enode * store, enode * select) { 202 unsigned num_args = select->get_num_args(); 203 unsigned i = 1; 204 for (; i < num_args; i++) 205 if (store->get_arg(i)->get_root() != select->get_arg(i)->get_root()) 206 break; 207 if (i == num_args) 208 return false; 209 if (ctx.add_fingerprint(store, store->get_owner_id(), select->get_num_args() - 1, select->get_args() + 1)) { 210 TRACE("array", tout << "adding axiom2 to todo queue\n";); 211 m_axiom2_todo.push_back(std::make_pair(store, select)); 212 return true; 213 } 214 TRACE("array", tout << "axiom already instantiated: #" << store->get_owner_id() << " #" << select->get_owner_id() << "\n";); 215 return false; 216 } 217 218 219 220 221 register_sort(sort * s_array)222 func_decl_ref_vector * theory_array_base::register_sort(sort * s_array) { 223 unsigned dimension = get_dimension(s_array); 224 func_decl_ref_vector * ext_skolems = nullptr; 225 if (!m_sort2skolem.find(s_array, ext_skolems)) { 226 array_util util(m); 227 ext_skolems = alloc(func_decl_ref_vector, m); 228 for (unsigned i = 0; i < dimension; ++i) { 229 func_decl * ext_sk_decl = util.mk_array_ext(s_array, i); 230 ext_skolems->push_back(ext_sk_decl); 231 } 232 m_sort2skolem.insert(s_array, ext_skolems); 233 m_sorts_trail.push_back(s_array); 234 } 235 return ext_skolems; 236 } 237 operator ()(enode * n1,enode * n2) const238 bool theory_array_base::value_eq_proc::operator()(enode * n1, enode * n2) const { 239 SASSERT(n1->get_num_args() == n2->get_num_args()); 240 unsigned n = n1->get_num_args(); 241 // skipping first argument of the select. 242 for(unsigned i = 1; i < n; i++) { 243 if (n1->get_arg(i)->get_root() != n2->get_arg(i)->get_root()) { 244 return false; 245 } 246 } 247 return true; 248 } 249 250 /** 251 \brief Return true if there is a select(v1', i1) and a select(v2', i2) such that: 252 v1' = v1, v2' = v2, i1 = i2, select(v1', i1) /= select(v2', i2) in the logical context. 253 */ already_diseq(enode * v1,enode * v2)254 bool theory_array_base::already_diseq(enode * v1, enode * v2) { 255 enode * r1 = v1->get_root(); 256 enode * r2 = v2->get_root(); 257 258 if (r1->get_class_size() > r2->get_class_size()) { 259 std::swap(r1, r2); 260 } 261 262 m_array_value.reset(); 263 // populate m_array_value if the select(a, i) parent terms of r1 264 for (enode* parent : r1->get_const_parents()) { 265 if (parent->is_cgr() && 266 ctx.is_relevant(parent) && 267 is_select(parent->get_owner()) && 268 parent->get_arg(0)->get_root() == r1) { 269 m_array_value.insert(parent); 270 } 271 } 272 // traverse select(a, i) parent terms of r2 trying to find a match. 273 for (enode * parent : r2->get_const_parents()) { 274 enode * other; 275 if (parent->is_cgr() && 276 ctx.is_relevant(parent) && 277 is_select(parent->get_owner()) && 278 parent->get_arg(0)->get_root() == r2 && 279 m_array_value.find(parent, other)) { 280 281 if (ctx.is_diseq(parent, other)) { 282 TRACE("array_ext", tout << "selects are disequal\n";); 283 return true; 284 } 285 } 286 } 287 return false; 288 } 289 assert_extensionality(enode * n1,enode * n2)290 bool theory_array_base::assert_extensionality(enode * n1, enode * n2) { 291 if (n1->get_owner_id() > n2->get_owner_id()) 292 std::swap(n1, n2); 293 enode * nodes[2] = { n1, n2 }; 294 if (!ctx.add_fingerprint(this, 0, 2, nodes)) 295 return false; // axiom was already instantiated 296 if (already_diseq(n1, n2)) 297 return false; 298 m_extensionality_todo.push_back(std::make_pair(n1, n2)); 299 return true; 300 } 301 assert_congruent(enode * a1,enode * a2)302 void theory_array_base::assert_congruent(enode * a1, enode * a2) { 303 TRACE("array", tout << "congruent: #" << a1->get_owner_id() << " #" << a2->get_owner_id() << "\n";); 304 SASSERT(is_array_sort(a1)); 305 SASSERT(is_array_sort(a2)); 306 if (a1->get_owner_id() > a2->get_owner_id()) 307 std::swap(a1, a2); 308 enode * nodes[2] = { a1, a2 }; 309 if (!ctx.add_fingerprint(this, 1, 2, nodes)) 310 return; // axiom was already instantiated 311 m_congruent_todo.push_back(std::make_pair(a1, a2)); 312 } 313 314 assert_extensionality_core(enode * n1,enode * n2)315 void theory_array_base::assert_extensionality_core(enode * n1, enode * n2) { 316 app * e1 = n1->get_owner(); 317 app * e2 = n2->get_owner(); 318 319 func_decl_ref_vector * funcs = nullptr; 320 sort * s = m.get_sort(e1); 321 322 VERIFY(m_sort2skolem.find(s, funcs)); 323 324 unsigned dimension = funcs->size(); 325 326 expr_ref_vector args1(m), args2(m); 327 args1.push_back(e1); 328 args2.push_back(e2); 329 for (unsigned i = 0; i < dimension; i++) { 330 expr * k = m.mk_app(funcs->get(i), e1, e2); 331 args1.push_back(k); 332 args2.push_back(k); 333 } 334 expr_ref sel1(mk_select(args1.size(), args1.c_ptr()), m); 335 expr_ref sel2(mk_select(args2.size(), args2.c_ptr()), m); 336 TRACE("ext", tout << mk_bounded_pp(sel1, m) << "\n" << mk_bounded_pp(sel2, m) << "\n";); 337 literal n1_eq_n2 = mk_eq(e1, e2, true); 338 literal sel1_eq_sel2 = mk_eq(sel1, sel2, true); 339 ctx.mark_as_relevant(n1_eq_n2); 340 ctx.mark_as_relevant(sel1_eq_sel2); 341 if (m.has_trace_stream()) { 342 app_ref body(m); 343 body = m.mk_implies(m.mk_not(ctx.bool_var2expr(n1_eq_n2.var())), m.mk_not(ctx.bool_var2expr(sel1_eq_sel2.var()))); 344 log_axiom_instantiation(body); 345 } 346 assert_axiom(n1_eq_n2, ~sel1_eq_sel2); 347 if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; 348 } 349 350 /** 351 \brief assert n1 = n2 => forall vars . (n1 vars) = (n2 vars) 352 */ assert_congruent_core(enode * n1,enode * n2)353 void theory_array_base::assert_congruent_core(enode * n1, enode * n2) { 354 app * e1 = n1->get_owner(); 355 app * e2 = n2->get_owner(); 356 sort* s = m.get_sort(e1); 357 unsigned dimension = get_array_arity(s); 358 literal n1_eq_n2 = mk_eq(e1, e2, true); 359 ctx.mark_as_relevant(n1_eq_n2); 360 expr_ref_vector args1(m), args2(m); 361 args1.push_back(instantiate_lambda(e1)); 362 args2.push_back(instantiate_lambda(e2)); 363 svector<symbol> names; 364 sort_ref_vector sorts(m); 365 for (unsigned i = 0; i < dimension; i++) { 366 sort * srt = get_array_domain(s, i); 367 sorts.push_back(srt); 368 names.push_back(symbol(i)); 369 expr * k = m.mk_var(dimension - i - 1, srt); 370 args1.push_back(k); 371 args2.push_back(k); 372 } 373 expr * sel1 = mk_select(dimension+1, args1.c_ptr()); 374 expr * sel2 = mk_select(dimension+1, args2.c_ptr()); 375 expr * eq = m.mk_eq(sel1, sel2); 376 expr_ref q(m.mk_forall(dimension, sorts.c_ptr(), names.c_ptr(), eq), m); 377 ctx.get_rewriter()(q); 378 if (!ctx.b_internalized(q)) { 379 ctx.internalize(q, true); 380 } 381 literal fa_eq = ctx.get_literal(q); 382 ctx.mark_as_relevant(fa_eq); 383 assert_axiom(~n1_eq_n2, fa_eq); 384 } 385 instantiate_lambda(app * e)386 expr_ref theory_array_base::instantiate_lambda(app* e) { 387 quantifier * q = m.is_lambda_def(e->get_decl()); 388 expr_ref f(e, m); 389 if (q) { 390 // the variables in q are maybe not consecutive. 391 var_subst sub(m, false); 392 expr_free_vars fv; 393 fv(q); 394 expr_ref_vector es(m); 395 es.resize(fv.size()); 396 for (unsigned i = 0, j = 0; i < e->get_num_args(); ++i) { 397 SASSERT(j < es.size()); 398 while (!fv[j]) { 399 ++j; 400 SASSERT(j < es.size()); 401 } 402 es[j++] = e->get_arg(i); 403 } 404 f = sub(q, es.size(), es.c_ptr()); 405 } 406 return f; 407 } 408 can_propagate()409 bool theory_array_base::can_propagate() { 410 return 411 !m_axiom1_todo.empty() || 412 !m_axiom2_todo.empty() || 413 !m_extensionality_todo.empty() || 414 !m_congruent_todo.empty() || 415 (!ctx.get_fparams().m_array_weak && has_propagate_up_trail()); 416 } 417 propagate()418 void theory_array_base::propagate() { 419 while (can_propagate()) { 420 for (unsigned i = 0; i < m_axiom1_todo.size(); i++) 421 assert_store_axiom1_core(m_axiom1_todo[i]); 422 m_axiom1_todo.reset(); 423 for (unsigned i = 0; i < m_axiom2_todo.size(); i++) 424 assert_store_axiom2_core(m_axiom2_todo[i].first, m_axiom2_todo[i].second); 425 m_axiom2_todo.reset(); 426 for (unsigned i = 0; i < m_extensionality_todo.size(); i++) 427 assert_extensionality_core(m_extensionality_todo[i].first, m_extensionality_todo[i].second); 428 for (unsigned i = 0; i < m_congruent_todo.size(); i++) 429 assert_congruent_core(m_congruent_todo[i].first, m_congruent_todo[i].second); 430 m_extensionality_todo.reset(); 431 m_congruent_todo.reset(); 432 if (!ctx.get_fparams().m_array_weak && has_propagate_up_trail()) { 433 ctx.push_trail(value_trail<context, unsigned>(m_array_weak_head)); 434 for (; m_array_weak_head < m_array_weak_trail.size(); ++m_array_weak_head) { 435 set_prop_upward(m_array_weak_trail[m_array_weak_head]); 436 } 437 } 438 } 439 } 440 441 /** 442 \brief Return true if v is shared between two different "instances" of the array theory. 443 It is shared if it is used in more than one role. The possible roles are: array, index, and value. 444 Example: 445 (store v i j) <--- v is used as an array 446 (select A v) <--- v is used as an index 447 (store A i v) <--- v is used as an value 448 */ is_shared(theory_var v) const449 bool theory_array_base::is_shared(theory_var v) const { 450 enode * n = get_enode(v); 451 enode * r = n->get_root(); 452 bool is_array = false; 453 bool is_index = false; 454 bool is_value = false; 455 int num_roles = 0; 456 #define SET_ARRAY(arg) if (arg->get_root() == r && !is_array) { is_array = true; num_roles++; } if (num_roles > 1) return true 457 #define SET_INDEX(arg) if (arg->get_root() == r && !is_index) { is_index = true; num_roles++; } if (num_roles > 1) return true 458 #define SET_VALUE(arg) if (arg->get_root() == r && !is_value) { is_value = true; num_roles++; } if (num_roles > 1) return true 459 enode_vector::const_iterator it = r->begin_parents(); 460 enode_vector::const_iterator end = r->end_parents(); 461 for (; it != end; ++it) { 462 enode * parent = *it; 463 #if 0 464 if (!ctx.is_relevant(parent)) 465 continue; 466 #endif 467 unsigned num_args = parent->get_num_args(); 468 if (is_store(parent)) { 469 SET_ARRAY(parent->get_arg(0)); 470 for (unsigned i = 1; i < num_args - 1; i++) { 471 SET_INDEX(parent->get_arg(i)); 472 } 473 SET_VALUE(parent->get_arg(num_args - 1)); 474 } 475 else if (is_select(parent)) { 476 SET_ARRAY(parent->get_arg(0)); 477 for (unsigned i = 1; i < num_args; i++) { 478 SET_INDEX(parent->get_arg(i)); 479 } 480 } 481 else if (is_const(parent)) { 482 SET_VALUE(parent->get_arg(0)); 483 } 484 } 485 return false; 486 } 487 488 #if 0 489 void theory_array_base::collect_shared_vars(sbuffer<theory_var> & result) { 490 TRACE("array_shared", tout << "collecting shared vars...\n";); 491 ptr_buffer<enode> to_unmark; 492 unsigned num_vars = get_num_vars(); 493 for (unsigned i = 0; i < num_vars; i++) { 494 enode * n = get_enode(i); 495 if (ctx.is_relevant(n) && ctx.is_shared(n)) { 496 enode * r = n->get_root(); 497 if (!r->is_marked() && is_array_sort(r)) { 498 TRACE("array_shared", tout << "new shared var: #" << r->get_expr_id() << "\n";); 499 r->set_mark(); 500 to_unmark.push_back(r); 501 theory_var r_th_var = r->get_var(get_id()); 502 SASSERT(r_th_var != null_theory_var); 503 result.push_back(r_th_var); 504 } 505 } 506 } 507 unmark_enodes(to_unmark.size(), to_unmark.c_ptr()); 508 } 509 #else 510 is_select_arg(enode * r)511 bool theory_array_base::is_select_arg(enode* r) { 512 for (enode* n : r->get_parents()) { 513 if (is_select(n)) { 514 for (unsigned i = 1; i < n->get_num_args(); ++i) { 515 if (r == n->get_arg(i)->get_root()) { 516 return true; 517 } 518 } 519 } 520 } 521 return false; 522 } 523 collect_shared_vars(sbuffer<theory_var> & result)524 void theory_array_base::collect_shared_vars(sbuffer<theory_var> & result) { 525 ptr_buffer<enode> to_unmark; 526 unsigned num_vars = get_num_vars(); 527 for (unsigned i = 0; i < num_vars; i++) { 528 enode * n = get_enode(i); 529 if (!ctx.is_relevant(n) || !is_array_sort(n)) { 530 continue; 531 } 532 enode * r = n->get_root(); 533 if (r->is_marked()) { 534 continue; 535 } 536 // arrays used as indices in other arrays have to be treated as shared. 537 // issue #3532, #3529 538 // 539 if (ctx.is_shared(r) || is_select_arg(r)) { 540 TRACE("array", tout << "new shared var: #" << r->get_owner_id() << "\n";); 541 theory_var r_th_var = r->get_th_var(get_id()); 542 SASSERT(r_th_var != null_theory_var); 543 result.push_back(r_th_var); 544 } 545 r->set_mark(); 546 to_unmark.push_back(r); 547 } 548 TRACE("array", tout << "collecting shared vars...\n" << unsigned_vector(result.size(), (unsigned*)result.c_ptr()) << "\n";); 549 unmark_enodes(to_unmark.size(), to_unmark.c_ptr()); 550 } 551 #endif 552 553 /** 554 \brief Create interface variables for shared array variables. 555 Return the number of new interface equalities. 556 */ mk_interface_eqs()557 unsigned theory_array_base::mk_interface_eqs() { 558 sbuffer<theory_var> roots; 559 collect_shared_vars(roots); 560 unsigned result = 0; 561 sbuffer<theory_var>::iterator it1 = roots.begin(); 562 sbuffer<theory_var>::iterator end1 = roots.end(); 563 for (; it1 != end1; ++it1) { 564 TRACE("array_bug", tout << "mk_interface_eqs: processing: v" << *it1 << "\n";); 565 theory_var v1 = *it1; 566 enode * n1 = get_enode(v1); 567 sort * s1 = m.get_sort(n1->get_owner()); 568 sbuffer<theory_var>::iterator it2 = it1; 569 ++it2; 570 for (; it2 != end1; ++it2) { 571 theory_var v2 = *it2; 572 enode * n2 = get_enode(v2); 573 sort * s2 = m.get_sort(n2->get_owner()); 574 if (s1 == s2 && !ctx.is_diseq(n1, n2)) { 575 app * eq = mk_eq_atom(n1->get_owner(), n2->get_owner()); 576 if (!ctx.b_internalized(eq) || !ctx.is_relevant(eq)) { 577 result++; 578 ctx.internalize(eq, true); 579 ctx.mark_as_relevant(eq); 580 } 581 } 582 } 583 } 584 return result; 585 } 586 push_scope_eh()587 void theory_array_base::push_scope_eh() { 588 m_scopes.push_back(scope(m_sorts_trail.size())); 589 theory::push_scope_eh(); 590 } 591 pop_scope_eh(unsigned num_scopes)592 void theory_array_base::pop_scope_eh(unsigned num_scopes) { 593 reset_queues(); 594 scope const & s = m_scopes[m_scopes.size() - num_scopes]; 595 restore_sorts(s.m_sorts_trail_lim); 596 m_scopes.shrink(m_scopes.size()-num_scopes); 597 theory::pop_scope_eh(num_scopes); 598 } 599 restore_sorts(unsigned old_size)600 void theory_array_base::restore_sorts(unsigned old_size) { 601 while (m_sorts_trail.size() > old_size) { 602 sort * s = m_sorts_trail.back(); 603 func_decl_ref_vector * funcs = nullptr; 604 if (m_sort2skolem.find(s, funcs)) { 605 m_sort2skolem.remove(s); 606 dealloc(funcs); 607 } 608 m_sorts_trail.pop_back(); 609 } 610 } 611 reset_eh()612 void theory_array_base::reset_eh() { 613 reset_queues(); 614 pop_scope_eh(0); 615 theory::reset_eh(); 616 } 617 reset_queues()618 void theory_array_base::reset_queues() { 619 m_axiom1_todo.reset(); 620 m_axiom2_todo.reset(); 621 m_extensionality_todo.reset(); 622 m_congruent_todo.reset(); 623 } 624 625 set_default(theory_var v,enode * n)626 void theory_array_base::set_default(theory_var v, enode* n) { 627 TRACE("array", tout << "set default: " << v << " " << mk_pp(n->get_owner(), m) << "\n";); 628 v = mg_find(v); 629 if (m_defaults[v] == 0) { 630 m_defaults[v] = n; 631 } 632 } 633 get_default(theory_var v)634 enode* theory_array_base::get_default(theory_var v) { 635 return m_defaults[mg_find(v)]; 636 } 637 mg_find(theory_var n)638 theory_var theory_array_base::mg_find(theory_var n) { 639 if (m_parents[n] < 0) { 640 return n; 641 } 642 theory_var n0 = n; 643 n = m_parents[n0]; 644 if (m_parents[n] < -1) { 645 return n; 646 } 647 while (m_parents[n] >= 0) { 648 n = m_parents[n]; 649 } 650 // compress path. 651 while (m_parents[n0] >= 0) { 652 theory_var n1 = m_parents[n0]; 653 m_parents[n0] = n; 654 n0 = n1; 655 } 656 return n; 657 } 658 mg_merge(theory_var u,theory_var v)659 void theory_array_base::mg_merge(theory_var u, theory_var v) { 660 u = mg_find(u); 661 v = mg_find(v); 662 if (u != v) { 663 SASSERT(m_parents[u] < 0); 664 SASSERT(m_parents[v] < 0); 665 if (m_parents[u] > m_parents[v]) { 666 std::swap(u, v); 667 } 668 m_parents[u] += m_parents[v]; 669 m_parents[v] = u; 670 671 if (m_defaults[u] == 0) { 672 m_defaults[u] = m_defaults[v]; 673 } 674 CTRACE("array", m_defaults[v], 675 tout << mk_pp(m_defaults[v]->get_root()->get_owner(), m) << "\n"; 676 tout << mk_pp(m_defaults[u]->get_root()->get_owner(), m) << "\n"; 677 ); 678 679 // NB. it may be the case that m_defaults[u] != m_defaults[v] 680 // when m and n are finite arrays. 681 682 } 683 } 684 685 init_model(model_generator & mg)686 void theory_array_base::init_model(model_generator & mg) { 687 m_factory = alloc(array_factory, m, mg.get_model()); 688 mg.register_factory(m_factory); 689 m_use_unspecified_default = is_unspecified_default_ok(); 690 collect_defaults(); 691 collect_selects(); 692 propagate_selects(); 693 if (m_bapa) m_bapa->init_model(); 694 } 695 696 /** 697 \brief It is ok to use an unspecified default value for arrays, when the 698 logical context does not contain store, default and const terms. 699 700 That is, other modules (such as smt_model_finder) may set the default value to an arbitrary value. 701 */ is_unspecified_default_ok() const702 bool theory_array_base::is_unspecified_default_ok() const { 703 int num_vars = get_num_vars(); 704 for (theory_var v = 0; v < num_vars; ++v) { 705 enode * n = get_enode(v); 706 707 // If n is not relevant, then it should not be used to set defaults. 708 if (!ctx.is_relevant(n)) 709 continue; 710 711 if (is_store(n) || is_const(n) || is_default(n) || is_set_has_size(n)) 712 return false; 713 } 714 return true; 715 } 716 717 collect_defaults()718 void theory_array_base::collect_defaults() { 719 int num_vars = get_num_vars(); 720 m_defaults.reset(); 721 m_else_values.reset(); 722 m_parents.reset(); 723 m_parents.resize(num_vars, -1); 724 m_defaults.resize(num_vars); 725 m_else_values.resize(num_vars); 726 727 if (m_use_unspecified_default) 728 return; 729 730 731 // 732 // Create equivalence classes for defaults. 733 // 734 for (theory_var v = 0; v < num_vars; ++v) { 735 enode * n = get_enode(v); 736 737 // If n is not relevant, then it should not be used to set defaults. 738 if (!ctx.is_relevant(n)) 739 continue; 740 741 theory_var r = get_representative(v); 742 743 mg_merge(v, r); 744 745 if (is_store(n)) { 746 theory_var w = n->get_arg(0)->get_th_var(get_id()); 747 SASSERT(w != null_theory_var); 748 749 mg_merge(v, get_representative(w)); 750 751 TRACE("array", tout << "merge: " << mk_pp(n->get_owner(), m) << " " << v << " " << w << "\n";); 752 } 753 else if (is_const(n)) { 754 set_default(v, n->get_arg(0)); 755 } 756 else if (is_default(n)) { 757 theory_var w = n->get_arg(0)->get_th_var(get_id()); 758 SASSERT(w != null_theory_var); 759 set_default(w, n); 760 } 761 } 762 } 763 operator ()(enode * n) const764 unsigned theory_array_base::sel_hash::operator()(enode * n) const { 765 return get_composite_hash<enode *, sel_khasher, sel_chasher>(n, n->get_num_args() - 1, sel_khasher(), sel_chasher()); 766 } 767 operator ()(enode * n1,enode * n2) const768 bool theory_array_base::sel_eq::operator()(enode * n1, enode * n2) const { 769 SASSERT(n1->get_num_args() == n2->get_num_args()); 770 unsigned num_args = n1->get_num_args(); 771 for (unsigned i = 1; i < num_args; i++) { 772 if (n1->get_arg(i)->get_root() != n2->get_arg(i)->get_root()) 773 return false; 774 } 775 return true; 776 } 777 get_select_set(enode * n)778 theory_array_base::select_set * theory_array_base::get_select_set(enode * n) { 779 enode * r = n->get_root(); 780 select_set * set = nullptr; 781 m_selects.find(r, set); 782 if (set == nullptr) { 783 set = alloc(select_set); 784 m_selects.insert(r, set); 785 m_selects_domain.push_back(r); 786 m_selects_range.push_back(set); 787 } 788 return set; 789 } 790 collect_selects()791 void theory_array_base::collect_selects() { 792 int num_vars = get_num_vars(); 793 794 m_selects.reset(); 795 m_selects_domain.reset(); 796 m_selects_range.reset(); 797 798 for (theory_var v = 0; v < num_vars; ++v) { 799 enode * r = get_enode(v)->get_root(); 800 if (is_representative(v) && ctx.is_relevant(r)) { 801 for (enode * parent : r->get_const_parents()) { 802 if (parent->get_cg() == parent && 803 ctx.is_relevant(parent) && 804 is_select(parent) && 805 parent->get_arg(0)->get_root() == r) { 806 select_set * s = get_select_set(r); 807 SASSERT(!s->contains(parent) || (*(s->find(parent)))->get_root() == parent->get_root()); 808 s->insert(parent); 809 } 810 } 811 } 812 } 813 } 814 propagate_select_to_store_parents(enode * r,enode * sel,enode_pair_vector & todo)815 void theory_array_base::propagate_select_to_store_parents(enode * r, enode * sel, enode_pair_vector & todo) { 816 SASSERT(r->get_root() == r); 817 SASSERT(is_select(sel)); 818 if (!ctx.is_relevant(r)) { 819 return; 820 } 821 for (enode * parent : r->get_const_parents()) { 822 if (ctx.is_relevant(parent) && 823 is_store(parent) && 824 parent->get_arg(0)->get_root() == r) { 825 // propagate upward 826 select_set * parent_sel_set = get_select_set(parent); 827 enode * parent_root = parent->get_root(); 828 829 if (parent_sel_set->contains(sel)) 830 continue; 831 832 SASSERT(sel->get_num_args() + 1 == parent->get_num_args()); 833 834 // check whether the sel idx was overwritten by the store 835 unsigned num_args = sel->get_num_args(); 836 unsigned i = 1; 837 for (; i < num_args; i++) { 838 if (sel->get_arg(i)->get_root() != parent->get_arg(i)->get_root()) 839 break; 840 } 841 842 if (i < num_args) { 843 SASSERT(!parent_sel_set->contains(sel) || (*(parent_sel_set->find(sel)))->get_root() == sel->get_root()); 844 parent_sel_set->insert(sel); 845 todo.push_back(std::make_pair(parent_root, sel)); 846 } 847 } 848 } 849 } 850 propagate_selects_to_store_parents(enode * r,enode_pair_vector & todo)851 void theory_array_base::propagate_selects_to_store_parents(enode * r, enode_pair_vector & todo) { 852 select_set * sel_set = get_select_set(r); 853 for (enode* sel : *sel_set) { 854 SASSERT(is_select(sel)); 855 propagate_select_to_store_parents(r, sel, todo); 856 } 857 } 858 propagate_selects()859 void theory_array_base::propagate_selects() { 860 enode_pair_vector todo; 861 for (enode * r : m_selects_domain) { 862 propagate_selects_to_store_parents(r, todo); 863 } 864 for (unsigned qhead = 0; qhead < todo.size(); qhead++) { 865 enode_pair & pair = todo[qhead]; 866 enode * r = pair.first; 867 enode * sel = pair.second; 868 propagate_select_to_store_parents(r, sel, todo); 869 } 870 } 871 finalize_model(model_generator & m)872 void theory_array_base::finalize_model(model_generator & m) { 873 std::for_each(m_selects_range.begin(), m_selects_range.end(), delete_proc<select_set>()); 874 } 875 876 class array_value_proc : public model_value_proc { 877 family_id m_fid; 878 sort * m_sort; 879 unsigned m_num_entries; 880 unsigned m_dim; //!< number of dimensions; 881 app * m_else; 882 bool m_unspecified_else; 883 svector<model_value_dependency> m_dependencies; 884 885 public: array_value_proc(family_id fid,sort * s,extra_fresh_value * v)886 array_value_proc(family_id fid, sort * s, extra_fresh_value * v): 887 m_fid(fid), 888 m_sort(s), 889 m_num_entries(0), 890 m_dim(0), 891 m_else(nullptr), 892 m_unspecified_else(false) { 893 m_dependencies.push_back(model_value_dependency(v)); 894 } 895 array_value_proc(family_id fid,sort * s,app * else_value)896 array_value_proc(family_id fid, sort * s, app * else_value): 897 m_fid(fid), 898 m_sort(s), 899 m_num_entries(0), 900 m_dim(0), 901 m_else(else_value), 902 m_unspecified_else(false) { 903 } 904 array_value_proc(family_id fid,sort * s,enode * else_value)905 array_value_proc(family_id fid, sort * s, enode * else_value): 906 m_fid(fid), 907 m_sort(s), 908 m_num_entries(0), 909 m_dim(0), 910 m_else(nullptr), 911 m_unspecified_else(false) { 912 m_dependencies.push_back(model_value_dependency(else_value)); 913 } 914 array_value_proc(family_id fid,sort * s)915 array_value_proc(family_id fid, sort * s): 916 m_fid(fid), 917 m_sort(s), 918 m_num_entries(0), 919 m_dim(0), 920 m_else(nullptr), 921 m_unspecified_else(true) { 922 } 923 ~array_value_proc()924 ~array_value_proc() override {} 925 add_entry(unsigned num_args,enode * const * args,enode * value)926 void add_entry(unsigned num_args, enode * const * args, enode * value) { 927 SASSERT(num_args > 0); 928 SASSERT(m_dim == 0 || m_dim == num_args); 929 m_dim = num_args; 930 m_num_entries ++; 931 for (unsigned i = 0; i < num_args; i++) 932 m_dependencies.push_back(model_value_dependency(args[i])); 933 m_dependencies.push_back(model_value_dependency(value)); 934 } 935 get_dependencies(buffer<model_value_dependency> & result)936 void get_dependencies(buffer<model_value_dependency> & result) override { 937 result.append(m_dependencies.size(), m_dependencies.c_ptr()); 938 } 939 mk_value(model_generator & mg,expr_ref_vector const & values)940 app * mk_value(model_generator & mg, expr_ref_vector const & values) override { 941 // values must have size = m_num_entries * (m_dim + 1) + ((m_else || m_unspecified_else) ? 0 : 1) 942 // an array value is a lookup table + else_value 943 // each entry has m_dim indexes that map to a value. 944 ast_manager & m = mg.get_manager(); 945 SASSERT(values.size() == m_dependencies.size()); 946 SASSERT(values.size() == m_num_entries * (m_dim + 1) + ((m_else || m_unspecified_else) ? 0 : 1)); 947 948 unsigned arity = get_array_arity(m_sort); 949 func_decl * f = mk_aux_decl_for_array_sort(m, m_sort); 950 func_interp * fi = alloc(func_interp, m, arity); 951 mg.get_model().register_decl(f, fi); 952 953 unsigned idx = 0; 954 if (m_else || m_unspecified_else) { 955 fi->set_else(m_else); 956 } 957 else { 958 fi->set_else(to_app(values[0])); 959 idx = 1; 960 } 961 962 ptr_buffer<expr> args; 963 for (unsigned i = 0; i < m_num_entries; i++) { 964 args.reset(); 965 // copy indices 966 for (unsigned j = 0; j < m_dim; j++, idx++) 967 args.push_back(values[idx]); 968 expr * result = values[idx]; 969 idx++; 970 fi->insert_entry(args.c_ptr(), result); 971 } 972 973 parameter p[1] = { parameter(f) }; 974 return m.mk_app(m_fid, OP_AS_ARRAY, 1, p); 975 } 976 }; 977 include_func_interp(func_decl * f)978 bool theory_array_base::include_func_interp(func_decl* f) { 979 return is_decl_of(f, get_id(), OP_ARRAY_EXT); 980 } 981 mk_value(enode * n,model_generator & mg)982 model_value_proc * theory_array_base::mk_value(enode * n, model_generator & mg) { 983 SASSERT(ctx.is_relevant(n)); 984 theory_var v = n->get_th_var(get_id()); 985 SASSERT(v != null_theory_var); 986 sort * s = m.get_sort(n->get_owner()); 987 enode * else_val_n = get_default(v); 988 array_value_proc * result = nullptr; 989 990 if (m_use_unspecified_default) { 991 SASSERT(else_val_n == 0); 992 result = alloc(array_value_proc, get_id(), s); 993 } 994 else { 995 if (else_val_n != nullptr) { 996 SASSERT(ctx.is_relevant(else_val_n)); 997 result = alloc(array_value_proc, get_id(), s, else_val_n); 998 } 999 else { 1000 theory_var r = mg_find(v); 1001 void * else_val = m_else_values[r]; 1002 // DISABLED. It seems wrong, since different nodes can share the same 1003 // else_val according to the mg class. 1004 // SASSERT(else_val == 0 || ctx.is_relevant(UNTAG(app*, else_val))); 1005 if (else_val == nullptr) { 1006 sort * range = to_sort(s->get_parameter(s->get_num_parameters() - 1).get_ast()); 1007 // IMPORTANT: 1008 // The implementation should not assume a fresh value is created for 1009 // the else_val if the range is finite 1010 1011 TRACE("array", tout << mk_pp(n->get_owner(), m) << " " << mk_pp(range, m) << " " << range->is_infinite() << "\n";); 1012 if (range->is_infinite()) 1013 else_val = TAG(void*, mg.mk_extra_fresh_value(range), 1); 1014 else 1015 else_val = TAG(void*, mg.get_some_value(range), 0); 1016 m_else_values[r] = else_val; 1017 } 1018 if (GET_TAG(else_val) == 0) { 1019 result = alloc(array_value_proc, get_id(), s, UNTAG(app*, else_val)); 1020 } 1021 else { 1022 result = alloc(array_value_proc, get_id(), s, UNTAG(extra_fresh_value*, else_val)); 1023 } 1024 } 1025 } 1026 SASSERT(result != 0); 1027 select_set * sel_set = nullptr; 1028 m_selects.find(n->get_root(), sel_set); 1029 if (sel_set != nullptr) { 1030 ptr_buffer<enode> args; 1031 for (enode * select : *sel_set) { 1032 args.reset(); 1033 unsigned num = select->get_num_args(); 1034 for (unsigned j = 1; j < num; ++j) 1035 args.push_back(select->get_arg(j)); 1036 SASSERT(ctx.is_relevant(select)); 1037 result->add_entry(args.size(), args.c_ptr(), select); 1038 } 1039 } 1040 TRACE("array", 1041 tout << mk_pp(n->get_root()->get_owner(), m) << "\n"; 1042 if (sel_set) { 1043 for (enode* s : *sel_set) { 1044 tout << "#" << s->get_root()->get_owner()->get_id() << " " << mk_pp(s->get_owner(), m) << "\n"; 1045 } 1046 } 1047 if (else_val_n) { 1048 tout << "else: " << mk_pp(else_val_n->get_owner(), m) << "\n"; 1049 }); 1050 return result; 1051 } 1052 1053 }; 1054