1 /*++ 2 Copyright (c) 2011 Microsoft Corporation 3 4 Module Name: 5 6 seq_eq_solver 7 8 Abstract: 9 10 Solver-agnostic equality solving routines for sequences 11 12 Author: 13 14 Nikolaj Bjorner (nbjorner) 2021-03-01 15 16 --*/ 17 18 #include "ast/ast_pp.h" 19 #include "ast/rewriter/seq_eq_solver.h" 20 #include "ast/bv_decl_plugin.h" 21 22 namespace seq { 23 reduce(expr * s,expr * t,eq_ptr & r)24 bool eq_solver::reduce(expr* s, expr* t, eq_ptr& r) { 25 expr_ref_vector ls(m), rs(m); 26 ls.push_back(s); 27 rs.push_back(t); 28 eqr e(ls, rs); 29 return reduce(e, r); 30 } 31 reduce(eqr const & e,eq_ptr & r)32 bool eq_solver::reduce(eqr const& e, eq_ptr& r) { 33 r = nullptr; 34 if (reduce_unit(e, r)) 35 return true; 36 if (reduce_itos1(e, r)) 37 return true; 38 if (reduce_itos2(e, r)) 39 return true; 40 if (reduce_itos3(e, r)) 41 return true; 42 if (reduce_ubv2s1(e, r)) 43 return true; 44 if (reduce_ubv2s2(e, r)) 45 return true; 46 if (reduce_binary_eq(e, r)) 47 return true; 48 if (reduce_nth_solved(e, r)) 49 return true; 50 51 return false; 52 } 53 54 branch(unsigned priority,eqr const & e)55 bool eq_solver::branch(unsigned priority, eqr const& e) { 56 switch (priority) { 57 case 0: 58 return branch_unit_variable(e); 59 case 1: 60 default: 61 break; 62 } 63 return false; 64 } 65 set_conflict()66 void eq_solver::set_conflict() { 67 m_clause.reset(); 68 ctx.add_consequence(true, m_clause); 69 } 70 add_consequence(expr_ref const & a)71 void eq_solver::add_consequence(expr_ref const& a) { 72 m_clause.reset(); 73 m_clause.push_back(a); 74 ctx.add_consequence(true, m_clause); 75 } 76 add_consequence(expr_ref const & a,expr_ref const & b)77 void eq_solver::add_consequence(expr_ref const& a, expr_ref const& b) { 78 m_clause.reset(); 79 m_clause.push_back(a); 80 m_clause.push_back(b); 81 ctx.add_consequence(true, m_clause); 82 } 83 84 /** 85 * from_int(s) == from_int(t) 86 * -------------------------- 87 * s = t or (s < 0 and t < 0) 88 */ 89 match_itos1(eqr const & e,expr * & a,expr * & b)90 bool eq_solver::match_itos1(eqr const& e, expr*& a, expr*& b) { 91 return 92 e.ls.size() == 1 && e.rs.size() == 1 && 93 seq.str.is_itos(e.ls[0], a) && seq.str.is_itos(e.rs[0], b); 94 } 95 reduce_itos1(eqr const & e,eq_ptr & r)96 bool eq_solver::reduce_itos1(eqr const& e, eq_ptr& r) { 97 expr* s = nullptr, * t = nullptr; 98 if (!match_itos1(e, s, t)) 99 return false; 100 expr_ref eq = mk_eq(s, t); 101 add_consequence(eq, mk_le(s, -1)); 102 add_consequence(eq, mk_le(t, -1)); 103 return true; 104 } 105 106 /** 107 * from_int(s) == "" 108 * ----------------- 109 * s < 0 110 */ 111 match_itos2(eqr const & e,expr * & s)112 bool eq_solver::match_itos2(eqr const& e, expr*& s) { 113 if (e.ls.size() == 1 && e.rs.empty() && seq.str.is_itos(e.ls[0], s)) 114 return true; 115 if (e.rs.size() == 1 && e.ls.empty() && seq.str.is_itos(e.rs[0], s)) 116 return true; 117 return false; 118 } 119 reduce_itos2(eqr const & e,eq_ptr & r)120 bool eq_solver::reduce_itos2(eqr const& e, eq_ptr& r) { 121 expr* s = nullptr; 122 if (!match_itos2(e, s)) 123 return false; 124 add_consequence(mk_le(s, -1)); 125 return true; 126 } 127 128 /** 129 * itos(n) = "" 130 * ------------ 131 * n <= -1 132 * 133 * itos(n) = [d1]+[d2]+...+[dk] 134 * --------------------------------- 135 * n = 10^{k-1}*d1 + ... + dk 136 * 137 * k > 1 => d1 > 0 138 */ 139 match_itos3(eqr const & e,expr * & n,expr_ref_vector const * & es)140 bool eq_solver::match_itos3(eqr const& e, expr*& n, expr_ref_vector const*& es) { 141 if (e.ls.size() == 1 && seq.str.is_itos(e.ls[0], n)) { 142 es = &e.rs; 143 return true; 144 } 145 if (e.rs.size() == 1 && seq.str.is_itos(e.rs[0], n)) { 146 es = &e.ls; 147 return true; 148 } 149 return false; 150 } 151 reduce_itos3(eqr const & e,eq_ptr & r)152 bool eq_solver::reduce_itos3(eqr const& e, eq_ptr& r) { 153 expr* n = nullptr; 154 expr_ref_vector const* _es = nullptr; 155 if (!match_itos3(e, n, _es)) 156 return false; 157 158 expr_ref_vector const& es = *_es; 159 160 if (es.empty()) { 161 add_consequence(m_ax.mk_le(n, -1)); 162 return true; 163 } 164 expr* u = nullptr; 165 for (expr* r : es) { 166 if (seq.str.is_unit(r, u)) { 167 expr_ref is_digit = m_ax.is_digit(u); 168 if (!m.is_true(ctx.expr2rep(is_digit))) 169 add_consequence(is_digit); 170 } 171 } 172 if (!all_units(es, 0, es.size())) 173 return false; 174 175 expr_ref num(m); 176 for (expr* r : es) { 177 VERIFY(seq.str.is_unit(r, u)); 178 expr_ref digit = m_ax.sk().mk_digit2int(u); 179 if (!num) 180 num = digit; 181 else 182 num = a.mk_add(a.mk_mul(a.mk_int(10), num), digit); 183 } 184 185 expr_ref eq(m.mk_eq(n, num), m); 186 m_ax.rewrite(eq); 187 add_consequence(eq); 188 if (es.size() > 1) { 189 VERIFY(seq.str.is_unit(es[0], u)); 190 expr_ref digit = m_ax.sk().mk_digit2int(u); 191 add_consequence(m_ax.mk_ge(digit, 1)); 192 } 193 expr_ref y(seq.str.mk_concat(es, es[0]->get_sort()), m); 194 ctx.add_solution(seq.str.mk_itos(n), y); 195 return true; 196 } 197 198 /** 199 * x = t, where x does not occur in t. 200 */ reduce_unit(eqr const & e,eq_ptr & r)201 bool eq_solver::reduce_unit(eqr const& e, eq_ptr& r) { 202 if (e.ls == e.rs) 203 return true; 204 if (e.ls.size() == 1 && is_var(e.ls[0]) && !occurs(e.ls[0], e.rs)) { 205 expr_ref y(seq.str.mk_concat(e.rs, e.ls[0]->get_sort()), m); 206 ctx.add_solution(e.ls[0], y); 207 return true; 208 } 209 if (e.rs.size() == 1 && is_var(e.rs[0]) && !occurs(e.rs[0], e.ls)) { 210 expr_ref y(seq.str.mk_concat(e.ls, e.rs[0]->get_sort()), m); 211 ctx.add_solution(e.rs[0], y); 212 return true; 213 } 214 return false; 215 } 216 217 218 219 /** 220 * from_ubv(s) == from_ubv(t) 221 * -------------------------- 222 * s = t 223 */ 224 match_ubv2s1(eqr const & e,expr * & a,expr * & b)225 bool eq_solver::match_ubv2s1(eqr const& e, expr*& a, expr*& b) { 226 return 227 e.ls.size() == 1 && e.rs.size() == 1 && 228 seq.str.is_ubv2s(e.ls[0], a) && seq.str.is_ubv2s(e.rs[0], b); 229 return false; 230 } 231 reduce_ubv2s1(eqr const & e,eq_ptr & r)232 bool eq_solver::reduce_ubv2s1(eqr const& e, eq_ptr& r) { 233 expr* s = nullptr, * t = nullptr; 234 if (!match_ubv2s1(e, s, t)) 235 return false; 236 expr_ref eq = mk_eq(s, t); 237 add_consequence(eq); 238 return true; 239 } 240 241 /** 242 * 243 * bv2s(n) = [d1]+[d2]+...+[dk] 244 * --------------------------------- 245 * n = 10^{k-1}*d1 + ... + dk 246 * 247 * k > 1 => d1 > 0 248 */ match_ubv2s2(eqr const & e,expr * & n,expr_ref_vector const * & es)249 bool eq_solver::match_ubv2s2(eqr const& e, expr*& n, expr_ref_vector const*& es) { 250 if (e.ls.size() == 1 && seq.str.is_ubv2s(e.ls[0], n)) { 251 es = &e.rs; 252 return true; 253 } 254 if (e.rs.size() == 1 && seq.str.is_ubv2s(e.rs[0], n)) { 255 es = &e.ls; 256 return true; 257 } 258 return false; 259 } 260 reduce_ubv2s2(eqr const & e,eq_ptr & r)261 bool eq_solver::reduce_ubv2s2(eqr const& e, eq_ptr& r) { 262 expr* n = nullptr; 263 expr_ref_vector const* _es = nullptr; 264 if (!match_ubv2s2(e, n, _es)) 265 return false; 266 267 expr_ref_vector const& es = *_es; 268 if (es.empty()) { 269 set_conflict(); 270 return true; 271 } 272 expr* u = nullptr; 273 for (expr* r : es) { 274 if (seq.str.is_unit(r, u)) { 275 expr_ref is_digit = m_ax.is_digit(u); 276 if (!m.is_true(ctx.expr2rep(is_digit))) 277 add_consequence(is_digit); 278 } 279 } 280 if (!all_units(es, 0, es.size())) 281 return false; 282 283 expr_ref num(m); 284 bv_util bv(m); 285 sort* bv_sort = n->get_sort(); 286 unsigned sz = bv.get_bv_size(n); 287 if (es.size() > (sz + log2(10)-1)/log2(10)) { 288 set_conflict(); 289 return true; 290 } 291 292 for (expr* r : es) { 293 VERIFY(seq.str.is_unit(r, u)); 294 expr_ref digit = m_ax.sk().mk_digit2bv(u, bv_sort); 295 if (!num) 296 num = digit; 297 else 298 num = bv.mk_bv_add(bv.mk_bv_mul(bv.mk_numeral(10, sz), num), digit); 299 } 300 301 expr_ref eq(m.mk_eq(n, num), m); 302 m_ax.rewrite(eq); 303 add_consequence(eq); 304 if (es.size() > 1) { 305 VERIFY(seq.str.is_unit(es[0], u)); 306 expr_ref digit = m_ax.sk().mk_digit2bv(u, bv_sort); 307 expr_ref eq0(m.mk_eq(digit, bv.mk_numeral(0, sz)), m); 308 expr_ref neq0(m.mk_not(eq0), m); 309 add_consequence(neq0); 310 } 311 expr_ref y(seq.str.mk_concat(es, es[0]->get_sort()), m); 312 ctx.add_solution(seq.str.mk_ubv2s(n), y); 313 return true; 314 } 315 316 317 /** 318 * Equation is of the form x ++ xs = ys ++ x 319 * where |xs| = |ys| are units of same length 320 * then xs is a wrap-around of ys 321 * x ++ ab = ba ++ x 322 * 323 * When it is of the form x ++ a = b ++ x 324 * Infer that a = b 325 * It is also the case that x is a repetition of a's 326 * But this information is not exposed with this inference. 327 * 328 */ reduce_binary_eq(eqr const & e,eq_ptr & r)329 bool eq_solver::reduce_binary_eq(eqr const& e, eq_ptr& r) { 330 ptr_vector<expr> xs, ys; 331 expr_ref x(m), y(m); 332 if (!match_binary_eq(e, x, xs, ys, y)) 333 return false; 334 335 if (xs.size() != ys.size()) { 336 set_conflict(); 337 return true; 338 } 339 if (xs.empty()) 340 return true; 341 342 if (xs.size() != 1) 343 return false; 344 345 if (ctx.expr2rep(xs[0]) == ctx.expr2rep(ys[0])) 346 return false; 347 expr_ref eq(m.mk_eq(xs[0], ys[0]), m); 348 expr* veq = ctx.expr2rep(eq); 349 if (m.is_true(veq)) 350 return false; 351 add_consequence(eq); 352 return m.is_false(veq); 353 } 354 355 /** 356 * x = nth(unit(x, 0)) ++ ... ++ nth(unit(x,i)) 357 * ------------------------------------------------ 358 * x -> nth(unit(x, 0)) ++ ... ++ nth(unit(x,i)) 359 */ 360 reduce_nth_solved(eqr const & e,eq_ptr & r)361 bool eq_solver::reduce_nth_solved(eqr const& e, eq_ptr& r) { 362 expr_ref x(m), y(m); 363 if (match_nth_solved(e, x, y)) { 364 ctx.add_solution(x, y); 365 return true; 366 } 367 return false; 368 } 369 match_nth_solved(eqr const & e,expr_ref & x,expr_ref & y)370 bool eq_solver::match_nth_solved(eqr const& e, expr_ref& x, expr_ref& y) { 371 if (match_nth_solved_aux(e.ls, e.rs, x, y)) 372 return true; 373 if (match_nth_solved_aux(e.rs, e.ls, x, y)) 374 return true; 375 return false; 376 } 377 match_nth_solved_aux(expr_ref_vector const & ls,expr_ref_vector const & rs,expr_ref & x,expr_ref & y)378 bool eq_solver::match_nth_solved_aux(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref& x, expr_ref& y) { 379 if (ls.size() != 1 || !is_var(ls[0])) 380 return false; 381 expr* n = nullptr, * u = nullptr; 382 unsigned j = 0, i = 0; 383 for (expr* r : rs) { 384 if (seq.str.is_unit(r, u) && seq.str.is_nth_i(u, n, i) && i == j && n == ls[0]) 385 ++j; 386 else 387 return false; 388 } 389 x = ls[0]; 390 y = seq.str.mk_concat(rs, x->get_sort()); 391 return true; 392 } 393 394 /** 395 * XV == abcdef, where V is an arbitrary string 396 * --------------------------------------------- 397 * |X| <= |abcdef| 398 * 399 * |X| = k => X = a_1...a_k 400 */ 401 branch_unit_variable(expr * X,expr_ref_vector const & units)402 bool eq_solver::branch_unit_variable(expr* X, expr_ref_vector const& units) { 403 SASSERT(is_var(X)); 404 rational lenX; 405 ctx.get_length(X, lenX); 406 407 if (lenX > units.size()) { 408 add_consequence(m_ax.mk_le(seq.str.mk_length(X), units.size())); 409 return true; 410 } 411 412 expr_ref eq_length(m.mk_eq(a.mk_int(lenX), seq.str.mk_length(X)), m); 413 expr* val = ctx.expr2rep(eq_length); 414 if (!m.is_false(val)) { 415 expr_ref Y(seq.str.mk_concat(lenX.get_unsigned(), units.data(), X->get_sort()), m); 416 expr_ref eq = m_ax.sk().mk_eq(X, Y); 417 add_consequence(~eq_length, eq); 418 return true; 419 } 420 return false; 421 } 422 branch_unit_variable(eqr const & e)423 bool eq_solver::branch_unit_variable(eqr const& e) { 424 if (!e.ls.empty() && is_var(e.ls[0]) && all_units(e.rs, 0, e.rs.size())) 425 return branch_unit_variable(e.ls[0], e.rs); 426 if (!e.rs.empty() && is_var(e.rs[0]) && all_units(e.ls, 0, e.ls.size())) 427 return branch_unit_variable(e.rs[0], e.ls); 428 return false; 429 } 430 431 is_var(expr * a) const432 bool eq_solver::is_var(expr* a) const { 433 return 434 seq.is_seq(a) && 435 !seq.str.is_concat(a) && 436 !seq.str.is_empty(a) && 437 !seq.str.is_string(a) && 438 !seq.str.is_unit(a) && 439 !seq.str.is_itos(a) && 440 !seq.str.is_nth_i(a) && 441 !m.is_ite(a); 442 } 443 occurs(expr * a,expr_ref_vector const & b)444 bool eq_solver::occurs(expr* a, expr_ref_vector const& b) { 445 for (auto const& elem : b) 446 if (a == elem || m.is_ite(elem)) 447 return true; 448 return false; 449 } 450 occurs(expr * a,expr * b)451 bool eq_solver::occurs(expr* a, expr* b) { 452 // true if a occurs under an interpreted function or under left/right selector. 453 SASSERT(is_var(a)); 454 SASSERT(m_todo.empty()); 455 expr* e1 = nullptr, * e2 = nullptr; 456 m_todo.push_back(b); 457 while (!m_todo.empty()) { 458 b = m_todo.back(); 459 if (a == b || m.is_ite(b)) { 460 m_todo.reset(); 461 return true; 462 } 463 m_todo.pop_back(); 464 if (seq.str.is_concat(b, e1, e2)) { 465 m_todo.push_back(e1); 466 m_todo.push_back(e2); 467 } 468 else if (seq.str.is_unit(b, e1)) { 469 m_todo.push_back(e1); 470 } 471 else if (seq.str.is_nth_i(b, e1, e2)) { 472 m_todo.push_back(e1); 473 } 474 } 475 return false; 476 } 477 set_prefix(expr_ref & x,expr_ref_vector const & xs,unsigned sz) const478 void eq_solver::set_prefix(expr_ref& x, expr_ref_vector const& xs, unsigned sz) const { 479 SASSERT(0 < xs.size() && sz <= xs.size()); 480 x = seq.str.mk_concat(sz, xs.data(), xs[0]->get_sort()); 481 } 482 set_suffix(expr_ref & x,expr_ref_vector const & xs,unsigned sz) const483 void eq_solver::set_suffix(expr_ref& x, expr_ref_vector const& xs, unsigned sz) const { 484 SASSERT(0 < xs.size() && sz <= xs.size()); 485 x = seq.str.mk_concat(sz, xs.data() + xs.size() - sz, xs[0]->get_sort()); 486 } 487 count_units_l2r(expr_ref_vector const & es,unsigned offset) const488 unsigned eq_solver::count_units_l2r(expr_ref_vector const& es, unsigned offset) const { 489 unsigned i = offset, sz = es.size(); 490 for (; i < sz && seq.str.is_unit(es[i]); ++i); 491 return i - offset; 492 } 493 count_units_r2l(expr_ref_vector const & es,unsigned offset) const494 unsigned eq_solver::count_units_r2l(expr_ref_vector const& es, unsigned offset) const { 495 SASSERT(offset < es.size()); 496 unsigned i = offset, count = 0; 497 do { 498 if (!seq.str.is_unit(es[i])) 499 break; 500 ++count; 501 } while (i-- > 0); 502 return count; 503 } 504 count_non_units_l2r(expr_ref_vector const & es,unsigned offset) const505 unsigned eq_solver::count_non_units_l2r(expr_ref_vector const& es, unsigned offset) const { 506 unsigned i = offset, sz = es.size(); 507 for (; i < sz && !seq.str.is_unit(es[i]); ++i); 508 return i - offset; 509 } 510 count_non_units_r2l(expr_ref_vector const & es,unsigned offset) const511 unsigned eq_solver::count_non_units_r2l(expr_ref_vector const& es, unsigned offset) const { 512 SASSERT(offset < es.size()); 513 unsigned i = offset, count = 0; 514 do { 515 if (seq.str.is_unit(es[i])) 516 break; 517 ++count; 518 } while (i-- > 0); 519 return count; 520 } 521 522 /** 523 * match: .. X abc = Y .. Z def U 524 * where U is a variable or concatenation of variables 525 */ 526 match_ternary_eq_r(expr_ref_vector const & ls,expr_ref_vector const & rs,expr_ref & x,expr_ref_vector & xs,expr_ref & y1,expr_ref_vector & ys,expr_ref & y2)527 bool eq_solver::match_ternary_eq_r(expr_ref_vector const& ls, expr_ref_vector const& rs, 528 expr_ref& x, expr_ref_vector& xs, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2) { 529 if (ls.size() > 1 && rs.size() > 1 && is_var(rs[0]) && is_var(rs.back())) { 530 unsigned num_ls_units = count_units_r2l(ls, ls.size() - 1); 531 if (num_ls_units == 0 || num_ls_units == ls.size()) 532 return false; 533 unsigned num_rs_non_units = count_non_units_r2l(rs, rs.size() - 1); 534 if (num_rs_non_units == rs.size()) 535 return false; 536 SASSERT(num_rs_non_units > 0); 537 unsigned num_rs_units = count_units_r2l(rs, rs.size() - 1 - num_rs_non_units); 538 if (num_rs_units == 0) 539 return false; 540 set_prefix(x, ls, ls.size() - num_ls_units); 541 set_suffix(xs, ls, num_ls_units); 542 unsigned offset = rs.size() - num_rs_non_units - num_rs_units; 543 set_prefix(y1, rs, offset); 544 set_extract(ys, rs, offset, num_rs_units); 545 set_suffix(y2, rs, num_rs_non_units); 546 return true; 547 } 548 return false; 549 } 550 match_ternary_eq_rhs(expr_ref_vector const & ls,expr_ref_vector const & rs,expr_ref & x,expr_ref_vector & xs,expr_ref & y1,expr_ref_vector & ys,expr_ref & y2)551 bool eq_solver::match_ternary_eq_rhs(expr_ref_vector const& ls, expr_ref_vector const& rs, 552 expr_ref& x, expr_ref_vector& xs, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2) { 553 if (match_ternary_eq_r(ls, rs, x, xs, y1, ys, y2)) 554 return true; 555 if (match_ternary_eq_r(rs, ls, x, xs, y1, ys, y2)) 556 return true; 557 return false; 558 } 559 560 /* 561 match: abc X .. = Y def Z .. 562 where Y is a variable or concatenation of variables 563 */ 564 match_ternary_eq_l(expr_ref_vector const & ls,expr_ref_vector const & rs,expr_ref_vector & xs,expr_ref & x,expr_ref & y1,expr_ref_vector & ys,expr_ref & y2)565 bool eq_solver::match_ternary_eq_l(expr_ref_vector const& ls, expr_ref_vector const& rs, 566 expr_ref_vector& xs, expr_ref& x, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2) { 567 if (ls.size() > 1 && rs.size() > 1 && is_var(rs[0]) && is_var(rs.back())) { 568 unsigned num_ls_units = count_units_l2r(ls, 0); 569 if (num_ls_units == 0 || num_ls_units == ls.size()) 570 return false; 571 unsigned num_rs_non_units = count_non_units_l2r(rs, 0); 572 if (num_rs_non_units == rs.size() || num_rs_non_units == 0) 573 return false; 574 unsigned num_rs_units = count_units_l2r(rs, num_rs_non_units); 575 if (num_rs_units == 0) 576 return false; 577 set_prefix(xs, ls, num_ls_units); 578 set_suffix(x, ls, ls.size() - num_ls_units); 579 set_prefix(y1, rs, num_rs_non_units); 580 set_extract(ys, rs, num_rs_non_units, num_rs_units); 581 set_suffix(y2, rs, rs.size() - num_rs_non_units - num_rs_units); 582 return true; 583 } 584 return false; 585 } 586 match_ternary_eq_lhs(expr_ref_vector const & ls,expr_ref_vector const & rs,expr_ref_vector & xs,expr_ref & x,expr_ref & y1,expr_ref_vector & ys,expr_ref & y2)587 bool eq_solver::match_ternary_eq_lhs(expr_ref_vector const& ls, expr_ref_vector const& rs, 588 expr_ref_vector& xs, expr_ref& x, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2) { 589 if (match_ternary_eq_l(ls, rs, xs, x, y1, ys, y2)) 590 return true; 591 if (match_ternary_eq_l(rs, ls, xs, x, y1, ys, y2)) 592 return true; 593 return false; 594 } 595 596 all_units(expr_ref_vector const & es,unsigned start,unsigned end) const597 bool eq_solver::all_units(expr_ref_vector const& es, unsigned start, unsigned end) const { 598 for (unsigned i = start; i < end; ++i) 599 if (!seq.str.is_unit(es[i])) 600 return false; 601 return true; 602 } 603 604 /** 605 match X abc = defg Y, for abc, defg non-empty 606 */ 607 match_binary_eq(expr_ref_vector const & ls,expr_ref_vector const & rs,expr_ref & x,ptr_vector<expr> & xs,ptr_vector<expr> & ys,expr_ref & y)608 bool eq_solver::match_binary_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, 609 expr_ref& x, ptr_vector<expr>& xs, ptr_vector<expr>& ys, expr_ref& y) { 610 if (ls.size() > 1 && is_var(ls[0]) && 611 rs.size() > 1 && is_var(rs.back()) && 612 all_units(ls, 1, ls.size()) && 613 all_units(rs, 0, rs.size() - 1)) { 614 x = ls[0]; 615 y = rs.back(); 616 set_suffix(xs, ls, ls.size() - 1); 617 set_prefix(ys, rs, rs.size() - 1); 618 return true; 619 } 620 return false; 621 } 622 match_binary_eq(eqr const & e,expr_ref & x,ptr_vector<expr> & xs,ptr_vector<expr> & ys,expr_ref & y)623 bool eq_solver::match_binary_eq(eqr const& e, expr_ref& x, ptr_vector<expr>& xs, ptr_vector<expr>& ys, expr_ref& y) { 624 if (match_binary_eq(e.ls, e.rs, x, xs, ys, y) && x == y) 625 return true; 626 if (match_binary_eq(e.rs, e.ls, x, xs, ys, y) && x == y) 627 return true; 628 return false; 629 } 630 631 /** 632 * match: X abc Y..Y' = Z def T..T', where X,Z are variables or concatenation of variables 633 */ 634 match_quat_eq(expr_ref_vector const & ls,expr_ref_vector const & rs,expr_ref & x1,expr_ref_vector & xs,expr_ref & x2,expr_ref & y1,expr_ref_vector & ys,expr_ref & y2)635 bool eq_solver::match_quat_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, 636 expr_ref& x1, expr_ref_vector& xs, expr_ref& x2, 637 expr_ref& y1, expr_ref_vector& ys, expr_ref& y2) { 638 if (ls.size() > 1 && is_var(ls[0]) && is_var(ls.back()) && 639 rs.size() > 1 && is_var(rs[0]) && is_var(rs.back())) { 640 unsigned ls_non_unit = count_non_units_l2r(ls, 0); 641 unsigned rs_non_unit = count_non_units_l2r(rs, 0); 642 if (ls_non_unit == ls.size()) 643 return false; 644 if (rs_non_unit == rs.size()) 645 return false; 646 unsigned ls_unit = count_units_l2r(ls, ls_non_unit); 647 unsigned rs_unit = count_units_l2r(rs, rs_non_unit); 648 if (ls_unit == 0) 649 return false; 650 if (rs_unit == 0) 651 return false; 652 set_prefix(x1, ls, ls_non_unit); 653 set_extract(xs, ls, ls_non_unit, ls_unit); 654 set_suffix(x2, ls, ls.size() - ls_non_unit - ls_unit); 655 set_prefix(y1, rs, rs_non_unit); 656 set_extract(ys, rs, rs_non_unit, rs_unit); 657 set_suffix(y2, rs, rs.size() - rs_non_unit - rs_unit); 658 return true; 659 } 660 return false; 661 } 662 663 664 // exists x, y, rs' != empty s.t. (ls = x ++ rs ++ y) || (ls = rs' ++ y && rs = x ++ rs') can_align_from_lhs_aux(expr_ref_vector const & ls,expr_ref_vector const & rs)665 bool eq_solver::can_align_from_lhs_aux(expr_ref_vector const& ls, expr_ref_vector const& rs) { 666 SASSERT(!ls.empty() && !rs.empty()); 667 668 for (unsigned i = 0; i < ls.size(); ++i) { 669 if (m.are_distinct(ls[i], rs.back())) 670 continue; 671 672 if (i == 0) 673 return true; 674 // ls = rs' ++ y && rs = x ++ rs', diff = |x| 675 bool same = true; 676 if (rs.size() > i) { 677 unsigned diff = rs.size() - (i + 1); 678 for (unsigned j = 0; same && j < i; ++j) 679 same = !m.are_distinct(ls[j], rs[diff + j]); 680 } 681 // ls = x ++ rs ++ y, diff = |x| 682 else { 683 unsigned diff = (i + 1) - rs.size(); 684 for (unsigned j = 0; same && j + 1 < rs.size(); ++j) 685 same = !m.are_distinct(ls[diff + j], rs[j]); 686 } 687 if (same) 688 return true; 689 } 690 return false; 691 } 692 693 // exists x, y, rs' != empty s.t. (ls = x ++ rs ++ y) || (ls = x ++ rs' && rs = rs' ++ y) can_align_from_rhs_aux(expr_ref_vector const & ls,expr_ref_vector const & rs)694 bool eq_solver::can_align_from_rhs_aux(expr_ref_vector const& ls, expr_ref_vector const& rs) { 695 SASSERT(!ls.empty() && !rs.empty()); 696 697 for (unsigned i = 0; i < ls.size(); ++i) { 698 unsigned diff = ls.size() - 1 - i; 699 if (m.are_distinct(ls[diff], rs[0])) 700 continue; 701 702 if (i == 0) 703 return true; 704 705 bool same = true; 706 // ls = x ++ rs' && rs = rs' ++ y, diff = |x| 707 if (rs.size() > i) { 708 for (unsigned j = 1; same && j <= i; ++j) { 709 same = !m.are_distinct(ls[diff + j], rs[j]); 710 } 711 } 712 // ls = x ++ rs ++ y, diff = |x| 713 else { 714 for (unsigned j = 1; same && j < rs.size(); ++j) 715 same = !m.are_distinct(ls[diff + j], rs[j]); 716 } 717 if (same) 718 return true; 719 } 720 721 return false; 722 } 723 724 725 726 727 }; 728 729