Source code

001package org.clafer.ir;
002
003import gnu.trove.TIntCollection;
004import gnu.trove.iterator.TIntIterator;
005import gnu.trove.set.TIntSet;
006import gnu.trove.set.hash.TIntHashSet;
007import java.util.ArrayList;
008import java.util.Arrays;
009import java.util.Collection;
010import java.util.List;
011import org.clafer.common.Util;
012
013/**
014 * Import this class to access all IR building functions.
015 * <pre>
016 * import static org.clafer.ast.Asts.*;
017 * </pre>
018 *
019 * @author jimmy
020 */
021public class Irs {
022
023    private Irs() {
024    }
025    /**
026     *******************
027     *
028     * Domain
029     *
030     *******************
031     */
032    public static final IrBoolDomain TrueDomain = IrBoolDomain.TrueDomain;
033    public static final IrBoolDomain FalseDomain = IrBoolDomain.FalseDomain;
034    public static final IrBoolDomain BoolDomain = IrBoolDomain.BoolDomain;
035    public static final IrDomain EmptyDomain = new IrEmptyDomain();
036    public static final IrDomain ZeroDomain = FalseDomain;
037    public static final IrDomain OneDomain = TrueDomain;
038    public static final IrDomain ZeroOneDomain = BoolDomain;
039    public static final IrSetVar EmptySet = new IrSetConstant(EmptyDomain);
040
041    public static IrBoolDomain domain(boolean value) {
042        return value ? TrueDomain : FalseDomain;
043    }
044
045    public static IrDomain constantDomain(int value) {
046        return boundDomain(value, value);
047    }
048
049    public static IrDomain fromToDomain(int from, int to) {
050        if (from == to) {
051            return EmptyDomain;
052        }
053        return boundDomain(from, to - 1);
054    }
055
056    public static IrDomain boundDomain(int low, int high) {
057        if (low == 0 && high == 0) {
058            return ZeroDomain;
059        }
060        if (low == 1 && high == 1) {
061            return OneDomain;
062        }
063        if (low == 0 && high == 1) {
064            return ZeroOneDomain;
065        }
066        return new IrBoundDomain(low, high);
067    }
068
069    public static IrDomain enumDomain(int... values) {
070        return enumDomain(new TIntHashSet(values));
071    }
072
073    public static IrDomain enumDomain(TIntCollection values) {
074        return enumDomain(new TIntHashSet(values));
075    }
076
077    public static IrDomain enumDomain(TIntSet values) {
078        switch (values.size()) {
079            case 0:
080                return EmptyDomain;
081            case 1:
082                int value = values.iterator().next();
083                return boundDomain(value, value);
084            default:
085                int[] array = values.toArray();
086                Arrays.sort(array);
087                // If the values are over a contiguous interval, then return a bound domain.
088                int low = array[0];
089                int high = array[array.length - 1];
090                if (high - low + 1 == array.length) {
091                    // A contigious interval.
092                    return boundDomain(low, high);
093                }
094                return new IrEnumDomain(array);
095        }
096    }
097    /**
098     *******************
099     *
100     * Boolean
101     *
102     *******************
103     */
104    public static final IrBoolVar True = new IrBoolConstant(true);
105    public static final IrBoolVar False = new IrBoolConstant(false);
106
107    public static IrBoolVar constant(boolean value) {
108        return value ? True : False;
109    }
110
111    public static IrBoolVar bool(String name) {
112        return new IrBoolVar(name, BoolDomain);
113    }
114
115    public static IrBoolExpr not(IrBoolExpr proposition) {
116        Boolean constant = IrUtil.getConstant(proposition);
117        if (constant != null) {
118            // Reverse the boolean
119            return constant.booleanValue() ? False : True;
120        }
121        return proposition.negate();
122    }
123
124    public static IrBoolExpr and(Collection<? extends IrBoolExpr> operands) {
125        return and(operands.toArray(new IrBoolExpr[operands.size()]));
126    }
127
128    public static IrBoolExpr and(IrBoolExpr... operands) {
129        List<IrBoolExpr> flatten = new ArrayList<>(operands.length);
130        for (IrBoolExpr operand : operands) {
131            if (operand instanceof IrAnd) {
132                // Invariant: No nested IrAnd
133                flatten.addAll(Arrays.asList(((IrAnd) operand).getOperands()));
134            } else {
135                flatten.add(operand);
136            }
137        }
138        List<IrBoolExpr> filter = new ArrayList<>(flatten.size());
139        for (IrBoolExpr operand : flatten) {
140            if (IrUtil.isFalse(operand)) {
141                return False;
142            }
143            if (!IrUtil.isTrue(operand)) {
144                filter.add(operand);
145            }
146        }
147        switch (filter.size()) {
148            case 0:
149                return True;
150            case 1:
151                return filter.get(0);
152            default:
153                return new IrAnd(filter.toArray(new IrBoolExpr[filter.size()]), BoolDomain);
154        }
155    }
156
157    public static IrBoolExpr lone(Collection<? extends IrBoolExpr> operands) {
158        return lone(operands.toArray(new IrBoolExpr[operands.size()]));
159    }
160
161    public static IrBoolExpr lone(IrBoolExpr... operands) {
162        List<IrBoolExpr> filter = new ArrayList<>(operands.length);
163        int count = 0;
164        for (IrBoolExpr operand : operands) {
165            if (IrUtil.isTrue(operand)) {
166                count++;
167                if (count > 1) {
168                    return False;
169                }
170            } else if (!IrUtil.isFalse(operand)) {
171                filter.add(operand);
172            }
173        }
174        assert count == 0 || count == 1;
175        switch (filter.size()) {
176            case 0:
177                return True;
178            case 1:
179                return count == 0 ? True : not(filter.get(0));
180            default:
181                IrBoolExpr[] f = filter.toArray(new IrBoolExpr[filter.size()]);
182                return count == 0
183                        ? new IrLone(f, BoolDomain)
184                        : not(or(f));
185        }
186    }
187
188    public static IrBoolExpr one(Collection<? extends IrBoolExpr> operands) {
189        return one(operands.toArray(new IrBoolExpr[operands.size()]));
190    }
191
192    public static IrBoolExpr one(IrBoolExpr... operands) {
193        List<IrBoolExpr> filter = new ArrayList<>(operands.length);
194        int count = 0;
195        for (IrBoolExpr operand : operands) {
196            if (IrUtil.isTrue(operand)) {
197                count++;
198                if (count > 1) {
199                    return False;
200                }
201            } else if (!IrUtil.isFalse(operand)) {
202                filter.add(operand);
203            }
204        }
205        assert count == 0 || count == 1;
206        switch (filter.size()) {
207            case 0:
208                return count == 0 ? False : True;
209            case 1:
210                return count == 0 ? filter.get(0) : not(filter.get(0));
211            case 2:
212                return count == 0
213                        ? xor(filter.get(0), filter.get(1))
214                        : and(not(filter.get(0)), not(filter.get(1)));
215            default:
216                IrBoolExpr[] f = filter.toArray(new IrBoolExpr[filter.size()]);
217                return count == 0
218                        ? new IrOne(f, BoolDomain)
219                        : not(or(f));
220        }
221    }
222
223    public static IrBoolExpr or(Collection<? extends IrBoolExpr> operands) {
224        return or(operands.toArray(new IrBoolExpr[operands.size()]));
225    }
226
227    public static IrBoolExpr or(IrBoolExpr... operands) {
228        List<IrBoolExpr> flatten = new ArrayList<>(operands.length);
229        for (IrBoolExpr operand : operands) {
230            if (operand instanceof IrOr) {
231                // Invariant: No nested IrOr
232                flatten.addAll(Arrays.asList(((IrOr) operand).getOperands()));
233            } else {
234                flatten.add(operand);
235            }
236        }
237        List<IrBoolExpr> filter = new ArrayList<>(flatten.size());
238        for (IrBoolExpr operand : flatten) {
239            if (IrUtil.isTrue(operand)) {
240                return True;
241            }
242            if (!IrUtil.isFalse(operand)) {
243                filter.add(operand);
244            }
245        }
246        switch (filter.size()) {
247            case 0:
248                return False;
249            case 1:
250                return filter.get(0);
251            default:
252                return new IrOr(filter.toArray(new IrBoolExpr[filter.size()]), BoolDomain);
253        }
254    }
255
256    public static IrBoolExpr implies(IrBoolExpr antecedent, IrBoolExpr consequent) {
257        if (antecedent.equals(consequent)) {
258            return True;
259        }
260        if (IrUtil.isTrue(antecedent)) {
261            return consequent;
262        }
263        if (IrUtil.isFalse(antecedent)) {
264            return True;
265        }
266        if (IrUtil.isTrue(consequent)) {
267            return True;
268        }
269        if (IrUtil.isFalse(consequent)) {
270            return not(antecedent);
271        }
272        if (consequent instanceof IrImplies) {
273            // a => (b => c) <=> !a or !b or c
274            IrImplies consequentImplies = (IrImplies) consequent;
275            return or(not(antecedent),
276                    not(consequentImplies.getAntecedent()),
277                    consequentImplies.getConsequent());
278        }
279        return new IrImplies(antecedent, consequent, BoolDomain);
280    }
281
282    public static IrBoolExpr notImplies(IrBoolExpr antecedent, IrBoolExpr consequent) {
283        if (antecedent.equals(consequent)) {
284            return False;
285        }
286        if (IrUtil.isTrue(antecedent)) {
287            return not(consequent);
288        }
289        if (IrUtil.isFalse(antecedent)) {
290            return False;
291        }
292        if (IrUtil.isTrue(consequent)) {
293            return False;
294        }
295        if (IrUtil.isFalse(consequent)) {
296            return antecedent;
297        }
298        return new IrNotImplies(antecedent, consequent, BoolDomain);
299    }
300
301    public static IrBoolExpr ifThenElse(IrBoolExpr antecedent, IrBoolExpr consequent, IrBoolExpr alternative) {
302        if (IrUtil.isTrue(antecedent)) {
303            return consequent;
304        }
305        if (IrUtil.isFalse(antecedent)) {
306            return alternative;
307        }
308        if (IrUtil.isTrue(consequent)) {
309            return or(antecedent, alternative);
310        }
311        if (IrUtil.isFalse(consequent)) {
312            return and(antecedent.negate(), alternative);
313        }
314        if (IrUtil.isTrue(alternative)) {
315            return or(antecedent.negate(), consequent);
316        }
317        if (IrUtil.isFalse(alternative)) {
318            return and(antecedent, consequent);
319        }
320        return new IrIfThenElse(antecedent, consequent, alternative, BoolDomain);
321    }
322
323    public static IrBoolExpr ifOnlyIf(IrBoolExpr left, IrBoolExpr right) {
324        if (left.equals(right)) {
325            return True;
326        }
327        if (IrUtil.isTrue(left)) {
328            return right;
329        }
330        if (IrUtil.isFalse(left)) {
331            return not(right);
332        }
333        if (IrUtil.isTrue(right)) {
334            return left;
335        }
336        if (IrUtil.isFalse(right)) {
337            return not(left);
338        }
339        if (left instanceof IrNot) {
340            return xor(((IrNot) left).getExpr(), right);
341        }
342        if (right instanceof IrNot) {
343            return xor(left, ((IrNot) right).getExpr());
344        }
345        return new IrIfOnlyIf(left, right, BoolDomain);
346    }
347
348    public static IrBoolExpr xor(IrBoolExpr left, IrBoolExpr right) {
349        if (IrUtil.isTrue(left)) {
350            return not(right);
351        }
352        if (IrUtil.isFalse(left)) {
353            return right;
354        }
355        if (IrUtil.isTrue(right)) {
356            return not(left);
357        }
358        if (IrUtil.isFalse(right)) {
359            return left;
360        }
361        if (left instanceof IrNot) {
362            return ifOnlyIf(((IrNot) left).getExpr(), right);
363        }
364        if (right instanceof IrNot) {
365            return ifOnlyIf(left, ((IrNot) right).getExpr());
366        }
367        return new IrXor(left, right, BoolDomain);
368    }
369
370    public static IrBoolExpr within(IrIntExpr value, IrDomain range) {
371        IrDomain domain = value.getDomain();
372        if (range.isBounded()
373                && domain.getLowBound() >= range.getLowBound()
374                && domain.getHighBound() <= range.getHighBound()) {
375            return True;
376        } else if (IrUtil.isSubsetOf(domain, range)) {
377            return True;
378        }
379        if (domain.getLowBound() > range.getHighBound()
380                || domain.getHighBound() < range.getLowBound()) {
381            return False;
382        }
383        if (range.size() == 1) {
384            return equal(value, range.getLowBound());
385        }
386        if (value.getDomain().getLowBound() == range.getLowBound()
387                && value.getDomain().getHighBound() - 1 == range.getHighBound()) {
388            return notEqual(value, value.getDomain().getHighBound());
389        }
390        if (value.getDomain().getLowBound() + 1 == range.getLowBound()
391                && value.getDomain().getHighBound() == range.getHighBound()) {
392            return notEqual(value, value.getDomain().getLowBound());
393        }
394        return new IrWithin(value, range, BoolDomain);
395    }
396
397    public static IrBoolExpr notWithin(IrIntExpr value, IrDomain range) {
398        IrDomain domain = value.getDomain();
399        if (range.isBounded()
400                && domain.getLowBound() >= range.getLowBound()
401                && domain.getHighBound() <= range.getHighBound()) {
402            return False;
403        }
404        if (domain.getLowBound() > range.getHighBound()
405                || domain.getHighBound() < range.getLowBound()) {
406            return True;
407        }
408        if (range.size() == 1) {
409            return notEqual(value, range.getLowBound());
410        }
411        return new IrNotWithin(value, range, BoolDomain);
412    }
413
414    public static IrBoolExpr compare(int left, IrCompare.Op op, IrIntExpr right) {
415        return compare(constant(left), op, right);
416    }
417
418    public static IrBoolExpr compare(IrIntExpr left, IrCompare.Op op, int right) {
419        return compare(left, op, constant(right));
420    }
421
422    public static IrBoolExpr compare(IrIntExpr left, IrCompare.Op op, IrIntExpr right) {
423        IrDomain leftDomain = left.getDomain();
424        IrDomain rightDomain = right.getDomain();
425        switch (op) {
426            case Equal:
427                if (left.equals(right)) {
428                    return True;
429                }
430                if (!IrUtil.intersects(leftDomain, rightDomain)) {
431                    return False;
432                }
433                if (left instanceof IrBoolExpr && right instanceof IrBoolExpr) {
434                    return ifOnlyIf((IrBoolExpr) left, (IrBoolExpr) right);
435                }
436                break;
437            case NotEqual:
438                if (left.equals(right)) {
439                    return False;
440                }
441                if (!IrUtil.intersects(leftDomain, rightDomain)) {
442                    return True;
443                }
444                if (left instanceof IrBoolExpr && right instanceof IrBoolExpr) {
445                    return xor((IrBoolExpr) left, (IrBoolExpr) right);
446                }
447                break;
448            case LessThan:
449                if (left.equals(right)) {
450                    return False;
451                }
452                if (leftDomain.getHighBound() < rightDomain.getLowBound()) {
453                    return True;
454                }
455                if (leftDomain.getLowBound() >= rightDomain.getHighBound()) {
456                    return False;
457                }
458                if (left instanceof IrBoolExpr && right instanceof IrBoolExpr) {
459                    return not(implies((IrBoolExpr) right, (IrBoolExpr) left));
460                }
461                if (left instanceof IrMinus && right instanceof IrMinus) {
462                    return greaterThan(((IrMinus) left).getExpr(), ((IrMinus) right).getExpr());
463                }
464                break;
465            case LessThanEqual:
466                if (left.equals(right)) {
467                    return True;
468                }
469                if (leftDomain.getHighBound() <= rightDomain.getLowBound()) {
470                    return True;
471                }
472                if (leftDomain.getLowBound() > rightDomain.getHighBound()) {
473                    return False;
474                }
475                if (leftDomain.getLowBound() == rightDomain.getHighBound()) {
476                    return equal(left, right);
477                }
478                if (left instanceof IrBoolExpr && right instanceof IrBoolExpr) {
479                    return implies((IrBoolExpr) left, (IrBoolExpr) right);
480                }
481                if (left instanceof IrMinus && right instanceof IrMinus) {
482                    return greaterThanEqual(((IrMinus) left).getExpr(), ((IrMinus) right).getExpr());
483                }
484                break;
485            default:
486                throw new IllegalArgumentException("Unknown op: " + op);
487        }
488        return new IrCompare(left, op, right, BoolDomain);
489    }
490
491    public static IrBoolExpr equal(int left, IrIntExpr right) {
492        return equal(constant(left), right);
493    }
494
495    public static IrBoolExpr equal(IrIntExpr left, int right) {
496        return equal(left, constant(right));
497    }
498
499    public static IrBoolExpr equal(IrIntExpr left, IrIntExpr right) {
500        return compare(left, IrCompare.Op.Equal, right);
501    }
502
503    public static IrBoolExpr equal(IrIntExpr[] left, IrIntExpr[] right) {
504        if (left.length != right.length) {
505            throw new IllegalArgumentException();
506        }
507        IrBoolExpr[] ands = new IrBoolExpr[left.length];
508        for (int i = 0; i < ands.length; i++) {
509            ands[i] = equal(left[i], right[i]);
510        }
511        return and(ands);
512    }
513
514    public static IrBoolExpr equality(IrSetExpr left, IrSetTest.Op op, IrSetExpr right) {
515        switch (op) {
516            case Equal:
517                if (left.equals(right)) {
518                    return True;
519                }
520                if (!IrUtil.isSubsetOf(left.getKer(), right.getEnv())
521                        || !IrUtil.isSubsetOf(right.getKer(), left.getEnv())) {
522                    return False;
523                }
524                if (!IrUtil.intersects(left.getCard(), right.getCard())) {
525                    return False;
526                }
527                int[] constant = IrUtil.getConstant(left);
528                if (constant != null) {
529                    /*
530                     * The idea is that integer constraints are easier to
531                     * optimize than set constraints. If the expression is a top
532                     * level expression than the cardinality propagator will
533                     * optimize this expression away anyways.
534                     */
535                    if (constant.length == 0) {
536                        return equal(card(right), 0);
537                    }
538                    if (constant.length == right.getEnv().size()) {
539                        return IrUtil.containsAll(constant, right.getEnv())
540                                ? equal(card(right), constant.length) : False;
541                    }
542                }
543                constant = IrUtil.getConstant(right);
544                if (constant != null) {
545                    if (constant.length == 0) {
546                        return equal(card(left), 0);
547                    }
548                    if (constant.length == left.getEnv().size()) {
549                        return IrUtil.containsAll(constant, left.getEnv())
550                                ? equal(card(left), constant.length) : False;
551                    }
552                }
553                IrIntExpr leftInt = IrUtil.asInt(left);
554                if (leftInt != null) {
555                    IrIntExpr rightInt = IrUtil.asInt(right);
556                    if (rightInt != null) {
557                        return equal(leftInt, rightInt);
558                    }
559                }
560                break;
561            case NotEqual:
562                if (left.equals(right)) {
563                    return False;
564                }
565                if (!IrUtil.isSubsetOf(left.getKer(), right.getEnv())
566                        || !IrUtil.isSubsetOf(right.getKer(), left.getEnv())) {
567                    return True;
568                }
569                if (!IrUtil.intersects(left.getCard(), right.getCard())) {
570                    return True;
571                }
572                constant = IrUtil.getConstant(left);
573                if (constant != null) {
574                    if (constant.length == 0) {
575                        return notEqual(card(right), 0);
576                    }
577                    if (constant.length == right.getEnv().size()) {
578                        return IrUtil.containsAll(constant, right.getEnv())
579                                ? notEqual(card(right), constant.length) : True;
580                    }
581                }
582                constant = IrUtil.getConstant(right);
583                if (constant != null) {
584                    if (constant.length == 0) {
585                        return notEqual(card(left), 0);
586                    }
587                    if (constant.length == left.getEnv().size()) {
588                        return IrUtil.containsAll(constant, left.getEnv())
589                                ? notEqual(card(left), constant.length) : True;
590                    }
591                }
592                leftInt = IrUtil.asInt(left);
593                if (leftInt != null) {
594                    IrIntExpr rightInt = IrUtil.asInt(right);
595                    if (rightInt != null) {
596                        return notEqual(leftInt, rightInt);
597                    }
598                }
599                break;
600            default:
601                throw new IllegalArgumentException();
602        }
603        return new IrSetTest(left, op, right, BoolDomain);
604    }
605
606    public static IrBoolExpr equal(IrSetExpr left, IrSetExpr right) {
607        return equality(left, IrSetTest.Op.Equal, right);
608    }
609
610    public static IrBoolExpr notEqual(int left, IrIntExpr right) {
611        return notEqual(constant(left), right);
612    }
613
614    public static IrBoolExpr notEqual(IrIntExpr left, int right) {
615        return notEqual(left, constant(right));
616    }
617
618    public static IrBoolExpr notEqual(IrIntExpr left, IrIntExpr right) {
619        return compare(left, IrCompare.Op.NotEqual, right);
620    }
621
622    public static IrBoolExpr notEqual(IrSetExpr left, IrSetExpr right) {
623        return equality(left, IrSetTest.Op.NotEqual, right);
624    }
625
626    public static IrBoolExpr lessThan(int left, IrIntExpr right) {
627        return lessThan(constant(left), right);
628    }
629
630    public static IrBoolExpr lessThan(IrIntExpr left, int right) {
631        return lessThan(left, constant(right));
632    }
633
634    public static IrBoolExpr lessThan(IrIntExpr left, IrIntExpr right) {
635        return compare(left, IrCompare.Op.LessThan, right);
636    }
637
638    public static IrBoolExpr lessThanEqual(int left, IrIntExpr right) {
639        return lessThanEqual(constant(left), right);
640    }
641
642    public static IrBoolExpr lessThanEqual(IrIntExpr left, int right) {
643        return lessThanEqual(left, constant(right));
644    }
645
646    public static IrBoolExpr lessThanEqual(IrIntExpr left, IrIntExpr right) {
647        return compare(left, IrCompare.Op.LessThanEqual, right);
648    }
649
650    public static IrBoolExpr greaterThan(int left, IrIntExpr right) {
651        return greaterThan(constant(left), right);
652    }
653
654    public static IrBoolExpr greaterThan(IrIntExpr left, int right) {
655        return greaterThan(left, constant(right));
656    }
657
658    public static IrBoolExpr greaterThan(IrIntExpr left, IrIntExpr right) {
659        return compare(right, IrCompare.Op.LessThan, left);
660    }
661
662    public static IrBoolExpr greaterThanEqual(int left, IrIntExpr right) {
663        return greaterThanEqual(constant(left), right);
664    }
665
666    public static IrBoolExpr greaterThanEqual(IrIntExpr left, int right) {
667        return greaterThanEqual(left, constant(right));
668    }
669
670    public static IrBoolExpr greaterThanEqual(IrIntExpr left, IrIntExpr right) {
671        return compare(right, IrCompare.Op.LessThanEqual, left);
672    }
673
674    public static IrBoolExpr member(IrIntExpr element, IrSetExpr set) {
675        if (IrUtil.isSubsetOf(element.getDomain(), set.getKer())) {
676            return True;
677        }
678        if (!IrUtil.intersects(element.getDomain(), set.getEnv())) {
679            return False;
680        }
681        if (IrUtil.isConstant(set)) {
682            return within(element, set.getEnv());
683        }
684        return new IrMember(element, set, BoolDomain);
685    }
686
687    public static IrBoolExpr notMember(IrIntExpr element, IrSetExpr set) {
688        if (!IrUtil.intersects(element.getDomain(), set.getEnv())) {
689            return True;
690        }
691        if (IrUtil.isSubsetOf(element.getDomain(), set.getKer())) {
692            return False;
693        }
694        if (IrUtil.isConstant(set)) {
695            return notWithin(element, set.getEnv());
696        }
697        return new IrNotMember(element, set, BoolDomain);
698    }
699
700    public static IrBoolExpr subsetEq(IrSetExpr subset, IrSetExpr superset) {
701        if (IrUtil.isSubsetOf(subset.getEnv(), superset.getKer())) {
702            return True;
703        }
704        if (subset.getCard().getLowBound() == superset.getCard().getHighBound()) {
705            return equal(subset, superset);
706        }
707        return new IrSubsetEq(subset, superset, BoolDomain);
708    }
709
710    public static IrBoolExpr boolChannel(IrBoolExpr[] bools, IrSetExpr set) {
711        if (set.getEnv().isEmpty()
712                || (set.getEnv().getLowBound() >= 0 && set.getEnv().getHighBound() < bools.length)) {
713            {
714                int[] constant = IrUtil.getConstant(set);
715                if (constant != null) {
716                    IrBoolExpr[] ands = new IrBoolExpr[bools.length];
717                    for (int i = 0; i < ands.length; i++) {
718                        ands[i] = equal(bools[i], Util.in(i, constant) ? True : False);
719                    }
720                    return and(ands);
721                }
722                if (bools.length == 1) {
723                    return equal(bools[0], card(set));
724                }
725            }
726            TIntHashSet values = new TIntHashSet();
727            IrDomain env = set.getEnv();
728            IrDomain ker = set.getKer();
729            boolean entailed = true;
730            for (int i = 0; i < bools.length; i++) {
731                Boolean constant = IrUtil.getConstant(bools[i]);
732                if (Boolean.TRUE.equals(constant)) {
733                    if (values != null) {
734                        values.add(i);
735                    }
736                    if (!env.contains(i)) {
737                        return False;
738                    }
739                    if (!ker.contains(i)) {
740                        entailed = false;
741                    }
742                } else if (Boolean.FALSE.equals(constant)) {
743                    if (ker.contains(i)) {
744                        return False;
745                    }
746                    if (env.contains(i)) {
747                        entailed = false;
748                    }
749                } else {
750                    values = null;
751                    entailed = false;
752                }
753            }
754            if (entailed) {
755                return True;
756            }
757            if (values != null) {
758                return equal(set, constant(enumDomain(values)));
759            }
760        }
761        return new IrBoolChannel(bools, set, BoolDomain);
762    }
763
764    public static IrBoolExpr intChannel(IrIntExpr[] ints, IrSetExpr[] sets) {
765        boolean entailed = true;
766        for (int i = 0; i < ints.length; i++) {
767            Integer constant = IrUtil.getConstant(ints[i]);
768            if (constant != null) {
769                IrSetExpr set = sets[constant.intValue()];
770                if (!set.getEnv().contains(i)) {
771                    return False;
772                } else if (!set.getKer().contains(i)) {
773                    entailed = false;
774                }
775            } else {
776                entailed = false;
777            }
778        }
779        if (entailed) {
780            return True;
781        }
782        return new IrIntChannel(ints, sets, BoolDomain);
783    }
784
785    public static IrBoolExpr sort(IrIntExpr... array) {
786        if (array.length <= 1) {
787            return True;
788        }
789        IrBoolExpr[] sort = new IrBoolExpr[array.length - 1];
790        for (int i = 0; i < array.length - 1; i++) {
791            sort[i] = lessThanEqual(array[i], array[i + 1]);
792        }
793        return and(sort);
794    }
795
796    public static IrBoolExpr sortStrict(IrIntExpr... array) {
797        if (array.length <= 1) {
798            return True;
799        }
800        IrBoolExpr[] sort = new IrBoolExpr[array.length - 1];
801        for (int i = 0; i < array.length - 1; i++) {
802            sort[i] = lessThan(array[i], array[i + 1]);
803        }
804        return and(sort);
805    }
806
807    public static IrBoolExpr sort(IrSetExpr... sets) {
808        List<IrSetExpr> filter = new ArrayList<>(sets.length);
809        boolean fixedCard = true;
810        for (IrSetExpr set : sets) {
811            if (!set.getEnv().isEmpty()) {
812                filter.add(set);
813                fixedCard = fixedCard && set.getCard().size() == 1;
814            }
815        }
816        if (filter.isEmpty()) {
817            return True;
818        }
819        if (filter.size() == 1) {
820            IrDomain env = filter.get(0).getEnv();
821            IrDomain ker = filter.get(0).getKer();
822            if (env.getLowBound() == 0) {
823                int i;
824                for (i = 0; i < env.getHighBound(); i++) {
825                    if (!ker.contains(i)) {
826                        break;
827                    }
828                }
829                if (i == env.getHighBound()) {
830                    // env = [0,1,...,n]
831                    // ker = [0,1,...,n] or [0,1,...,n-1]
832                    return True;
833                }
834            }
835        }
836        if (fixedCard) {
837            List<IrBoolExpr> ands = new ArrayList<>();
838            int i = 0;
839            for (IrSetExpr set : filter) {
840                assert set.getCard().size() == 1;
841                int card = set.getCard().getLowBound();
842                ands.add(equal(set, constant(Util.fromTo(i, i + card))));
843                i += card;
844            }
845            return and(ands);
846        }
847        return new IrSortSets(filter.toArray(new IrSetExpr[filter.size()]), BoolDomain);
848    }
849
850    private static IrBoolExpr sortStrings(IrIntExpr[][] strings, boolean strict) {
851        List<IrIntExpr[]> filterStrings = new ArrayList<>(strings.length);
852        for (int i = 0; i < strings.length - 1; i++) {
853            switch (IrUtil.compareString(strings[i], strings[i + 1])) {
854                case EQ:
855                case LE:
856                    if (!strict) {
857                        break;
858                    }
859                // fallthrough
860                case GT:
861                case GE:
862                case UNKNOWN:
863                    filterStrings.add(strings[i]);
864            }
865        }
866        filterStrings.add(strings[strings.length - 1]);
867        IrIntExpr[][] fstrings = filterStrings.toArray(new IrIntExpr[filterStrings.size()][]);
868
869        if (fstrings.length < 2) {
870            return True;
871        }
872
873        IrIntExpr[] array = new IrIntExpr[fstrings.length];
874        for (int i = 0; i < fstrings.length; i++) {
875            IrIntExpr[] string = fstrings[i];
876            if (string.length != 1) {
877                return new IrSortStrings(fstrings, strict, BoolDomain);
878            }
879            array[i] = fstrings[i][0];
880        }
881        return strict ? sortStrict(array) : sort(array);
882    }
883
884    public static IrBoolExpr sort(IrIntExpr[]... strings) {
885        return sortStrings(strings, false);
886    }
887
888    public static IrBoolExpr sortStrict(IrIntExpr[]... strings) {
889        return sortStrings(strings, true);
890    }
891
892    public static IrBoolExpr sortChannel(IrIntExpr[][] strings, IrIntExpr[] ints) {
893        if (strings.length != ints.length) {
894            throw new IllegalArgumentException();
895        }
896        for (int i = 1; i < strings.length; i++) {
897            if (strings[0].length != strings[i].length) {
898                throw new IllegalArgumentException();
899            }
900        }
901        List<IrIntExpr[]> filterStrings = new ArrayList<>(strings.length);
902        List<IrIntExpr> filterInts = new ArrayList<>(ints.length);
903        for (int i = 0; i < ints.length; i++) {
904            boolean equivalence = false;
905            for (int j = i + 1; j < ints.length; j++) {
906                if (IrUtil.Ordering.EQ.equals(IrUtil.compare(ints[i], ints[j]))
907                        && IrUtil.Ordering.EQ.equals(IrUtil.compareString(strings[i], strings[j]))) {
908                    equivalence = true;
909                    break;
910                }
911            }
912            if (!equivalence) {
913                filterStrings.add(strings[i]);
914                filterInts.add(ints[i]);
915            }
916        }
917        assert !filterInts.isEmpty();
918        if (filterInts.size() == 1) {
919            return equal(filterInts.get(0), 0);
920        }
921        IrIntExpr[][] fstrings = filterStrings.toArray(new IrIntExpr[filterStrings.size()][]);
922        IrIntExpr[] fints = filterInts.toArray(new IrIntExpr[filterInts.size()]);
923        int[] constant = IrUtil.getConstant(fints);
924        if (constant != null) {
925            IrIntExpr[][] partialOrdering = new IrIntExpr[constant.length][];
926            for (int i = 0; i < constant.length; i++) {
927                int val = constant[i];
928                if (val < 0 || val >= constant.length) {
929                    return False;
930                }
931                if (partialOrdering[constant[i]] != null) {
932                    throw new IllegalStateException();
933                }
934                partialOrdering[constant[i]] = fstrings[i];
935            }
936            return sortStrict(partialOrdering);
937        }
938        return new IrSortStringsChannel(fstrings, fints, BoolDomain);
939    }
940
941    public static IrBoolExpr allDifferent(IrIntExpr[] ints) {
942        if (ints.length < 2) {
943            return True;
944        }
945        if (ints.length == 2) {
946            return notEqual(ints[0], ints[1]);
947        }
948        IrDomain domain = ints[0].getDomain();
949        int size = ints[0].getDomain().size();
950        for (int i = 1; i < ints.length; i++) {
951            domain = IrUtil.union(domain, ints[i].getDomain());
952            size += ints[i].getDomain().size();
953            if (size != domain.size()) {
954                return new IrAllDifferent(ints, BoolDomain);
955            }
956        }
957        return True;
958    }
959
960    public static IrBoolExpr selectN(IrBoolExpr[] bools, IrIntExpr n) {
961        if (bools.length == 1) {
962            if (bools[0].equals(n)) {
963                return True;
964            }
965        }
966        boolean entailed = true;
967        IrDomain nDomain = n.getDomain();
968        for (int i = 0; i < bools.length; i++) {
969            Boolean constant = IrUtil.getConstant(bools[i]);
970            if (Boolean.TRUE.equals(constant)) {
971                if (i >= nDomain.getHighBound()) {
972                    return False;
973                }
974                if (i >= nDomain.getLowBound()) {
975                    entailed = false;
976                }
977            } else if (Boolean.FALSE.equals(constant)) {
978                if (i < nDomain.getLowBound()) {
979                    return False;
980                }
981                if (i < nDomain.getHighBound()) {
982                    entailed = false;
983                }
984            } else {
985                entailed = false;
986            }
987        }
988        if (entailed) {
989            return True;
990        }
991        Integer constant = IrUtil.getConstant(n);
992        if (constant != null) {
993            IrBoolExpr[] ands = new IrBoolExpr[bools.length];
994            System.arraycopy(bools, 0, ands, 0, constant.intValue());
995            for (int i = constant.intValue(); i < bools.length; i++) {
996                ands[i] = not(bools[i]);
997            }
998            return and(ands);
999        }
1000        return new IrSelectN(bools, n, BoolDomain);
1001    }
1002
1003    public static IrBoolExpr acyclic(IrIntExpr[] edges) {
1004        return new IrAcyclic(edges, BoolDomain);
1005    }
1006
1007    public static IrBoolExpr unreachable(IrIntExpr[] edges, int from, int to) {
1008        return new IrUnreachable(edges, from, to, BoolDomain);
1009    }
1010
1011    public static IrBoolExpr filterString(IrSetExpr set, IrIntExpr[] string, IrIntExpr[] result) {
1012        if (set.getEnv().isEmpty()) {
1013            return filterString(set, 0, new IrIntExpr[0], result);
1014        }
1015        int offset = set.getEnv().getLowBound();
1016        int end = set.getEnv().getHighBound();
1017        return filterString(set, offset,
1018                Arrays.copyOfRange(string, offset, end + 1),
1019                result);
1020    }
1021
1022    public static IrBoolExpr filterString(IrSetExpr set, int offset, IrIntExpr[] string, IrIntExpr[] result) {
1023        int[] constant = IrUtil.getConstant(set);
1024        if (constant != null) {
1025            IrBoolExpr[] ands = new IrBoolExpr[result.length];
1026            for (int i = 0; i < constant.length; i++) {
1027                ands[i] = equal(string[constant[i] - offset], result[i]);
1028            }
1029            for (int i = constant.length; i < result.length; i++) {
1030                ands[i] = equal(result[i], -1);
1031            }
1032            return and(ands);
1033        }
1034        IrIntExpr[] filterString = Arrays.copyOf(string, string.length);
1035        IrIntExpr[] filterResult = Arrays.copyOf(result, result.length);
1036        TIntIterator iter = set.getEnv().iterator();
1037        int i = 0;
1038        while (iter.hasNext()) {
1039            int env = iter.next();
1040            int x = env - offset;
1041            if (!set.getKer().contains(env) || !filterString[x].equals(filterResult[i])) {
1042                break;
1043            }
1044            filterString[x] = Zero;
1045            filterResult[i] = Zero;
1046            i++;
1047        }
1048        int cut = filterResult.length;
1049        while (cut > 0 && Integer.valueOf(-1).equals(IrUtil.getConstant(filterResult[cut - 1]))) {
1050            cut--;
1051        }
1052        if (cut != filterResult.length) {
1053            filterResult = Arrays.copyOf(filterResult, cut);
1054        }
1055        return new IrFilterString(set, offset, filterString, filterResult, BoolDomain);
1056    }
1057    /**
1058     *******************
1059     *
1060     * Integer
1061     *
1062     *******************
1063     */
1064    public static IrIntVar Zero = False;
1065    public static IrIntVar One = True;
1066
1067    public static IrIntVar domainInt(String name, IrDomain domain) {
1068        if (domain.size() == 1) {
1069            return constant(domain.getLowBound());
1070        }
1071        if (domain instanceof IrBoolDomain) {
1072            return new IrBoolVar(name, (IrBoolDomain) domain);
1073        }
1074        return new IrIntVar(name, domain);
1075    }
1076
1077    public static IrIntVar boundInt(String name, int low, int high) {
1078        return domainInt(name, boundDomain(low, high));
1079    }
1080
1081    public static IrIntVar enumInt(String name, int[] values) {
1082        return domainInt(name, enumDomain(values));
1083    }
1084
1085    public static IrIntVar constant(int value) {
1086        switch (value) {
1087            case 0:
1088                return Zero;
1089            case 1:
1090                return One;
1091            default:
1092                return new IrIntConstant(value);
1093        }
1094    }
1095
1096    public static IrIntExpr minus(IrIntExpr expr) {
1097        Integer constant = IrUtil.getConstant(expr);
1098        if (constant != null) {
1099            return constant(-constant.intValue());
1100        }
1101        if (expr instanceof IrMinus) {
1102            IrMinus minus = (IrMinus) expr;
1103            return minus.getExpr();
1104        }
1105        return new IrMinus(expr, IrUtil.minus(expr.getDomain()));
1106
1107    }
1108
1109    public static IrIntExpr card(IrSetExpr set) {
1110        IrDomain domain = set.getCard();
1111        if (domain.size() == 1) {
1112            return constant(domain.getLowBound());
1113        }
1114        return new IrCard(set, domain);
1115    }
1116
1117    public static IrIntExpr add(int addend1, IrIntExpr addend2) {
1118        return add(constant(addend1), addend2);
1119    }
1120
1121    public static IrIntExpr add(IrIntExpr addend1, int addend2) {
1122        return add(addend1, constant(addend2));
1123    }
1124
1125    public static IrIntExpr add(Collection<? extends IrIntExpr> addends) {
1126        return add(addends.toArray(new IrIntExpr[addends.size()]));
1127    }
1128
1129    public static IrIntExpr add(IrIntExpr... addends) {
1130        int constants = 0;
1131        List<IrIntExpr> filter = new ArrayList<>(addends.length);
1132        for (IrIntExpr addend : addends) {
1133            if (addend instanceof IrAdd) {
1134                IrAdd add = (IrAdd) addend;
1135                // Invariant: No nested IrAdd or constants
1136                filter.addAll(Arrays.asList(add.getAddends()));
1137                constants += add.getOffset();
1138            } else {
1139                Integer constant = IrUtil.getConstant(addend);
1140                if (constant != null) {
1141                    constants += constant.intValue();
1142                } else {
1143                    filter.add(addend);
1144                }
1145            }
1146        }
1147        if (filter.isEmpty()) {
1148            return constant(constants);
1149        }
1150        if (filter.size() == 1) {
1151            IrIntExpr first = filter.get(0);
1152            if (constants == 0) {
1153                return first;
1154            }
1155            return new IrAdd(new IrIntExpr[]{first}, constants,
1156                    IrUtil.offset(first.getDomain(), constants));
1157        }
1158        int low = constants;
1159        int high = constants;
1160        for (IrIntExpr addend : filter) {
1161            low += addend.getDomain().getLowBound();
1162            high += addend.getDomain().getHighBound();
1163        }
1164        IrDomain domain = boundDomain(low, high);
1165        return new IrAdd(filter.toArray(new IrIntExpr[filter.size()]), constants, domain);
1166    }
1167
1168    public static IrIntExpr sub(int minuend, IrIntExpr subtrahend) {
1169        return sub(constant(minuend), subtrahend);
1170    }
1171
1172    public static IrIntExpr sub(IrIntExpr minuend, int subtrahend) {
1173        return sub(minuend, constant(subtrahend));
1174    }
1175
1176    public static IrIntExpr sub(Collection<? extends IrIntExpr> subtrahends) {
1177        return sub(subtrahends.toArray(new IrIntExpr[subtrahends.size()]));
1178    }
1179
1180    public static IrIntExpr sub(IrIntExpr... subtrahends) {
1181        if (subtrahends.length == 0) {
1182            return Zero;
1183        }
1184        IrIntExpr[] flip = new IrIntExpr[subtrahends.length];
1185        flip[0] = subtrahends[0];
1186        for (int i = 1; i < flip.length; i++) {
1187            flip[i] = minus(subtrahends[i]);
1188        }
1189        return add(flip);
1190    }
1191
1192    public static IrIntExpr mul(int multiplicand, IrIntExpr multiplier) {
1193        return mul(constant(multiplicand), multiplier);
1194    }
1195
1196    public static IrIntExpr mul(IrIntExpr multiplicand, int multiplier) {
1197        return mul(multiplicand, constant(multiplier));
1198    }
1199
1200    public static IrIntExpr mul(IrIntExpr multiplicand, IrIntExpr multiplier) {
1201        Integer multiplicandConstant = IrUtil.getConstant(multiplicand);
1202        Integer multiplierConstant = IrUtil.getConstant(multiplier);
1203        if (multiplicandConstant != null) {
1204            switch (multiplicandConstant.intValue()) {
1205                case 0:
1206                    return multiplicand;
1207                case 1:
1208                    return multiplier;
1209            }
1210        }
1211        if (multiplierConstant != null) {
1212            switch (multiplierConstant.intValue()) {
1213                case 0:
1214                    return multiplier;
1215                case 1:
1216                    return multiplicand;
1217            }
1218        }
1219        if (multiplicandConstant != null && multiplierConstant != null) {
1220            return constant(multiplicandConstant.intValue() * multiplierConstant.intValue());
1221        }
1222        int low1 = multiplicand.getDomain().getLowBound();
1223        int high1 = multiplicand.getDomain().getHighBound();
1224        int low2 = multiplier.getDomain().getLowBound();
1225        int high2 = multiplier.getDomain().getHighBound();
1226        int min = Util.min(low1 * low2, low1 * high2, high1 * low2, high1 * high2);
1227        int max = Util.max(low1 * low2, low1 * high2, high1 * low2, high1 * high2);
1228        return new IrMul(multiplicand, multiplier, boundDomain(min, max));
1229    }
1230
1231    public static IrIntExpr div(int dividend, IrIntExpr divisor) {
1232        return div(constant(dividend), divisor);
1233    }
1234
1235    public static IrIntExpr div(IrIntExpr dividend, int divisor) {
1236        return div(dividend, constant(divisor));
1237    }
1238
1239    public static IrIntExpr div(IrIntExpr dividend, IrIntExpr divisor) {
1240        Integer dividendConstant = IrUtil.getConstant(dividend);
1241        Integer divisorConstant = IrUtil.getConstant(divisor);
1242        if (dividendConstant != null && dividendConstant.intValue() == 0) {
1243            return dividend;
1244        }
1245        if (divisorConstant != null && divisorConstant.intValue() == 1) {
1246            return dividend;
1247        }
1248        if (dividendConstant != null && divisorConstant != null) {
1249            return constant(dividendConstant.intValue() / divisorConstant.intValue());
1250        }
1251        int low1 = dividend.getDomain().getLowBound();
1252        int high1 = dividend.getDomain().getHighBound();
1253        int low2 = divisor.getDomain().getLowBound();
1254        int high2 = divisor.getDomain().getHighBound();
1255        int min = Util.min(low1, -low1, high1, -high1);
1256        int max = Util.max(low1, -low1, high1, -high1);
1257        return new IrDiv(dividend, divisor, boundDomain(min, max));
1258    }
1259
1260    public static IrIntExpr element(IrIntExpr[] array, IrIntExpr index) {
1261        IrIntExpr[] $array = index.getDomain().getHighBound() + 1 < array.length
1262                ? Arrays.copyOf(array, index.getDomain().getHighBound() + 1)
1263                : array.clone();
1264        for (int i = 0; i < $array.length; i++) {
1265            if (!index.getDomain().contains(i)) {
1266                $array[i] = Zero;
1267            }
1268        }
1269
1270        Integer constant = IrUtil.getConstant(index);
1271        if (constant != null) {
1272            return $array[constant.intValue()];
1273        }
1274        TIntIterator iter = index.getDomain().iterator();
1275        assert iter.hasNext();
1276
1277        IrDomain domain = $array[iter.next()].getDomain();
1278        int low = domain.getLowBound();
1279        int high = domain.getHighBound();
1280        while (iter.hasNext()) {
1281            int val = iter.next();
1282            if (val < $array.length) {
1283                domain = $array[val].getDomain();
1284                low = Math.min(low, domain.getLowBound());
1285                high = Math.max(high, domain.getHighBound());
1286            }
1287        }
1288        domain = boundDomain(low, high);
1289        return new IrElement($array, index, domain);
1290    }
1291
1292    public static IrIntExpr count(int value, IrIntExpr[] array) {
1293        List<IrIntExpr> filter = new ArrayList<>();
1294        int count = 0;
1295        for (IrIntExpr i : array) {
1296            Integer constant = IrUtil.getConstant(i);
1297            if (constant != null) {
1298                if (constant.intValue() == value) {
1299                    count++;
1300                }
1301            } else if (i.getDomain().contains(value)) {
1302                filter.add(i);
1303            }
1304        }
1305        switch (filter.size()) {
1306            case 0:
1307                return constant(count);
1308            case 1:
1309                return add(equal(value, filter.get(0)), count);
1310            default:
1311                return add(
1312                        new IrCount(value, filter.toArray(new IrIntExpr[filter.size()]), boundDomain(0, filter.size())),
1313                        count);
1314        }
1315    }
1316
1317    public static IrIntExpr sum(IrSetExpr set) {
1318        int sum = Util.sum(set.getKer().iterator());
1319        int count = set.getKer().size();
1320
1321        // Calculate low
1322        int low = sum;
1323        int lowCount = count;
1324        TIntIterator envIter = set.getEnv().iterator();
1325        while (lowCount < set.getCard().getHighBound() && envIter.hasNext()) {
1326            int env = envIter.next();
1327            if (env >= 0 && lowCount >= set.getCard().getLowBound()) {
1328                break;
1329            }
1330            if (!set.getKer().contains(env)) {
1331                low += env;
1332                lowCount++;
1333            }
1334        }
1335
1336        // Calculate high
1337        int high = sum;
1338        int highCount = count;
1339        envIter = set.getEnv().iterator(false);
1340        while (highCount < set.getCard().getHighBound() && envIter.hasNext()) {
1341            int env = envIter.next();
1342            if (env <= 0 && highCount >= set.getCard().getLowBound()) {
1343                break;
1344            }
1345            if (!set.getKer().contains(env)) {
1346                high += env;
1347                highCount++;
1348            }
1349        }
1350
1351        return new IrSetSum(set, boundDomain(low, high));
1352    }
1353
1354    public static IrIntExpr ternary(IrBoolExpr antecedent, IrIntExpr consequent, IrIntExpr alternative) {
1355        if (IrUtil.isTrue(antecedent)) {
1356            return consequent;
1357        }
1358        if (IrUtil.isFalse(antecedent)) {
1359            return alternative;
1360        }
1361        if (consequent.equals(alternative)) {
1362            return consequent;
1363        }
1364        Integer consequentConstant = IrUtil.getConstant(consequent);
1365        Integer alternativeConstant = IrUtil.getConstant(alternative);
1366        if (consequentConstant != null && consequentConstant.equals(alternativeConstant)) {
1367            return constant(consequentConstant);
1368        }
1369        IrDomain domain = IrUtil.union(consequent.getDomain(), alternative.getDomain());
1370        return new IrTernary(antecedent, consequent, alternative, domain);
1371    }
1372
1373    /**
1374     *******************
1375     *
1376     * Set
1377     *
1378     *******************
1379     */
1380    public static IrSetVar set(String name, int lowEnv, int highEnv) {
1381        return set(name, boundDomain(lowEnv, highEnv));
1382    }
1383
1384    public static IrSetVar set(String name, int lowEnv, int highEnv, int lowKer, int highKer) {
1385        return set(name, boundDomain(lowEnv, highEnv), boundDomain(lowKer, highKer));
1386    }
1387
1388    public static IrSetVar set(String name, int lowEnv, int highEnv, int[] ker) {
1389        return set(name, boundDomain(lowEnv, highEnv), enumDomain(ker));
1390    }
1391
1392    public static IrSetVar set(String name, int[] env) {
1393        return set(name, enumDomain(env));
1394    }
1395
1396    public static IrSetVar set(String name, int[] env, int lowKer, int highKer) {
1397        return set(name, enumDomain(env), boundDomain(lowKer, highKer));
1398    }
1399
1400    public static IrSetVar set(String name, int[] env, int[] ker) {
1401        return set(name, enumDomain(env), enumDomain(ker));
1402    }
1403
1404    public static IrSetVar set(String name, IrDomain env) {
1405        return set(name, env, EmptyDomain);
1406    }
1407
1408    public static IrSetVar set(String name, IrDomain env, IrDomain ker) {
1409        return set(name, env, ker, boundDomain(ker.size(), env.size()));
1410    }
1411
1412    public static IrSetVar set(String name, IrDomain env, IrDomain ker, IrDomain card) {
1413        return IrUtil.asConstant(new IrSetVar(name, env, ker, card));
1414    }
1415
1416    public static IrSetVar constant(int[] value) {
1417        return constant(enumDomain(value));
1418    }
1419
1420    public static IrSetVar constant(TIntCollection value) {
1421        return constant(enumDomain(value));
1422    }
1423
1424    public static IrSetVar constant(TIntSet value) {
1425        return constant(enumDomain(value));
1426    }
1427
1428    public static IrSetVar constant(IrDomain value) {
1429        if (value.isEmpty()) {
1430            return EmptySet;
1431        }
1432        return new IrSetConstant(value);
1433    }
1434
1435    public static IrSetExpr singleton(IrIntExpr value) {
1436        Integer constant = IrUtil.getConstant(value);
1437        if (constant != null) {
1438            return constant(new int[]{constant.intValue()});
1439        }
1440        return new IrSingleton(value, value.getDomain(), EmptyDomain);
1441    }
1442
1443    public static IrSetExpr arrayToSet(IrIntExpr[] array, Integer globalCardinality) {
1444        switch (array.length) {
1445            case 0:
1446                return EmptySet;
1447            case 1:
1448                return singleton(array[0]);
1449            default:
1450                IrDomain env = array[0].getDomain();
1451                for (int i = 1; i < array.length; i++) {
1452                    env = IrUtil.union(env, array[i].getDomain());
1453                }
1454                TIntSet values = new TIntHashSet();
1455                for (IrIntExpr i : array) {
1456                    Integer constant = IrUtil.getConstant(i);
1457                    if (constant != null) {
1458                        values.add(constant.intValue());
1459                    }
1460                }
1461                IrDomain ker = enumDomain(values);
1462                int lowCard = Math.max(
1463                        globalCardinality == null ? 1 : divRoundUp(array.length, globalCardinality),
1464                        ker.size());
1465                int highCard = Math.min(array.length, env.size());
1466                IrDomain card = boundDomain(lowCard, highCard);
1467                return IrUtil.asConstant(new IrArrayToSet(array, env, ker, card, globalCardinality));
1468        }
1469    }
1470
1471    /**
1472     * Relational join.
1473     *
1474     * Union{for all i in take} children[i]
1475     *
1476     * @param take
1477     * @param children
1478     * @param injective
1479     * @return the join expression take.children
1480     */
1481    public static IrSetExpr joinRelation(IrSetExpr take, IrSetExpr[] children, boolean injective) {
1482        if (take.getEnv().isEmpty()) {
1483            return EmptySet;
1484        }
1485        IrSetExpr[] $children = take.getEnv().getHighBound() + 1 < children.length
1486                ? Arrays.copyOf(children, take.getEnv().getHighBound() + 1)
1487                : children.clone();
1488        for (int i = 0; i < $children.length; i++) {
1489            if (!take.getEnv().contains(i)) {
1490                $children[i] = EmptySet;
1491            }
1492        }
1493
1494        IrIntExpr[] ints = IrUtil.asInts(children);
1495        if (ints != null) {
1496            return joinFunction(take, ints, injective ? 1 : 0);
1497        }
1498
1499        int[] constant = IrUtil.getConstant(take);
1500        if (constant != null) {
1501            IrSetExpr[] to = new IrSetExpr[constant.length];
1502            for (int i = 0; i < to.length; i++) {
1503                to[i] = $children[constant[i]];
1504            }
1505            return union(to, injective);
1506        }
1507
1508        // Compute env
1509        TIntIterator iter = take.getEnv().iterator();
1510        IrDomain env;
1511        if (iter.hasNext()) {
1512            IrDomain domain = $children[iter.next()].getEnv();
1513            while (iter.hasNext()) {
1514                domain = IrUtil.union(domain, $children[iter.next()].getEnv());
1515            }
1516            env = domain;
1517        } else {
1518            env = EmptyDomain;
1519        }
1520
1521        // Compute ker
1522        iter = take.getKer().iterator();
1523        IrDomain ker;
1524        if (iter.hasNext()) {
1525            IrDomain domain = $children[iter.next()].getKer();
1526            while (iter.hasNext()) {
1527                domain = IrUtil.union(domain, $children[iter.next()].getKer());
1528            }
1529            ker = domain;
1530        } else {
1531            ker = EmptyDomain;
1532        }
1533
1534        // Compute card
1535        IrDomain takeEnv = take.getEnv();
1536        IrDomain takeKer = take.getKer();
1537        IrDomain takeCard = take.getCard();
1538        int index = 0;
1539        int[] childrenLowCards = new int[takeEnv.size() - takeKer.size()];
1540        int[] childrenHighCards = new int[takeEnv.size() - takeKer.size()];
1541        int cardLow = 0, cardHigh = 0;
1542
1543        iter = takeEnv.iterator();
1544        while (iter.hasNext()) {
1545            int val = iter.next();
1546            IrDomain childDomain = $children[val].getCard();
1547            if (takeKer.contains(val)) {
1548                cardLow = injective
1549                        ? cardLow + childDomain.getLowBound()
1550                        : Math.max(cardLow, childDomain.getLowBound());
1551                cardHigh = injective
1552                        ? cardHigh + childDomain.getHighBound()
1553                        : Math.max(cardHigh, childDomain.getHighBound());
1554            } else {
1555                childrenLowCards[index] = childDomain.getLowBound();
1556                childrenHighCards[index] = childDomain.getHighBound();
1557                index++;
1558            }
1559        }
1560        assert index == childrenLowCards.length;
1561        assert index == childrenHighCards.length;
1562
1563        Arrays.sort(childrenLowCards);
1564        Arrays.sort(childrenHighCards);
1565
1566        for (int i = 0; i < takeCard.getLowBound() - takeKer.size(); i++) {
1567            cardLow = injective
1568                    ? cardLow + childrenLowCards[i]
1569                    : Math.max(cardLow, childrenLowCards[i]);
1570        }
1571        for (int i = 0; i < takeCard.getHighBound() - takeKer.size(); i++) {
1572            cardHigh = injective
1573                    ? cardHigh + childrenHighCards[childrenHighCards.length - 1 - i]
1574                    : Math.max(cardHigh, childrenHighCards[childrenHighCards.length - 1 - i]);
1575        }
1576        cardLow = Math.max(cardLow, ker.size());
1577        cardHigh = Math.min(cardHigh, env.size());
1578        IrDomain card = boundDomain(cardLow, cardHigh);
1579
1580        return new IrJoinRelation(take, $children, env, ker, card, injective);
1581    }
1582
1583    public static IrSetExpr joinFunction(IrSetExpr take, IrIntExpr[] refs, Integer globalCardinality) {
1584        if (take.getEnv().isEmpty()) {
1585            return EmptySet;
1586        }
1587        IrIntExpr[] $refs = take.getEnv().getHighBound() + 1 < refs.length
1588                ? Arrays.copyOf(refs, take.getEnv().getHighBound() + 1)
1589                : refs.clone();
1590        for (int i = 0; i < $refs.length; i++) {
1591            if (!take.getEnv().contains(i)) {
1592                $refs[i] = Zero;
1593            }
1594        }
1595
1596        int[] constant = IrUtil.getConstant(take);
1597        if (constant != null) {
1598            IrIntExpr[] to = new IrIntExpr[constant.length];
1599            for (int i = 0; i < to.length; i++) {
1600                to[i] = $refs[constant[i]];
1601            }
1602            return arrayToSet(to, globalCardinality);
1603        }
1604
1605        // Compute env
1606        TIntIterator iter = take.getEnv().iterator();
1607        IrDomain env;
1608        if (iter.hasNext()) {
1609            IrDomain domain = $refs[iter.next()].getDomain();
1610            while (iter.hasNext()) {
1611                domain = IrUtil.union(domain, $refs[iter.next()].getDomain());
1612            }
1613            env = domain;
1614        } else {
1615            env = EmptyDomain;
1616        }
1617
1618        // Compute ker
1619        iter = take.getKer().iterator();
1620        TIntHashSet values = new TIntHashSet(0);
1621        while (iter.hasNext()) {
1622            Integer constantRef = IrUtil.getConstant($refs[iter.next()]);
1623            if (constantRef != null) {
1624                values.add(constantRef.intValue());
1625            }
1626        }
1627        IrDomain ker = values.isEmpty() ? EmptyDomain : new IrEnumDomain(values.toArray());
1628
1629        // Compute card
1630        IrDomain takeCard = take.getCard();
1631        int lowTakeCard = takeCard.getLowBound();
1632        int highTakeCard = takeCard.getHighBound();
1633        IrDomain card;
1634        if (globalCardinality == null) {
1635            card = lowTakeCard == 0
1636                    ? boundDomain(Math.max(0, ker.size()), Math.min(highTakeCard, env.size()))
1637                    : boundDomain(Math.max(1, ker.size()), Math.min(highTakeCard, env.size()));
1638        } else {
1639            card = boundDomain(
1640                    divRoundUp(Math.max(lowTakeCard, ker.size()), globalCardinality),
1641                    Math.min(highTakeCard, env.size()));
1642        }
1643
1644        return new IrJoinFunction(take, $refs, env, ker, card, globalCardinality);
1645    }
1646
1647    private static int divRoundUp(int a, int b) {
1648        assert a >= 0;
1649        assert b > 0;
1650
1651        return (a + b - 1) / b;
1652    }
1653
1654    public static IrSetExpr difference(IrSetExpr minuend, IrSetExpr subtrahend) {
1655        IrDomain env = IrUtil.difference(minuend.getEnv(), subtrahend.getKer());
1656        IrDomain ker = IrUtil.difference(minuend.getKer(), subtrahend.getEnv());
1657        int low = Math.max(0, minuend.getCard().getLowBound() - subtrahend.getCard().getHighBound());
1658        int high = minuend.getCard().getHighBound();
1659        IrDomain card = boundDomain(Math.max(low, ker.size()), Math.min(high, env.size()));
1660        return new IrSetDifference(minuend, subtrahend, env, ker, card);
1661    }
1662
1663    public static IrSetExpr intersection(IrSetExpr... operands) {
1664        List<IrSetExpr> flatten = new ArrayList<>(operands.length);
1665        for (IrSetExpr operand : operands) {
1666            if (operand instanceof IrSetIntersection) {
1667                // Invariant: No nested IrSetIntersection
1668                flatten.addAll(Arrays.asList(((IrSetIntersection) operand).getOperands()));
1669            } else {
1670                flatten.add(operand);
1671            }
1672        }
1673        TIntSet constants = null;
1674        List<IrSetExpr> filter = new ArrayList<>();
1675        for (IrSetExpr operand : flatten) {
1676            int[] constant = IrUtil.getConstant(operand);
1677            if (constant == null) {
1678                filter.add(operand);
1679            } else {
1680                if (constants == null) {
1681                    constants = new TIntHashSet(constant);
1682                } else {
1683                    constants.retainAll(constant);
1684                }
1685            }
1686        }
1687        if (constants != null) {
1688            filter.add(constant(constants));
1689        }
1690        IrSetExpr[] ops = filter.toArray(new IrSetExpr[filter.size()]);
1691        switch (ops.length) {
1692            case 0:
1693                return EmptySet;
1694            case 1:
1695                return ops[0];
1696            default:
1697                IrDomain env = IrUtil.intersectionEnvs(ops);
1698                IrDomain ker = IrUtil.intersectionKers(ops);
1699                int low = 0;
1700                int high = ops[0].getCard().getHighBound();
1701                for (int i = 1; i < ops.length; i++) {
1702                    high = Math.max(high, ops[0].getCard().getHighBound());
1703                }
1704                IrDomain card = boundDomain(
1705                        Math.max(low, ker.size()),
1706                        Math.min(high, env.size()));
1707                return new IrSetIntersection(ops, env, ker, card);
1708        }
1709    }
1710
1711    public static IrSetExpr union(IrSetExpr... operands) {
1712        return union(operands, false);
1713    }
1714
1715    public static IrSetExpr union(IrSetExpr[] operands, boolean disjoint) {
1716        List<IrSetExpr> flatten = new ArrayList<>(operands.length);
1717        for (IrSetExpr operand : operands) {
1718            if (operand instanceof IrSetUnion) {
1719                // Invariant: No nested IrSetUnion
1720                flatten.addAll(Arrays.asList(((IrSetUnion) operand).getOperands()));
1721            } else {
1722                flatten.add(operand);
1723            }
1724        }
1725        TIntSet constants = new TIntHashSet();
1726        List<IrSetExpr> filter = new ArrayList<>();
1727        for (IrSetExpr operand : flatten) {
1728            int[] constant = IrUtil.getConstant(operand);
1729            if (constant == null) {
1730                filter.add(operand);
1731            } else {
1732                constants.addAll(constant);
1733            }
1734        }
1735        if (!constants.isEmpty()) {
1736            filter.add(constant(constants));
1737        }
1738        IrSetExpr[] ops = filter.toArray(new IrSetExpr[filter.size()]);
1739        switch (ops.length) {
1740            case 0:
1741                return EmptySet;
1742            case 1:
1743                return ops[0];
1744            default:
1745                IrDomain env = IrUtil.unionEnvs(ops);
1746                IrDomain ker = IrUtil.unionKers(ops);
1747                IrDomain operandCard = ops[0].getCard();
1748                int low = operandCard.getLowBound();
1749                int high = operandCard.getHighBound();
1750                for (int i = 1; i < ops.length; i++) {
1751                    operandCard = ops[i].getCard();
1752                    low = disjoint
1753                            ? low + operandCard.getLowBound()
1754                            : Math.max(low, operandCard.getLowBound());
1755                    high += operandCard.getHighBound();
1756                }
1757                IrDomain card = boundDomain(
1758                        Math.max(low, ker.size()),
1759                        Math.min(high, env.size()));
1760                return IrUtil.asConstant(new IrSetUnion(ops, env, ker, card, disjoint));
1761        }
1762    }
1763
1764    public static IrSetExpr offset(IrSetExpr set, int offset) {
1765        if (offset == 0) {
1766            return set;
1767        }
1768        if (set instanceof IrOffset) {
1769            IrOffset nested = (IrOffset) set;
1770            return offset(nested.getSet(), offset + nested.getOffset());
1771        }
1772        IrDomain env = IrUtil.offset(set.getEnv(), offset);
1773        IrDomain ker = IrUtil.offset(set.getKer(), offset);
1774        IrDomain card = set.getCard();
1775        return IrUtil.asConstant(new IrOffset(set, offset, env, ker, card));
1776    }
1777
1778    public static IrSetExpr mask(IrSetExpr set, int from, int to) {
1779        if (from > to) {
1780            throw new IllegalArgumentException();
1781        }
1782
1783        if (from <= set.getEnv().getLowBound() && to > set.getEnv().getHighBound()) {
1784            return offset(set, -from);
1785        }
1786        IrDomain env = IrUtil.mask(set.getEnv(), from, to);
1787        IrDomain ker = IrUtil.mask(set.getKer(), from, to);
1788        IrDomain card = boundDomain(ker.size(), Math.min(env.size(), set.getCard().getHighBound()));
1789        return IrUtil.asConstant(new IrMask(set, from, to, env, ker, card));
1790    }
1791
1792    public static IrSetExpr ternary(IrBoolExpr antecedent, IrSetExpr consequent, IrSetExpr alternative) {
1793        if (IrUtil.isTrue(antecedent)) {
1794            return consequent;
1795        }
1796        if (IrUtil.isFalse(antecedent)) {
1797            return alternative;
1798        }
1799        if (consequent.equals(alternative)) {
1800            return consequent;
1801        }
1802        IrDomain env = IrUtil.union(consequent.getEnv(), alternative.getEnv());
1803        IrDomain ker = IrUtil.intersection(consequent.getKer(), alternative.getKer());
1804        IrDomain card = IrUtil.union(consequent.getCard(), alternative.getCard());
1805        return new IrSetTernary(antecedent, consequent, alternative, env, ker, card);
1806    }
1807}