1 /*++ 2 Copyright (c) 2010 Microsoft Corporation 3 4 Module Name: 5 6 dl_interval_relation.cpp 7 8 Abstract: 9 10 Basic interval reatlion. 11 12 Author: 13 14 Nikolaj Bjorner (nbjorner) 2010-2-11 15 16 Revision History: 17 18 --*/ 19 20 #include "util/debug.h" 21 #include "ast/ast_pp.h" 22 #include "muz/rel/dl_interval_relation.h" 23 #include "muz/rel/dl_relation_manager.h" 24 #include "ast/rewriter/bool_rewriter.h" 25 26 27 namespace datalog { 28 // ------------------------- 29 // interval_relation_plugin 30 interval_relation_plugin(relation_manager & m)31 interval_relation_plugin::interval_relation_plugin(relation_manager& m): 32 relation_plugin(interval_relation_plugin::get_name(), m), 33 m_empty(m_dep), 34 m_arith(get_ast_manager()) { 35 } 36 can_handle_signature(const relation_signature & sig)37 bool interval_relation_plugin::can_handle_signature(const relation_signature & sig) { 38 for (unsigned i = 0; i < sig.size(); ++i) { 39 if (!m_arith.is_int(sig[i]) && !m_arith.is_real(sig[i])) { 40 return false; 41 } 42 } 43 return true; 44 } 45 46 mk_empty(const relation_signature & s)47 relation_base * interval_relation_plugin::mk_empty(const relation_signature & s) { 48 return alloc(interval_relation, *this, s, true); 49 } 50 mk_full(func_decl * p,const relation_signature & s)51 relation_base * interval_relation_plugin::mk_full(func_decl* p, const relation_signature & s) { 52 return alloc(interval_relation, *this, s, false); 53 } 54 55 class interval_relation_plugin::join_fn : public convenient_relation_join_fn { 56 public: join_fn(const relation_signature & o1_sig,const relation_signature & o2_sig,unsigned col_cnt,const unsigned * cols1,const unsigned * cols2)57 join_fn(const relation_signature & o1_sig, const relation_signature & o2_sig, unsigned col_cnt, 58 const unsigned * cols1, const unsigned * cols2) 59 : convenient_relation_join_fn(o1_sig, o2_sig, col_cnt, cols1, cols2){ 60 } 61 operator ()(const relation_base & _r1,const relation_base & _r2)62 relation_base * operator()(const relation_base & _r1, const relation_base & _r2) override { 63 interval_relation const& r1 = get(_r1); 64 interval_relation const& r2 = get(_r2); 65 interval_relation_plugin& p = r1.get_plugin(); 66 interval_relation* result = dynamic_cast<interval_relation*>(p.mk_full(nullptr, get_result_signature())); 67 result->mk_join(r1, r2, m_cols1.size(), m_cols1.data(), m_cols2.data()); 68 return result; 69 } 70 }; 71 mk_join_fn(const relation_base & r1,const relation_base & r2,unsigned col_cnt,const unsigned * cols1,const unsigned * cols2)72 relation_join_fn * interval_relation_plugin::mk_join_fn(const relation_base & r1, const relation_base & r2, 73 unsigned col_cnt, const unsigned * cols1, const unsigned * cols2) { 74 if (!check_kind(r1) || !check_kind(r2)) { 75 return nullptr; 76 } 77 return alloc(join_fn, r1.get_signature(), r2.get_signature(), col_cnt, cols1, cols2); 78 } 79 80 81 class interval_relation_plugin::project_fn : public convenient_relation_project_fn { 82 public: project_fn(const relation_signature & orig_sig,unsigned removed_col_cnt,const unsigned * removed_cols)83 project_fn(const relation_signature & orig_sig, unsigned removed_col_cnt, const unsigned * removed_cols) 84 : convenient_relation_project_fn(orig_sig, removed_col_cnt, removed_cols) { 85 } 86 operator ()(const relation_base & _r)87 relation_base * operator()(const relation_base & _r) override { 88 interval_relation const& r = get(_r); 89 interval_relation_plugin& p = r.get_plugin(); 90 interval_relation* result = dynamic_cast<interval_relation*>(p.mk_full(nullptr, get_result_signature())); 91 result->mk_project(r, m_removed_cols.size(), m_removed_cols.data()); 92 return result; 93 } 94 }; 95 mk_project_fn(const relation_base & r,unsigned col_cnt,const unsigned * removed_cols)96 relation_transformer_fn * interval_relation_plugin::mk_project_fn(const relation_base & r, 97 unsigned col_cnt, const unsigned * removed_cols) { 98 return alloc(project_fn, r.get_signature(), col_cnt, removed_cols); 99 } 100 101 class interval_relation_plugin::rename_fn : public convenient_relation_rename_fn { 102 public: rename_fn(const relation_signature & orig_sig,unsigned cycle_len,const unsigned * cycle)103 rename_fn(const relation_signature & orig_sig, unsigned cycle_len, const unsigned * cycle) 104 : convenient_relation_rename_fn(orig_sig, cycle_len, cycle) { 105 } 106 operator ()(const relation_base & _r)107 relation_base * operator()(const relation_base & _r) override { 108 interval_relation const& r = get(_r); 109 interval_relation_plugin& p = r.get_plugin(); 110 interval_relation* result = dynamic_cast<interval_relation*>(p.mk_full(nullptr, get_result_signature())); 111 result->mk_rename(r, m_cycle.size(), m_cycle.data()); 112 return result; 113 } 114 }; 115 mk_rename_fn(const relation_base & r,unsigned cycle_len,const unsigned * permutation_cycle)116 relation_transformer_fn * interval_relation_plugin::mk_rename_fn(const relation_base & r, 117 unsigned cycle_len, const unsigned * permutation_cycle) { 118 if(!check_kind(r)) { 119 return nullptr; 120 } 121 return alloc(rename_fn, r.get_signature(), cycle_len, permutation_cycle); 122 } 123 unite(interval const & src1,interval const & src2)124 interval interval_relation_plugin::unite(interval const& src1, interval const& src2) { 125 bool l_open = src1.is_lower_open(); 126 bool r_open = src1.is_upper_open(); 127 ext_numeral low = src1.inf(); 128 ext_numeral high = src1.sup(); 129 if (src2.inf() < low || (src2.inf() == low && l_open)) { 130 low = src2.inf(); 131 l_open = src2.is_lower_open(); 132 } 133 if (src2.sup() > high || (src2.sup() == high && r_open)) { 134 high = src2.sup(); 135 r_open = src2.is_upper_open(); 136 } 137 return interval(dep(), low, l_open, nullptr, high, r_open, nullptr); 138 } 139 widen(interval const & src1,interval const & src2)140 interval interval_relation_plugin::widen(interval const& src1, interval const& src2) { 141 bool l_open = src1.is_lower_open(); 142 bool r_open = src1.is_upper_open(); 143 ext_numeral low = src1.inf(); 144 ext_numeral high = src1.sup(); 145 146 if (src2.inf() < low || (low == src2.inf() && l_open && !src2.is_lower_open())) { 147 low = ext_numeral(false); 148 l_open = true; 149 } 150 if (high < src2.sup() || (src2.sup() == high && !r_open && src2.is_upper_open())) { 151 high = ext_numeral(true); 152 r_open = true; 153 } 154 return interval(dep(), low, l_open, nullptr, high, r_open, nullptr); 155 } 156 meet(interval const & src1,interval const & src2,bool & isempty)157 interval interval_relation_plugin::meet(interval const& src1, interval const& src2, bool& isempty) { 158 isempty = false; 159 if (is_empty(0, src1) || is_infinite(src2)) { 160 return src1; 161 } 162 if (is_empty(0, src2) || is_infinite(src1)) { 163 return src2; 164 } 165 bool l_open = src1.is_lower_open(); 166 bool r_open = src1.is_upper_open(); 167 ext_numeral low = src1.inf(); 168 ext_numeral high = src1.sup(); 169 if (src2.inf() > low || (src2.inf() == low && !l_open)) { 170 low = src2.inf(); 171 l_open = src2.is_lower_open(); 172 } 173 if (src2.sup() < high || (src2.sup() == high && !r_open)) { 174 high = src2.sup(); 175 r_open = src2.is_upper_open(); 176 } 177 if (low > high || (low == high && (l_open || r_open))) { 178 isempty = true; 179 return interval(dep()); 180 } 181 else { 182 return interval(dep(), low, l_open, nullptr, high, r_open, nullptr); 183 } 184 } 185 is_infinite(interval const & i)186 bool interval_relation_plugin::is_infinite(interval const& i) { 187 return i.plus_infinity() && i.minus_infinity(); 188 } 189 is_empty(unsigned,interval const & i)190 bool interval_relation_plugin::is_empty(unsigned, interval const& i) { 191 return i.sup() < i.inf(); 192 } 193 194 class interval_relation_plugin::union_fn : public relation_union_fn { 195 bool m_is_widen; 196 public: union_fn(bool is_widen)197 union_fn(bool is_widen) : 198 m_is_widen(is_widen) { 199 } 200 operator ()(relation_base & _r,const relation_base & _src,relation_base * _delta)201 void operator()(relation_base & _r, const relation_base & _src, relation_base * _delta) override { 202 203 TRACE("interval_relation", _r.display(tout << "dst:\n"); _src.display(tout << "src:\n");); 204 205 interval_relation& r = get(_r); 206 interval_relation const& src = get(_src); 207 if (_delta) { 208 interval_relation& d = get(*_delta); 209 r.mk_union(src, &d, m_is_widen); 210 } 211 else { 212 r.mk_union(src, nullptr, m_is_widen); 213 } 214 } 215 }; 216 mk_union_fn(const relation_base & tgt,const relation_base & src,const relation_base * delta)217 relation_union_fn * interval_relation_plugin::mk_union_fn(const relation_base & tgt, const relation_base & src, 218 const relation_base * delta) { 219 if (!check_kind(tgt) || !check_kind(src) || (delta && !check_kind(*delta))) { 220 return nullptr; 221 } 222 return alloc(union_fn, false); 223 } 224 mk_widen_fn(const relation_base & tgt,const relation_base & src,const relation_base * delta)225 relation_union_fn * interval_relation_plugin::mk_widen_fn( 226 const relation_base & tgt, const relation_base & src, 227 const relation_base * delta) { 228 if (!check_kind(tgt) || !check_kind(src) || (delta && !check_kind(*delta))) { 229 return nullptr; 230 } 231 return alloc(union_fn, true); 232 } 233 234 class interval_relation_plugin::filter_identical_fn : public relation_mutator_fn { 235 unsigned_vector m_identical_cols; 236 public: filter_identical_fn(unsigned col_cnt,const unsigned * identical_cols)237 filter_identical_fn(unsigned col_cnt, const unsigned * identical_cols) 238 : m_identical_cols(col_cnt, identical_cols) {} 239 operator ()(relation_base & r)240 void operator()(relation_base & r) override { 241 interval_relation & pr = get(r); 242 for (unsigned i = 1; i < m_identical_cols.size(); ++i) { 243 unsigned c1 = m_identical_cols[0]; 244 unsigned c2 = m_identical_cols[i]; 245 pr.equate(c1, c2); 246 } 247 } 248 }; 249 mk_filter_identical_fn(const relation_base & t,unsigned col_cnt,const unsigned * identical_cols)250 relation_mutator_fn * interval_relation_plugin::mk_filter_identical_fn( 251 const relation_base & t, unsigned col_cnt, const unsigned * identical_cols) { 252 if(!check_kind(t)) { 253 return nullptr; 254 } 255 return alloc(filter_identical_fn, col_cnt, identical_cols); 256 } 257 258 259 class interval_relation_plugin::filter_equal_fn : public relation_mutator_fn { 260 unsigned m_col; 261 rational m_value; 262 public: filter_equal_fn(relation_manager & m,const relation_element & value,unsigned col)263 filter_equal_fn(relation_manager & m, const relation_element & value, unsigned col) 264 : m_col(col) { 265 arith_util arith(m.get_context().get_manager()); 266 VERIFY(arith.is_numeral(value, m_value)); 267 } 268 operator ()(relation_base & _r)269 void operator()(relation_base & _r) override { 270 interval_relation & r = get(_r); 271 interval_relation_plugin & p = r.get_plugin(); 272 r.mk_intersect(m_col, interval(p.dep(), m_value)); 273 TRACE("interval_relation", tout << m_value << "\n"; r.display(tout);); 274 } 275 }; 276 mk_filter_equal_fn(const relation_base & r,const relation_element & value,unsigned col)277 relation_mutator_fn * interval_relation_plugin::mk_filter_equal_fn(const relation_base & r, 278 const relation_element & value, unsigned col) { 279 if(check_kind(r)) { 280 return alloc(filter_equal_fn, get_manager(), value, col); 281 } 282 return nullptr; 283 } 284 285 286 class interval_relation_plugin::filter_interpreted_fn : public relation_mutator_fn { 287 app_ref m_cond; 288 public: filter_interpreted_fn(interval_relation const & t,app * cond)289 filter_interpreted_fn(interval_relation const& t, app* cond): 290 m_cond(cond, t.get_plugin().get_ast_manager()) { 291 } 292 operator ()(relation_base & t)293 void operator()(relation_base& t) override { 294 get(t).filter_interpreted(m_cond); 295 TRACE("interval_relation", tout << mk_pp(m_cond, m_cond.get_manager()) << "\n"; t.display(tout);); 296 } 297 }; 298 mk_filter_interpreted_fn(const relation_base & t,app * condition)299 relation_mutator_fn * interval_relation_plugin::mk_filter_interpreted_fn(const relation_base & t, app * condition) { 300 if (check_kind(t)) { 301 return alloc(filter_interpreted_fn, get(t), condition); 302 } 303 return nullptr; 304 } 305 get(relation_base & r)306 interval_relation& interval_relation_plugin::get(relation_base& r) { 307 return dynamic_cast<interval_relation&>(r); 308 } 309 get(relation_base const & r)310 interval_relation const & interval_relation_plugin::get(relation_base const& r) { 311 return dynamic_cast<interval_relation const&>(r); 312 } 313 314 // ----------------------- 315 // interval_relation 316 interval_relation(interval_relation_plugin & p,relation_signature const & s,bool is_empty)317 interval_relation::interval_relation(interval_relation_plugin& p, relation_signature const& s, bool is_empty): 318 vector_relation<interval>(p, s, is_empty, interval(p.dep())) 319 { 320 TRACE("interval_relation", tout << s.size() << "\n";); 321 } 322 add_fact(const relation_fact & f)323 void interval_relation::add_fact(const relation_fact & f) { 324 interval_relation r(get_plugin(), get_signature(), false); 325 ast_manager& m = get_plugin().get_ast_manager(); 326 for (unsigned i = 0; i < f.size(); ++i) { 327 app_ref eq(m); 328 expr* e = f[i]; 329 eq = m.mk_eq(m.mk_var(i, e->get_sort()), e); 330 r.filter_interpreted(eq.get()); 331 } 332 mk_union(r, nullptr, false); 333 } 334 contains_fact(const relation_fact & f) const335 bool interval_relation::contains_fact(const relation_fact & f) const { 336 SASSERT(f.size() == get_signature().size()); 337 interval_relation_plugin& p = get_plugin(); 338 339 for (unsigned i = 0; i < f.size(); ++i) { 340 if (f[i] != f[find(i)]) { 341 return false; 342 } 343 interval const& iv = (*this)[i]; 344 if (p.is_infinite(iv)) { 345 continue; 346 } 347 rational v; 348 if (p.m_arith.is_numeral(f[i], v)) { 349 if (!iv.contains(v)) { 350 return false; 351 } 352 } 353 else { 354 // TBD: may or must? 355 } 356 } 357 return true; 358 } 359 clone() const360 interval_relation * interval_relation::clone() const { 361 interval_relation* result = alloc(interval_relation, get_plugin(), get_signature(), empty()); 362 result->copy(*this); 363 return result; 364 } 365 complement(func_decl *) const366 interval_relation * interval_relation::complement(func_decl*) const { 367 UNREACHABLE(); 368 return nullptr; 369 } 370 to_formula(expr_ref & fml) const371 void interval_relation::to_formula(expr_ref& fml) const { 372 ast_manager& m = get_plugin().get_ast_manager(); 373 arith_util& arith = get_plugin().m_arith; 374 expr_ref_vector conjs(m); 375 relation_signature const& sig = get_signature(); 376 for (unsigned i = 0; i < sig.size(); ++i) { 377 if (i != find(i)) { 378 conjs.push_back(m.mk_eq(m.mk_var(i, sig[i]), 379 m.mk_var(find(i), sig[find(i)]))); 380 continue; 381 } 382 interval const& iv = (*this)[i]; 383 sort* ty = sig[i]; 384 expr_ref var(m.mk_var(i, ty), m); 385 if (!iv.minus_infinity()) { 386 expr* lo = arith.mk_numeral(iv.get_lower_value(), ty); 387 if (iv.is_lower_open()) { 388 conjs.push_back(arith.mk_lt(lo, var)); 389 } 390 else { 391 conjs.push_back(arith.mk_le(lo, var)); 392 } 393 } 394 if (!iv.plus_infinity()) { 395 expr* hi = arith.mk_numeral(iv.get_upper_value(), ty); 396 if (iv.is_upper_open()) { 397 conjs.push_back(arith.mk_lt(var, hi)); 398 } 399 else { 400 conjs.push_back(arith.mk_le(var, hi)); 401 } 402 } 403 } 404 bool_rewriter br(m); 405 br.mk_and(conjs.size(), conjs.data(), fml); 406 } 407 408 display_index(unsigned i,interval const & j,std::ostream & out) const409 void interval_relation::display_index(unsigned i, interval const& j, std::ostream & out) const { 410 out << i << " in " << j << "\n"; 411 } 412 get_plugin() const413 interval_relation_plugin& interval_relation::get_plugin() const { 414 return static_cast<interval_relation_plugin &>(relation_base::get_plugin()); 415 } 416 mk_intersect(unsigned idx,interval const & i)417 void interval_relation::mk_intersect(unsigned idx, interval const& i) { 418 bool isempty; 419 (*this)[idx] = mk_intersect((*this)[idx], i, isempty); 420 if (isempty || is_empty(idx, (*this)[idx])) { 421 set_empty(); 422 } 423 } 424 mk_rename_elem(interval & i,unsigned,unsigned const *)425 void interval_relation::mk_rename_elem(interval& i, unsigned, unsigned const* ) { 426 427 } 428 filter_interpreted(app * cond)429 void interval_relation::filter_interpreted(app* cond) { 430 interval_relation_plugin& p = get_plugin(); 431 rational k; 432 unsigned x, y; 433 if (p.is_lt(cond, x, k, y)) { 434 // 0 < x - y + k 435 if (x == UINT_MAX) { 436 // y < k 437 mk_intersect(y, interval(p.dep(), k, true, false, nullptr)); 438 return; 439 } 440 if (y == UINT_MAX) { 441 // -k < x 442 mk_intersect(x, interval(p.dep(), -k, true, true, nullptr)); 443 return; 444 } 445 // y < x + k 446 ext_numeral x_hi = (*this)[x].sup(); 447 ext_numeral y_lo = (*this)[y].inf(); 448 if (!x_hi.is_infinite()) { 449 mk_intersect(y, interval(p.dep(), k + x_hi.to_rational(), true, false, nullptr)); 450 } 451 if (!y_lo.is_infinite()) { 452 mk_intersect(x, interval(p.dep(), y_lo.to_rational() - k, true, true, nullptr)); 453 } 454 return; 455 } 456 bool is_int = false; 457 if (p.is_le(cond, x, k, y, is_int)) { 458 // 0 <= x - y + k 459 if (x == UINT_MAX) { 460 // y <= k 461 mk_intersect(y, interval(p.dep(), k, false, false, nullptr)); 462 return; 463 } 464 if (y == UINT_MAX) { 465 // -k <= x 466 mk_intersect(x, interval(p.dep(), -k, false, true, nullptr)); 467 return; 468 } 469 ext_numeral x_hi = (*this)[x].sup(); 470 ext_numeral y_lo = (*this)[y].inf(); 471 if (!x_hi.is_infinite()) { 472 mk_intersect(y, interval(p.dep(), k + x_hi.to_rational(), false, false, nullptr)); 473 } 474 if (!y_lo.is_infinite()) { 475 mk_intersect(x, interval(p.dep(), y_lo.to_rational() - k, false, true, nullptr)); 476 } 477 return; 478 } 479 if (p.is_eq(cond, x, k, y)) { 480 // y = x + k 481 if (x == UINT_MAX) { 482 SASSERT(y != UINT_MAX); 483 mk_intersect(y, interval(p.dep(), k)); 484 return; 485 } 486 if (y == UINT_MAX) { 487 // x = - k 488 SASSERT(x != UINT_MAX); 489 mk_intersect(x, interval(p.dep(), -k)); 490 return; 491 } 492 interval x_i = (*this)[x]; 493 interval y_i = (*this)[y]; 494 x_i += interval(p.dep(), k); 495 y_i -= interval(p.dep(), k); 496 mk_intersect(x, y_i); 497 mk_intersect(y, x_i); 498 } 499 if (get_plugin().get_ast_manager().is_false(cond)) { 500 set_empty(); 501 } 502 } 503 is_linear(expr * e,unsigned & neg,unsigned & pos,rational & k,bool is_pos) const504 bool interval_relation_plugin::is_linear(expr* e, unsigned& neg, unsigned& pos, rational& k, bool is_pos) const { 505 #define SET_VAR(_idx_) \ 506 if (is_pos &&pos == UINT_MAX) { \ 507 pos = _idx_; \ 508 return true; \ 509 } \ 510 if (!is_pos && neg == UINT_MAX) { \ 511 neg = _idx_; \ 512 return true; \ 513 } \ 514 else { \ 515 return false; \ 516 } 517 518 if (is_var(e)) { 519 SET_VAR(to_var(e)->get_idx()); 520 } 521 if (!is_app(e)) { 522 return false; 523 } 524 app* a = to_app(e); 525 526 if (m_arith.is_add(e)) { 527 for (unsigned i = 0; i < a->get_num_args(); ++i) { 528 if (!is_linear(a->get_arg(i), neg, pos, k, is_pos)) return false; 529 } 530 return true; 531 } 532 if (m_arith.is_sub(e)) { 533 SASSERT(a->get_num_args() == 2); 534 return 535 is_linear(a->get_arg(0), neg, pos, k, is_pos) && 536 is_linear(a->get_arg(1), neg, pos, k, !is_pos); 537 } 538 rational k1; 539 SASSERT(!m_arith.is_mul(e) || a->get_num_args() == 2); 540 if (m_arith.is_mul(e) && 541 m_arith.is_numeral(a->get_arg(0), k1) && 542 k1.is_minus_one() && 543 is_var(a->get_arg(1))) { 544 SET_VAR(to_var(a->get_arg(1))->get_idx()); 545 } 546 547 if (m_arith.is_numeral(e, k1)) { 548 if (is_pos) { 549 k += k1; 550 } 551 else { 552 k -= k1; 553 } 554 return true; 555 } 556 return false; 557 } 558 559 // 0 <= x - y + k is_le(app * cond,unsigned & x,rational & k,unsigned & y,bool & is_int) const560 bool interval_relation_plugin::is_le(app* cond, unsigned& x, rational& k, unsigned& y, bool& is_int) const { 561 ast_manager& m = get_ast_manager(); 562 k.reset(); 563 x = UINT_MAX; 564 y = UINT_MAX; 565 566 if (m_arith.is_le(cond)) { 567 is_int = m_arith.is_int(cond->get_arg(0)); 568 if (!is_linear(cond->get_arg(0), y, x, k, false)) return false; 569 if (!is_linear(cond->get_arg(1), y, x, k, true)) return false; 570 return (x != UINT_MAX || y != UINT_MAX); 571 } 572 if (m_arith.is_ge(cond)) { 573 is_int = m_arith.is_int(cond->get_arg(0)); 574 if (!is_linear(cond->get_arg(0), y, x, k, true)) return false; 575 if (!is_linear(cond->get_arg(1), y, x, k, false)) return false; 576 return (x != UINT_MAX || y != UINT_MAX); 577 } 578 if (m_arith.is_lt(cond) && m_arith.is_int(cond->get_arg(0))) { 579 is_int = true; 580 if (!is_linear(cond->get_arg(0), y, x, k, false)) return false; 581 if (!is_linear(cond->get_arg(1), y, x, k, true)) return false; 582 k -= rational::one(); 583 return (x != UINT_MAX || y != UINT_MAX); 584 } 585 if (m_arith.is_gt(cond) && m_arith.is_int(cond->get_arg(0))) { 586 is_int = true; 587 if (!is_linear(cond->get_arg(0), y, x, k, true)) return false; 588 if (!is_linear(cond->get_arg(1), y, x, k, false)) return false; 589 k += rational::one(); 590 return (x != UINT_MAX || y != UINT_MAX); 591 } 592 if (m.is_not(cond) && is_app(cond->get_arg(0))) { 593 // not (0 <= x - y + k) 594 // <=> 595 // 0 > x - y + k 596 // <=> 597 // 0 <= y - x - k - 1 598 if (is_le(to_app(cond->get_arg(0)), x, k, y, is_int) && is_int) { 599 k.neg(); 600 k -= rational::one(); 601 std::swap(x, y); 602 return true; 603 } 604 // not (0 < x - y + k) 605 // <=> 606 // 0 >= x - y + k 607 // <=> 608 // 0 <= y - x - k 609 if (is_lt(to_app(cond->get_arg(0)), x, k, y)) { 610 is_int = false; 611 k.neg(); 612 std::swap(x, y); 613 return true; 614 } 615 } 616 return false; 617 } 618 619 // 0 < x - y + k is_lt(app * cond,unsigned & x,rational & k,unsigned & y) const620 bool interval_relation_plugin::is_lt(app* cond, unsigned& x, rational& k, unsigned& y) const { 621 k.reset(); 622 x = UINT_MAX; 623 y = UINT_MAX; 624 if (m_arith.is_lt(cond) && m_arith.is_real(cond->get_arg(0))) { 625 if (!is_linear(cond->get_arg(0), y, x, k, false)) return false; 626 if (!is_linear(cond->get_arg(1), y, x, k, true)) return false; 627 return (x != UINT_MAX || y != UINT_MAX); 628 } 629 if (m_arith.is_gt(cond) && m_arith.is_real(cond->get_arg(0))) { 630 if (!is_linear(cond->get_arg(0), y, x, k, true)) return false; 631 if (!is_linear(cond->get_arg(1), y, x, k, false)) return false; 632 return (x != UINT_MAX || y != UINT_MAX); 633 } 634 return false; 635 } 636 637 // 0 = x - y + k is_eq(app * cond,unsigned & x,rational & k,unsigned & y) const638 bool interval_relation_plugin::is_eq(app* cond, unsigned& x, rational& k, unsigned& y) const { 639 ast_manager& m = get_ast_manager(); 640 k.reset(); 641 x = UINT_MAX; 642 y = UINT_MAX; 643 if (m.is_eq(cond)) { 644 if (!is_linear(cond->get_arg(0), y, x, k, false)) return false; 645 if (!is_linear(cond->get_arg(1), y, x, k, true)) return false; 646 return (x != UINT_MAX || y != UINT_MAX); 647 } 648 return false; 649 } 650 651 }; 652 653