1 /*++ 2 Copyright (c) 2011 Microsoft Corporation 3 4 Module Name: 5 6 seq_axioms.cpp 7 8 Abstract: 9 10 Axiomatize string operations that can be reduced to 11 more basic operations. These axioms are kept outside 12 of a particular solver: they are mainly solver independent. 13 14 Author: 15 16 Nikolaj Bjorner (nbjorner) 2020-4-16 17 18 Revision History: 19 20 --*/ 21 22 #include "ast/ast_pp.h" 23 #include "ast/ast_ll_pp.h" 24 #include "ast/rewriter/seq_axioms.h" 25 26 namespace seq { 27 axioms(th_rewriter & r)28 axioms::axioms(th_rewriter& r): 29 m(r.m()), 30 m_rewrite(r), 31 a(m), 32 seq(m), 33 m_sk(m, r), 34 m_clause(m), 35 m_trail(m) 36 {} 37 mk_sub(expr * x,expr * y)38 expr_ref axioms::mk_sub(expr* x, expr* y) { 39 expr_ref result(a.mk_sub(x, y), m); 40 m_rewrite(result); 41 return result; 42 } 43 mk_ge_e(expr * x,expr * y)44 expr_ref axioms::mk_ge_e(expr* x, expr* y) { 45 expr_ref ge(a.mk_ge(x, y), m); 46 m_rewrite(ge); 47 return ge; 48 } 49 mk_le_e(expr * x,expr * y)50 expr_ref axioms::mk_le_e(expr* x, expr* y) { 51 expr_ref le(a.mk_le(x, y), m); 52 m_rewrite(le); 53 return le; 54 } 55 mk_seq_eq(expr * a,expr * b)56 expr_ref axioms::mk_seq_eq(expr* a, expr* b) { 57 SASSERT(seq.is_seq(a) && seq.is_seq(b)); 58 expr_ref result(m_sk.mk_eq(a, b), m); 59 m_set_phase(result); 60 return result; 61 } 62 63 /** 64 * Create a special equality predicate for sequences. 65 * The sequence solver ignores the predicate when it 66 * is assigned to false. If the predicate is assigned 67 * to true it enforces the equality. 68 * 69 * This is intended to save the solver from satisfying disequality 70 * constraints that are not relevant. The use of this predicate 71 * needs some care because it can lead to incompleteness. 72 * The clauses where this predicate are used have to ensure 73 * that whenever it is assigned false, the clause 74 * is satisfied by a solution where the equality is either false 75 * or irrelevant. 76 */ mk_eq_empty(expr * e)77 expr_ref axioms::mk_eq_empty(expr* e) { 78 return mk_seq_eq(seq.str.mk_empty(e->get_sort()), e); 79 } 80 purify(expr * e)81 expr_ref axioms::purify(expr* e) { 82 if (!e) 83 return expr_ref(m); 84 if (get_depth(e) == 1) 85 return expr_ref(e, m); 86 if (m.is_value(e)) 87 return expr_ref(e, m); 88 89 expr_ref p(e, m); 90 m_rewrite(p); 91 if (p == e) 92 return p; 93 94 expr* r = nullptr; 95 if (m_purified.find(e, r)) 96 p = r; 97 else { 98 gc_purify(); 99 p = expr_ref(m.mk_fresh_const("seq.purify", e->get_sort()), m); 100 m_purified.insert(e, p); 101 m_trail.push_back(e); 102 m_trail.push_back(p); 103 } 104 add_clause(mk_eq(p, e)); 105 return expr_ref(p, m); 106 } 107 gc_purify()108 void axioms::gc_purify() { 109 if (m_trail.size() != 4000) 110 return; 111 unsigned new_size = 2000; 112 expr_ref_vector new_trail(m, new_size, m_trail.data() + new_size); 113 m_purified.reset(); 114 for (unsigned i = 0; i < new_size; i += 2) 115 m_purified.insert(new_trail.get(i), new_trail.get(i + 1)); 116 m_trail.reset(); 117 m_trail.append(new_trail); 118 } 119 mk_len(expr * s)120 expr_ref axioms::mk_len(expr* s) { 121 expr_ref result(seq.str.mk_length(s), m); 122 m_rewrite(result); 123 return result; 124 } 125 add_clause(expr_ref const & a)126 void axioms::add_clause(expr_ref const& a) { 127 m_clause.reset(); 128 m_clause.push_back(a); 129 m_add_clause(m_clause); 130 } 131 add_clause(expr_ref const & a,expr_ref const & b)132 void axioms::add_clause(expr_ref const& a, expr_ref const& b) { 133 m_clause.reset(); 134 m_clause.push_back(a); 135 m_clause.push_back(b); 136 m_add_clause(m_clause); 137 } 138 add_clause(expr_ref const & a,expr_ref const & b,expr_ref const & c)139 void axioms::add_clause(expr_ref const& a, expr_ref const& b, expr_ref const& c) { 140 m_clause.reset(); 141 m_clause.push_back(a); 142 m_clause.push_back(b); 143 m_clause.push_back(c); 144 m_add_clause(m_clause); 145 } 146 add_clause(expr_ref const & a,expr_ref const & b,expr_ref const & c,expr_ref const & d)147 void axioms::add_clause(expr_ref const& a, expr_ref const& b, expr_ref const& c, expr_ref const & d) { 148 m_clause.reset(); 149 m_clause.push_back(a); 150 m_clause.push_back(b); 151 m_clause.push_back(c); 152 m_clause.push_back(d); 153 m_add_clause(m_clause); 154 } 155 add_clause(expr_ref const & a,expr_ref const & b,expr_ref const & c,expr_ref const & d,expr_ref const & e)156 void axioms::add_clause(expr_ref const& a, expr_ref const& b, expr_ref const& c, expr_ref const & d, expr_ref const& e) { 157 m_clause.reset(); 158 m_clause.push_back(a); 159 m_clause.push_back(b); 160 m_clause.push_back(c); 161 m_clause.push_back(d); 162 m_clause.push_back(e); 163 m_add_clause(m_clause); 164 } 165 166 /*** 167 let e = extract(s, i, l) 168 169 i is start index, l is length of substring starting at index. 170 171 i < 0 => e = "" 172 i >= |s| => e = "" 173 l <= 0 => e = "" 174 0 <= i < |s| & l > 0 => s = xey, |x| = i, |e| = min(l, |s|-i) 175 l <= 0 => e = "" 176 177 this translates to: 178 179 0 <= i <= |s| -> s = xey 180 0 <= i <= |s| -> len(x) = i 181 0 <= i <= |s| & 0 <= l <= |s| - i -> |e| = l 182 0 <= i <= |s| & |s| < l + i -> |e| = |s| - i 183 |e| = 0 <=> i < 0 | |s| <= i | l <= 0 | |s| <= 0 184 185 It follows that: 186 |e| = min(l, |s| - i) for 0 <= i < |s| and 0 < |l| 187 188 */ 189 extract_axiom(expr * e)190 void axioms::extract_axiom(expr* e) { 191 TRACE("seq", tout << mk_pp(e, m) << "\n";); 192 expr* _s = nullptr, *_i = nullptr, *_l = nullptr; 193 VERIFY(seq.str.is_extract(e, _s, _i, _l)); 194 auto s = purify(_s); 195 auto i = purify(_i); 196 auto l = purify(_l); 197 if (small_segment_axiom(e, _s, _i, _l)) 198 return; 199 200 if (is_tail(s, _i, _l)) { 201 tail_axiom(e, s); 202 return; 203 } 204 if (is_drop_last(s, _i, _l)) { 205 drop_last_axiom(e, s); 206 return; 207 } 208 if (is_extract_prefix(s, _i, _l)) { 209 extract_prefix_axiom(e, s, l); 210 return; 211 } 212 if (is_extract_suffix(s, _i, _l)) { 213 extract_suffix_axiom(e, s, i); 214 return; 215 } 216 TRACE("seq", tout << s << " " << i << " " << l << "\n";); 217 expr_ref x = m_sk.mk_pre(s, i); 218 expr_ref ls = mk_len(_s); 219 expr_ref lx = mk_len(x); 220 expr_ref le = mk_len(e); 221 expr_ref ls_minus_i_l(mk_sub(mk_sub(ls, _i), _l), m); 222 expr_ref y = m_sk.mk_post(s, a.mk_add(i, l)); 223 expr_ref xe = mk_concat(x, e); 224 expr_ref xey = mk_concat(x, e, y); 225 expr_ref zero(a.mk_int(0), m); 226 227 expr_ref i_ge_0 = mk_ge(_i, 0); 228 expr_ref i_le_ls = mk_le(mk_sub(_i, ls), 0); 229 expr_ref ls_le_i = mk_le(mk_sub(ls, _i), 0); 230 expr_ref ls_ge_li = mk_ge(ls_minus_i_l, 0); 231 expr_ref l_ge_0 = mk_ge(l, 0); 232 expr_ref l_le_0 = mk_le(l, 0); 233 expr_ref ls_le_0 = mk_le(ls, 0); 234 expr_ref le_is_0 = mk_eq(le, zero); 235 236 237 // 0 <= i & i <= |s| & 0 <= l => xey = s 238 // 0 <= i & i <= |s| => |x| = i 239 // 0 <= i & i <= |s| & l >= 0 & |s| >= l + i => |e| = l 240 // 0 <= i & i <= |s| & |s| < l + i => |e| = |s| - i 241 // i < 0 => |e| = 0 242 // |s| <= i => |e| = 0 243 // |s| <= 0 => |e| = 0 244 // l <= 0 => |e| = 0 245 // |e| = 0 & i >= 0 & |s| > i & |s| > 0 => l <= 0 246 add_clause(~i_ge_0, ~i_le_ls, ~l_ge_0, mk_seq_eq(xey, s)); 247 add_clause(~i_ge_0, ~i_le_ls, mk_eq(lx, i)); 248 add_clause(~i_ge_0, ~i_le_ls, ~l_ge_0, ~ls_ge_li, mk_eq(le, l)); 249 add_clause(~i_ge_0, ~i_le_ls, ~l_ge_0, ls_ge_li, mk_eq(le, mk_sub(ls, i))); 250 add_clause(i_ge_0, le_is_0); 251 add_clause(~ls_le_i, le_is_0); 252 add_clause(~ls_le_0, le_is_0); 253 add_clause(~l_le_0, le_is_0); 254 add_clause(~le_is_0, ~i_ge_0, ls_le_i, ls_le_0, l_le_0); 255 } 256 tail_axiom(expr * e,expr * s)257 void axioms::tail_axiom(expr* e, expr* s) { 258 expr_ref head(m), tail(m); 259 m_sk.decompose(s, head, tail); 260 TRACE("seq", tout << "tail " << mk_bounded_pp(e, m, 2) << " " << mk_bounded_pp(s, m, 2) << "\n";); 261 expr_ref emp = mk_eq_empty(s); 262 add_clause(emp, mk_seq_eq(s, mk_concat(head, e))); 263 add_clause(~emp, mk_eq_empty(e)); 264 } 265 drop_last_axiom(expr * e,expr * s)266 void axioms::drop_last_axiom(expr* e, expr* s) { 267 TRACE("seq", tout << "drop last " << mk_bounded_pp(e, m, 2) << " " << mk_bounded_pp(s, m, 2) << "\n";); 268 expr_ref emp = mk_eq_empty(s); 269 add_clause(emp, mk_seq_eq(s, mk_concat(e, seq.str.mk_unit(m_sk.mk_last(s))))); 270 add_clause(~emp, mk_eq_empty(e)); 271 } 272 is_drop_last(expr * s,expr * i,expr * l)273 bool axioms::is_drop_last(expr* s, expr* i, expr* l) { 274 rational i1; 275 if (!a.is_numeral(i, i1) || !i1.is_zero()) { 276 return false; 277 } 278 expr_ref l2(m), l1(l, m); 279 l2 = mk_sub(mk_len(s), a.mk_int(1)); 280 m_rewrite(l1); 281 m_rewrite(l2); 282 return l1 == l2; 283 } 284 small_segment_axiom(expr * s,expr * e,expr * i,expr * l)285 bool axioms::small_segment_axiom(expr* s, expr* e, expr* i, expr* l) { 286 rational ln; 287 if (a.is_numeral(i, ln) && ln >= 0 && a.is_numeral(l, ln) && ln <= 5) { 288 expr_ref_vector es(m); 289 for (unsigned j = 0; j < ln; ++j) 290 es.push_back(seq.str.mk_at(e, a.mk_add(i, a.mk_int(j)))); 291 expr_ref r(seq.str.mk_concat(es, e->get_sort()), m); 292 add_clause(mk_seq_eq(r, s)); 293 return true; 294 } 295 return false; 296 } 297 298 is_tail(expr * s,expr * i,expr * l)299 bool axioms::is_tail(expr* s, expr* i, expr* l) { 300 rational i1; 301 if (!a.is_numeral(i, i1) || !i1.is_one()) 302 return false; 303 expr_ref l2(m), l1(l, m); 304 l2 = mk_sub(mk_len(s), a.mk_int(1)); 305 m_rewrite(l1); 306 m_rewrite(l2); 307 return l1 == l2; 308 } 309 is_extract_prefix(expr * s,expr * i,expr * l)310 bool axioms::is_extract_prefix(expr* s, expr* i, expr* l) { 311 rational i1; 312 return a.is_numeral(i, i1) && i1.is_zero(); 313 } 314 is_extract_suffix(expr * s,expr * i,expr * l)315 bool axioms::is_extract_suffix(expr* s, expr* i, expr* l) { 316 expr_ref len(a.mk_add(l, i), m); 317 m_rewrite(len); 318 return seq.str.is_length(len, l) && l == s; 319 } 320 321 322 /* 323 s = ey 324 l <= 0 => e = empty 325 0 <= l <= len(s) => len(e) = l 326 len(s) < l => e = s 327 */ extract_prefix_axiom(expr * e,expr * s,expr * l)328 void axioms::extract_prefix_axiom(expr* e, expr* s, expr* l) { 329 330 TRACE("seq", tout << "prefix " << mk_bounded_pp(e, m, 2) << " " << mk_bounded_pp(s, m, 2) << " " << mk_bounded_pp(l, m, 2) << "\n";); 331 expr_ref le = mk_len(e); 332 expr_ref ls = mk_len(s); 333 expr_ref ls_minus_l(mk_sub(ls, l), m); 334 expr_ref y = m_sk.mk_post(s, l); 335 expr_ref ey = mk_concat(e, y); 336 expr_ref l_le_s = mk_le(mk_sub(l, ls), 0); 337 add_clause(mk_seq_eq(s, ey)); 338 add_clause(~mk_le(l, 0), mk_eq_empty(e)); 339 add_clause(~mk_ge(l, 0), ~l_le_s, mk_eq(le, l)); 340 add_clause(l_le_s, mk_eq(e, s)); 341 } 342 343 /* 344 s = xe 345 0 <= i <= len(s) => i = len(x) 346 i < 0 => e = empty 347 i > len(s) => e = empty 348 */ extract_suffix_axiom(expr * e,expr * s,expr * i)349 void axioms::extract_suffix_axiom(expr* e, expr* s, expr* i) { 350 TRACE("seq", tout << "suffix " << mk_bounded_pp(e, m, 2) << " " << mk_bounded_pp(s, m, 2) << "\n";); 351 expr_ref x = m_sk.mk_pre(s, i); 352 expr_ref lx = mk_len(x); 353 expr_ref ls = mk_len(s); 354 expr_ref xe = mk_concat(x, e); 355 expr_ref emp = mk_eq_empty(e); 356 expr_ref i_ge_0 = mk_ge(i, 0); 357 expr_ref i_le_s = mk_le(mk_sub(i, ls), 0); 358 add_clause(mk_eq(s, xe)); 359 add_clause(~i_ge_0, ~i_le_s, mk_eq(i, lx)); 360 add_clause(i_ge_0, emp); 361 add_clause(i_le_s, emp); 362 } 363 364 365 /* 366 encode that s is not contained in of xs1 367 where s1 is all of s, except the last element. 368 369 s = "" or s = s1*(unit c) 370 s = "" or !contains(x*s1, s) 371 */ tightest_prefix(expr * s,expr * x)372 void axioms::tightest_prefix(expr* s, expr* x) { 373 expr_ref s_eq_emp = mk_eq_empty(s); 374 if (seq.str.max_length(s) <= 1) { 375 add_clause(s_eq_emp, ~expr_ref(seq.str.mk_contains(x, s), m)); 376 return; 377 } 378 expr_ref s1 = m_sk.mk_first(s); 379 expr_ref c = m_sk.mk_last(s); 380 expr_ref s1c = mk_concat(s1, seq.str.mk_unit(c)); 381 add_clause(s_eq_emp, mk_seq_eq(s, s1c)); 382 add_clause(s_eq_emp, ~expr_ref(seq.str.mk_contains(mk_concat(x, s1), s), m)); 383 } 384 385 /* 386 [[str.indexof]](w, w2, i) is the smallest n such that for some some w1, w3 387 - w = w1w2w3 388 - i <= n = |w1| 389 390 if [[str.contains]](w, w2) = true, |w2| > 0 and i >= 0. 391 392 [[str.indexof]](w,w2,i) = -1 otherwise. 393 394 395 let i = Index(t, s, offset): 396 // index of s in t starting at offset. 397 398 399 |t| = 0 => |s| = 0 or indexof(t,s,offset) = -1 400 |t| = 0 & |s| = 0 => indexof(t,s,offset) = 0 401 402 offset >= len(t) => |s| = 0 or i = -1 403 404 len(t) != 0 & !contains(t, s) => i = -1 405 406 407 offset = 0 & len(t) != 0 & contains(t, s) => t = xsy & i = len(x) 408 tightest_prefix(x, s) 409 410 411 0 <= offset < len(t) => xy = t & 412 len(x) = offset & 413 (-1 = indexof(y, s, 0) => -1 = i) & 414 (indexof(y, s, 0) >= 0 => indexof(t, s, 0) + offset = i) 415 416 offset < 0 => i = -1 417 418 optional lemmas: 419 (len(s) > len(t) -> i = -1) 420 (len(s) <= len(t) -> i <= len(t)-len(s)) 421 */ indexof_axiom(expr * i)422 void axioms::indexof_axiom(expr* i) { 423 expr* _s = nullptr, *_t = nullptr, *_offset = nullptr; 424 rational r; 425 VERIFY(seq.str.is_index(i, _t, _s) || 426 seq.str.is_index(i, _t, _s, _offset)); 427 expr_ref minus_one(a.mk_int(-1), m); 428 expr_ref zero(a.mk_int(0), m); 429 auto offset = purify(_offset); 430 auto s = purify(_s); 431 auto t = purify(_t); 432 expr_ref xsy(m); 433 expr_ref cnt(seq.str.mk_contains(t, s), m); 434 expr_ref i_eq_m1 = mk_eq(i, minus_one); 435 expr_ref i_eq_0 = mk_eq(i, zero); 436 expr_ref s_eq_empty = mk_eq(s, seq.str.mk_empty(s->get_sort())); 437 expr_ref t_eq_empty = mk_eq_empty(t); 438 439 // |t| = 0 => |s| = 0 or indexof(t,s,offset) = -1 440 // ~contains(t,s) => indexof(t,s,offset) = -1 441 442 add_clause(cnt, i_eq_m1); 443 add_clause(~t_eq_empty, s_eq_empty, i_eq_m1); 444 445 if (!offset || (a.is_numeral(offset, r) && r.is_zero())) { 446 // |s| = 0 => indexof(t,s,0) = 0 447 add_clause(~s_eq_empty, i_eq_0); 448 #if 1 449 expr_ref x = m_sk.mk_indexof_left(t, s); 450 expr_ref y = m_sk.mk_indexof_right(t, s); 451 xsy = mk_concat(x, s, y); 452 expr_ref lenx = mk_len(x); 453 // contains(t,s) & |s| != 0 => t = xsy & indexof(t,s,0) = |x| 454 add_clause(~cnt, s_eq_empty, mk_seq_eq(t, xsy)); 455 add_clause(~cnt, s_eq_empty, mk_eq(i, lenx)); 456 add_clause(~cnt, mk_ge(i, 0)); 457 tightest_prefix(s, x); 458 #else 459 // let i := indexof(t,s,0) 460 // contains(t, s) & |s| != 0 => ~contains(substr(t,0,i+len(s)-1), s) 461 // => substr(t,0,i+len(s)) = substr(t,0,i) ++ s 462 // 463 expr_ref len_s = mk_len(s); 464 expr_ref mone(a.mk_int(-1), m); 465 add_clause(~cnt, s_eq_empty, ~mk_literal(seq.str.mk_contains(seq.str.mk_substr(t,zero,a.mk_add(i,len_s,mone)),s))); 466 add_clause(~cnt, s_eq_empty, mk_seq_eq(seq.str.mk_substr(t,zero,a.mk_add(i,len_s)), 467 seq.str.mk_concat(seq.str.mk_substr(t,zero,i), s))); 468 #endif 469 } 470 else { 471 // offset >= len(t) => |s| = 0 or indexof(t, s, offset) = -1 472 // offset > len(t) => indexof(t, s, offset) = -1 473 // offset = len(t) & |s| = 0 => indexof(t, s, offset) = offset 474 expr_ref len_t = mk_len(t); 475 expr_ref offset_ge_len = mk_ge(mk_sub(offset, len_t), 0); 476 expr_ref offset_le_len = mk_le(mk_sub(offset, len_t), 0); 477 expr_ref i_eq_offset = mk_eq(i, offset); 478 add_clause(~offset_ge_len, s_eq_empty, i_eq_m1); 479 add_clause(offset_le_len, i_eq_m1); 480 add_clause(~offset_ge_len, ~offset_le_len, ~s_eq_empty, i_eq_offset); 481 482 expr_ref x = m_sk.mk_indexof_left(t, s, offset); 483 expr_ref y = m_sk.mk_indexof_right(t, s, offset); 484 expr_ref indexof0(seq.str.mk_index(y, s, zero), m); 485 expr_ref offset_p_indexof0(a.mk_add(offset, indexof0), m); 486 expr_ref offset_ge_0 = mk_ge(offset, 0); 487 488 // 0 <= offset & offset < len(t) => t = xy 489 // 0 <= offset & offset < len(t) => len(x) = offset 490 // 0 <= offset & offset < len(t) & indexof(y,s,0) = -1 => -1 = i 491 // 0 <= offset & offset < len(t) & indexof(y,s,0) >= 0 => 492 // indexof(y,s,0) + offset = indexof(t, s, offset) 493 494 add_clause(~offset_ge_0, offset_ge_len, mk_seq_eq(t, mk_concat(x, y))); 495 add_clause(~offset_ge_0, offset_ge_len, mk_eq(mk_len(x), offset)); 496 add_clause(~offset_ge_0, offset_ge_len, 497 ~mk_eq(indexof0, minus_one), i_eq_m1); 498 add_clause(~offset_ge_0, offset_ge_len, 499 ~mk_ge(indexof0, 0), 500 mk_eq(offset_p_indexof0, i)); 501 502 // offset < 0 => -1 = i 503 add_clause(offset_ge_0, i_eq_m1); 504 } 505 } 506 507 /** 508 !contains(t, s) => i = -1 509 |t| = 0 => |s| = 0 or i = -1 510 |t| = 0 & |s| = 0 => i = 0 511 |t| != 0 & contains(t, s) => t = xsy & i = len(x) 512 |s| = 0 or s = s_head*s_tail 513 |s| = 0 or !contains(s_tail*y, s) 514 515 */ last_indexof_axiom(expr * i)516 void axioms::last_indexof_axiom(expr* i) { 517 expr* _s = nullptr, *_t = nullptr; 518 VERIFY(seq.str.is_last_index(i, _t, _s)); 519 auto t = purify(_t); 520 auto s = purify(_s); 521 expr_ref minus_one(a.mk_int(-1), m); 522 expr_ref zero(a.mk_int(0), m); 523 expr_ref x = m_sk.mk_last_indexof_left(t, s); 524 expr_ref y = m_sk.mk_last_indexof_right(t, s); 525 expr_ref s_head(m), s_tail(m); 526 m_sk.decompose(s, s_head, s_tail); 527 expr_ref cnt = expr_ref(seq.str.mk_contains(t, s), m); 528 expr_ref cnt2 = expr_ref(seq.str.mk_contains(mk_concat(s_tail, y), s), m); 529 expr_ref i_eq_m1 = mk_eq(i, minus_one); 530 expr_ref i_eq_0 = mk_eq(i, zero); 531 expr_ref s_eq_empty = mk_eq_empty(s); 532 expr_ref t_eq_empty = mk_eq_empty(t); 533 expr_ref xsy = mk_concat(x, s, y); 534 535 add_clause(cnt, i_eq_m1); 536 add_clause(~t_eq_empty, s_eq_empty, i_eq_m1); 537 add_clause(~t_eq_empty, ~s_eq_empty, i_eq_0); 538 add_clause(t_eq_empty, ~cnt, mk_seq_eq(t, xsy)); 539 add_clause(t_eq_empty, ~cnt, mk_eq(i, mk_len(x))); 540 add_clause(s_eq_empty, mk_eq(s, mk_concat(s_head, s_tail))); 541 add_clause(s_eq_empty, ~cnt2); 542 } 543 544 545 /* 546 let r = replace(u, s, t) 547 548 549 - if s is empty, the result is to prepend t to u; 550 - if s does not occur in u then the result is u. 551 552 s = "" => r = t+u 553 u = "" => s = "" or r = u 554 ~contains(u,s) => r = u 555 556 tightest_prefix(s, x) 557 contains(u, s) => r = xty & u = xsy 558 ~contains(u, s) => r = u 559 560 */ replace_axiom(expr * r)561 void axioms::replace_axiom(expr* r) { 562 expr* _u = nullptr, *_s = nullptr, *_t = nullptr; 563 VERIFY(seq.str.is_replace(r, _u, _s, _t)); 564 auto u = purify(_u); 565 auto s = purify(_s); 566 auto t = purify(_t); 567 expr_ref x = m_sk.mk_indexof_left(u, s); 568 expr_ref y = m_sk.mk_indexof_right(u, s); 569 expr_ref xty = mk_concat(x, t, y); 570 expr_ref xsy = mk_concat(x, s, y); 571 expr_ref u_emp = mk_eq_empty(u); 572 expr_ref s_emp = mk_eq_empty(s); 573 expr_ref cnt = expr_ref(seq.str.mk_contains(u, s), m); 574 add_clause(~s_emp, mk_seq_eq(r, mk_concat(t, u))); 575 add_clause(~u_emp, s_emp, mk_seq_eq(r, u)); 576 add_clause(cnt, mk_seq_eq(r, u)); 577 add_clause(~cnt, u_emp, s_emp, mk_seq_eq(u, xsy)); 578 add_clause(~cnt, u_emp, s_emp, mk_seq_eq(r, xty)); 579 tightest_prefix(s, x); 580 } 581 582 /* 583 let e = at(s, i) 584 585 0 <= i < len(s) -> s = xey & len(x) = i & len(e) = 1 586 i < 0 \/ i >= len(s) -> e = empty 587 588 */ at_axiom(expr * e)589 void axioms::at_axiom(expr* e) { 590 TRACE("seq", tout << "at-axiom: " << mk_bounded_pp(e, m) << "\n";); 591 expr* _s = nullptr, *_i = nullptr; 592 VERIFY(seq.str.is_at(e, _s, _i)); 593 auto s = purify(_s); 594 auto i = purify(_i); 595 expr_ref zero(a.mk_int(0), m); 596 expr_ref one(a.mk_int(1), m); 597 expr_ref emp(seq.str.mk_empty(e->get_sort()), m); 598 expr_ref len_s = mk_len(s); 599 expr_ref i_ge_0 = mk_ge(i, 0); 600 expr_ref i_ge_len_s = mk_ge(mk_sub(i, mk_len(s)), 0); 601 expr_ref len_e = mk_len(e); 602 603 rational iv; 604 if (a.is_numeral(i, iv) && iv.is_unsigned()) { 605 expr_ref_vector es(m); 606 expr_ref nth(m); 607 unsigned k = iv.get_unsigned(); 608 for (unsigned j = 0; j <= k; ++j) { 609 es.push_back(seq.str.mk_unit(mk_nth(s, j))); 610 } 611 nth = es.back(); 612 es.push_back(m_sk.mk_tail(s, i)); 613 add_clause(~i_ge_0, i_ge_len_s, mk_seq_eq(s, seq.str.mk_concat(es, e->get_sort()))); 614 add_clause(~i_ge_0, i_ge_len_s, mk_seq_eq(nth, e)); 615 } 616 else { 617 expr_ref x = m_sk.mk_pre(s, i); 618 expr_ref y = m_sk.mk_tail(s, i); 619 expr_ref xey = mk_concat(x, e, y); 620 expr_ref len_x = mk_len(x); 621 add_clause(~i_ge_0, i_ge_len_s, mk_seq_eq(s, xey)); 622 add_clause(~i_ge_0, i_ge_len_s, mk_eq(i, len_x)); 623 } 624 625 add_clause(i_ge_0, mk_eq(e, emp)); 626 add_clause(~i_ge_len_s, mk_eq(e, emp)); 627 add_clause(~i_ge_0, i_ge_len_s, mk_eq(one, len_e)); 628 add_clause(mk_le(len_e, 1)); 629 } 630 631 632 /** 633 i >= 0 i < len(s) => unit(nth_i(s, i)) = at(s, i) 634 nth_i(unit(nth_i(s, i)), 0) = nth_i(s, i) 635 */ 636 nth_axiom(expr * e)637 void axioms::nth_axiom(expr* e) { 638 expr* s = nullptr, *i = nullptr; 639 rational n; 640 zstring str; 641 VERIFY(seq.str.is_nth_i(e, s, i)); 642 if (seq.str.is_string(s, str) && a.is_numeral(i, n) && 643 n.is_unsigned() && n.get_unsigned() < str.length()) { 644 app_ref ch(seq.str.mk_char(str[n.get_unsigned()]), m); 645 add_clause(mk_eq(ch, e)); 646 } 647 else { 648 expr_ref zero(a.mk_int(0), m); 649 expr_ref i_ge_0 = mk_ge(i, 0); 650 expr_ref i_ge_len_s = mk_ge(mk_sub(i, mk_len(s)), 0); 651 // at(s,i) = [nth(s,i)] 652 expr_ref rhs(s, m); 653 expr_ref lhs(seq.str.mk_unit(e), m); 654 if (!seq.str.is_at(s) || zero != i) rhs = seq.str.mk_at(s, i); 655 m_rewrite(rhs); 656 add_clause(~i_ge_0, i_ge_len_s, mk_eq(lhs, rhs)); 657 } 658 } 659 660 itos_axiom(expr * e)661 void axioms::itos_axiom(expr* e) { 662 expr* n = nullptr; 663 TRACE("seq", tout << mk_pp(e, m) << "\n";); 664 VERIFY(seq.str.is_itos(e, n)); 665 666 // itos(n) = "" <=> n < 0 667 expr_ref zero(a.mk_int(0), m); 668 expr_ref eq1 = expr_ref(seq.str.mk_is_empty(e), m); 669 expr_ref ge0 = mk_ge(n, 0); 670 // n >= 0 => itos(n) != "" 671 // itos(n) = "" or n >= 0 672 add_clause(~eq1, ~ge0); 673 add_clause(eq1, ge0); 674 add_clause(mk_ge(mk_len(e), 0)); 675 676 // n >= 0 => stoi(itos(n)) = n 677 app_ref stoi(seq.str.mk_stoi(e), m); 678 expr_ref eq = mk_eq(stoi, n); 679 add_clause(~ge0, eq); 680 m_set_phase(eq); 681 682 // itos(n) does not start with "0" when n > 0 683 // n = 0 or at(itos(n),0) != "0" 684 // alternative: n >= 0 => itos(stoi(itos(n))) = itos(n) 685 expr_ref zs(seq.str.mk_string("0"), m); 686 m_rewrite(zs); 687 expr_ref eq0 = mk_eq(n, zero); 688 expr_ref at0 = mk_eq(seq.str.mk_at(e, zero), zs); 689 add_clause(eq0, ~at0); 690 add_clause(~eq0, mk_eq(e, zs)); 691 } 692 693 /** 694 stoi(s) >= -1 695 stoi("") = -1 696 stoi(s) >= 0 => is_digit(nth(s,0)) 697 stoi(s) >= 0 => len(s) >= 1 698 */ stoi_axiom(expr * e)699 void axioms::stoi_axiom(expr* e) { 700 TRACE("seq", tout << mk_pp(e, m) << "\n";); 701 expr_ref ge0 = mk_ge(e, 0); 702 expr* s = nullptr; 703 VERIFY (seq.str.is_stoi(e, s)); 704 add_clause(mk_ge(e, -1)); // stoi(s) >= -1 705 add_clause(mk_eq(seq.str.mk_stoi(seq.str.mk_empty(s->get_sort())), a.mk_int(-1))); 706 // add_clause(~mk_eq_empty(s), mk_eq(e, a.mk_int(-1))); // s = "" => stoi(s) = -1 707 add_clause(~ge0, is_digit(mk_nth(s, 0))); // stoi(s) >= 0 => is_digit(nth(s,0)) 708 add_clause(~ge0, mk_ge(mk_len(s), 1)); // stoi(s) >= 0 => len(s) >= 1 709 } 710 711 712 /** 713 714 len(s) <= k => stoi(s) = stoi(s, k) 715 len(s) > 0, is_digit(nth(s,0)) => stoi(s, 0) = digit(nth_i(s, 0)) 716 len(s) > 0, ~is_digit(nth(s,0)) => stoi(s, 0) = -1 717 718 0 < i, len(s) <= i => stoi(s, i) = stoi(s, i - 1) 719 0 < i, len(s) > i, stoi(s, i - 1) >= 0, is_digit(nth(s, i - 1)) => stoi(s, i) = 10*stoi(s, i - 1) + digit(nth_i(s, i - 1)) 720 0 < i, len(s) > i, stoi(s, i - 1) < 0 => stoi(s, i) = -1 721 0 < i, len(s) > i, ~is_digit(nth(s, i - 1)) => stoi(s, i) = -1 722 723 724 725 Define auxiliary function with the property: 726 for 0 <= i < k 727 stoi(s, i) := stoi(extract(s, 0, i+1)) 728 729 for 0 < i < k: 730 len(s) > i => stoi(s, i) := stoi(extract(s, 0, i))*10 + stoi(extract(s, i, 1)) 731 len(s) <= i => stoi(s, i) := stoi(extract(s, 0, i-1), i-1) 732 733 for i <= i < k: 734 stoi(s) > = 0, len(s) > i => is_digit(nth(s, i)) 735 736 */ stoi_axiom(expr * e,unsigned k)737 void axioms::stoi_axiom(expr* e, unsigned k) { 738 SASSERT(k > 0); 739 expr* _s = nullptr; 740 VERIFY (seq.str.is_stoi(e, _s)); 741 expr_ref s(_s, m); 742 m_rewrite(s); 743 auto stoi2 = [&](unsigned j) { return m_sk.mk("seq.stoi", s, a.mk_int(j), a.mk_int()); }; 744 auto digit = [&](unsigned j) { return mk_digit2int(mk_nth(s, j)); }; 745 auto is_digit_ = [&](unsigned j) { return is_digit(mk_nth(s, j)); }; 746 expr_ref len = mk_len(s); 747 expr_ref ge0 = mk_ge(e, 0); 748 expr_ref lek = mk_le(len, k); 749 add_clause(~lek, mk_eq(e, stoi2(k-1))); // len(s) <= k => stoi(s) = stoi(s, k-1) 750 add_clause(mk_le(len, 0), ~is_digit_(0), mk_eq(stoi2(0), digit(0))); // len(s) > 0, is_digit(nth(s, 0)) => stoi(s,0) = digit(s,0) 751 add_clause(mk_le(len, 0), is_digit_(0), mk_eq(stoi2(0), a.mk_int(-1))); // len(s) > 0, ~is_digit(nth(s, 0)) => stoi(s,0) = -1 752 for (unsigned i = 1; i < k; ++i) { 753 754 // len(s) <= i => stoi(s, i) = stoi(s, i - 1) 755 756 add_clause(~mk_le(len, i), mk_eq(stoi2(i), stoi2(i-1))); 757 758 // len(s) > i, stoi(s, i - 1) >= 0, is_digit(nth(s, i)) => stoi(s, i) = 10*stoi(s, i - 1) + digit(i) 759 // len(s) > i, stoi(s, i - 1) < 0 => stoi(s, i) = -1 760 // len(s) > i, ~is_digit(nth(s, i)) => stoi(s, i) = -1 761 762 add_clause(mk_le(len, i), ~mk_ge(stoi2(i-1), 0), ~is_digit_(i), mk_eq(stoi2(i), a.mk_add(a.mk_mul(a.mk_int(10), stoi2(i-1)), digit(i)))); 763 add_clause(mk_le(len, i), is_digit_(i), mk_eq(stoi2(i), a.mk_int(-1))); 764 add_clause(mk_le(len, i), mk_ge(stoi2(i-1), 0), mk_eq(stoi2(i), a.mk_int(-1))); 765 766 // stoi(s) >= 0, i < len(s) => is_digit(nth(s, i)) 767 768 add_clause(~ge0, mk_le(len, i), is_digit_(i)); 769 } 770 } 771 ubv2s_axiom(expr * b,unsigned k)772 void axioms::ubv2s_axiom(expr* b, unsigned k) { 773 expr_ref ge10k(m), ge10k1(m), eq(m); 774 bv_util bv(m); 775 sort* bv_sort = b->get_sort(); 776 rational pow(1); 777 for (unsigned i = 0; i < k; ++i) 778 pow *= 10; 779 ge10k = bv.mk_ule(bv.mk_numeral(pow, bv_sort), b); 780 ge10k1 = bv.mk_ule(bv.mk_numeral(pow * 10, bv_sort), b); 781 unsigned sz = bv.get_bv_size(b); 782 expr_ref_vector es(m); 783 expr_ref bb(b, m), ten(bv.mk_numeral(10, sz), m); 784 rational p(1); 785 for (unsigned i = 0; i <= k; ++i) { 786 if (p > 1) 787 bb = bv.mk_bv_udiv(b, bv.mk_numeral(p, bv_sort)); 788 es.push_back(seq.str.mk_unit(m_sk.mk_ubv2ch(bv.mk_bv_urem(bb, ten)))); 789 p *= 10; 790 } 791 es.reverse(); 792 eq = m.mk_eq(seq.str.mk_ubv2s(b), seq.str.mk_concat(es, seq.str.mk_string_sort())); 793 SASSERT(pow < rational::power_of_two(sz)); 794 if (k == 0) 795 add_clause(ge10k1, eq); 796 else if (pow * 10 >= rational::power_of_two(sz)) 797 add_clause(~ge10k, eq); 798 else 799 add_clause(~ge10k, ge10k1, eq); 800 } 801 802 /* 803 * 1 <= len(ubv2s(b)) <= k, where k is min such that 10^k > 2^sz 804 */ ubv2s_len_axiom(expr * b)805 void axioms::ubv2s_len_axiom(expr* b) { 806 bv_util bv(m); 807 sort* bv_sort = b->get_sort(); 808 unsigned sz = bv.get_bv_size(bv_sort); 809 unsigned k = 1; 810 rational pow(10); 811 while (pow <= rational::power_of_two(sz)) 812 ++k, pow *= 10; 813 expr_ref len(seq.str.mk_length(seq.str.mk_ubv2s(b)), m); 814 expr_ref ge(a.mk_ge(len, a.mk_int(1)), m); 815 expr_ref le(a.mk_le(len, a.mk_int(k)), m); 816 add_clause(le); 817 add_clause(ge); 818 } 819 820 /* 821 * len(ubv2s(b)) = k => 10^k-1 <= b < 10^{k} k > 1 822 * len(ubv2s(b)) = 1 => b < 10^{1} k = 1 823 * len(ubv2s(b)) >= k => is_digit(nth(ubv2s(b), 0)) & ... & is_digit(nth(ubv2s(b), k-1)) 824 */ ubv2s_len_axiom(expr * b,unsigned k)825 void axioms::ubv2s_len_axiom(expr* b, unsigned k) { 826 expr_ref ge10k(m), ge10k1(m), eq(m), is_digit(m); 827 expr_ref ubvs(seq.str.mk_ubv2s(b), m); 828 expr_ref len(seq.str.mk_length(ubvs), m); 829 expr_ref ge_len(a.mk_ge(len, a.mk_int(k)), m); 830 bv_util bv(m); 831 sort* bv_sort = b->get_sort(); 832 unsigned sz = bv.get_bv_size(bv_sort); 833 rational pow(1); 834 for (unsigned i = 1; i < k; ++i) 835 pow *= 10; 836 837 if (pow >= rational::power_of_two(sz)) { 838 expr_ref ge(a.mk_ge(len, a.mk_int(k)), m); 839 add_clause(~ge); 840 return; 841 } 842 843 ge10k = bv.mk_ule(bv.mk_numeral(pow, bv_sort), b); 844 ge10k1 = bv.mk_ule(bv.mk_numeral(pow * 10, bv_sort), b); 845 eq = m.mk_eq(len, a.mk_int(k)); 846 847 if (pow * 10 < rational::power_of_two(sz)) 848 add_clause(~eq, ~ge10k1); 849 if (k > 1) 850 add_clause(~eq, ge10k); 851 852 for (unsigned i = 0; i < k; ++i) { 853 expr* ch = seq.str.mk_nth_c(ubvs, i); 854 is_digit = seq.mk_char_is_digit(ch); 855 add_clause(~ge_len, is_digit); 856 } 857 } 858 ubv2ch_axiom(sort * bv_sort)859 void axioms::ubv2ch_axiom(sort* bv_sort) { 860 bv_util bv(m); 861 expr_ref eq(m); 862 unsigned sz = bv.get_bv_size(bv_sort); 863 for (unsigned i = 0; i < 10; ++i) { 864 eq = m.mk_eq(m_sk.mk_ubv2ch(bv.mk_numeral(i, sz)), seq.mk_char('0' + i)); 865 add_clause(eq); 866 } 867 } 868 869 /** 870 Let s := itos(e) 871 872 Relate values of e with len(s) where len(s) is bounded by k. 873 874 |s| = 0 => e < 0 875 876 |s| <= 1 => e < 10 877 |s| <= 2 => e < 100 878 |s| <= 3 => e < 1000 879 880 |s| >= 1 => e >= 0 881 |s| >= 2 => e >= 10 882 |s| >= 3 => e >= 100 883 884 There are no constraints to ensure that the string itos(e) 885 contains the valid digits corresponding to e >= 0. 886 The validity of itos(e) is ensured by the following property: 887 e is either of the form stoi(s) for some s, or there is a term 888 stoi(itos(e)) and axiom e >= 0 => stoi(itos(e)) = e. 889 Then the axioms for stoi(itos(e)) ensure that the characters of 890 itos(e) are valid digits and the axiom stoi(itos(e)) = e ensures 891 these digits encode e. 892 The option of constraining itos(e) digits directly does not 893 seem appealing becaues it requires an order of quadratic number 894 of constraints for all possible lengths of itos(e) (e.g, log_10(e)). 895 896 */ 897 itos_axiom(expr * s,unsigned k)898 void axioms::itos_axiom(expr* s, unsigned k) { 899 expr* e = nullptr; 900 VERIFY(seq.str.is_itos(s, e)); 901 expr_ref len = mk_len(s); 902 add_clause(mk_ge(e, 10), mk_le(len, 1)); 903 add_clause(mk_le(e, -1), mk_ge(len, 1)); 904 rational lo(1); 905 for (unsigned i = 1; i <= k; ++i) { 906 lo *= rational(10); 907 add_clause(mk_ge(e, lo), mk_le(len, i)); 908 add_clause(mk_le(e, lo - 1), mk_ge(len, i + 1)); 909 } 910 } 911 is_digit(expr * ch)912 expr_ref axioms::is_digit(expr* ch) { 913 return expr_ref(seq.mk_char_is_digit(ch), m); 914 } 915 mk_digit2int(expr * ch)916 expr_ref axioms::mk_digit2int(expr* ch) { 917 m_ensure_digits(); 918 return expr_ref(m_sk.mk_digit2int(ch), m); 919 } 920 921 /** 922 e1 < e2 => prefix(e1, e2) or e1 = xcy 923 e1 < e2 => prefix(e1, e2) or c < d 924 e1 < e2 => prefix(e1, e2) or e2 = xdz 925 e1 < e2 => e1 != e2 926 !(e1 < e2) => prefix(e2, e1) or e2 = xdz 927 !(e1 < e2) => prefix(e2, e1) or d < c 928 !(e1 < e2) => prefix(e2, e1) or e1 = xcy 929 !(e1 = e2) or !(e1 < e2) 930 931 optional: 932 e1 < e2 or e1 = e2 or e2 < e1 933 !(e1 = e2) or !(e2 < e1) 934 !(e1 < e2) or !(e2 < e1) 935 */ lt_axiom(expr * n)936 void axioms::lt_axiom(expr* n) { 937 expr* _e1 = nullptr, *_e2 = nullptr; 938 VERIFY(seq.str.is_lt(n, _e1, _e2)); 939 auto e1 = purify(_e1); 940 auto e2 = purify(_e2); 941 sort* s = e1->get_sort(); 942 sort* char_sort = nullptr; 943 VERIFY(seq.is_seq(s, char_sort)); 944 expr_ref lt = expr_ref(n, m); 945 expr_ref x = m_sk.mk("str.<.x", e1, e2); 946 expr_ref y = m_sk.mk("str.<.y", e1, e2); 947 expr_ref z = m_sk.mk("str.<.z", e1, e2); 948 expr_ref c = m_sk.mk("str.<.c", e1, e2, char_sort); 949 expr_ref d = m_sk.mk("str.<.d", e1, e2, char_sort); 950 expr_ref xcy = mk_concat(x, seq.str.mk_unit(c), y); 951 expr_ref xdz = mk_concat(x, seq.str.mk_unit(d), z); 952 expr_ref eq = mk_eq(e1, e2); 953 expr_ref pref21 = expr_ref(seq.str.mk_prefix(e2, e1), m); 954 expr_ref pref12 = expr_ref(seq.str.mk_prefix(e1, e2), m); 955 expr_ref e1xcy = mk_eq(e1, xcy); 956 expr_ref e2xdz = mk_eq(e2, xdz); 957 expr_ref ltcd = expr_ref(seq.mk_lt(c, d), m); 958 expr_ref ltdc = expr_ref(seq.mk_lt(d, c), m); 959 add_clause(~lt, pref12, e2xdz); 960 add_clause(~lt, pref12, e1xcy); 961 add_clause(~lt, pref12, ltcd); 962 add_clause(lt, pref21, e1xcy); 963 add_clause(lt, pref21, ltdc); 964 add_clause(lt, pref21, e2xdz); 965 add_clause(~eq, ~lt); 966 } 967 968 /** 969 e1 <= e2 <=> e1 < e2 or e1 = e2 970 */ le_axiom(expr * n)971 void axioms::le_axiom(expr* n) { 972 expr* e1 = nullptr, *e2 = nullptr; 973 VERIFY(seq.str.is_le(n, e1, e2)); 974 expr_ref lt = expr_ref(seq.str.mk_lex_lt(e1, e2), m); 975 expr_ref le = expr_ref(n, m); 976 expr_ref eq = mk_eq(e1, e2); 977 add_clause(~le, lt, eq); 978 add_clause(~eq, le); 979 add_clause(~lt, le); 980 } 981 982 /** 983 is_digit(e) <=> to_code('0') <= to_code(e) <= to_code('9') 984 */ is_digit_axiom(expr * n)985 void axioms::is_digit_axiom(expr* n) { 986 expr* e = nullptr; 987 VERIFY(seq.str.is_is_digit(n, e)); 988 expr_ref is_digit = expr_ref(n, m); 989 expr_ref to_code(seq.str.mk_to_code(e), m); 990 expr_ref ge0 = mk_ge(to_code, (unsigned)'0'); 991 expr_ref le9 = mk_le(to_code, (unsigned)'9'); 992 add_clause(~is_digit, ge0); 993 add_clause(~is_digit, le9); 994 add_clause(is_digit, ~ge0, ~le9); 995 } 996 997 /** 998 len(e) = 1 => 0 <= to_code(e) <= max_code 999 len(e) = 1 => from_code(to_code(e)) = e 1000 len(e) != 1 => to_code(e) = -1 1001 */ str_to_code_axiom(expr * n)1002 void axioms::str_to_code_axiom(expr* n) { 1003 expr* e = nullptr; 1004 VERIFY(seq.str.is_to_code(n, e)); 1005 expr_ref len_is1 = mk_eq(mk_len(e), a.mk_int(1)); 1006 add_clause(~len_is1, mk_ge(n, 0)); 1007 add_clause(~len_is1, mk_le(n, seq.max_char())); 1008 add_clause(~len_is1, mk_eq(n, seq.mk_char2int(mk_nth(e, 0)))); 1009 if (!seq.str.is_from_code(e)) 1010 add_clause(~len_is1, mk_eq(e, seq.str.mk_from_code(n))); 1011 add_clause(len_is1, mk_eq(n, a.mk_int(-1))); 1012 } 1013 1014 /** 1015 0 <= e <= max_char => len(from_code(e)) = 1 1016 0 <= e <= max_char => to_code(from_code(e)) = e 1017 e < 0 or e > max_char => len(from_code(e)) = "" 1018 */ str_from_code_axiom(expr * n)1019 void axioms::str_from_code_axiom(expr* n) { 1020 expr* e = nullptr; 1021 VERIFY(seq.str.is_from_code(n, e)); 1022 expr_ref ge = mk_ge(e, 0); 1023 expr_ref le = mk_le(e, seq.max_char()); 1024 expr_ref emp = expr_ref(seq.str.mk_is_empty(n), m); 1025 add_clause(~ge, ~le, mk_eq(mk_len(n), a.mk_int(1))); 1026 if (!seq.str.is_to_code(e)) 1027 add_clause(~ge, ~le, mk_eq(seq.str.mk_to_code(n), e)); 1028 add_clause(ge, emp); 1029 add_clause(le, emp); 1030 } 1031 1032 1033 /** 1034 Unit is injective: 1035 1036 u = inv-unit(unit(u)) 1037 */ 1038 unit_axiom(expr * n)1039 void axioms::unit_axiom(expr* n) { 1040 expr* u = nullptr; 1041 VERIFY(seq.str.is_unit(n, u)); 1042 add_clause(mk_eq(u, m_sk.mk_unit_inv(n))); 1043 } 1044 1045 /** 1046 suffix(s, t): 1047 - the sequence s is a suffix of t. 1048 1049 Positive case is handled by the solver when the atom is asserted 1050 suffix(s, t) => t = seq.suffix_inv(s, t) + s 1051 1052 Negative case is handled by axioms when the negation of the atom is asserted 1053 ~suffix(s, t) => len(s) > len(t) or s = y(s, t) + unit(c(s, t)) + x(s, t) 1054 ~suffix(s, t) => len(s) > len(t) or t = z(s, t) + unit(d(s, t)) + x(s, t) 1055 ~suffix(s, t) => len(s) > len(t) or c(s,t) != d(s,t) 1056 1057 Symmetric axioms are provided for prefix 1058 1059 */ 1060 suffix_axiom(expr * e)1061 void axioms::suffix_axiom(expr* e) { 1062 expr* _s = nullptr, *_t = nullptr; 1063 VERIFY(seq.str.is_suffix(e, _s, _t)); 1064 auto s = purify(_s); 1065 auto t = purify(_t); 1066 expr_ref lit = expr_ref(e, m); 1067 expr_ref s_gt_t = mk_ge(mk_sub(mk_len(s), mk_len(t)), 1); 1068 #if 0 1069 expr_ref x = m_sk.mk_pre(t, mk_sub(mk_len(t), mk_len(s))); 1070 expr_ref y = m_sk.mk_tail(t, mk_sub(mk_len(s), a.mk_int(1))); 1071 add_clause(lit, s_gt_t, mk_seq_eq(t, mk_concat(x, y))); 1072 add_clause(lit, s_gt_t, mk_eq(mk_len(y), mk_len(s))); 1073 add_clause(lit, s_gt_t, ~mk_eq(y, s)); 1074 #else 1075 sort* char_sort = nullptr; 1076 VERIFY(seq.is_seq(s->get_sort(), char_sort)); 1077 expr_ref x = m_sk.mk("seq.suffix.x", s, t); 1078 expr_ref y = m_sk.mk("seq.suffix.y", s, t); 1079 expr_ref z = m_sk.mk("seq.suffix.z", s, t); 1080 expr_ref c = m_sk.mk("seq.suffix.c", s, t, char_sort); 1081 expr_ref d = m_sk.mk("seq.suffix.d", s, t, char_sort); 1082 add_clause(lit, s_gt_t, mk_seq_eq(s, mk_concat(y, seq.str.mk_unit(c), x))); 1083 add_clause(lit, s_gt_t, mk_seq_eq(t, mk_concat(z, seq.str.mk_unit(d), x))); 1084 add_clause(lit, s_gt_t, ~mk_eq(c, d)); 1085 #endif 1086 } 1087 prefix_axiom(expr * e)1088 void axioms::prefix_axiom(expr* e) { 1089 expr* _s = nullptr, *_t = nullptr; 1090 VERIFY(seq.str.is_prefix(e, _s, _t)); 1091 auto s = purify(_s); 1092 auto t = purify(_t); 1093 expr_ref lit = expr_ref(e, m); 1094 expr_ref s_gt_t = mk_ge(mk_sub(mk_len(s), mk_len(t)), 1); 1095 #if 0 1096 expr_ref x = m_sk.mk_pre(t, mk_len(s)); 1097 expr_ref y = m_sk.mk_tail(t, mk_sub(mk_sub(mk_len(t), mk_len(s)), a.mk_int(1))); 1098 add_clause(lit, s_gt_t, mk_seq_eq(t, mk_concat(x, y))); 1099 add_clause(lit, s_gt_t, mk_eq(mk_len(x), mk_len(s))); 1100 add_clause(lit, s_gt_t, ~mk_eq(x, s)); 1101 1102 #else 1103 sort* char_sort = nullptr; 1104 VERIFY(seq.is_seq(s->get_sort(), char_sort)); 1105 expr_ref x = m_sk.mk("seq.prefix.x", s, t); 1106 expr_ref y = m_sk.mk("seq.prefix.y", s, t); 1107 expr_ref z = m_sk.mk("seq.prefix.z", s, t); 1108 expr_ref c = m_sk.mk("seq.prefix.c", s, t, char_sort); 1109 expr_ref d = m_sk.mk("seq.prefix.d", s, t, char_sort); 1110 add_clause(lit, s_gt_t, mk_seq_eq(s, mk_concat(x, seq.str.mk_unit(c), y))); 1111 add_clause(lit, s_gt_t, mk_seq_eq(t, mk_concat(x, seq.str.mk_unit(d), z))); 1112 add_clause(lit, s_gt_t, ~mk_eq(c, d)); 1113 #endif 1114 } 1115 1116 /*** 1117 let n = len(x) 1118 - len(a ++ b) = len(a) + len(b) if x = a ++ b 1119 - len(unit(u)) = 1 if x = unit(u) 1120 - len(str) = str.length() if x = str 1121 - len(empty) = 0 if x = empty 1122 - len(int.to.str(i)) >= 1 if x = int.to.str(i) and more generally if i = 0 then 1 else 1+floor(log(|i|)) 1123 - len(x) >= 0 otherwise 1124 */ length_axiom(expr * n)1125 void axioms::length_axiom(expr* n) { 1126 expr* x = nullptr; 1127 VERIFY(seq.str.is_length(n, x)); 1128 if (seq.str.is_concat(x) || 1129 seq.str.is_unit(x) || 1130 seq.str.is_empty(x) || 1131 seq.str.is_string(x)) { 1132 expr_ref len(n, m); 1133 m_rewrite(len); 1134 SASSERT(n != len); 1135 add_clause(mk_eq(len, n)); 1136 } 1137 else { 1138 add_clause(mk_ge(n, 0)); 1139 } 1140 } 1141 1142 1143 /** 1144 ~contains(a, b) => ~prefix(b, a) 1145 ~contains(a, b) => ~contains(tail(a), b) 1146 a = empty => tail(a) = empty 1147 ~(a = empty) => a = head + tail 1148 */ unroll_not_contains(expr * e)1149 void axioms::unroll_not_contains(expr* e) { 1150 expr_ref head(m), tail(m); 1151 expr* a = nullptr, *b = nullptr; 1152 VERIFY(seq.str.is_contains(e, a, b)); 1153 m_sk.decompose(a, head, tail); 1154 expr_ref pref(seq.str.mk_prefix(b, a), m); 1155 expr_ref postf(seq.str.mk_contains(tail, b), m); 1156 expr_ref emp = mk_eq_empty(a); 1157 expr_ref cnt = expr_ref(e, m); 1158 add_clause(cnt, ~pref); 1159 add_clause(cnt, ~postf); 1160 add_clause(~emp, mk_eq_empty(tail)); 1161 add_clause(emp, mk_eq(a, seq.str.mk_concat(head, tail))); 1162 } 1163 length_limit(expr * s,unsigned k)1164 expr_ref axioms::length_limit(expr* s, unsigned k) { 1165 expr_ref bound_tracker = m_sk.mk_length_limit(s, k); 1166 expr* s0 = nullptr; 1167 if (seq.str.is_stoi(s, s0)) 1168 s = s0; 1169 add_clause(~bound_tracker, mk_le(mk_len(s), k)); 1170 return bound_tracker; 1171 } 1172 1173 } 1174