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}