001package org.clafer.ir; 002 003import gnu.trove.iterator.TIntIterator; 004import gnu.trove.list.TIntList; 005import gnu.trove.list.array.TIntArrayList; 006import gnu.trove.set.hash.TIntHashSet; 007 008/** 009 * 010 * @author jimmy 011 */ 012public class IrUtil { 013 014 private IrUtil() { 015 } 016 017 public static boolean isTrue(IrBoolExpr b) { 018 return IrBoolDomain.TrueDomain.equals(b.getDomain()); 019 } 020 021 public static boolean isFalse(IrBoolExpr b) { 022 return IrBoolDomain.FalseDomain.equals(b.getDomain()); 023 } 024 025 public static boolean isConstant(IrBoolExpr b) { 026 return !IrBoolDomain.BoolDomain.equals(b.getDomain()); 027 } 028 029 public static Boolean getConstant(IrBoolExpr b) { 030 switch (b.getDomain()) { 031 case TrueDomain: 032 return Boolean.TRUE; 033 case FalseDomain: 034 return Boolean.FALSE; 035 case BoolDomain: 036 return null; 037 default: 038 throw new IllegalArgumentException(); 039 } 040 } 041 042 public static IrBoolVar asConstant(IrBoolVar b) { 043 switch (b.getDomain()) { 044 case TrueDomain: 045 return Irs.True; 046 case FalseDomain: 047 return Irs.False; 048 case BoolDomain: 049 return b; 050 default: 051 throw new IllegalArgumentException(); 052 } 053 } 054 055 public static boolean isConstant(IrIntExpr i) { 056 IrDomain domain = i.getDomain(); 057 return domain.size() == 1; 058 } 059 060 public static Integer getConstant(IrIntExpr i) { 061 IrDomain domain = i.getDomain(); 062 return domain.size() == 1 ? domain.getLowBound() : null; 063 } 064 065 public static int[] getConstant(IrIntExpr[] is) { 066 if (is.length == 0) { 067 return new int[0]; 068 } 069 if (is[0].getDomain().size() == 1) { 070 int[] constant = new int[is.length]; 071 constant[0] = is[0].getDomain().getLowBound(); 072 for (int i = 1; i < is.length; i++) { 073 if (is[i].getDomain().size() == 1) { 074 constant[i] = is[i].getDomain().getLowBound(); 075 } else { 076 return null; 077 } 078 } 079 return constant; 080 } 081 return null; 082 } 083 084 public static IrIntVar asConstant(IrIntVar i) { 085 IrDomain domain = i.getDomain(); 086 return domain.size() == 1 ? Irs.constant(domain.getLowBound()) : i; 087 } 088 089 public static boolean isConstant(IrSetExpr s) { 090 IrDomain env = s.getEnv(); 091 IrDomain ker = s.getKer(); 092 assert IrUtil.isSubsetOf(ker, env); 093 return env.size() == ker.size(); 094 } 095 096 public static int[] getConstant(IrSetExpr s) { 097 IrDomain env = s.getEnv(); 098 IrDomain ker = s.getKer(); 099 assert IrUtil.isSubsetOf(ker, env); 100 return env.size() == ker.size() ? ker.getValues() : null; 101 } 102 103 public static IrSetVar asConstant(IrSetVar s) { 104 IrDomain env = s.getEnv(); 105 IrDomain ker = s.getKer(); 106 assert IrUtil.isSubsetOf(ker, env); 107 if (env.size() == ker.size()) { 108 return Irs.constant(ker); 109 } 110 IrDomain card = s.getCard(); 111 if (card.size() == 1) { 112 int constantCard = card.getLowBound(); 113 if (constantCard == ker.size()) { 114 return Irs.constant(ker); 115 } 116 if (constantCard == env.size()) { 117 return Irs.constant(env); 118 } 119 } 120 return s; 121 } 122 123 public static IrSetExpr asConstant(IrSetExpr s) { 124 IrDomain env = s.getEnv(); 125 IrDomain ker = s.getKer(); 126 assert IrUtil.isSubsetOf(ker, env); 127 if (env.size() == ker.size()) { 128 return Irs.constant(env); 129 } 130 IrDomain card = s.getCard(); 131 if (card.size() == 1) { 132 int constantCard = card.getLowBound(); 133 if (constantCard == ker.size()) { 134 return Irs.constant(ker); 135 } 136 } 137 return s; 138 } 139 140 public static IrIntExpr asInt(IrSetExpr set) { 141 if (set instanceof IrSingleton) { 142 return ((IrSingleton) set).getValue(); 143 } 144 int[] constant = getConstant(set); 145 if (constant != null && constant.length == 1) { 146 return Irs.constant(constant[0]); 147 } 148 return null; 149 } 150 151 public static IrIntExpr[] asInts(IrSetExpr[] sets) { 152 if (sets.length == 0) { 153 return new IrIntExpr[0]; 154 } 155 IrIntExpr asInt = asInt(sets[0]); 156 if (asInt == null) { 157 return null; 158 } 159 IrIntExpr[] ints = new IrIntExpr[sets.length]; 160 ints[0] = asInt; 161 for (int i = 1; i < sets.length; i++) { 162 asInt = asInt(sets[i]); 163 if (asInt == null) { 164 return null; 165 } 166 ints[i] = asInt; 167 } 168 return ints; 169 } 170 171 public static boolean containsAll(int[] values, IrDomain domain) { 172 for (int value : values) { 173 if (!domain.contains(value)) { 174 return false; 175 } 176 } 177 return true; 178 } 179 180 public static boolean intersects(IrDomain d1, IrDomain d2) { 181 if (d1.isEmpty() || d2.isEmpty()) { 182 return false; 183 } 184 if (d1 == d2) { 185 return true; 186 } 187 if (d1.getLowBound() > d2.getHighBound()) { 188 return false; 189 } 190 if (d1.getHighBound() < d2.getLowBound()) { 191 return false; 192 } 193 if (d1.isBounded() 194 && (d2.isBounded() 195 || d2.getLowBound() >= d1.getLowBound() 196 || (d2.getHighBound() <= d1.getHighBound()))) { 197 // Bounds are already checked. 198 return true; 199 } 200 if (d2.isBounded() 201 && (d1.getLowBound() >= d2.getLowBound() 202 || (d1.getHighBound() <= d2.getHighBound()))) { 203 // Bounds are already checked. 204 return true; 205 } 206 if (d1.size() <= d2.size()) { 207 TIntIterator iter = d1.iterator(); 208 while (iter.hasNext()) { 209 if (d2.contains(iter.next())) { 210 return true; 211 } 212 } 213 } else { 214 TIntIterator iter = d2.iterator(); 215 while (iter.hasNext()) { 216 if (d1.contains(iter.next())) { 217 return true; 218 } 219 } 220 } 221 return false; 222 } 223 224 public static boolean isSubsetOf(IrDomain sub, IrDomain sup) { 225 if (sub == sup) { 226 return true; 227 } 228 if (sub.isEmpty()) { 229 return true; 230 } 231 if (sub.size() > sup.size()) { 232 return false; 233 } 234 if (sub.getLowBound() < sup.getLowBound()) { 235 return false; 236 } 237 if (sub.getHighBound() > sup.getHighBound()) { 238 return false; 239 } 240 if (sup.isBounded()) { 241 // Bounds are already checked. 242 return true; 243 } 244 TIntIterator iter = sub.iterator(); 245 while (iter.hasNext()) { 246 if (!sup.contains(iter.next())) { 247 return false; 248 } 249 } 250 return true; 251 } 252 253 public static IrDomain add(IrDomain domain, int value) { 254 if (domain.isEmpty()) { 255 return Irs.constantDomain(value); 256 } 257 if (domain.contains(value)) { 258 return domain; 259 } 260 if (domain.isBounded()) { 261 if (value == domain.getLowBound() - 1) { 262 return Irs.boundDomain(domain.getLowBound() - 1, domain.getHighBound()); 263 } 264 if (value == domain.getHighBound() + 1) { 265 return Irs.boundDomain(domain.getLowBound(), domain.getHighBound() + 1); 266 } 267 } 268 TIntHashSet values = new TIntHashSet(domain.size() + 1); 269 domain.transferTo(values); 270 values.add(value); 271 return Irs.enumDomain(values); 272 } 273 274 public static IrDomain remove(IrDomain domain, int value) { 275 if (!domain.contains(value)) { 276 return domain; 277 } 278 if (domain.isBounded()) { 279 if (value == domain.getLowBound()) { 280 return domain.size() == 1 281 ? Irs.EmptyDomain 282 : Irs.boundDomain(domain.getLowBound() + 1, domain.getHighBound()); 283 } 284 if (value == domain.getHighBound()) { 285 return domain.size() == 1 286 ? Irs.EmptyDomain 287 : Irs.boundDomain(domain.getLowBound(), domain.getHighBound() - 1); 288 } 289 } 290 TIntHashSet values = new TIntHashSet(domain.size()); 291 domain.transferTo(values); 292 values.remove(value); 293 return Irs.enumDomain(values); 294 } 295 296 public static IrDomain boundLow(IrDomain domain, int lb) { 297 if (domain.isEmpty()) { 298 return domain; 299 } 300 if (lb > domain.getHighBound()) { 301 return Irs.EmptyDomain; 302 } 303 if (lb == domain.getHighBound()) { 304 return Irs.constantDomain(lb); 305 } 306 if (lb <= domain.getLowBound()) { 307 return domain; 308 } 309 if (domain.isBounded()) { 310 return Irs.boundDomain(lb, domain.getHighBound()); 311 } 312 TIntHashSet values = new TIntHashSet(Math.min(domain.size(), domain.getHighBound() - lb + 1)); 313 TIntIterator iter = domain.iterator(); 314 while (iter.hasNext()) { 315 int value = iter.next(); 316 if (value >= lb) { 317 values.add(value); 318 } 319 } 320 return Irs.enumDomain(values); 321 } 322 323 public static IrDomain boundHigh(IrDomain domain, int hb) { 324 if (domain.isEmpty()) { 325 return domain; 326 } 327 if (hb < domain.getLowBound()) { 328 return Irs.EmptyDomain; 329 } 330 if (hb == domain.getLowBound()) { 331 return Irs.constantDomain(hb); 332 } 333 if (hb >= domain.getHighBound()) { 334 return domain; 335 } 336 if (domain.isBounded()) { 337 return Irs.boundDomain(domain.getLowBound(), hb); 338 } 339 TIntHashSet values = new TIntHashSet(Math.min(domain.size(), hb - domain.getLowBound() + 1)); 340 TIntIterator iter = domain.iterator(); 341 while (iter.hasNext()) { 342 int value = iter.next(); 343 if (value <= hb) { 344 values.add(value); 345 } 346 } 347 return Irs.enumDomain(values); 348 } 349 350 public static IrDomain difference(IrDomain minuend, IrDomain subtrahend) { 351 if (!intersects(minuend, subtrahend)) { 352 return minuend; 353 } 354 if (minuend.isBounded() && subtrahend.isBounded()) { 355 if (minuend.getLowBound() < subtrahend.getLowBound() 356 && minuend.getHighBound() <= subtrahend.getHighBound()) { 357 return Irs.boundDomain(minuend.getLowBound(), subtrahend.getLowBound() - 1); 358 } 359 if (minuend.getHighBound() > subtrahend.getHighBound() 360 && minuend.getLowBound() >= subtrahend.getLowBound()) { 361 return Irs.boundDomain(subtrahend.getHighBound() + 1, minuend.getHighBound()); 362 } 363 } 364 TIntHashSet values = new TIntHashSet(minuend.size()); 365 minuend.transferTo(values); 366 values.removeAll(subtrahend.getValues()); 367 return Irs.enumDomain(values); 368 } 369 370 public static IrDomain intersection(IrDomain d1, IrDomain d2) { 371 if (isSubsetOf(d1, d2)) { 372 return d1; 373 } 374 if (isSubsetOf(d2, d1)) { 375 return d2; 376 } 377 if (d1.isBounded() && d2.isBounded()) { 378 if (d1.getLowBound() <= d2.getLowBound() 379 && d1.getHighBound() >= d2.getLowBound()) { 380 return Irs.boundDomain(d2.getLowBound(), d1.getHighBound()); 381 } 382 if (d2.getLowBound() <= d1.getLowBound() 383 && d2.getHighBound() >= d1.getLowBound()) { 384 return Irs.boundDomain(d1.getLowBound(), d2.getHighBound()); 385 } 386 } 387 TIntHashSet values = new TIntHashSet(d1.size()); 388 d1.transferTo(values); 389 values.retainAll(d2.getValues()); 390 return Irs.enumDomain(values); 391 } 392 393 public static IrDomain intersectionEnvs(IrSetExpr... sets) { 394 if (sets.length == 0) { 395 return Irs.EmptyDomain; 396 } 397 IrDomain domain = sets[0].getEnv(); 398 for (int i = 1; i < sets.length; i++) { 399 domain = intersection(domain, sets[i].getEnv()); 400 } 401 return domain; 402 } 403 404 public static IrDomain intersectionKers(IrSetExpr... sets) { 405 if (sets.length == 0) { 406 return Irs.EmptyDomain; 407 } 408 IrDomain domain = sets[0].getKer(); 409 for (int i = 1; i < sets.length; i++) { 410 domain = intersection(domain, sets[i].getKer()); 411 } 412 return domain; 413 } 414 415 public static IrDomain union(IrDomain d1, IrDomain d2) { 416 if (isSubsetOf(d1, d2)) { 417 return d2; 418 } 419 if (isSubsetOf(d2, d1)) { 420 return d1; 421 } 422 if (d1.isBounded() && d2.isBounded()) { 423 if (d1.getLowBound() <= d2.getLowBound() 424 && d1.getHighBound() >= d2.getLowBound()) { 425 return Irs.boundDomain(d1.getLowBound(), d2.getHighBound()); 426 } 427 if (d2.getLowBound() <= d1.getLowBound() 428 && d2.getHighBound() >= d1.getLowBound()) { 429 return Irs.boundDomain(d2.getLowBound(), d1.getHighBound()); 430 } 431 } 432 TIntHashSet values = new TIntHashSet(d1.size() + d2.size()); 433 d1.transferTo(values); 434 d2.transferTo(values); 435 return Irs.enumDomain(values); 436 } 437 438 public static IrDomain unionEnvs(IrSetExpr... sets) { 439 if (sets.length == 0) { 440 return Irs.EmptyDomain; 441 } 442 IrDomain domain = sets[0].getEnv(); 443 for (int i = 1; i < sets.length; i++) { 444 domain = union(domain, sets[i].getEnv()); 445 } 446 return domain; 447 } 448 449 public static IrDomain unionKers(IrSetExpr... sets) { 450 if (sets.length == 0) { 451 return Irs.EmptyDomain; 452 } 453 IrDomain domain = sets[0].getKer(); 454 for (int i = 1; i < sets.length; i++) { 455 domain = union(domain, sets[i].getKer()); 456 } 457 return domain; 458 } 459 460 public static IrDomain minus(IrDomain domain) { 461 if (domain.isEmpty()) { 462 return Irs.EmptyDomain; 463 } 464 if (domain.isBounded()) { 465 return Irs.boundDomain(-domain.getHighBound(), -domain.getLowBound()); 466 } 467 int[] values = domain.getValues(); 468 int[] minusValues = new int[values.length]; 469 for (int i = 0; i < minusValues.length; i++) { 470 minusValues[i] = -values[i]; 471 } 472 return Irs.enumDomain(minusValues); 473 } 474 475 public static IrDomain offset(IrDomain domain, int offset) { 476 if (domain.isEmpty()) { 477 return Irs.EmptyDomain; 478 } 479 if (domain.isBounded()) { 480 return Irs.boundDomain(domain.getLowBound() + offset, domain.getHighBound() + offset); 481 } 482 int[] values = domain.getValues(); 483 int[] offsetValues = new int[values.length]; 484 for (int i = 0; i < offsetValues.length; i++) { 485 offsetValues[i] = values[i] + offset; 486 } 487 return Irs.enumDomain(offsetValues); 488 } 489 490 public static IrDomain mask(IrDomain domain, int from, int to) { 491 if (from > to) { 492 throw new IllegalArgumentException(); 493 } 494 if (from == to || domain.isEmpty()) { 495 return Irs.EmptyDomain; 496 } 497 if (from > domain.getHighBound() || to <= domain.getLowBound()) { 498 return Irs.EmptyDomain; 499 } 500 if (domain.isBounded()) { 501 return Irs.boundDomain( 502 Math.max(0, domain.getLowBound() - from), 503 Math.min(to - 1, domain.getHighBound()) - from); 504 } 505 TIntList mask = new TIntArrayList(); 506 for (int value : domain.getValues()) { 507 if (value >= from && value < to) { 508 mask.add(value - from); 509 } 510 } 511 return Irs.enumDomain(mask); 512 } 513 514 public static Ordering compare(IrIntExpr a, IrIntExpr b) { 515 if (a.equals(b)) { 516 return Ordering.EQ; 517 } 518 IrDomain da = a.getDomain(); 519 IrDomain db = b.getDomain(); 520 if (da.size() == 1 && db.size() == 1 && da.getLowBound() == db.getLowBound()) { 521 return Ordering.EQ; 522 } 523 int aLb = da.getLowBound(); 524 int aUb = da.getHighBound(); 525 int bLb = db.getLowBound(); 526 int bUb = db.getHighBound(); 527 if (aLb > bUb) { 528 return Ordering.GT; 529 } 530 if (aLb >= bUb) { 531 return Ordering.GE; 532 } 533 if (aUb < bLb) { 534 return Ordering.LT; 535 } 536 if (aUb <= bLb) { 537 return Ordering.LE; 538 } 539 return Ordering.UNKNOWN; 540 } 541 542 public static Ordering compareString(IrIntExpr[] a, IrIntExpr[] b) { 543 return compareString(a, b, 0); 544 } 545 546 public static Ordering compareString(IrIntExpr[] a, IrIntExpr[] b, int index) { 547 if (index == a.length) { 548 return a.length == b.length ? Ordering.EQ : Ordering.LT; 549 } 550 if (index == b.length) { 551 assert a.length != b.length; 552 return Ordering.GT; 553 } 554 Ordering ord = compare(a[index], b[index]); 555 switch (ord) { 556 case EQ: 557 return compareString(a, b, index + 1); 558 case LE: 559 switch (compareString(a, b, index + 1)) { 560 case LT: 561 return Ordering.LT; 562 case LE: 563 case EQ: 564 return Ordering.LE; 565 default: 566 return Ordering.UNKNOWN; 567 } 568 case GE: 569 switch (compareString(a, b, index + 1)) { 570 case GT: 571 return Ordering.GT; 572 case GE: 573 case EQ: 574 return Ordering.GE; 575 default: 576 return Ordering.UNKNOWN; 577 } 578 default: 579 return ord; 580 } 581 } 582 583 public static enum Ordering { 584 585 LT, 586 LE, 587 GT, 588 GE, 589 EQ, 590 UNKNOWN; 591 } 592}