Source code

001package org.clafer.ir.compiler;
002
003import gnu.trove.set.hash.TIntHashSet;
004import java.util.ArrayList;
005import java.util.Arrays;
006import java.util.Collections;
007import java.util.HashMap;
008import java.util.HashSet;
009import java.util.List;
010import java.util.Map;
011import java.util.Map.Entry;
012import java.util.Set;
013import org.clafer.choco.constraint.Constraints;
014import org.clafer.collection.Pair;
015import org.clafer.collection.Triple;
016import org.clafer.common.Check;
017import org.clafer.common.Util;
018import org.clafer.ir.IrAcyclic;
019import org.clafer.ir.IrAdd;
020import org.clafer.ir.IrAllDifferent;
021import org.clafer.ir.IrAnd;
022import org.clafer.ir.IrArrayToSet;
023import org.clafer.ir.IrBoolChannel;
024import org.clafer.ir.IrBoolDomain;
025import org.clafer.ir.IrBoolExpr;
026import org.clafer.ir.IrBoolExprVisitor;
027import org.clafer.ir.IrBoolVar;
028import org.clafer.ir.IrCard;
029import org.clafer.ir.IrCompare;
030import org.clafer.ir.IrCount;
031import org.clafer.ir.IrDiv;
032import org.clafer.ir.IrDomain;
033import org.clafer.ir.IrElement;
034import org.clafer.ir.IrExpr;
035import org.clafer.ir.IrFilterString;
036import org.clafer.ir.IrIfOnlyIf;
037import org.clafer.ir.IrIfThenElse;
038import org.clafer.ir.IrImplies;
039import org.clafer.ir.IrIntChannel;
040import org.clafer.ir.IrIntConstant;
041import org.clafer.ir.IrIntExpr;
042import org.clafer.ir.IrIntExprVisitor;
043import org.clafer.ir.IrIntVar;
044import org.clafer.ir.IrJoinFunction;
045import org.clafer.ir.IrJoinRelation;
046import org.clafer.ir.IrLone;
047import org.clafer.ir.IrMask;
048import org.clafer.ir.IrMember;
049import org.clafer.ir.IrMinus;
050import org.clafer.ir.IrModule;
051import org.clafer.ir.IrMul;
052import org.clafer.ir.IrNot;
053import org.clafer.ir.IrNotImplies;
054import org.clafer.ir.IrNotMember;
055import org.clafer.ir.IrNotWithin;
056import org.clafer.ir.IrOffset;
057import org.clafer.ir.IrOne;
058import org.clafer.ir.IrOr;
059import org.clafer.ir.IrSelectN;
060import org.clafer.ir.IrSetDifference;
061import org.clafer.ir.IrSetExpr;
062import org.clafer.ir.IrSetExprVisitor;
063import org.clafer.ir.IrSetIntersection;
064import org.clafer.ir.IrSetSum;
065import org.clafer.ir.IrSetTernary;
066import org.clafer.ir.IrSetTest;
067import org.clafer.ir.IrSetUnion;
068import org.clafer.ir.IrSetVar;
069import org.clafer.ir.IrSingleton;
070import org.clafer.ir.IrSortSets;
071import org.clafer.ir.IrSortStrings;
072import org.clafer.ir.IrSortStringsChannel;
073import org.clafer.ir.IrSubsetEq;
074import org.clafer.ir.IrTernary;
075import org.clafer.ir.IrUnreachable;
076import org.clafer.ir.IrUtil;
077import org.clafer.ir.IrVar;
078import org.clafer.ir.IrWithin;
079import org.clafer.ir.IrXor;
080import org.clafer.ir.analysis.AnalysisUtil;
081import org.clafer.ir.analysis.Canonicalizer;
082import org.clafer.ir.analysis.Coalescer;
083import org.clafer.ir.analysis.CommonSubexpression;
084import org.clafer.ir.analysis.DuplicateConstraints;
085import org.clafer.ir.analysis.Optimizer;
086import solver.Solver;
087import solver.constraints.Constraint;
088import solver.constraints.ICF;
089import solver.constraints.Operator;
090import solver.constraints.set.SCF;
091import solver.variables.BoolVar;
092import solver.variables.IntVar;
093import solver.variables.SetVar;
094import solver.variables.VF;
095import solver.variables.view.SetConstantView;
096
097/**
098 * Compile from IR to Choco.
099 *
100 * @author jimmy
101 */
102public class IrCompiler {
103
104    private final Solver solver;
105    private final boolean coalesceVariables;
106    private int varNum = 0;
107
108    private IrCompiler(Solver solver, boolean coalesceVariables) {
109        this.solver = Check.notNull(solver);
110        this.coalesceVariables = coalesceVariables;
111    }
112
113    public static IrSolutionMap compile(IrModule in, Solver out) {
114        return compile(in, out, true);
115    }
116
117    public static IrSolutionMap compile(IrModule in, Solver out, boolean coalesceVariables) {
118        IrCompiler compiler = new IrCompiler(out, coalesceVariables);
119        return compiler.compile(in);
120    }
121
122    private IrSolutionMap compile(IrModule module) {
123        IrModule optModule = Optimizer.optimize(Canonicalizer.canonical(module));
124
125        List<IrBoolExpr> constraints = optModule.getConstraints();
126        Map<IrIntVar, IrIntVar> coalescedIntVars = Collections.emptyMap();
127        Map<IrSetVar, IrSetVar> coalescedSetVars = Collections.emptyMap();
128        if (coalesceVariables) {
129            Triple<Map<IrIntVar, IrIntVar>, Map<IrSetVar, IrSetVar>, IrModule> coalesceTriple = Coalescer.coalesce(optModule);
130            coalescedIntVars = coalesceTriple.getFst();
131            coalescedSetVars = coalesceTriple.getSnd();
132            optModule = coalesceTriple.getThd();
133            while (!coalesceTriple.getFst().isEmpty()
134                    || !coalesceTriple.getSnd().isEmpty()) {
135                coalesceTriple = Coalescer.coalesce(optModule);
136                coalescedIntVars = compose(coalescedIntVars, coalesceTriple.getFst());
137                coalescedSetVars = compose(coalescedSetVars, coalesceTriple.getSnd());
138                optModule = coalesceTriple.getThd();
139            }
140            optModule = DuplicateConstraints.removeDuplicates(optModule);
141
142            constraints = new ArrayList<>(optModule.getConstraints().size());
143            for (IrBoolExpr constraint : optModule.getConstraints()) {
144                Pair<IrIntExpr, IrSetVar> cardinality = AnalysisUtil.getAssignCardinality(constraint);
145                if (cardinality != null && cardinality.getFst() instanceof IrIntVar) {
146                    IrIntVar leftInt = (IrIntVar) cardinality.getFst();
147                    SetVar rightSet = getSetVar(cardinality.getSnd());
148
149                    CSet duplicate = cardIntVarMap.get(leftInt);
150                    if (duplicate == null) {
151                        cardIntVarMap.put(leftInt,
152                                new CSet(rightSet,
153                                IrUtil.intersection(leftInt.getDomain(), cardinality.getSnd().getCard())));
154                    } else {
155                        /*
156                         * Case where
157                         *     c = |A|
158                         *     c = |B|
159                         */
160                        cardIntVarMap.put(leftInt, new CSet(rightSet, duplicate.getCard()));
161                        post(SCF.cardinality(rightSet, duplicate.getCard()));
162                    }
163                } else {
164                    constraints.add(constraint);
165                }
166            }
167        }
168
169        commonSubexpressions.addAll(CommonSubexpression.findCommonSubexpressions(optModule));
170
171        for (IrBoolExpr constraint : constraints) {
172            post(compileAsConstraint(constraint));
173        }
174        for (IrVar variable : optModule.getVariables()) {
175            if (variable instanceof IrBoolVar) {
176                compile((IrBoolVar) variable);
177            } else if (variable instanceof IrIntVar) {
178                compile((IrIntVar) variable);
179            } else {
180                compile((IrSetVar) variable);
181            }
182        }
183        return new IrSolutionMap(
184                coalescedIntVars, intVarMap,
185                coalescedSetVars, setVarMap);
186    }
187
188    private static <T> Map<T, T> compose(Map<T, T> f1, Map<T, T> f2) {
189        if (f1.isEmpty()) {
190            return f2;
191        }
192        if (f2.isEmpty()) {
193            return f1;
194        }
195        Map<T, T> composed = new HashMap<>(f1.size() + f2.size());
196        composed.putAll(f2);
197        for (Entry<T, T> e : f1.entrySet()) {
198            T key = e.getKey();
199            T value = f2.get(e.getValue());
200            if (value == null) {
201                value = e.getValue();
202            }
203            composed.put(key, value);
204        }
205        return composed;
206    }
207    private final Map<TIntHashSet, SetVar> cachedSetConstants = new HashMap<>();
208    private final Map<SetVar, IntVar> cachedSetCardVars = new HashMap<>();
209    private final Map<IntVar, IntVar> cachedMinus = new HashMap<>();
210    private final Map<Pair<IntVar, Integer>, IntVar> cachedOffset = new HashMap<>();
211    private final Set<IrExpr> commonSubexpressions = new HashSet<>();
212    private final Map<IrIntExpr, IntVar> cachedCommonIntSubexpressions = new HashMap<>();
213    private final Map<IrSetExpr, CSet> cachedCommonSetSubexpressions = new HashMap<>();
214
215    private void post(Constraint constraint) {
216        if (!solver.TRUE.equals(constraint)) {
217            solver.post(constraint);
218        }
219    }
220
221    private BoolVar boolVar(String name, IrBoolDomain domain) {
222        switch (domain) {
223            case TrueDomain:
224                return VF.one(solver);
225            case FalseDomain:
226                return VF.zero(solver);
227            default:
228                return VF.bool(name, solver);
229        }
230    }
231
232    private IntVar intVar(String name, IrDomain domain) {
233        if (domain.size() == 1) {
234            int constant = domain.getLowBound();
235            switch (domain.getLowBound()) {
236                case 0:
237                    return VF.zero(solver);
238                case 1:
239                    return VF.one(solver);
240                default:
241                    return VF.fixed(constant, solver);
242            }
243        }
244        if (domain.getLowBound() == 0 && domain.getHighBound() == 1) {
245            return VF.bool(name, solver);
246        }
247        if (domain.isBounded()) {
248            return VF.enumerated(name, domain.getLowBound(), domain.getHighBound(), solver);
249        }
250        return VF.enumerated(name, domain.getValues(), solver);
251    }
252
253    private SetVar setVar(String name, IrDomain env, IrDomain ker) {
254        assert IrUtil.isSubsetOf(ker, env);
255        if (env.size() == ker.size()) {
256            int[] values = ker.getValues();
257            TIntHashSet valueSet = new TIntHashSet(values);
258            SetVar var = cachedSetConstants.get(valueSet);
259            if (var == null) {
260                var = new SetConstantView(Arrays.toString(values), valueSet, solver);
261                cachedSetConstants.put(valueSet, var);
262            }
263            return var;
264        }
265        return VF.set(name, env.getValues(), ker.getValues(), solver);
266    }
267
268    private CSet cset(String name, IrDomain env, IrDomain ker, IrDomain card) {
269        SetVar set = setVar(name, env, ker);
270        return new CSet(set, card);
271    }
272
273    private IntVar setCardVar(SetVar set, IrDomain card) {
274        IntVar setCardVar = cachedSetCardVars.get(set);
275        if (setCardVar == null) {
276            setCardVar = intVar("|" + set.getName() + "|", card);
277            if (!(set.instantiated() && card.size() == 1 && card.getLowBound() == set.getKernelSize())) {
278                post(SCF.cardinality(set, setCardVar));
279            }
280            assert !cachedSetCardVars.containsKey(set);
281            cachedSetCardVars.put(set, setCardVar);
282        }
283        return setCardVar;
284    }
285
286    private BoolVar numBoolVar(String name) {
287        return boolVar(name + "#" + varNum++, IrBoolDomain.BoolDomain);
288    }
289
290    private IntVar numIntVar(String name, IrDomain domain) {
291        return intVar(name + "#" + varNum++, domain);
292    }
293
294    private SetVar numSetVar(String name, IrDomain env, IrDomain ker) {
295        return setVar(name + "#" + varNum++, env, ker);
296    }
297
298    private CSet numCset(String name, IrDomain env, IrDomain ker, IrDomain card) {
299        return cset(name + "#" + varNum++, env, ker, card);
300    }
301
302    private BoolVar getBoolVar(IrBoolVar var) {
303        BoolVar bool = (BoolVar) intVarMap.get(var);
304        if (bool == null) {
305            CSet set = cardIntVarMap.get(var);
306            bool = set == null ? boolVar(var.getName(), var.getDomain()) : (BoolVar) set.getCard();
307            intVarMap.put(var, bool);
308        }
309        return bool;
310    }
311
312    private IntVar getIntVar(IrIntVar var) {
313        IntVar iint = intVarMap.get(var);
314        if (iint == null) {
315            CSet set = cardIntVarMap.get(var);
316            iint = set == null ? intVar(var.getName(), var.getDomain()) : set.getCard();
317            intVarMap.put(var, iint);
318        }
319        return iint;
320    }
321    private final Map<IrIntVar, IntVar> intVarMap = new HashMap<>();
322    private final Map<IrIntVar, CSet> cardIntVarMap = new HashMap<>();
323
324    private SetVar getSetVar(IrSetVar var) {
325        SetVar set = setVarMap.get(var);
326        if (set == null) {
327            set = setVar(var.getName(), var.getEnv(), var.getKer());
328            setVarMap.put(var, set);
329        }
330        return set;
331    }
332    private final Map<IrSetVar, SetVar> setVarMap = new HashMap<>();
333
334    private BoolVar asBoolVar(Object obj) {
335        if (obj instanceof Constraint) {
336            return asBoolVar((Constraint) obj);
337        }
338        return (BoolVar) obj;
339    }
340
341    private BoolVar asBoolVar(Constraint op) {
342        return op.reif();
343    }
344
345    private BoolVar compileAsBoolVar(IrBoolExpr expr) {
346        return asBoolVar(expr.accept(boolExprCompiler, BoolVarNoReify));
347    }
348
349    private BoolVar[] compileAsBoolVars(IrBoolExpr[] exprs) {
350        BoolVar[] vars = new BoolVar[exprs.length];
351        for (int i = 0; i < vars.length; i++) {
352            vars[i] = compileAsBoolVar(exprs[i]);
353        }
354        return vars;
355    }
356
357    private IntVar compileAsIntVar(IrBoolExpr expr) {
358        return asBoolVar(expr.accept(boolExprCompiler, BoolVarNoReify));
359    }
360
361    private IntVar[] compileAsIntVars(IrBoolExpr[] exprs) {
362        IntVar[] vars = new IntVar[exprs.length];
363        for (int i = 0; i < vars.length; i++) {
364            vars[i] = compileAsIntVar(exprs[i]);
365        }
366        return vars;
367    }
368
369    private Constraint asConstraint(Object obj) {
370        if (obj instanceof BoolVar) {
371            return asConstraint((BoolVar) obj);
372        }
373        return (Constraint) obj;
374    }
375
376    private Constraint asConstraint(BoolVar var) {
377        return _arithm(var, "=", 1);
378    }
379
380    private Constraint compileAsConstraint(IrBoolExpr expr) {
381        return asConstraint(expr.accept(boolExprCompiler, ConstraintNoReify));
382    }
383
384    private Constraint compileAsConstraint(IrBoolExpr expr, BoolVar reify) {
385        BoolArg arg = new BoolArg(reify, Preference.Constraint);
386        Object result = expr.accept(boolExprCompiler, arg);
387        if (result instanceof Constraint) {
388            Constraint constraint = (Constraint) result;
389            if (arg.hasReify()) {
390                // The compliation failed to reify, explicitly reify now.
391                return _arithm(arg.useReify(), "=", constraint.reif());
392            }
393            return constraint;
394        }
395        BoolVar var = (BoolVar) result;
396        if (arg.hasReify()) {
397            return _arithm(arg.useReify(), "=", var);
398        }
399        return asConstraint(var);
400    }
401
402    private Constraint compileAsEqual(IrIntExpr expr, IntVar value, BoolVar reify) {
403        Object result = commonSubexpressions.contains(expr)
404                ? compile(expr)
405                : expr.accept(intExprCompiler, value);
406        if (result instanceof IntVar) {
407            // The compliation failed to reify, explicitly reify now.
408            return _reify_equal(reify, value, (IntVar) result);
409        }
410        return _arithm(((Constraint) result).reif(), "=", reify);
411    }
412
413    private Constraint compileAsNotEqual(IrIntExpr expr, IntVar value, BoolVar reify) {
414        Object result = commonSubexpressions.contains(expr)
415                ? compile(expr)
416                : expr.accept(intExprCompiler, value);
417        if (result instanceof IntVar) {
418            // The compliation failed to reify, explicitly reify now.
419            return _reify_not_equal(reify, value, (IntVar) result);
420        }
421        return _arithm(((Constraint) result).reif(), "!=", reify);
422    }
423
424    private Constraint compileAsConstraint(IrIntExpr expr, IntVar reify) {
425        Object result = commonSubexpressions.contains(expr)
426                ? compile(expr)
427                : expr.accept(intExprCompiler, reify);
428        if (result instanceof IntVar) {
429            // The compliation failed to reify, explicitly reify now.
430            return _arithm(reify, "=", (IntVar) result);
431        }
432        return (Constraint) result;
433    }
434
435    private Constraint compileAsConstraint(IrSetExpr expr, CSet reify) {
436        Object result = commonSubexpressions.contains(expr)
437                ? compile(expr)
438                : expr.accept(setExprCompiler, reify);
439        if (result instanceof CSet) {
440            CSet set = (CSet) result;
441            // The compliation failed to reify, explicitly reify now.
442            return _equal(reify, set);
443        }
444        return (Constraint) result;
445    }
446
447    private Constraint compileArithm(IrIntExpr a, Rel op, IrIntExpr b) {
448        if (a instanceof IrMinus) {
449            IrMinus minus = (IrMinus) a;
450            // -a ◁ b <=> a + b ▷ 0
451            return compileArithm(minus.getExpr(), Arithm.ADD, b, op.reverse(), 0);
452        }
453        if (b instanceof IrMinus) {
454            IrMinus minus = (IrMinus) b;
455            // a ◁ -b <=> a + b ◁ 0
456            return compileArithm(a, Arithm.ADD, minus.getExpr(), op, 0);
457        }
458        if (a instanceof IrNot) {
459            IrNot not = (IrNot) a;
460            // !a ◁ b <=> 1 - a ◁ b <=> a + b ▷ 1
461            return compileArithm(not.getExpr(), Arithm.ADD, b, op.reverse(), 1);
462        }
463        if (b instanceof IrNot) {
464            IrNot not = (IrNot) b;
465            // a ◁ !b <=> a ◁ 1 - b <=> a + b ◁ 1
466            return compileArithm(a, Arithm.ADD, not.getExpr(), op, 1);
467        }
468        if (a instanceof IrIntConstant) {
469            IrIntConstant constant = (IrIntConstant) a;
470            return _arithm(compile(b), op.reverse().getSyntax(), constant.getValue());
471        }
472        if (b instanceof IrIntConstant) {
473            IrIntConstant constant = (IrIntConstant) b;
474            return _arithm(compile(a), op.getSyntax(), constant.getValue());
475        }
476        switch (op) {
477            case EQ:
478                if (b instanceof IrBoolVar) {
479                    return compileAsConstraint(a, compile(b));
480                }
481                return compileAsConstraint(b, compile(a));
482            case NQ:
483                if (a instanceof IrVar && b instanceof IrVar) {
484                    return _arithm(compile(a), "!=", compile(b));
485                }
486                if (a instanceof IrBoolExpr && b instanceof IrBoolExpr) {
487                    IrBoolExpr boolA = (IrBoolExpr) a;
488                    IrBoolExpr boolB = (IrBoolExpr) b;
489                    if (boolA instanceof IrCompare) {
490                        return compileAsConstraint(boolA.negate(), compileAsIntVar(boolB));
491                    }
492                    if (boolB instanceof IrCompare) {
493                        return compileAsConstraint(boolB.negate(), compileAsIntVar(boolA));
494                    }
495                    if (boolA instanceof IrBoolVar) {
496                        return compileAsConstraint(boolB, compileAsIntVar(boolA.negate()));
497                    }
498                    return compileAsConstraint(boolA, compileAsIntVar(boolB.negate()));
499                }
500        }
501        return _arithm(compile(a), op.getSyntax(), compile(b));
502    }
503
504    private Constraint compileArithm(IrIntExpr a, Rel op1, IrIntExpr b, Arithm op2, int c) {
505        if (c == 0) {
506            return compileArithm(a, op1, b);
507        }
508        if (a instanceof IrMinus) {
509            IrMinus minus = (IrMinus) a;
510            // -a ◁ b + c <=> a + b ▷ -c
511            // -a ◁ b - c <=> a + b ▷ c
512            return compileArithm(minus.getExpr(), Arithm.ADD, b, op1.reverse(),
513                    Arithm.ADD.equals(op2) ? -c : c);
514        }
515        if (b instanceof IrMinus) {
516            IrMinus minus = (IrMinus) b;
517            // a ◁ -b + c <=> a + b ▷ c
518            // a ◁ -b - c <=> a + b ▷ -c
519            return compileArithm(a, Arithm.ADD, minus.getExpr(), op1.reverse(),
520                    Arithm.ADD.equals(op2) ? c : -c);
521        }
522        if (a instanceof IrAdd) {
523            IrAdd add = (IrAdd) a;
524            IrIntExpr[] addends = add.getAddends();
525            if (addends.length == 1) {
526                // a + d ◁ b + c <=> a ◁ b + (c - d)
527                // a + d ◁ b - c <=> a ◁ b - (c + d)
528                return compileArithm(addends[0], op1, b, op2,
529                        Arithm.ADD.equals(op2) ? c - add.getOffset() : c + add.getOffset());
530            }
531        }
532        if (b instanceof IrAdd) {
533            IrAdd add = (IrAdd) b;
534            IrIntExpr[] addends = add.getAddends();
535            if (addends.length == 1) {
536                // a ◁ b + d + c <=> a ◁ b + (c + d)
537                // a ◁ b + d - c <=> a ◁ b - (c - d)
538                return compileArithm(a, op1, addends[0], op2,
539                        Arithm.ADD.equals(op2) ? c + add.getOffset() : c - add.getOffset());
540            }
541        }
542        if (a instanceof IrNot) {
543            IrNot not = (IrNot) a;
544            // !a ◁ b + c <=> 1 - a ◁ b + c <=> a + b ▷ 1 - c
545            // !a ◁ b - c <=> 1 - a ◁ b - c <=> a + b ▷ 1 + c
546            return compileArithm(not.getExpr(), Arithm.ADD, b, op1.reverse(),
547                    Arithm.ADD.equals(op2) ? 1 - c : 1 + c);
548        }
549        if (b instanceof IrNot) {
550            IrNot not = (IrNot) b;
551            // a ◁ !b + c <=> a ◁ 1 - b + c <=> a + b ▷ 1 + c
552            // a ◁ !b - c <=> a ◁ 1 - b - c <=> a + b ▷ 1 - c
553            return compileArithm(a, Arithm.ADD, not.getExpr(), op1.reverse(),
554                    Arithm.ADD.equals(op2) ? 1 + c : 1 - c);
555        }
556        return _arithm(compile(a), op1.getSyntax(), compile(b), op2.getSyntax(), c);
557    }
558
559    private Constraint compileArithm(IrIntExpr a, Arithm op1, IrIntExpr b, Rel op2, int c) {
560        if (b instanceof IrMinus) {
561            IrMinus minus = (IrMinus) b;
562            // a + (-b) ◁ c <=> a - b ◁ c
563            // a - (-b) ◁ c <=> a + b ◁ c
564            return compileArithm(a, op1.negate(), minus.getExpr(), op2, c);
565        }
566        if (a instanceof IrAdd) {
567            IrAdd add = (IrAdd) a;
568            IrIntExpr[] addends = add.getAddends();
569            if (addends.length == 1) {
570                // a + d + b ◁ c <=> a + b ◁ (c - d)
571                // a + d - b ◁ c <=> a - b ◁ (c - d)
572                return compileArithm(addends[0], op1, b, op2, c - add.getOffset());
573            }
574        }
575        if (b instanceof IrAdd) {
576            IrAdd add = (IrAdd) b;
577            IrIntExpr[] addends = add.getAddends();
578            if (addends.length == 1) {
579                // a + b + d ◁ c <=> a + b ◁ (c - d)
580                // a - (b + d) ◁ c <=> a - b ◁ (c + d)
581                return compileArithm(a, op1, addends[0], op2,
582                        Arithm.ADD.equals(op2) ? c - add.getOffset() : c + add.getOffset());
583            }
584        }
585        switch (op1) {
586            case ADD:
587                if (a instanceof IrNot) {
588                    IrNot not = (IrNot) a;
589                    // !a + b ◁ c <=> 1 - a + b ◁ c <=> b ◁ a + c - 1
590                    return compileArithm(b, op2, not.getExpr(), Arithm.ADD, c - 1);
591                }
592                if (b instanceof IrNot) {
593                    IrNot not = (IrNot) b;
594                    // a + !b ◁ c <=> a + 1 - b ◁ c <=> a ◁ b + c - 1
595                    return compileArithm(a, op2, not.getExpr(), Arithm.ADD, c - 1);
596                }
597                if (a instanceof IrMinus) {
598                    IrMinus minus = (IrMinus) a;
599                    // (-a) + b ◁ c <=> b - a ◁ c
600                    return compileArithm(b, Arithm.MINUS, minus.getExpr(), op2, c);
601                }
602                break;
603            case MINUS:
604                if (a instanceof IrNot) {
605                    IrNot not = (IrNot) a;
606                    // !a - b ◁ c <=> 1 - a - b ◁ c <=> -a - b ◁ c - 1 <=> a + b ▷ 1 - c
607                    return compileArithm(not.getExpr(), Arithm.ADD, b, op2.reverse(), 1 - c);
608                }
609                if (b instanceof IrNot) {
610                    IrNot not = (IrNot) b;
611                    // a - !b ◁ c <=> a - 1 + b ◁ c <=> a + b ◁ c + 1
612                    return compileArithm(a, Arithm.ADD, not.getExpr(), op2, c + 1);
613                }
614                if (a instanceof IrMinus) {
615                    IrMinus minus = (IrMinus) a;
616                    // (-a) - b ◁ c <=> a + b ▷ -c
617                    return compileArithm(minus.getExpr(), Arithm.ADD, b, op2.reverse(), -c);
618                }
619                break;
620        }
621        return _arithm(compile(a), op1.getSyntax(), compile(b), op2.getSyntax(), c);
622    }
623
624    private Constraint compileArithm(IrIntExpr a, IrCompare.Op op, IrIntExpr b) {
625        return compileArithm(a, Rel.from(op), b);
626    }
627
628    private Constraint compileArithm(IrIntExpr a, IrCompare.Op op1, IrIntExpr b, Arithm op2, int c) {
629        return compileArithm(a, Rel.from(op1), b, op2, c);
630    }
631
632    private Constraint compileArithm(IrIntExpr a, Arithm op1, IrIntExpr b, IrCompare.Op op2, int c) {
633        return compileArithm(a, op1, b, Rel.from(op2), c);
634    }
635
636    private Constraint compileArithm(int c, IrCompare.Op op1, IrIntExpr a, Arithm op2, IrIntExpr b) {
637        return compileArithm(b, op2, a, Rel.from(op1).reverse(), c);
638    }
639
640    private Constraint compileArithm(int c, Arithm op1, IrIntExpr a, IrCompare.Op op2, IrIntExpr b) {
641        return compileArithm(b, Rel.from(op2).reverse(), a, op1, c);
642    }
643
644    private Object compile(IrBoolExpr expr) {
645        return expr.accept(boolExprCompiler, ConstraintNoReify);
646    }
647
648    private IntVar compile(IrIntExpr expr) {
649        IntVar var = cachedCommonIntSubexpressions.get(expr);
650        if (var == null) {
651            var = (IntVar) expr.accept(intExprCompiler, null);
652            if (commonSubexpressions.contains(expr)) {
653                cachedCommonIntSubexpressions.put(expr, var);
654            }
655        }
656        return var;
657    }
658
659    private IntVar[] compile(IrIntExpr[] exprs) {
660        IntVar[] vars = new IntVar[exprs.length];
661        for (int i = 0; i < vars.length; i++) {
662            vars[i] = compile(exprs[i]);
663        }
664        return vars;
665    }
666
667    private CSet compile(IrSetExpr expr) {
668        CSet set = cachedCommonSetSubexpressions.get(expr);
669        if (set == null) {
670            set = (CSet) expr.accept(setExprCompiler, null);
671            if (commonSubexpressions.contains(expr)) {
672                cachedCommonSetSubexpressions.put(expr, set);
673            }
674        }
675        return set;
676    }
677
678    private CSet[] compile(IrSetExpr[] exprs) {
679        CSet[] vars = new CSet[exprs.length];
680        for (int i = 0; i < vars.length; i++) {
681            vars[i] = compile(exprs[i]);
682        }
683        return vars;
684    }
685    private final IrBoolExprVisitor<BoolArg, Object> boolExprCompiler = new IrBoolExprVisitor<BoolArg, Object>() {
686        @Override
687        public Object visit(IrBoolVar ir, BoolArg a) {
688            return getBoolVar(ir);
689        }
690
691        @Override
692        public Object visit(IrNot ir, BoolArg a) {
693            BoolVar var = compileAsBoolVar(ir.getExpr());
694            if (a.hasReify()) {
695                return _arithm(a.useReify(), "!=", var);
696            }
697            return Preference.Constraint.equals(a.getPreference())
698                    ? _arithm(var, "=", 0)
699                    : var.not();
700        }
701
702        @Override
703        public Object visit(IrAnd ir, BoolArg a) {
704            IrBoolExpr[] operands = ir.getOperands();
705            switch (operands.length) {
706                case 1:
707                    // delegate
708                    return operands[0].accept(this, a);
709                case 2:
710                    return compileArithm(operands[0], Arithm.ADD, operands[1], Rel.EQ, 2);
711                default:
712                    return Constraints.and(compileAsBoolVars(ir.getOperands()));
713            }
714        }
715
716        @Override
717        public Object visit(IrLone ir, BoolArg a) {
718            IrBoolExpr[] operands = ir.getOperands();
719            switch (operands.length) {
720                case 1:
721                    return solver.TRUE;
722                case 2:
723                    return compileArithm(operands[0], Arithm.ADD, operands[1], Rel.LE, 1);
724                default:
725                    return Constraints.lone(compileAsBoolVars(ir.getOperands()));
726            }
727        }
728
729        @Override
730        public Object visit(IrOne ir, BoolArg a) {
731            IrBoolExpr[] operands = ir.getOperands();
732            switch (operands.length) {
733                case 1:
734                    // delegate
735                    return operands[0].accept(this, a);
736                case 2:
737                    return compileArithm(operands[0], Arithm.ADD, operands[1], Rel.EQ, 1);
738                default:
739                    return Constraints.one(compileAsBoolVars(ir.getOperands()));
740            }
741        }
742
743        @Override
744        public Object visit(IrOr ir, BoolArg a) {
745            IrBoolExpr[] operands = ir.getOperands();
746            switch (operands.length) {
747                case 1:
748                    // delegate
749                    return operands[0].accept(this, a);
750                case 2:
751                    return compileArithm(operands[0], Arithm.ADD, operands[1], Rel.GE, 1);
752                default:
753                    return Constraints.or(compileAsBoolVars(ir.getOperands()));
754            }
755        }
756
757        @Override
758        public Object visit(IrImplies ir, BoolArg a) {
759            return compileArithm(ir.getAntecedent(), Rel.LE, ir.getConsequent());
760        }
761
762        @Override
763        public Object visit(IrNotImplies ir, BoolArg a) {
764            return compileArithm(ir.getAntecedent(), Rel.GT, ir.getConsequent());
765        }
766
767        @Override
768        public Object visit(IrIfThenElse ir, BoolArg a) {
769            BoolVar antecedent = compileAsBoolVar(ir.getAntecedent());
770            BoolVar consequent = compileAsBoolVar(ir.getConsequent());
771            BoolVar alternative = compileAsBoolVar(ir.getAlternative());
772            return _ifThenElse(antecedent, consequent, alternative);
773        }
774
775        @Override
776        public Object visit(IrIfOnlyIf ir, BoolArg a) {
777            return compileArithm(ir.getLeft(), Rel.EQ, ir.getRight());
778        }
779
780        @Override
781        public Object visit(IrXor ir, BoolArg a) {
782            return compileArithm(ir.getLeft(), Rel.NQ, ir.getRight());
783        }
784
785        @Override
786        public Object visit(IrWithin ir, BoolArg a) {
787            IntVar var = compile(ir.getValue());
788            IrDomain range = ir.getRange();
789            if (range.isBounded()) {
790                return _within(var, range.getLowBound(), range.getHighBound());
791            }
792            return _within(var, range.getValues());
793        }
794
795        @Override
796        public Object visit(IrNotWithin ir, BoolArg a) {
797            IntVar var = compile(ir.getValue());
798            IrDomain range = ir.getRange();
799            if (range.isBounded()) {
800                return _not_within(var, range.getLowBound(), range.getHighBound());
801            }
802            return _not_within(var, range.getValues());
803        }
804
805        @Override
806        public Object visit(IrCompare ir, BoolArg a) {
807            IrCompare.Op op = ir.getOp();
808            IrIntExpr left = ir.getLeft();
809            IrIntExpr right = ir.getRight();
810            if (left instanceof IrAdd) {
811                IrAdd add = (IrAdd) left;
812                IrIntExpr[] addends = add.getAddends();
813                if (addends.length == 1) {
814                    return compileArithm(addends[0], Arithm.MINUS, right, op, -add.getOffset());
815                }
816                if (addends.length == 2) {
817                    Integer constant = IrUtil.getConstant(right);
818                    if (constant != null) {
819                        return compileArithm(addends[0], Arithm.ADD, addends[1], op, constant.intValue() - add.getOffset());
820                    }
821                }
822            }
823            if (right instanceof IrAdd) {
824                IrAdd add = (IrAdd) right;
825                IrIntExpr[] addends = add.getAddends();
826                if (addends.length == 1) {
827                    return compileArithm(left, Arithm.MINUS, addends[0], op, add.getOffset());
828                }
829                if (addends.length == 2) {
830                    Integer constant = IrUtil.getConstant(left);
831                    if (constant != null) {
832                        return compileArithm(constant.intValue() - add.getOffset(), op, addends[0], Arithm.ADD, addends[1]);
833                    }
834                }
835            }
836            if (IrCompare.Op.Equal.equals(op)) {
837                if (a.hasReify()) {
838                    BoolVar reify = a.useReify();
839                    return right instanceof IrIntVar
840                            ? compileAsEqual(left, compile(right), reify)
841                            : compileAsEqual(right, compile(left), reify);
842                }
843                if (a.getPreference().equals(Preference.BoolVar)) {
844                    BoolVar reify = numBoolVar("ReifyEqual");
845                    post(right instanceof IrIntVar
846                            ? compileAsEqual(left, compile(right), reify)
847                            : compileAsEqual(right, compile(left), reify));
848                    return reify;
849                }
850            } else if (IrCompare.Op.NotEqual.equals(op)) {
851                if (a.hasReify()) {
852                    BoolVar reify = a.useReify();
853                    return right instanceof IrIntVar
854                            ? compileAsNotEqual(left, compile(right), reify)
855                            : compileAsNotEqual(right, compile(left), reify);
856                }
857                if (a.getPreference().equals(Preference.BoolVar)) {
858                    BoolVar reify = numBoolVar("ReifyNotEqual");
859                    post(right instanceof IrIntVar
860                            ? compileAsNotEqual(left, compile(right), reify)
861                            : compileAsNotEqual(right, compile(left), reify));
862                    return reify;
863                }
864            }
865            return compileArithm(left, op, right);
866        }
867
868        private Triple<String, IrIntExpr, Integer> getOffset(IrIntExpr expr) {
869            if (expr instanceof IrAdd) {
870                IrAdd add = (IrAdd) expr;
871                IrIntExpr[] addends = add.getAddends();
872                if (addends.length == 1) {
873                    return new Triple<>("-", addends[0], add.getOffset());
874                }
875            }
876            return null;
877        }
878
879        @Override
880        public Object visit(IrSetTest ir, BoolArg a) {
881            switch (ir.getOp()) {
882                case Equal:
883                    if (ir.getRight() instanceof IrSetVar) {
884                        return compileAsConstraint(ir.getLeft(), compile(ir.getRight()));
885                    }
886                    return compileAsConstraint(ir.getRight(), compile(ir.getLeft()));
887                case NotEqual:
888                    return _not_equal(compile(ir.getLeft()), compile(ir.getRight()));
889                default:
890                    throw new IllegalArgumentException("Unexpected operator.");
891            }
892        }
893
894        @Override
895        public Object visit(IrMember ir, BoolArg a) {
896            return _member(compile(ir.getElement()), compile(ir.getSet()).getSet());
897        }
898
899        @Override
900        public Object visit(IrNotMember ir, BoolArg a) {
901            return _not_member(compile(ir.getElement()), compile(ir.getSet()).getSet());
902        }
903
904        @Override
905        public Object visit(IrSubsetEq ir, BoolArg a) {
906            return _subset_eq(compile(ir.getSubset()), compile(ir.getSuperset()));
907        }
908
909        @Override
910        public Constraint visit(IrBoolChannel ir, BoolArg a) {
911            BoolVar[] bools = compileAsBoolVars(ir.getBools());
912            CSet set = compile(ir.getSet());
913            return SCF.bool_channel(bools, set.getSet(), 0);
914        }
915
916        @Override
917        public Constraint visit(IrIntChannel ir, BoolArg a) {
918            IntVar[] ints = compile(ir.getInts());
919            CSet[] sets = compile(ir.getSets());
920            return Constraints.intChannel(mapSet(sets), ints);
921        }
922
923        @Override
924        public Object visit(IrSortStrings ir, BoolArg a) {
925            IntVar[][] strings = new IntVar[ir.getStrings().length][];
926            for (int i = 0; i < strings.length; i++) {
927                strings[i] = compile(ir.getStrings()[i]);
928            }
929            return ir.isStrict() ? _lex_chain_less(strings) : _lex_chain_less_eq(strings);
930        }
931
932        @Override
933        public Object visit(IrSortSets ir, BoolArg a) {
934            CSet[] sets = compile(ir.getSets());
935            return Constraints.sortedSets(mapSet(sets), mapCard(sets));
936        }
937
938        @Override
939        public Object visit(IrSortStringsChannel ir, BoolArg a) {
940            IntVar[][] strings = new IntVar[ir.getStrings().length][];
941            for (int i = 0; i < strings.length; i++) {
942                strings[i] = compile(ir.getStrings()[i]);
943            }
944            return _lex_chain_channel(strings, compile(ir.getInts()));
945        }
946
947        @Override
948        public Constraint visit(IrAllDifferent ir, BoolArg a) {
949            IrIntExpr[] operands = ir.getOperands();
950
951            IntVar[] $operands = new IntVar[operands.length];
952            for (int i = 0; i < $operands.length; i++) {
953                $operands[i] = compile(operands[i]);
954            }
955            return _all_different($operands);
956        }
957
958        @Override
959        public Constraint visit(IrSelectN ir, BoolArg a) {
960            BoolVar[] bools = compileAsBoolVars(ir.getBools());
961            IntVar n = compile(ir.getN());
962            return Constraints.selectN(bools, n);
963        }
964
965        @Override
966        public Object visit(IrAcyclic ir, BoolArg a) {
967            IntVar[] edges = compile(ir.getEdges());
968            return Constraints.acyclic(edges);
969        }
970
971        @Override
972        public Object visit(IrUnreachable ir, BoolArg a) {
973            IntVar[] edges = compile(ir.getEdges());
974            return Constraints.unreachable(edges, ir.getFrom(), ir.getTo());
975        }
976
977        @Override
978        public Object visit(IrFilterString ir, BoolArg a) {
979            CSet set = compile(ir.getSet());
980            int offset = ir.getOffset();
981            IntVar[] string = compile(ir.getString());
982            IntVar[] result = compile(ir.getResult());
983            return Constraints.filterString(set.getSet(), set.getCard(), offset, string, result);
984        }
985    };
986    private final IrIntExprVisitor<IntVar, Object> intExprCompiler = new IrIntExprVisitor<IntVar, Object>() {
987        @Override
988        public IntVar visit(IrIntVar ir, IntVar reify) {
989            return getIntVar(ir);
990        }
991
992        @Override
993        public IntVar visit(IrMinus ir, IntVar reify) {
994            IntVar expr = compile(ir.getExpr());
995            IntVar minus = cachedMinus.get(expr);
996            if (minus == null) {
997                minus = VF.minus(compile(ir.getExpr()));
998                cachedMinus.put(expr, minus);
999            }
1000            return minus;
1001        }
1002
1003        @Override
1004        public Object visit(IrCard ir, IntVar reify) {
1005            CSet set = compile(ir.getSet());
1006            return set.getCard();
1007        }
1008
1009        private Pair<Integer, IrIntExpr> getCoefficient(IrIntExpr e) {
1010            if (e instanceof IrMinus) {
1011                return new Pair<>(-1, ((IrMinus) e).getExpr());
1012            } else if (e instanceof IrMul) {
1013                IrMul mul = (IrMul) e;
1014                Integer constant = IrUtil.getConstant(mul.getMultiplicand());
1015                if (constant != null) {
1016                    return new Pair<>(constant, mul.getMultiplier());
1017                }
1018                constant = IrUtil.getConstant(mul.getMultiplier());
1019                if (constant != null) {
1020                    return new Pair<>(constant, mul.getMultiplicand());
1021                }
1022            }
1023            return new Pair<>(1, e);
1024        }
1025
1026        private Pair<int[], IrIntExpr[]> getCoefficients(IrIntExpr[] es) {
1027            int[] coefficients = new int[es.length];
1028            IrIntExpr[] exprs = new IrIntExpr[es.length];
1029            for (int i = 0; i < es.length; i++) {
1030                Pair<Integer, IrIntExpr> coef = getCoefficient(es[i]);
1031                coefficients[i] = coef.getFst();
1032                exprs[i] = coef.getSnd();
1033            }
1034            return new Pair<>(coefficients, exprs);
1035        }
1036
1037        @Override
1038        public Object visit(IrAdd ir, IntVar reify) {
1039            int offset = ir.getOffset();
1040            IrIntExpr[] addends = ir.getAddends();
1041            switch (addends.length) {
1042                case 0:
1043                    // This case should have already been optimized earlier.
1044                    return VF.fixed(offset, solver);
1045                case 1:
1046                    if (reify == null) {
1047                        return _offset(compile(addends[0]), offset);
1048                    }
1049                    return _arithm(reify, "-", compile(addends[0]), "=", offset);
1050                default:
1051                    Pair<int[], IrIntExpr[]> coeffs = getCoefficients(addends);
1052                    int[] coefficients = coeffs.getFst();
1053                    IntVar[] operands = compile(coeffs.getSnd());
1054                    if (reify == null) {
1055                        IntVar sum = numIntVar("Sum", IrUtil.offset(ir.getDomain(), -offset));
1056                        post(_scalar(sum, coefficients, operands));
1057                        return _offset(sum, offset);
1058                    }
1059                    if (offset != 0) {
1060                        coefficients = Util.cons(1, coefficients);
1061                        operands = Util.cons(VF.fixed(offset, solver), operands);
1062                    }
1063                    return _scalar(reify, coefficients, operands);
1064            }
1065        }
1066
1067        @Override
1068        public Object visit(IrMul ir, IntVar reify) {
1069            IrIntExpr multiplicand = ir.getMultiplicand();
1070            IrIntExpr multiplier = ir.getMultiplier();
1071            Integer multiplicandConstant = IrUtil.getConstant(multiplicand);
1072            Integer multiplierConstant = IrUtil.getConstant(multiplier);
1073            if (multiplicandConstant != null) {
1074                switch (multiplicandConstant.intValue()) {
1075                    case 0:
1076                        return compileAsConstraint(multiplicand, reify);
1077                    case 1:
1078                        return compileAsConstraint(multiplier, reify);
1079                    default:
1080                        if (multiplicandConstant.intValue() >= -1) {
1081                            return VF.scale(compile(multiplier), multiplicandConstant.intValue());
1082                        }
1083                }
1084            }
1085            if (multiplierConstant != null) {
1086                switch (multiplierConstant.intValue()) {
1087                    case 0:
1088                        return compileAsConstraint(multiplier, reify);
1089                    case 1:
1090                        return compileAsConstraint(multiplicand, reify);
1091                    default:
1092                        if (multiplierConstant.intValue() >= -1) {
1093                            return VF.scale(compile(multiplicand), multiplierConstant.intValue());
1094                        }
1095                }
1096            }
1097            if (reify == null) {
1098                IntVar product = numIntVar("Mul", ir.getDomain());
1099                post(_times(compile(multiplicand), compile(multiplier), product));
1100                return product;
1101            }
1102            return _times(compile(multiplicand), compile(multiplier), reify);
1103        }
1104
1105        @Override
1106        public Object visit(IrDiv ir, IntVar reify) {
1107            IrIntExpr dividend = ir.getDividend();
1108            IrIntExpr divisor = ir.getDivisor();
1109            if (reify == null) {
1110                IntVar quotient = numIntVar("Div", ir.getDomain());
1111                post(_div(compile(dividend), compile(divisor), quotient));
1112                return quotient;
1113            }
1114            return _div(compile(dividend), compile(divisor), reify);
1115        }
1116
1117        @Override
1118        public Object visit(IrElement ir, IntVar reify) {
1119            if (reify == null) {
1120                IntVar element = numIntVar("Element", ir.getDomain());
1121                post(_element(compile(ir.getIndex()), compile(ir.getArray()), element));
1122                return element;
1123            }
1124            return _element(compile(ir.getIndex()), compile(ir.getArray()), reify);
1125        }
1126
1127        @Override
1128        public Object visit(IrCount ir, IntVar reify) {
1129            IntVar[] array = compile(ir.getArray());
1130            if (reify == null) {
1131                IntVar count = numIntVar("Count", ir.getDomain());
1132                post(_count(ir.getValue(), array, count));
1133                return count;
1134            }
1135            return _count(ir.getValue(), array, reify);
1136        }
1137
1138        @Override
1139        public Object visit(IrSetSum ir, IntVar reify) {
1140            CSet set = compile(ir.getSet());
1141            if (reify == null) {
1142                IntVar sum = numIntVar("SetSum", ir.getDomain());
1143                post(Constraints.setSum(set.getSet(), set.getCard(), sum));
1144                return sum;
1145            }
1146            return Constraints.setSum(set.getSet(), set.getCard(), reify);
1147        }
1148
1149        @Override
1150        public Object visit(IrTernary ir, IntVar reify) {
1151            BoolVar antecedent = compileAsBoolVar(ir.getAntecedent());
1152            IntVar consequent = compile(ir.getConsequent());
1153            IntVar alternative = compile(ir.getAlternative());
1154            if (reify == null) {
1155                IntVar ternary = numIntVar("Ternary", ir.getDomain());
1156                BoolVar reifyConsequent = numBoolVar("ReifyEqual");
1157                BoolVar reifyAlternative = numBoolVar("ReifyEqual");
1158                solver.post(_reify_equal(reifyConsequent, consequent, ternary));
1159                solver.post(_reify_equal(reifyAlternative, alternative, ternary));
1160                post(_ifThenElse(antecedent, reifyConsequent, reifyAlternative));
1161                return ternary;
1162            }
1163            BoolVar reifyConsequent = numBoolVar("ReifyEqual");
1164            BoolVar reifyAlternative = numBoolVar("ReifyEqual");
1165            solver.post(_reify_equal(reifyConsequent, consequent, reify));
1166            solver.post(_reify_equal(reifyAlternative, alternative, reify));
1167            return _ifThenElse(antecedent, reifyConsequent, reifyAlternative);
1168        }
1169
1170        private Object compileBool(IrBoolExpr expr, IntVar a) {
1171            if (a instanceof BoolVar) {
1172                return compileAsConstraint(expr, (BoolVar) a);
1173            }
1174            IntVar var = compileAsIntVar(expr);
1175            return a == null ? var : _arithm(var, "=", a);
1176        }
1177
1178        @Override
1179        public Object visit(IrBoolVar ir, IntVar a) {
1180            return compileBool(ir, a);
1181        }
1182
1183        @Override
1184        public Object visit(IrNot ir, IntVar a) {
1185            return compileBool(ir, a);
1186        }
1187
1188        @Override
1189        public Object visit(IrAnd ir, IntVar a) {
1190            return compileBool(ir, a);
1191        }
1192
1193        @Override
1194        public Object visit(IrLone ir, IntVar a) {
1195            return compileBool(ir, a);
1196        }
1197
1198        @Override
1199        public Object visit(IrOne ir, IntVar a) {
1200            return compileBool(ir, a);
1201        }
1202
1203        @Override
1204        public Object visit(IrOr ir, IntVar a) {
1205            return compileBool(ir, a);
1206        }
1207
1208        @Override
1209        public Object visit(IrImplies ir, IntVar a) {
1210            return compileBool(ir, a);
1211        }
1212
1213        @Override
1214        public Object visit(IrNotImplies ir, IntVar a) {
1215            return compileBool(ir, a);
1216        }
1217
1218        @Override
1219        public Object visit(IrIfThenElse ir, IntVar a) {
1220            return compileBool(ir, a);
1221        }
1222
1223        @Override
1224        public Object visit(IrIfOnlyIf ir, IntVar a) {
1225            return compileBool(ir, a);
1226        }
1227
1228        @Override
1229        public Object visit(IrXor ir, IntVar a) {
1230            return compileBool(ir, a);
1231        }
1232
1233        @Override
1234        public Object visit(IrWithin ir, IntVar a) {
1235            return compileBool(ir, a);
1236        }
1237
1238        @Override
1239        public Object visit(IrNotWithin ir, IntVar a) {
1240            return compileBool(ir, a);
1241        }
1242
1243        @Override
1244        public Object visit(IrCompare ir, IntVar a) {
1245            return compileBool(ir, a);
1246        }
1247
1248        @Override
1249        public Object visit(IrSetTest ir, IntVar a) {
1250            return compileBool(ir, a);
1251        }
1252
1253        @Override
1254        public Object visit(IrMember ir, IntVar a) {
1255            return compileBool(ir, a);
1256        }
1257
1258        @Override
1259        public Object visit(IrNotMember ir, IntVar a) {
1260            return compileBool(ir, a);
1261        }
1262
1263        @Override
1264        public Object visit(IrSubsetEq ir, IntVar a) {
1265            return compileBool(ir, a);
1266        }
1267
1268        @Override
1269        public Object visit(IrBoolChannel ir, IntVar a) {
1270            return compileBool(ir, a);
1271        }
1272
1273        @Override
1274        public Object visit(IrIntChannel ir, IntVar a) {
1275            return compileBool(ir, a);
1276        }
1277
1278        @Override
1279        public Object visit(IrSortStrings ir, IntVar a) {
1280            return compileBool(ir, a);
1281        }
1282
1283        @Override
1284        public Object visit(IrSortSets ir, IntVar a) {
1285            return compileBool(ir, a);
1286        }
1287
1288        @Override
1289        public Object visit(IrSortStringsChannel ir, IntVar a) {
1290            return compileBool(ir, a);
1291        }
1292
1293        @Override
1294        public Object visit(IrAllDifferent ir, IntVar a) {
1295            return compileBool(ir, a);
1296        }
1297
1298        @Override
1299        public Object visit(IrSelectN ir, IntVar a) {
1300            return compileBool(ir, a);
1301        }
1302
1303        @Override
1304        public Object visit(IrAcyclic ir, IntVar a) {
1305            return compileBool(ir, a);
1306        }
1307
1308        @Override
1309        public Object visit(IrUnreachable ir, IntVar a) {
1310            return compileBool(ir, a);
1311        }
1312
1313        @Override
1314        public Object visit(IrFilterString ir, IntVar a) {
1315            return compileBool(ir, a);
1316        }
1317    };
1318    private final IrSetExprVisitor<CSet, Object> setExprCompiler = new IrSetExprVisitor<CSet, Object>() {
1319        @Override
1320        public Object visit(IrSetVar ir, CSet reify) {
1321            return new CSet(getSetVar(ir), ir.getCard());
1322        }
1323
1324        @Override
1325        public Object visit(IrSingleton ir, CSet reify) {
1326            IntVar value = compile(ir.getValue());
1327            if (reify == null) {
1328                SetVar singleton = numSetVar("Singleton", ir.getEnv(), ir.getKer());
1329                post(Constraints.singleton(value, singleton));
1330                return new CSet(singleton, VF.one(solver));
1331            }
1332            return Constraints.singleton(value, reify.getSet(), reify.getCard());
1333        }
1334
1335        @Override
1336        public Object visit(IrArrayToSet ir, CSet reify) {
1337            IntVar[] array = compile(ir.getArray());
1338            if (reify == null) {
1339                CSet set = numCset("ArrayToSet", ir.getEnv(), ir.getKer(), ir.getCard());
1340                post(Constraints.arrayToSet(array, set.getSet(), set.getCard(), ir.getGlobalCardinality()));
1341                return set;
1342            }
1343            return Constraints.arrayToSet(array, reify.getSet(), reify.getCard(), ir.getGlobalCardinality());
1344        }
1345
1346        @Override
1347        public Object visit(IrJoinRelation ir, CSet reify) {
1348            CSet take = compile(ir.getTake());
1349            CSet[] children = compile(ir.getChildren());
1350            if (reify == null) {
1351                CSet joinRelation = numCset("JoinRelation", ir.getEnv(), ir.getKer(), ir.getCard());
1352                if (ir.isInjective()) {
1353                    post(Constraints.joinInjectiveRelation(take.getSet(), take.getCard(),
1354                            mapSet(children), mapCard(children), joinRelation.getSet(), joinRelation.getCard()));
1355                    return joinRelation;
1356                } else {
1357                    post(Constraints.joinRelation(take.getSet(), mapSet(children), joinRelation.getSet()));
1358                    return joinRelation;
1359                }
1360            }
1361            if (ir.isInjective()) {
1362                return Constraints.joinInjectiveRelation(take.getSet(), take.getCard(),
1363                        mapSet(children), mapCard(children), reify.getSet(), reify.getCard());
1364            }
1365            return Constraints.joinRelation(take.getSet(), mapSet(children), reify.getSet());
1366        }
1367
1368        @Override
1369        public Object visit(IrJoinFunction ir, CSet reify) {
1370            CSet take = compile(ir.getTake());
1371            IntVar[] refs = compile(ir.getRefs());
1372            if (reify == null) {
1373                CSet joinFunction = numCset("JoinFunction", ir.getEnv(), ir.getKer(), ir.getCard());
1374                post(Constraints.joinFunction(take.getSet(), take.getCard(), refs, joinFunction.getSet(), joinFunction.getCard(), ir.getGlobalCardinality()));
1375                return joinFunction;
1376            }
1377            return Constraints.joinFunction(take.getSet(), take.getCard(), refs, reify.getSet(), reify.getCard(), ir.getGlobalCardinality());
1378        }
1379
1380        @Override
1381        public Object visit(IrSetDifference ir, CSet reify) {
1382            CSet minuend = compile(ir.getMinuend());
1383            CSet subtrahend = compile(ir.getSubtrahend());
1384            if (reify == null) {
1385                CSet difference = numCset("Difference", ir.getEnv(), ir.getKer(), ir.getCard());
1386                post(_difference(minuend, subtrahend, difference));
1387                return difference;
1388            }
1389            return _difference(minuend, subtrahend, reify);
1390        }
1391
1392        @Override
1393        public Object visit(IrSetIntersection ir, CSet reify) {
1394            CSet[] operands = compile(ir.getOperands());
1395            if (reify == null) {
1396                CSet intersection = numCset("Intersection", ir.getEnv(), ir.getKer(), ir.getCard());
1397                post(_intersection(operands, intersection));
1398                return intersection;
1399            }
1400            return _intersection(operands, reify);
1401        }
1402
1403        @Override
1404        public Object visit(IrSetUnion ir, CSet reify) {
1405            CSet[] operands = compile(ir.getOperands());
1406            if (reify == null) {
1407                CSet union = numCset("Union", ir.getEnv(), ir.getKer(), ir.getCard());
1408                post(_union(operands, union, ir.isDisjoint()));
1409                return union;
1410            }
1411            return _union(operands, reify, ir.isDisjoint());
1412        }
1413
1414        @Override
1415        public Object visit(IrOffset ir, CSet reify) {
1416            CSet set = compile(ir.getSet());
1417            if (reify == null) {
1418                SetVar offset = numSetVar("Offset", ir.getEnv(), ir.getKer());
1419                post(_offset(set.getSet(), offset, ir.getOffset()));
1420                return new CSet(offset, set.getCard());
1421            }
1422            return _offset(set.getSet(), reify.getSet(), ir.getOffset());
1423        }
1424
1425        @Override
1426        public Object visit(IrMask ir, CSet reify) {
1427            CSet set = compile(ir.getSet());
1428            if (reify == null) {
1429                CSet mask = numCset("Mask", ir.getEnv(), ir.getKer(), ir.getCard());
1430                post(_mask(set, mask, ir.getFrom(), ir.getTo()));
1431                return mask;
1432            }
1433            return _mask(set, reify, ir.getFrom(), ir.getTo());
1434        }
1435
1436        @Override
1437        public Object visit(IrSetTernary ir, CSet reify) {
1438            BoolVar antecedent = compileAsBoolVar(ir.getAntecedent());
1439            CSet consequent = compile(ir.getConsequent());
1440            CSet alternative = compile(ir.getAlternative());
1441            if (reify == null) {
1442                CSet ternary = numCset("Ternary", ir.getEnv(), ir.getKer(), ir.getCard());
1443                post(_ifThenElse(antecedent,
1444                        _equal(ternary, consequent),
1445                        _equal(ternary, alternative)));
1446                return ternary;
1447            }
1448            return _ifThenElse(antecedent,
1449                    _equal(reify, consequent),
1450                    _equal(reify, alternative));
1451        }
1452    };
1453
1454    private static Constraint _implies(BoolVar antecedent, Constraint consequent) {
1455        return _implies(antecedent, consequent.reif());
1456    }
1457
1458    private static Constraint _ifThenElse(BoolVar antecedent, BoolVar consequent, BoolVar alternative) {
1459        return Constraints.ifThenElse(antecedent, consequent, alternative);
1460    }
1461
1462    private static Constraint _ifThenElse(BoolVar antecedent, Constraint consequent, Constraint alternative) {
1463        Constraint thenClause = _implies(antecedent, consequent);
1464        Constraint elseClause = _implies(antecedent.not(), alternative);
1465        return _arithm(thenClause.reif(), "+", elseClause.reif(), "=", 2);
1466    }
1467
1468    private static Constraint _sum(IntVar sum, IntVar... vars) {
1469        for (IntVar var : vars) {
1470            if (!(var instanceof BoolVar)) {
1471                return ICF.sum(vars, sum);
1472            }
1473        }
1474        return _sum(sum, Arrays.copyOf(vars, vars.length, BoolVar[].class));
1475    }
1476
1477    private static Constraint _sum(IntVar sum, BoolVar... vars) {
1478        return ICF.sum(vars, sum);
1479    }
1480
1481    private static Constraint _scalar(IntVar sum, int[] coefficients, IntVar[] vars) {
1482        boolean allOnes = true;
1483        for (int coefficient : coefficients) {
1484            if (coefficient != 1) {
1485                allOnes = false;
1486                break;
1487            }
1488        }
1489        if (allOnes) {
1490            return _sum(sum, vars);
1491        }
1492        return ICF.scalar(vars, coefficients, sum);
1493    }
1494
1495    private static Constraint _times(IntVar multiplicand, IntVar multiplier, IntVar product) {
1496        return ICF.times(multiplicand, multiplier, product);
1497    }
1498
1499    private static Constraint _div(IntVar dividend, IntVar divisor, IntVar quotient) {
1500        return ICF.eucl_div(dividend, divisor, quotient);
1501    }
1502
1503    private static Constraint _arithm(IntVar var1, String op1, IntVar var2, String op2, int cste) {
1504        if (cste == 0) {
1505            switch (Operator.get(op2)) {
1506                case PL:
1507                    return ICF.arithm(var1, op1, var2);
1508                case MN:
1509                    return ICF.arithm(var1, op1, var2);
1510            }
1511        }
1512        return ICF.arithm(var1, op1, var2, op2, cste);
1513    }
1514
1515    private static Constraint _implies(BoolVar antecedent, IntVar consequent) {
1516        return _arithm(antecedent, "<=", consequent);
1517    }
1518
1519    private static Constraint _arithm(IntVar var1, String op, IntVar var2) {
1520        if (var2.instantiated()) {
1521            return ICF.arithm(var1, op, var2.getValue());
1522        }
1523        return ICF.arithm(var1, op, var2);
1524    }
1525
1526    private static Constraint _arithm(IntVar var1, String op, int c) {
1527        return ICF.arithm(var1, op, c);
1528    }
1529
1530    private Constraint _reify_equal(BoolVar reify, IntVar var1, IntVar var2) {
1531        if (var1.instantiated()) {
1532            if (var2.instantiated()) {
1533                return _arithm(reify, "=", var1.getValue() == var2.getValue() ? 1 : 0);
1534            }
1535            return Constraints.reifyEqual(reify, var2, var1.getValue());
1536        } else if (var2.instantiated()) {
1537            return Constraints.reifyEqual(reify, var1, var2.getValue());
1538        } else {
1539            return Constraints.reifyEqual(reify, var1, var2);
1540        }
1541    }
1542
1543    private Constraint _reify_not_equal(BoolVar reify, IntVar var1, IntVar var2) {
1544        if (var1.instantiated()) {
1545            if (var2.instantiated()) {
1546                return _arithm(reify, "=", var1.getValue() != var2.getValue() ? 1 : 0);
1547            }
1548            return Constraints.reifyNotEqual(reify, var2, var1.getValue());
1549        } else if (var2.instantiated()) {
1550            return Constraints.reifyNotEqual(reify, var1, var2.getValue());
1551        } else {
1552            return Constraints.reifyNotEqual(reify, var1, var2);
1553        }
1554    }
1555
1556    private static Constraint _element(IntVar index, IntVar[] array, IntVar value) {
1557        return ICF.element(value, array, index, 0);
1558    }
1559
1560    private static Constraint _count(int value, IntVar[] array, IntVar count) {
1561        return ICF.count(value, array, count);
1562    }
1563
1564    private static Constraint _equal(CSet var1, CSet var2) {
1565        return Constraints.equal(var1.getSet(), var1.getCard(), var2.getSet(), var2.getCard());
1566    }
1567
1568    private static Constraint _not_equal(CSet var1, CSet var2) {
1569        if (var1.getSet().instantiated()) {
1570            return Constraints.notEqual(var2.getSet(), var1.getSet().getValue());
1571        }
1572        if (var2.getSet().instantiated()) {
1573            return Constraints.notEqual(var1.getSet(), var2.getSet().getValue());
1574        }
1575        return Constraints.notEqual(var1.getSet(), var1.getCard(), var2.getSet(), var2.getCard());
1576    }
1577
1578    private static Constraint _all_different(IntVar... vars) {
1579        return ICF.alldifferent(vars, "AC");
1580    }
1581
1582    private static Constraint _within(IntVar var, int low, int high) {
1583        return ICF.member(var, low, high);
1584    }
1585
1586    private static Constraint _within(IntVar var, int[] values) {
1587        return ICF.member(var, values);
1588    }
1589
1590    private static Constraint _not_within(IntVar var, int low, int high) {
1591        return ICF.not_member(var, low, high);
1592    }
1593
1594    private static Constraint _not_within(IntVar var, int[] values) {
1595        return ICF.not_member(var, values);
1596    }
1597
1598    private static Constraint _member(IntVar element, SetVar set) {
1599        return SCF.member(element, set);
1600    }
1601
1602    private static Constraint _not_member(IntVar element, SetVar set) {
1603        return Constraints.notMember(element, set);
1604    }
1605
1606    private static Constraint _lex_chain_less(IntVar[]... vars) {
1607        if (vars.length == 2) {
1608            return ICF.lex_less(vars[0], vars[1]);
1609        }
1610        return ICF.lex_chain_less(vars);
1611    }
1612
1613    private static Constraint _lex_chain_less_eq(IntVar[]... vars) {
1614        if (vars.length == 2) {
1615            return ICF.lex_less_eq(vars[0], vars[1]);
1616        }
1617        return ICF.lex_chain_less_eq(vars);
1618    }
1619
1620    private static Constraint _lex_chain_channel(IntVar[][] strings, IntVar[] ints) {
1621        return Constraints.lexChainChannel(strings, ints);
1622    }
1623
1624    private static Constraint _difference(CSet minuend, CSet subtrahend, CSet difference) {
1625        return Constraints.difference(
1626                minuend.getSet(), minuend.getCard(),
1627                subtrahend.getSet(), subtrahend.getCard(),
1628                difference.getSet(), difference.getCard());
1629    }
1630
1631    private static Constraint _intersection(CSet[] operands, CSet intersection) {
1632        return Constraints.intersection(mapSet(operands), mapCard(operands), intersection.getSet(), intersection.getCard());
1633    }
1634
1635    private static Constraint _union(CSet[] operands, CSet union, boolean disjoint) {
1636        return Constraints.union(
1637                mapSet(operands), mapCard(operands),
1638                union.getSet(), union.getCard(),
1639                disjoint);
1640    }
1641
1642    private IntVar _offset(IntVar var, int offset) {
1643        Pair<IntVar, Integer> pair = new Pair<>(var, offset);
1644        IntVar cache = cachedOffset.get(pair);
1645        if (cache == null) {
1646            cache = VF.offset(var, offset);
1647            cachedOffset.put(pair, cache);
1648        }
1649        return cache;
1650    }
1651
1652    private static Constraint _offset(SetVar set, SetVar offseted, int offset) {
1653        return SCF.offSet(set, offseted, offset);
1654    }
1655
1656    private static Constraint _mask(CSet set, CSet masked, int from, int to) {
1657        return Constraints.mask(set.getSet(), set.getCard(), masked.getSet(), masked.getCard(), from, to);
1658    }
1659
1660    private static Constraint _subset_eq(CSet sub, CSet sup) {
1661        return Constraints.subsetEq(sub.getSet(), sub.getCard(), sup.getSet(), sup.getCard());
1662    }
1663
1664    private static enum Rel {
1665
1666        EQ("="),
1667        NQ("!="),
1668        LT("<"),
1669        LE("<="),
1670        GT(">"),
1671        GE(">=");
1672        private final String syntax;
1673
1674        private Rel(String syntax) {
1675            this.syntax = syntax;
1676        }
1677
1678        private String getSyntax() {
1679            return syntax;
1680        }
1681
1682        private static Rel from(IrCompare.Op op) {
1683            switch (op) {
1684                case Equal:
1685                    return EQ;
1686                case NotEqual:
1687                    return NQ;
1688                case LessThan:
1689                    return LT;
1690                case LessThanEqual:
1691                    return LE;
1692                default:
1693                    throw new IllegalArgumentException();
1694            }
1695        }
1696
1697        private Rel reverse() {
1698            switch (this) {
1699                case LT:
1700                    return GT;
1701                case LE:
1702                    return GE;
1703                case GT:
1704                    return LT;
1705                case GE:
1706                    return LE;
1707                default:
1708                    return this;
1709            }
1710        }
1711    }
1712
1713    private static enum Arithm {
1714
1715        ADD("+"),
1716        MINUS("-");
1717        private final String syntax;
1718
1719        private Arithm(String syntax) {
1720            this.syntax = syntax;
1721        }
1722
1723        private String getSyntax() {
1724            return syntax;
1725        }
1726
1727        private Arithm negate() {
1728            switch (this) {
1729                case ADD:
1730                    return MINUS;
1731                case MINUS:
1732                    return ADD;
1733                default:
1734                    throw new IllegalStateException();
1735            }
1736        }
1737    }
1738    private static final BoolArg ConstraintNoReify = new BoolArg(null, Preference.Constraint);
1739    private static final BoolArg BoolVarNoReify = new BoolArg(null, Preference.BoolVar);
1740
1741    private static class BoolArg {
1742
1743        // The solution needs to be reified in this variable.
1744        // Set to null if no reification needed.
1745        private BoolVar reify;
1746        // The prefered type of solution.
1747        private final Preference preference;
1748
1749        BoolArg(BoolVar reify, Preference preference) {
1750            this.reify = reify;
1751            this.preference = preference;
1752        }
1753
1754        boolean hasReify() {
1755            return reify != null;
1756        }
1757
1758        BoolVar useReify() {
1759            BoolVar tmp = reify;
1760            reify = null;
1761            return tmp;
1762        }
1763
1764        Preference getPreference() {
1765            return preference;
1766        }
1767    }
1768
1769    private static enum Preference {
1770
1771        Constraint,
1772        BoolVar;
1773    }
1774
1775    private class CSet {
1776
1777        private final SetVar set;
1778        private final IrDomain cardDomain;
1779        private IntVar card;
1780
1781        CSet(SetVar set, IrDomain cardDomain) {
1782            this.set = Check.notNull(set);
1783            this.cardDomain = Check.notNull(cardDomain);
1784            this.card =
1785                    cardDomain.getLowBound() > set.getKernelSize() || cardDomain.getHighBound() < set.getEnvelopeSize()
1786                    ? setCardVar(set, cardDomain)
1787                    : null;
1788        }
1789
1790        CSet(SetVar set, IntVar card) {
1791            this.set = Check.notNull(set);
1792            this.cardDomain = null;
1793            this.card = Check.notNull(card);
1794        }
1795
1796        SetVar getSet() {
1797            return set;
1798        }
1799
1800        boolean hasCardCached() {
1801            return card != null;
1802        }
1803
1804        IntVar getCard() {
1805            if (card == null) {
1806                assert cardDomain != null;
1807                card = setCardVar(set, cardDomain);
1808            }
1809            return card;
1810        }
1811    }
1812
1813    private static SetVar[] mapSet(CSet[] sets) {
1814        SetVar[] vars = new SetVar[sets.length];
1815        for (int i = 0; i < sets.length; i++) {
1816            vars[i] = sets[i].getSet();
1817        }
1818        return vars;
1819    }
1820
1821    private static IntVar[] mapCard(CSet[] sets) {
1822        IntVar[] vars = new IntVar[sets.length];
1823        for (int i = 0; i < sets.length; i++) {
1824            vars[i] = sets[i].getCard();
1825        }
1826        return vars;
1827    }
1828}