Source code

001package org.clafer.ast.compiler;
002
003import gnu.trove.list.array.TIntArrayList;
004import java.util.ArrayList;
005import java.util.Arrays;
006import java.util.Collections;
007import java.util.HashMap;
008import java.util.List;
009import java.util.Map;
010import java.util.Map.Entry;
011import java.util.Set;
012import org.clafer.ast.AstAbstractClafer;
013import org.clafer.ast.AstArithm;
014import org.clafer.ast.AstBoolArithm;
015import org.clafer.ast.AstBoolExpr;
016import org.clafer.ast.AstCard;
017import org.clafer.ast.AstClafer;
018import org.clafer.ast.AstCompare;
019import org.clafer.ast.AstConcreteClafer;
020import org.clafer.ast.AstConstant;
021import org.clafer.ast.AstConstraint;
022import org.clafer.ast.AstDecl;
023import org.clafer.ast.AstDifference;
024import org.clafer.ast.AstDowncast;
025import org.clafer.ast.AstException;
026import org.clafer.ast.AstExpr;
027import org.clafer.ast.AstExprVisitor;
028import org.clafer.ast.AstGlobal;
029import org.clafer.ast.AstIfThenElse;
030import org.clafer.ast.AstIntClafer;
031import org.clafer.ast.AstIntersection;
032import org.clafer.ast.AstJoin;
033import org.clafer.ast.AstJoinParent;
034import org.clafer.ast.AstJoinRef;
035import org.clafer.ast.AstLocal;
036import org.clafer.ast.AstMembership;
037import org.clafer.ast.AstMinus;
038import org.clafer.ast.AstModel;
039import org.clafer.ast.AstNot;
040import org.clafer.ast.AstQuantify;
041import org.clafer.ast.AstQuantify.Quantifier;
042import org.clafer.ast.AstRef;
043import org.clafer.ast.AstSetExpr;
044import org.clafer.ast.AstSetTest;
045import org.clafer.ast.AstSum;
046import org.clafer.ast.AstTernary;
047import org.clafer.ast.AstThis;
048import org.clafer.ast.AstUnion;
049import org.clafer.ast.AstUpcast;
050import org.clafer.ast.AstUtil;
051import org.clafer.ast.Card;
052import org.clafer.ast.analysis.AbstractOffsetAnalyzer;
053import org.clafer.ast.analysis.Analysis;
054import org.clafer.ast.analysis.Analyzer;
055import org.clafer.ast.analysis.CardAnalyzer;
056import org.clafer.ast.analysis.Format;
057import org.clafer.ast.analysis.FormatAnalyzer;
058import org.clafer.ast.analysis.GlobalCardAnalyzer;
059import org.clafer.ast.analysis.OptimizerAnalyzer;
060import org.clafer.ast.analysis.PartialIntAnalyzer;
061import org.clafer.ast.analysis.PartialSolution;
062import org.clafer.ast.analysis.PartialSolutionAnalyzer;
063import org.clafer.ast.analysis.ScopeAnalyzer;
064import org.clafer.ast.analysis.SymmetryAnalyzer;
065import org.clafer.ast.analysis.Type;
066import org.clafer.ast.analysis.TypeAnalyzer;
067import org.clafer.collection.DisjointSets;
068import org.clafer.collection.Pair;
069import org.clafer.collection.Triple;
070import org.clafer.common.Check;
071import org.clafer.common.Util;
072import org.clafer.graph.GraphUtil;
073import org.clafer.graph.KeyGraph;
074import org.clafer.graph.Vertex;
075import org.clafer.ir.IrBoolExpr;
076import org.clafer.ir.IrBoolVar;
077import org.clafer.ir.IrDomain;
078import org.clafer.ir.IrExpr;
079import org.clafer.ir.IrIntExpr;
080import org.clafer.ir.IrIntVar;
081import org.clafer.ir.IrModule;
082import org.clafer.ir.IrSetExpr;
083import org.clafer.ir.IrSetVar;
084import org.clafer.ir.IrUtil;
085import static org.clafer.ir.Irs.*;
086import org.clafer.objective.Objective;
087import org.clafer.scope.Scope;
088
089/**
090 * Compile from AST to IR.
091 *
092 * @author jimmy
093 */
094public class AstCompiler {
095
096    public static final Analyzer[] DefaultAnalyzers = new Analyzer[]{
097        new TypeAnalyzer(),
098        new GlobalCardAnalyzer(),
099        new ScopeAnalyzer(),
100        new CardAnalyzer(),
101        new FormatAnalyzer(),
102        new AbstractOffsetAnalyzer(),
103        new OptimizerAnalyzer(),
104        new PartialSolutionAnalyzer(),
105        new PartialIntAnalyzer(),
106        new SymmetryAnalyzer(),
107        // Reanalyze types
108        new TypeAnalyzer()
109    };
110    private final Analysis analysis;
111    private final IrModule module;
112    private final boolean fullSymmetryBreaking;
113
114    private AstCompiler(AstModel model, Scope scope, IrModule module, Analyzer[] analyzers, boolean fullSymmetryBreaking) {
115        this(model, scope, Collections.<Objective>emptyList(), module, analyzers, fullSymmetryBreaking);
116    }
117
118    private AstCompiler(AstModel model, Scope scope, List<Objective> objectives, IrModule module, Analyzer[] analyzers, boolean fullSymmetryBreaking) {
119        this.analysis = Analysis.analyze(model, scope, objectives, analyzers);
120        this.module = Check.notNull(module);
121        this.fullSymmetryBreaking = fullSymmetryBreaking;
122    }
123
124    public static AstSolutionMap compile(AstModel in, Scope scope, IrModule out, boolean fullSymmetryBreaking) {
125        return compile(in, scope, out, DefaultAnalyzers, fullSymmetryBreaking);
126    }
127
128    public static AstSolutionMap compile(AstModel in, Scope scope, IrModule out, Analyzer[] analyzers, boolean fullSymmetryBreaking) {
129        AstCompiler compiler = new AstCompiler(in, scope, out, analyzers, fullSymmetryBreaking);
130        return compiler.compile();
131    }
132
133    public static AstSolutionMap compile(AstModel in, Scope scope, Objective objective, IrModule out, boolean fullSymmetryBreaking) {
134        return compile(in, scope, objective, out, DefaultAnalyzers, fullSymmetryBreaking);
135    }
136
137    public static AstSolutionMap compile(AstModel in, Scope scope, Objective objective, IrModule out, Analyzer[] analyzers, boolean fullSymmetryBreaking) {
138        AstCompiler compiler = new AstCompiler(in, scope, Collections.singletonList(objective),
139                out, analyzers, fullSymmetryBreaking);
140        return compiler.compile();
141    }
142
143    /**
144     * @return the order to initialize regular variables
145     */
146    private List<AstClafer> initOrder() {
147        List<AstAbstractClafer> abstractClafers = analysis.getAbstractClafers();
148        List<AstConcreteClafer> concreteClafers = analysis.getConcreteClafers();
149
150        KeyGraph<AstClafer> dependency = new KeyGraph<>();
151        for (AstAbstractClafer abstractClafer : abstractClafers) {
152            Vertex<AstClafer> node = dependency.getVertex(abstractClafer);
153            for (AstClafer sub : abstractClafer.getSubs()) {
154                node.addNeighbour(dependency.getVertex(sub));
155            }
156        }
157        for (AstConcreteClafer concreteClafer : concreteClafers) {
158            Vertex<AstClafer> node = dependency.getVertex(concreteClafer);
159            if (Format.ParentGroup.equals(getFormat(concreteClafer))) {
160                /*
161                 * Low group does not create the dependency because it does not
162                 * require the parent to initialize first. This allows for
163                 * models like the one below.
164                 *
165                 * abstract Path
166                 *     p : Path ?
167                 *
168                 * If the "?" were a fixed cardinality instead, then an
169                 * exception will occur, but the model would not be satisfiable
170                 * anyways for any fixed cardinality greater than zero.
171                 */
172                node.addNeighbour(dependency.getVertex(concreteClafer.getParent()));
173            }
174        }
175        List<Set<AstClafer>> components = GraphUtil.computeStronglyConnectedComponents(dependency);
176        List<AstClafer> clafers = new ArrayList<>();
177        for (Set<AstClafer> component : components) {
178            if (component.size() != 1) {
179                // See the above comment about low groups.
180                throw new AstException("Cannot satisfy the cycle " + component);
181            }
182            clafers.addAll(component);
183        }
184        return clafers;
185    }
186
187    private AstSolutionMap compile() {
188        IrSetVar rootSet = constant(new int[]{0});
189        sets.put(analysis.getModel(), rootSet);
190        siblingSets.put(analysis.getModel(), new IrSetVar[]{rootSet});
191        memberships.put(analysis.getModel(), new IrBoolExpr[]{True});
192
193        List<AstClafer> clafers = initOrder();
194        for (AstClafer clafer : clafers) {
195            if (clafer instanceof AstConcreteClafer && !AstUtil.isRoot((AstConcreteClafer) clafer)) {
196                initConcrete((AstConcreteClafer) clafer);
197            } else if (clafer instanceof AstAbstractClafer) {
198                initAbstract((AstAbstractClafer) clafer);
199            }
200        }
201        for (AstClafer clafer : clafers) {
202            if (clafer instanceof AstConcreteClafer && !AstUtil.isRoot((AstConcreteClafer) clafer)) {
203                constrainConcrete((AstConcreteClafer) clafer);
204            } else if (clafer instanceof AstAbstractClafer) {
205                constrainAbstract((AstAbstractClafer) clafer);
206            }
207            constrainGroupCardinality(clafer);
208        }
209
210        Map<AstConstraint, IrBoolVar> softVars = new HashMap<>();
211        for (AstConstraint constraint : analysis.getConstraints()) {
212            AstClafer clafer = constraint.getContext();
213            int scope = getScope(clafer);
214            if (analysis.isHard(constraint)) {
215                for (int j = 0; j < scope; j++) {
216                    ExpressionCompiler expressionCompiler = new ExpressionCompiler(j);
217                    IrBoolExpr thisConstraint = expressionCompiler.compile(analysis.getExpr(constraint));
218                    module.addConstraint(implies(memberships.get(clafer)[j], thisConstraint));
219                }
220            } else {
221                IrBoolVar softVar = bool(constraint.toString());
222                softVars.put(constraint, softVar);
223                for (int j = 0; j < scope; j++) {
224                    ExpressionCompiler expressionCompiler = new ExpressionCompiler(j);
225                    IrBoolExpr thisConstraint = expressionCompiler.compile(analysis.getExpr(constraint));
226                    module.addConstraint(ifOnlyIf(softVar, implies(memberships.get(clafer)[j], thisConstraint)));
227                }
228                module.addVariable(softVar);
229            }
230        }
231        IrIntExpr softSum = add(softVars.values());
232        IrIntVar sumSoftVars = domainInt("SumSoftVar", softSum.getDomain());
233        module.addConstraint(equal(sumSoftVars, softSum));
234
235        for (IrSetVar[] childSet : siblingSets.values()) {
236            for (IrSetVar set : childSet) {
237                module.addVariable(set);
238            }
239        }
240        for (IrIntVar[] refs : refPointers.values()) {
241            for (IrIntVar ref : refs) {
242                module.addVariable(ref);
243            }
244        }
245
246        for (Set<AstClafer> component : analysis.getClafersInParentAndSubOrder()) {
247            if (component.size() > 1) {
248                /*
249                 * Add additional constraints for to handle cases where a
250                 * descendent inherits an ancestor.
251                 *
252                 * Let A be an abstract Clafer and B be a descendant of A that
253                 * inherits A. Let F be a mapping every B to its ancestor A.
254                 * Enforce that F is an acyclic function.
255                 */
256                List<AstClafer> types = new ArrayList<>();
257                for (AstClafer clafer : component) {
258                    types.add(clafer);
259                }
260                AstAbstractClafer unionType = (AstAbstractClafer) AstUtil.getLowestCommonSupertype(types);
261                IrIntExpr[] edges = new IrIntExpr[getScope(unionType)];
262                IrIntExpr uninitialized = constant(edges.length);
263                Arrays.fill(edges, uninitialized);
264                for (AstClafer clafer : component) {
265                    if (clafer instanceof AstConcreteClafer) {
266                        AstConcreteClafer concreteChild = (AstConcreteClafer) clafer;
267                        IrBoolExpr[] members = memberships.get(concreteChild);
268                        IrIntExpr[] parents = parentPointers.get(concreteChild);
269                        int offset = getOffset(unionType, concreteChild);
270                        int parentOffset = getOffset(unionType, concreteChild.getParent());
271                        for (int i = 0; i < members.length; i++) {
272                            assert edges[i + offset] == uninitialized;
273                            IrIntExpr value = ternary(members[i],
274                                    // Add the offset to upcast the parent pointer
275                                    add(parents[i], parentOffset),
276                                    uninitialized);
277                            IrIntVar edge = domainInt(
278                                    "Edge@" + concreteChild + "->" + concreteChild.getParent() + "#" + i,
279                                    value.getDomain());
280                            module.addConstraint(equal(edge, value));
281                            edges[i + offset] = edge;
282                        }
283                    }
284                }
285                for (AstClafer clafer : component) {
286                    if (clafer instanceof AstConcreteClafer) {
287                        IrBoolExpr[] members = memberships.get(clafer);
288                        int offset = getOffset(unionType, clafer);
289                        for (int i = 0; i < members.length; i++) {
290                            for (int j = i + 1; j < members.length; j++) {
291                                /*
292                                 * Symmetry breaking. The lower indexed element
293                                 * appears on top of the higher indexed element.
294                                 */
295                                module.addConstraint(unreachable(edges, i + offset, j + offset));
296                            }
297                        }
298                    }
299                }
300                module.addConstraint(acyclic(edges));
301            }
302        }
303
304        ExpressionCompiler expressionCompiler = new ExpressionCompiler(0);
305        Map<Objective, IrIntVar> objectiveVars = new HashMap<>();
306        Map<Objective, AstSetExpr> objectives = analysis.getObjectiveExprs();
307        for (Entry<Objective, AstSetExpr> objective : objectives.entrySet()) {
308            IrIntExpr objectiveExpr = expressionCompiler.asInt(
309                    expressionCompiler.compile(objective.getValue()));
310            IrIntVar objectiveVar = domainInt("Objective" + objective.getKey(),
311                    objectiveExpr.getDomain());
312            module.addConstraint(equal(objectiveVar, objectiveExpr));
313            objectiveVars.put(objective.getKey(), objectiveVar);
314        }
315        return new AstSolutionMap(analysis.getModel(), siblingSets, refPointers,
316                softVars, sumSoftVars,
317                objectiveVars, analysis);
318    }
319
320    private void initConcrete(AstConcreteClafer clafer) {
321        parentPointers.put(clafer, buildParentPointers(clafer));
322        if (clafer.hasRef()) {
323            refPointers.put(clafer.getRef(), buildRefPointers(clafer.getRef()));
324        }
325        switch (getFormat(clafer)) {
326            case LowGroup:
327                initLowGroupConcrete(clafer);
328                break;
329            case ParentGroup:
330                initParentGroupConcrete(clafer);
331                break;
332            default:
333                throw new AstException();
334        }
335
336        IrSetVar[] siblingSet = siblingSets.get(clafer);
337        switch (siblingSet.length) {
338            case 0:
339                sets.put(clafer, EmptySet);
340                break;
341            case 1:
342                sets.put(clafer, siblingSet[0]);
343                break;
344            default:
345                IrSetExpr union = union(siblingSet, true);
346                IrSetVar set = set(clafer.getName(), union.getEnv(), union.getKer(), union.getCard());
347                module.addConstraint(equal(set, union));
348                sets.put(clafer, set);
349                break;
350        }
351
352        if (fullSymmetryBreaking) {
353            int scope = getScope(clafer);
354            int parentScope = getScope(clafer.getParent());
355            IrIntExpr[][] index;
356            AstRef ref = AstUtil.getInheritedRef(clafer);
357            // If the Clafer either needs children or reference to be introduce symmetry.
358            if (analysis.hasInteritedBreakableChildren(clafer)
359                    || (ref != null && analysis.isBreakableRef(ref))
360                    || analysis.isInheritedBreakableTarget(clafer)) {
361                index = new IrIntExpr[parentScope][getCard(clafer).getHigh()];
362                for (int i = 0; i < index.length; i++) {
363                    for (int j = 0; j < index[i].length; j++) {
364                        index[i][j] =
365                                boundInt(clafer.getName() + "@Index#" + i + "#" + j, -1, scope);
366                    }
367                }
368            } else {
369                // Optimize for nonsymmetric nodes. Don't compute the smallest indices, 
370                // just use the cardinalities.
371                IrSetVar[] childSet = siblingSets.get(clafer);
372                index = new IrIntExpr[childSet.length][];
373                for (int i = 0; i < index.length; i++) {
374                    index[i] = new IrIntExpr[]{card(childSet[i])};
375                }
376            }
377            indices.put(clafer, index);
378        }
379    }
380
381    private void constrainConcrete(AstConcreteClafer clafer) {
382        IrSetExpr[] siblingSet = siblingSets.get(clafer);
383        IrIntExpr[] parents = parentPointers.get(clafer);
384        if (!getPartialSolution(clafer).parentSolutionKnown()) {
385            if (getGlobalCard(clafer).isExact()) {
386                // No unused
387                module.addConstraint(intChannel(parents, siblingSet));
388            } else {
389                IrSetVar unused = set(clafer.getName() + "@Unused", getPartialSolution(clafer).getUnknownClafers());
390                module.addConstraint(intChannel(parents, Util.snoc(siblingSet, unused)));
391            }
392        }
393
394        Pair<AstRef, Integer> refPair = analysis.getInheritedRefId(clafer);
395        AstRef ref = refPair == null ? null : refPair.getFst();
396        int refOffset = refPair == null ? 0 : refPair.getSnd().intValue();
397
398        int scope = getScope(clafer);
399        IrBoolExpr[] members = memberships.get(clafer);
400
401        // Two ids a and b are in the same partition if symmetry breaking guarantees
402        // that ref[a] and ref[b] ard different.
403        DisjointSets<Integer> refPartitions = null;
404        // If the Clafer either needs children or reference to be introduce symmetry.
405        if (fullSymmetryBreaking && scope > 1
406                && (analysis.hasInteritedBreakableChildren(clafer)
407                || (ref != null && analysis.isBreakableRef(ref))
408                || analysis.isInheritedBreakableTarget(clafer))) {
409
410            IrIntExpr[] weight = new IrIntExpr[scope];
411            weights.put(clafer, weight);
412            IrIntExpr[][] index = indices.get(clafer);
413
414            analysis.getHierarcyIds(clafer, refOffset);
415            IrIntExpr[][] childIndices = new IrIntExpr[weight.length][];
416
417            List<Pair<AstClafer, Integer>> offsets = analysis.getHierarcyOffsets(clafer);
418            Collections.reverse(offsets);
419            boolean[] breakableRefIds = new boolean[childIndices.length];
420            for (int i = 0; i < childIndices.length; i++) {
421                List<IrIntExpr> childIndex = new ArrayList<>();
422                for (Pair<AstClafer, Integer> offset : offsets) {
423                    for (AstConcreteClafer child : analysis.getBreakableChildren(offset.getFst())) {
424                        childIndex.addAll(Arrays.asList(indices.get(child)[i + offset.getSnd()]));
425                    }
426                }
427                if (ref != null && analysis.isBreakableRef(ref)) {
428                    breakableRefIds[i] = analysis.isBreakableRefId(ref, i + refOffset);
429                    // References need a positive weight, so to use their value as
430                    // a weight, need to offset it so that it always positive.
431                    childIndex.add(
432                            breakableRefIds[i]
433                            // The id of the target is the weight.
434                            ? minus(refPointers.get(ref)[i + refOffset])
435                            // If analysis says that this id does not need breaking
436                            // then give it a constant weight. Any constant is fine.
437                            : Zero);
438                }
439                if (analysis.isInheritedBreakableTarget(clafer)) {
440                    for (Pair<AstClafer, Integer> hierarchy : analysis.getHierarcyIds(clafer, i)) {
441                        for (AstRef sourceRef : analysis.getBreakableTarget(hierarchy.getFst())) {
442                            IrIntVar[] sourceRefs = refPointers.get(sourceRef);
443
444                            IrIntExpr[] array = new IrIntExpr[sourceRefs.length];
445                            System.arraycopy(sourceRefs, 0, array, 0, array.length);
446                            IrIntExpr count = count(hierarchy.getSnd().intValue(), array);
447                            IrIntVar countVar = domainInt("CountVar" + countCount++, count.getDomain());
448                            module.addConstraint(equal(countVar, count));
449                            childIndex.add(countVar);
450                        }
451                    }
452                }
453                childIndices[i] = childIndex.toArray(new IrIntExpr[childIndex.size()]);
454            }
455            for (int i = 0; i < weight.length; i++) {
456                weight[i] =
457                        childIndices[i].length == 0 ? Zero
458                        : boundInt(clafer.getName() + "#" + i + "@Weight", 0, scope - 1);
459            }
460            if (getScope(clafer.getParent()) > 1) {
461                module.addConstraint(sortChannel(childIndices, weight));
462                for (int i = 0; i < siblingSet.length; i++) {
463                    module.addConstraint(filterString(siblingSet[i], weight, index[i]));
464                }
465            }
466            for (int i = 0; i < parents.length - 1; i++) {
467                if (ref != null && analysis.isBreakableRef(ref) && ref.isUnique()) {
468                    assert childIndices[i + 1].length == childIndices[i].length;
469                    if (childIndices[i].length == 1 && breakableRefIds[i]) {
470                        if (refPartitions == null) {
471                            refPartitions = new DisjointSets<>();
472                        }
473                        refPartitions.union(i, i + 1);
474                    }
475                    // Refs are unique and part of the weight. It is impossible for
476                    // two weights to be the same. Enforce a strict order.
477                    module.addConstraint(implies(and(members[i], equal(parents[i], parents[i + 1])),
478                            sortStrict(childIndices[i + 1], childIndices[i])));
479                } else {
480                    module.addConstraint(implies(equal(parents[i], parents[i + 1]),
481                            sort(childIndices[i + 1], childIndices[i])));
482                }
483            }
484        }
485
486        if (ref != null) {
487            AstClafer tar = ref.getTargetType();
488            IrIntVar[] refs = Arrays.copyOfRange(refPointers.get(ref),
489                    refOffset, refOffset + getScope(clafer));
490            if (ref.isUnique()) {
491                if (getCard(clafer).getHigh() > 1) {
492                    for (int i = 0; i < refs.length - 1; i++) {
493                        for (int j = i + 1; j < refs.length; j++) {
494                            if (refPartitions == null || !refPartitions.connected(i, j)) {
495                                module.addConstraint(
496                                        implies(and(members[i], equal(parents[i], parents[j])),
497                                        notEqual(refs[i], refs[j])));
498                            }
499                        }
500                    }
501                }
502                IrIntExpr size =
503                        ref.getTargetType() instanceof AstIntClafer
504                        ? constant(analysis.getScope().getIntHigh() - analysis.getScope().getIntLow() + 1)
505                        : card(sets.get(ref.getTargetType()));
506                for (IrSetExpr sibling : siblingSet) {
507                    module.addConstraint(lessThanEqual(card(sibling), size));
508                }
509            }
510            assert refs.length == members.length;
511            for (int i = 0; i < members.length; i++) {
512                // The ref pointers must point to the special uninitialized value
513                // if the Clafer owning the ref pointers does not exists.
514                module.addConstraint(ifOnlyIf(not(members[i]), equal(refs[i], getUninitalizedRef(tar))));
515            }
516            if (!(ref.getTargetType() instanceof AstIntClafer)) {
517                IrSetVar targetSet = sets.get(ref.getTargetType());
518                for (int i = 0; i < refs.length; i++) {
519                    // The ref pointers must point to a target that exists.
520                    module.addConstraint(ifOnlyIf(members[i], member(refs[i], targetSet)));
521                }
522            }
523        }
524
525        switch (getFormat(clafer)) {
526            case LowGroup:
527                constrainLowGroupConcrete(clafer);
528                break;
529            case ParentGroup:
530                constrainParentGroupConcrete(clafer);
531                break;
532            default:
533                throw new AstException();
534        }
535    }
536
537    private void constrainGroupCardinality(AstClafer clafer) {
538        Card groupCard = clafer.getGroupCard();
539        List<AstConcreteClafer> children = clafer.getChildren();
540        if (groupCard.isBounded()) {
541            IrBoolExpr[] members = memberships.get(clafer);
542            IrSetVar[][] childrenSets = new IrSetVar[children.size()][];
543            for (int i = 0; i < childrenSets.length; i++) {
544                AstConcreteClafer child = children.get(i);
545                childrenSets[i] = siblingSets.get(child);
546            }
547            int scope = getScope(clafer);
548            for (int i = 0; i < scope; i++) {
549                IrIntExpr[] cards = new IrIntExpr[childrenSets.length];
550                for (int j = 0; j < cards.length; j++) {
551                    cards[j] = card(childrenSets[j][i]);
552                }
553                module.addConstraint(implies(members[i], constrainCard(add(cards), groupCard)));
554            }
555        }
556    }
557
558    private void initLowGroupConcrete(AstConcreteClafer clafer) {
559        PartialSolution partialSolution = getPartialSolution(clafer);
560
561        IrSetVar[] childSet = buildChildSet(clafer);
562        siblingSets.put(clafer, childSet);
563
564        IrBoolExpr[] members = new IrBoolExpr[getScope(clafer)];
565        for (int i = 0; i < members.length; i++) {
566            if (partialSolution.hasClafer(i)) {
567                members[i] = True;
568            } else {
569                members[i] = bool(clafer.getName() + "@Membership#" + i);
570                if (childSet.length == 1 && members.length == 1) {
571                    module.addConstraint(equal(members[i], card(childSet[0])));
572                }
573            }
574        }
575        Check.noNulls(members);
576        memberships.put(clafer, members);
577    }
578
579    private void constrainLowGroupConcrete(AstConcreteClafer clafer) {
580        IrBoolExpr[] members = memberships.get(clafer);
581        IrSetVar set = sets.get(clafer);
582
583        IrBoolExpr[] parentMembership = memberships.get(clafer.getParent());
584        Card card = getCard(clafer);
585        IrSetVar[] childSet = siblingSets.get(clafer);
586
587        if (fullSymmetryBreaking) {
588            module.addConstraint(selectN(members, card(set)));
589            module.addConstraint(sort(childSet));
590        }
591
592        for (int i = 0; i < parentMembership.length; i++) {
593            IrBoolExpr parentMember = parentMembership[i];
594            if (card.isBounded()) {
595                // Enforce cardinality.
596                module.addConstraint(implies(parentMember, constrainCard(card(childSet[i]), card)));
597            }
598            module.addConstraint(implies(not(parentMember), equal(childSet[i], EmptySet)));
599        }
600
601
602        if (!(childSet.length == 1 && members.length == 1)) {
603            module.addConstraint(boolChannel(members, set));
604        }
605
606        /**
607         * What is this optimization?
608         *
609         * Force the lower number atoms to choose lower number parents. For
610         * example consider the following Clafer model:
611         *
612         * <pre>
613         * Person 2
614         *     Hand 2
615         * </pre>
616         *
617         * The constraint forbids the case where Hand0 belongs to Person1 and
618         * Hand1 belongs to Person0. Otherwise, the children can swap around
619         * creating many isomorphic solutions.
620         */
621        if (fullSymmetryBreaking) {
622            module.addConstraint(sort(parentPointers.get(clafer)));
623        }
624    }
625
626    private void initParentGroupConcrete(AstConcreteClafer clafer) {
627        PartialSolution partialParentSolution = getPartialParentSolution(clafer);
628
629        IrSetVar[] children = new IrSetVar[partialParentSolution.size()];
630        assert getCard(clafer).getLow() == getCard(clafer).getHigh();
631        int lowCard = getCard(clafer).getLow();
632        for (int i = 0; i < children.length; i++) {
633            if (partialParentSolution.hasClafer(i)) {
634                children[i] = constant(Util.fromTo(i * lowCard, i * lowCard + lowCard));
635            } else {
636                children[i] = set(clafer.getName() + "#" + i, Util.fromTo(i * lowCard, i * lowCard + lowCard));
637            }
638        }
639
640        siblingSets.put(clafer, children);
641
642        IrBoolExpr[] members = new IrBoolExpr[getScope(clafer)];
643        IrBoolExpr[] parentMembership = memberships.get(clafer.getParent());
644        if (lowCard == 1) {
645            if (members.length == parentMembership.length) {
646                members = parentMembership;
647            } else {
648                System.arraycopy(parentMembership, 0, members, 0, parentMembership.length);
649                Arrays.fill(members, parentMembership.length, members.length, False);
650            }
651        } else {
652            for (int i = 0; i < parentMembership.length; i++) {
653                for (int j = 0; j < lowCard; j++) {
654                    members[i * lowCard + j] = parentMembership[i];
655                }
656            }
657            Arrays.fill(members, parentMembership.length * lowCard, members.length, False);
658        }
659        Check.noNulls(members);
660        memberships.put(clafer, members);
661    }
662
663    private void constrainParentGroupConcrete(AstConcreteClafer clafer) {
664        PartialSolution partialParentSolution = getPartialParentSolution(clafer);
665
666        IrSetVar[] children = siblingSets.get(clafer);
667        assert getCard(clafer).getLow() == getCard(clafer).getHigh();
668        int lowCard = getCard(clafer).getLow();
669        for (int i = 0; i < children.length; i++) {
670            if (!partialParentSolution.hasClafer(i)) {
671                if (lowCard == 1) {
672                    module.addConstraint(equal(memberships.get(clafer.getParent())[i],
673                            card(children[i])));
674                }
675                module.addConstraint(implies(memberships.get(clafer.getParent())[i],
676                        equal(children[i], constant(Util.fromTo(i * lowCard, i * lowCard + lowCard)))));
677                module.addConstraint(implies(not(memberships.get(clafer.getParent())[i]),
678                        equal(children[i], EmptySet)));
679
680            }
681        }
682    }
683
684    private void initAbstract(AstAbstractClafer clafer) {
685        IrSetVar[] subSets = new IrSetVar[clafer.getSubs().size()];
686        IrBoolExpr[] members = new IrBoolExpr[getScope(clafer)];
687        for (int i = 0; i < subSets.length; i++) {
688            AstClafer sub = clafer.getSubs().get(i);
689            subSets[i] = sets.get(sub);
690            IrBoolExpr[] subMembers = memberships.get(sub);
691            int offset = getOffset(clafer, sub);
692            for (int j = 0; j < subMembers.length; j++) {
693                assert members[offset + j] == null;
694                members[offset + j] = Check.notNull(subMembers[j]);
695            }
696        }
697        if (subSets.length == 1) {
698            sets.put(clafer, sets.get(clafer.getSubs().get(0)));
699        } else {
700            TIntArrayList env = new TIntArrayList();
701            TIntArrayList ker = new TIntArrayList();
702            for (int i = 0; i < members.length; i++) {
703                if (IrUtil.isTrue(members[i])) {
704                    ker.add(i);
705                }
706                if (!IrUtil.isFalse(members[i])) {
707                    env.add(i);
708                }
709            }
710            IrSetVar unionSet = set(clafer.getName(), env.toArray(), ker.toArray());
711            if (!AstUtil.isTypeRoot(clafer)) {
712                module.addConstraint(boolChannel(members, unionSet));
713            }
714            sets.put(clafer, unionSet);
715        }
716        Check.noNulls(members);
717        memberships.put(clafer, members);
718
719        if (clafer.hasRef()) {
720            refPointers.put(clafer.getRef(), buildRefPointers(clafer.getRef()));
721        }
722    }
723
724    private void constrainAbstract(AstAbstractClafer clafer) {
725        // Do nothing.
726    }
727    private final Map<AstClafer, IrSetVar> sets = new HashMap<>();
728    private final Map<AstClafer, IrSetVar[]> siblingSets = new HashMap<>();
729    private final Map<AstClafer, IrBoolExpr[]> memberships = new HashMap<>();
730    private final Map<AstConcreteClafer, IrIntVar[]> parentPointers = new HashMap<>();
731    private final Map<AstRef, IrIntVar[]> refPointers = new HashMap<>();
732    private final Map<AstClafer, IrIntExpr[][]> indices = new HashMap<>();
733    // The weight of an uninitialed Clafer is always zero.
734    private final Map<AstClafer, IrIntExpr[]> weights = new HashMap<>();
735    private int countCount = 0;
736    private int localCount = 0;
737
738    private class ExpressionCompiler implements AstExprVisitor<Void, IrExpr> {
739
740        private final int thisId;
741        private final Map<AstLocal, IrIntExpr> locals = new HashMap<>();
742
743        private ExpressionCompiler(int thisId) {
744            this.thisId = thisId;
745        }
746
747        private IrExpr compile(AstExpr expr) {
748            return expr.accept(this, null);
749        }
750
751        private IrExpr[] compile(AstExpr[] exprs) {
752            IrExpr[] compiled = new IrExpr[exprs.length];
753            for (int i = 0; i < compiled.length; i++) {
754                compiled[i] = compile(exprs[i]);
755            }
756            return compiled;
757        }
758
759        private IrBoolExpr compile(AstBoolExpr expr) {
760            return (IrBoolExpr) compile((AstExpr) expr);
761        }
762
763        private IrBoolExpr[] compile(AstBoolExpr[] exprs) {
764            IrBoolExpr[] compiled = new IrBoolExpr[exprs.length];
765            for (int i = 0; i < compiled.length; i++) {
766                compiled[i] = compile(exprs[i]);
767            }
768            return compiled;
769        }
770
771        private IrIntExpr asInt(IrExpr expr) {
772            if (expr instanceof IrIntExpr) {
773                return (IrIntExpr) expr;
774            }
775            if (expr instanceof IrSetExpr) {
776                return sum((IrSetExpr) expr);
777            }
778            // Bug.
779            throw new AstException("Should not have passed type checking.");
780        }
781
782        private IrIntExpr[] asInts(IrExpr[] exprs) {
783            IrIntExpr[] ints = new IrIntExpr[exprs.length];
784            for (int i = 0; i < ints.length; i++) {
785                ints[i] = asInt(exprs[i]);
786            }
787            return ints;
788        }
789
790        private IrSetExpr asSet(IrExpr expr) {
791            if (expr instanceof IrIntExpr) {
792                return singleton((IrIntExpr) expr);
793            }
794            if (expr instanceof IrSetExpr) {
795                return (IrSetExpr) expr;
796            }
797            // Bug.
798            throw new AstException("Should not have passed type checking.");
799        }
800
801        private IrSetExpr[] asSets(IrExpr[] exprs) {
802            IrSetExpr[] sets = new IrSetExpr[exprs.length];
803            for (int i = 0; i < sets.length; i++) {
804                sets[i] = asSet(exprs[i]);
805            }
806            return sets;
807        }
808
809        @Override
810        public IrExpr visit(AstThis ast, Void a) {
811            return constant(thisId);
812        }
813
814        @Override
815        public IrExpr visit(AstGlobal ast, Void a) {
816            IrSetVar global = sets.get(ast.getType());
817            if (global.getEnv().size() == 1) {
818                int[] constant = IrUtil.getConstant(global);
819                if (constant != null) {
820                    return constant(constant[0]);
821                }
822            }
823            return global;
824        }
825
826        @Override
827        public IrExpr visit(AstConstant ast, Void a) {
828            int[] value = ast.getValue();
829            if (value.length == 1) {
830                return constant(value[0]);
831            }
832            return constant(value);
833        }
834
835        @Override
836        public IrExpr visit(AstJoin ast, Void a) {
837            return doJoin(compile(ast.getLeft()), ast.getRight());
838        }
839
840        private IrExpr doJoin(IrExpr left, AstConcreteClafer right) {
841            if (left instanceof IrIntExpr) {
842                IrIntExpr $intLeft = (IrIntExpr) left;
843                if (Format.ParentGroup.equals(getFormat(right)) && getCard(right).getLow() == 1) {
844                    assert getCard(right).isExact();
845                    return $intLeft;
846                }
847                // Why empty set? The "take" var can contain unused.
848                return joinRelation(singleton($intLeft), Util.snoc(siblingSets.get(right), EmptySet), true);
849            } else if (left instanceof IrSetExpr) {
850                IrSetExpr $setLeft = (IrSetExpr) left;
851                // Why empty set? The "take" var can contain unused.
852                return joinRelation($setLeft, Util.snoc(siblingSets.get(right), EmptySet), true);
853            }
854            throw new AstException();
855        }
856
857        @Override
858        public IrExpr visit(AstJoinParent ast, Void a) {
859            AstConcreteClafer childrenType = (AstConcreteClafer) getCommonSupertype(ast.getChildren());
860
861            IrExpr children = compile(ast.getChildren());
862            if (children instanceof IrIntExpr) {
863                IrIntExpr intChildren = (IrIntExpr) children;
864                switch (getFormat(childrenType)) {
865                    case ParentGroup:
866                        assert getCard(childrenType).isExact();
867                        int lowCard = getCard(childrenType).getLow();
868                        return div(intChildren, constant(lowCard));
869                    case LowGroup:
870                        return element(parentPointers.get(childrenType), intChildren);
871                }
872            } else if (children instanceof IrSetExpr) {
873                IrSetExpr setChildren = (IrSetExpr) children;
874                return joinFunction(setChildren, parentPointers.get(childrenType), null);
875            }
876            throw new AstException();
877        }
878
879        @Override
880        public IrExpr visit(AstJoinRef ast, Void a) {
881            AstSetExpr deref = ast.getDeref();
882            AstClafer derefType = getCommonSupertype(deref);
883
884            Integer globalCardinality = null;
885            IrExpr $deref;
886            if (derefType.getRef().isUnique()) {
887                if (deref instanceof AstJoin) {
888                    AstJoin join = (AstJoin) deref;
889                    IrExpr left = compile(join.getLeft());
890                    $deref = doJoin(left, join.getRight());
891
892                    globalCardinality = left instanceof IrSetExpr
893                            ? ((IrSetExpr) left).getCard().getHighBound()
894                            : 1;
895                } else {
896                    $deref = compile(deref);
897                    if (derefType instanceof AstConcreteClafer) {
898                        globalCardinality = getScope(((AstConcreteClafer) derefType).getParent());
899                    }
900                }
901            } else {
902                $deref = compile(deref);
903            }
904
905            if ($deref instanceof IrIntExpr) {
906                IrIntExpr $intDeref = (IrIntExpr) $deref;
907                // Why zero? The "take" var can contain unused.
908                return element(Util.snoc(refPointers.get(derefType.getRef()), Zero), $intDeref);
909            } else if ($deref instanceof IrSetExpr) {
910                IrSetExpr $setDeref = (IrSetExpr) $deref;
911                // Why zero? The "take" var can contain unused.
912                return joinFunction($setDeref, Util.snoc(refPointers.get(derefType.getRef()), Zero), globalCardinality);
913            }
914            throw new AstException();
915        }
916
917        @Override
918        public IrExpr visit(AstCard ast, Void a) {
919            IrExpr set = compile(ast.getSet());
920            if (set instanceof IrIntExpr) {
921                return One;
922            }
923            return card((IrSetExpr) set);
924        }
925
926        @Override
927        public IrExpr visit(AstNot ast, Void a) {
928            return not(compile(ast.getExpr()));
929        }
930
931        @Override
932        public IrExpr visit(AstMinus ast, Void a) {
933            return minus(asInt(compile(ast.getExpr())));
934        }
935
936        @Override
937        public IrExpr visit(AstSetTest ast, Void a) {
938            IrExpr left = compile(ast.getLeft());
939            IrExpr right = compile(ast.getRight());
940
941            if (left instanceof IrIntExpr && right instanceof IrIntExpr) {
942                IrIntExpr $intLeft = (IrIntExpr) left;
943                IrIntExpr $intRight = (IrIntExpr) right;
944
945                switch (ast.getOp()) {
946                    case Equal:
947                        return equal($intLeft, $intRight);
948                    case NotEqual:
949                        return notEqual($intLeft, $intRight);
950                }
951            }
952
953            switch (ast.getOp()) {
954                case Equal:
955                    return equal(asSet(left), asSet(right));
956                case NotEqual:
957                    return notEqual(asSet(left), asSet(right));
958                default:
959                    throw new AstException();
960            }
961        }
962
963        @Override
964        public IrExpr visit(AstCompare ast, Void a) {
965            IrIntExpr left = asInt(compile(ast.getLeft()));
966            IrIntExpr right = asInt(compile(ast.getRight()));
967            switch (ast.getOp()) {
968                case LessThan:
969                    return lessThan(left, right);
970                case LessThanEqual:
971                    return lessThanEqual(left, right);
972                case GreaterThan:
973                    return greaterThan(left, right);
974                case GreaterThanEqual:
975                    return greaterThanEqual(left, right);
976                default:
977                    throw new AstException();
978            }
979        }
980
981        @Override
982        public IrExpr visit(AstArithm ast, Void a) {
983            IrIntExpr[] operands = asInts(compile(ast.getOperands()));
984            switch (ast.getOp()) {
985                case Add:
986                    return add(operands);
987                case Sub:
988                    return sub(operands);
989                case Mul:
990                    IrIntExpr product = operands[0];
991                    for (int i = 1; i < operands.length; i++) {
992                        product = mul(product, operands[i]);
993                    }
994                    return product;
995                case Div:
996                    IrIntExpr quotient = operands[0];
997                    for (int i = 1; i < operands.length; i++) {
998                        quotient = div(quotient, operands[i]);
999                    }
1000                    return quotient;
1001                default:
1002                    throw new AstException();
1003            }
1004        }
1005
1006        @Override
1007        public IrExpr visit(AstSum ast, Void a) {
1008            AstSetExpr set = ast.getSet();
1009            AstClafer setType = getCommonSupertype(set);
1010            assert setType.hasRef();
1011            IrIntVar[] refs = refPointers.get(setType.getRef());
1012
1013            IrBoolExpr[] members;
1014            if (ast.getSet() instanceof AstGlobal) {
1015                members = memberships.get(setType);
1016            } else {
1017                IrExpr $set = compile(ast.getSet());
1018                if (set instanceof IrIntExpr) {
1019                    IrIntExpr intSet = (IrIntExpr) set;
1020                    return element(refs, intSet);
1021                }
1022                IrSetExpr setSet = (IrSetExpr) $set;
1023                assert setSet.getEnv().getLowBound() >= 0;
1024                members = new IrBoolExpr[setSet.getEnv().getHighBound() + 1];
1025                for (int i = 0; i < members.length; i++) {
1026                    members[i] = bool("SumMember@" + i);
1027                }
1028                module.addConstraint(boolChannel(members, setSet));
1029            }
1030            assert members.length <= refs.length;
1031
1032            IrIntVar[] score = new IrIntVar[members.length];
1033            for (int i = 0; i < members.length; i++) {
1034                IrDomain domain = refs[i].getDomain();
1035                int uninitializedRef = getUninitalizedRef(setType.getRef().getTargetType());
1036                // Score's use 0 as the uninitialized value.
1037                domain = IrUtil.add(IrUtil.remove(domain, uninitializedRef), 0);
1038                score[i] = domainInt("Score@" + i, domain);
1039                module.addConstraint(ifThenElse(members[i],
1040                        equal(score[i], refs[i]), equal(score[i], 0)));
1041            }
1042            return add(score);
1043        }
1044
1045        @Override
1046        public IrExpr visit(AstBoolArithm ast, Void a) {
1047            IrBoolExpr[] operands = compile(ast.getOperands());
1048            switch (ast.getOp()) {
1049                case And:
1050                    return and(operands);
1051                case IfOnlyIf:
1052                    IrBoolExpr ifOnlyIf = operands[0];
1053                    for (int i = 1; i < operands.length; i++) {
1054                        ifOnlyIf = ifOnlyIf(ifOnlyIf, operands[i]);
1055                    }
1056                    return ifOnlyIf;
1057                case Implies:
1058                    IrBoolExpr implies = operands[0];
1059                    for (int i = 1; i < operands.length; i++) {
1060                        implies = implies(implies, operands[i]);
1061                    }
1062                    return implies;
1063                case Or:
1064                    return or(operands);
1065                case Xor:
1066                    IrBoolExpr xor = operands[0];
1067                    for (int i = 1; i < operands.length; i++) {
1068                        xor = xor(xor, operands[i]);
1069                    }
1070                    return xor;
1071                default:
1072                    throw new AstException();
1073            }
1074        }
1075
1076        @Override
1077        public IrExpr visit(AstDifference ast, Void a) {
1078            return difference(
1079                    asSet(compile(ast.getLeft())),
1080                    asSet(compile(ast.getRight())));
1081        }
1082
1083        @Override
1084        public IrExpr visit(AstIntersection ast, Void a) {
1085            return intersection(
1086                    asSet(compile(ast.getLeft())),
1087                    asSet(compile(ast.getRight())));
1088        }
1089
1090        @Override
1091        public IrExpr visit(AstUnion ast, Void a) {
1092            return union(
1093                    asSet(compile(ast.getLeft())),
1094                    asSet(compile(ast.getRight())));
1095        }
1096
1097        @Override
1098        public IrExpr visit(AstMembership ast, Void a) {
1099            IrExpr member = compile(ast.getMember());
1100            IrExpr set = compile(ast.getSet());
1101            if (member instanceof IrIntExpr && set instanceof IrIntExpr) {
1102                return AstMembership.Op.In.equals(ast.getOp())
1103                        ? equal((IrIntExpr) member, (IrIntExpr) set)
1104                        : notEqual((IrIntExpr) member, (IrIntExpr) set);
1105            }
1106            if (member instanceof IrIntExpr && set instanceof IrSetExpr) {
1107                return AstMembership.Op.In.equals(ast.getOp())
1108                        ? member((IrIntExpr) member, (IrSetExpr) set)
1109                        : notMember((IrIntExpr) member, (IrSetExpr) set);
1110            }
1111            if (member instanceof IrSetExpr && set instanceof IrIntExpr) {
1112                return AstMembership.Op.In.equals(ast.getOp())
1113                        ? equal((IrSetExpr) member, singleton((IrIntExpr) set))
1114                        : notEqual((IrSetExpr) member, singleton((IrIntExpr) set));
1115            }
1116            return AstMembership.Op.In.equals(ast.getOp())
1117                    ? subsetEq(asSet(member), asSet(set))
1118                    : not(subsetEq(asSet(member), asSet(set)));
1119        }
1120
1121        @Override
1122        public IrExpr visit(AstTernary ast, Void a) {
1123            IrBoolExpr antecedent = compile(ast.getAntecedent());
1124            IrExpr consequent = compile(ast.getConsequent());
1125            IrExpr alternative = compile(ast.getAlternative());
1126            if (consequent instanceof IrIntExpr && alternative instanceof IrIntExpr) {
1127                return ternary(antecedent, (IrIntExpr) consequent, (IrIntExpr) alternative);
1128            }
1129            return ternary(antecedent, asSet(consequent), asSet(alternative));
1130        }
1131
1132        @Override
1133        public IrExpr visit(AstIfThenElse ast, Void a) {
1134            return ifThenElse(compile(ast.getAntecedent()), compile(ast.getConsequent()), compile(ast.getAlternative()));
1135        }
1136
1137        @Override
1138        public IrExpr visit(AstDowncast ast, Void a) {
1139            AstSetExpr base = ast.getBase();
1140            int offset = getOffset((AstAbstractClafer) getCommonSupertype(base), ast.getTarget());
1141
1142            IrExpr $base = compile(ast.getBase());
1143            if ($base instanceof IrIntExpr) {
1144                IrIntExpr intBase = (IrIntExpr) $base;
1145                return sub(intBase, constant(offset));
1146            }
1147            return mask((IrSetExpr) $base, offset, offset + getScope(ast.getTarget()));
1148        }
1149
1150        @Override
1151        public IrExpr visit(AstUpcast ast, Void a) {
1152            AstSetExpr base = ast.getBase();
1153            int offset = getOffset(ast.getTarget(), getCommonSupertype(base));
1154
1155            IrExpr $base = compile(ast.getBase());
1156            if ($base instanceof IrIntExpr) {
1157                IrIntExpr intBase = (IrIntExpr) $base;
1158                return add(intBase, constant(offset));
1159            }
1160            return offset((IrSetExpr) $base, offset);
1161        }
1162
1163        @Override
1164        public IrExpr visit(AstLocal ast, Void a) {
1165            return locals.get(ast);
1166        }
1167
1168        private Triple<AstLocal, IrIntExpr, IrBoolExpr>[][] compileDecl(AstDecl decl) {
1169            IrExpr body = compile(decl.getBody());
1170            if (body instanceof IrIntExpr) {
1171                IrIntExpr intBody = (IrIntExpr) body;
1172                @SuppressWarnings("unchecked")
1173                Triple<AstLocal, IrIntExpr, IrBoolExpr>[] labeledPermutation = new Triple[decl.getLocals().length];
1174                for (int i = 0; i < labeledPermutation.length; i++) {
1175                    labeledPermutation[i] = new Triple<AstLocal, IrIntExpr, IrBoolExpr>(
1176                            decl.getLocals()[i], intBody, True);
1177                }
1178                @SuppressWarnings("unchecked")
1179                Triple<AstLocal, IrIntExpr, IrBoolExpr>[][] labeledSequence = new Triple[][]{labeledPermutation};
1180                return labeledSequence;
1181            }
1182            if (body instanceof IrSetExpr) {
1183                IrSetExpr setBody = (IrSetExpr) body;
1184                IrDomain env = setBody.getEnv();
1185                IrDomain ker = setBody.getKer();
1186                // TODO: need a different strategy otherwise
1187                assert env.getLowBound() >= 0;
1188                @SuppressWarnings("unchecked")
1189                Pair<IrIntExpr, IrBoolExpr>[] members = new Pair[env.getHighBound() + 1];
1190                for (int i = 0; i < env.getLowBound(); i++) {
1191                    members[i] = new Pair<IrIntExpr, IrBoolExpr>(constant(i), False);
1192                }
1193                for (int i = env.getLowBound(); i <= env.getHighBound(); i++) {
1194                    members[i] = new Pair<IrIntExpr, IrBoolExpr>(constant(i),
1195                            ker.contains(i) ? True
1196                            : bool(Util.intercalate("/", AstUtil.getNames(decl.getLocals())) + "#" + i + "#" + localCount++));
1197                }
1198                module.addConstraint(boolChannel(Pair.mapSnd(members), setBody));
1199                Pair<IrIntExpr, IrBoolExpr>[][] sequence = decl.isDisjoint() ? Util.permutations(members,
1200                        decl.getLocals().length) : Util.sequence(members, decl.getLocals().length);
1201
1202                @SuppressWarnings("unchecked")
1203                Triple<AstLocal, IrIntExpr, IrBoolExpr>[][] labeledSequence = new Triple[sequence.length][];
1204                for (int i = 0; i < labeledSequence.length; i++) {
1205                    Pair<IrIntExpr, IrBoolExpr>[] permutation = sequence[i];
1206                    @SuppressWarnings("unchecked")
1207                    Triple<AstLocal, IrIntExpr, IrBoolExpr>[] labeledPermutation = new Triple[permutation.length];
1208                    for (int j = 0; j < labeledPermutation.length; j++) {
1209                        labeledPermutation[j] = new Triple<>(
1210                                decl.getLocals()[j], permutation[j]);
1211                    }
1212                    labeledSequence[i] = labeledPermutation;
1213                }
1214                return labeledSequence;
1215            }
1216            throw new AstException();
1217        }
1218
1219        // TODO optimize SOME
1220        @Override
1221        public IrExpr visit(AstQuantify ast, Void a) {
1222            AstDecl decls[] = ast.getDecls();
1223            @SuppressWarnings("unchecked")
1224            Triple<AstLocal, IrIntExpr, IrBoolExpr>[][][] compiledDecls = new Triple[decls.length][][];
1225            for (int i = 0; i < compiledDecls.length; i++) {
1226                compiledDecls[i] = compileDecl(decls[i]);
1227            }
1228            compiledDecls = Util.sequence(compiledDecls);
1229
1230            List<IrBoolExpr> compiled = new ArrayList<>();
1231            for (Triple<AstLocal, IrIntExpr, IrBoolExpr>[][] quants : compiledDecls) {
1232                List<IrBoolExpr> constraints = new ArrayList<>();
1233                for (Triple<AstLocal, IrIntExpr, IrBoolExpr>[] quantDecls : quants) {
1234                    for (Triple<AstLocal, IrIntExpr, IrBoolExpr> quantLocals : quantDecls) {
1235                        constraints.add(quantLocals.getThd());
1236                        locals.put(quantLocals.getFst(), quantLocals.getSnd());
1237                    }
1238                }
1239                IrBoolExpr compiledBody = compile(ast.getBody());
1240                if (Quantifier.All.equals(ast.getQuantifier())) {
1241                    compiled.add(implies(and(constraints), compiledBody));
1242                } else {
1243                    constraints.add(compiledBody);
1244                    compiled.add(and(constraints));
1245                }
1246            }
1247
1248            switch (ast.getQuantifier()) {
1249                case All:
1250                    return and(compiled);
1251                case Lone:
1252                    return lone(compiled);
1253                case None:
1254                    return not(or(compiled));
1255                case One:
1256                    return one(compiled);
1257                case Some:
1258                    return or(compiled);
1259                default:
1260                    throw new AstException();
1261
1262            }
1263        }
1264    };
1265
1266    /*
1267     ******************
1268     * Build functions.
1269     ******************
1270     */
1271    /**
1272     * Build the child set for the Clafer.
1273     *
1274     * @param clafer the Clafer
1275     * @return the variables to represent the child relation
1276     */
1277    private IrSetVar[] buildChildSet(AstConcreteClafer clafer) {
1278        assert Format.LowGroup.equals(getFormat(clafer));
1279
1280        int parentScope = getScope(clafer.getParent());
1281        PartialSolution partialParentSolution = getPartialSolution(clafer.getParent());
1282
1283        int claferScope = getScope(clafer);
1284        Card card = getCard(clafer);
1285        assert card.hasHigh();
1286
1287        int low = 0;
1288        int high = card.getHigh();
1289        int max = claferScope - 1;
1290
1291        IrSetVar[] skip = new IrSetVar[parentScope];
1292        for (int i = 0; i < skip.length; i++) {
1293            if (low <= max) {
1294                IrDomain env = boundDomain(low, Math.min(high - 1, max));
1295                IrDomain ker = EmptyDomain;
1296                int cardLow = 0;
1297                int cardHigh = card.getHigh();
1298                if (partialParentSolution.hasClafer(i)) {
1299                    int prevHigh = high - card.getHigh();
1300                    int nextLow = low + card.getLow();
1301                    if (nextLow > prevHigh) {
1302                        ker = boundDomain(prevHigh, Math.min(nextLow - 1, max));
1303                    }
1304                    cardLow = card.getLow();
1305                }
1306                cardLow = Math.max(cardLow, ker.size());
1307                cardHigh = Math.min(cardHigh, env.size());
1308                skip[i] = set(clafer.getName() + "#" + i, env, ker, boundDomain(cardLow, cardHigh));
1309            } else {
1310                skip[i] = EmptySet;
1311            }
1312            if (partialParentSolution.hasClafer(i)) {
1313                low += card.getLow();
1314            }
1315            high += card.getHigh();
1316        }
1317        return skip;
1318    }
1319
1320    /**
1321     * Create the parent pointers for the Clafer.
1322     *
1323     * @param clafer the Clafer
1324     * @return the variables to represent the parent relation
1325     */
1326    private IrIntVar[] buildParentPointers(AstConcreteClafer clafer) {
1327        PartialSolution solution = getPartialSolution(clafer);
1328        boolean known = solution.parentSolutionKnown();
1329        IrIntVar[] pointers = new IrIntVar[solution.size()];
1330        for (int i = 0; i < pointers.length; i++) {
1331            int[] possibleParents = solution.getPossibleParents(i);
1332            pointers[i] = enumInt(clafer.getName() + "@Parent#" + i,
1333                    solution.hasClafer(i) || known
1334                    ? possibleParents
1335                    : Util.snoc(possibleParents, getScope(clafer.getParent())));
1336        }
1337        return pointers;
1338    }
1339
1340    /**
1341     * Create the references pointers for the Clafer.
1342     *
1343     * @param ref the reference Clafer
1344     * @return the variables to represent the reference relation
1345     */
1346    private IrIntVar[] buildRefPointers(AstRef ref) {
1347        AstClafer src = ref.getSourceType();
1348        AstClafer tar = ref.getTargetType();
1349
1350        PartialSolution partialSolution = getPartialSolution(src);
1351        IrDomain[] partialInts = getPartialInts(ref);
1352        IrIntVar[] ivs = new IrIntVar[getScope(src)];
1353        for (int i = 0; i < ivs.length; i++) {
1354            if (partialSolution.hasClafer(i)) {
1355                ivs[i] = domainInt(src.getName() + "@Ref" + i, partialInts[i]);
1356            } else {
1357                ivs[i] = domainInt(src.getName() + "@Ref" + i, IrUtil.add(partialInts[i], getUninitalizedRef(tar)));
1358            }
1359        }
1360
1361        return ivs;
1362    }
1363
1364    /**
1365     * Enforce the size of a set to be within the cardinality.
1366     *
1367     * @param setCard the set to constrain
1368     * @param card the cardinality
1369     * @return card.low &le; |setCard| &le; card.high
1370     */
1371    private IrBoolExpr constrainCard(IrIntExpr setCard, Card card) {
1372        if (card.isExact()) {
1373            return equal(setCard, card.getLow());
1374        }
1375        if (card.hasLow() && card.hasHigh()) {
1376            return within(setCard, boundDomain(card.getLow(), card.getHigh()));
1377        }
1378        if (card.hasLow()) {
1379            return greaterThanEqual(setCard, card.getLow());
1380        }
1381        if (card.hasHigh()) {
1382            return lessThanEqual(setCard, card.getHigh());
1383        }
1384        return True;
1385    }
1386
1387    /*
1388     ************************
1389     * Convenience functions.
1390     ************************
1391     */
1392    private int getUninitalizedRef(AstClafer clafer) {
1393        return getScopeHigh(clafer) + 1;
1394    }
1395
1396    private int getScopeLow(AstClafer clafer) {
1397        return clafer instanceof AstIntClafer ? analysis.getScope().getIntLow() : 0;
1398    }
1399
1400    private int getScopeHigh(AstClafer clafer) {
1401        return clafer instanceof AstIntClafer ? analysis.getScope().getIntHigh() : getScope(clafer) - 1;
1402    }
1403
1404    private int getScope(AstClafer clafer) {
1405        return analysis.getScope().getScope(clafer);
1406    }
1407
1408    private Format getFormat(AstClafer clafer) {
1409        return analysis.getFormat(clafer);
1410    }
1411
1412    private PartialSolution getPartialSolution(AstClafer clafer) {
1413        return analysis.getPartialSolution(clafer);
1414    }
1415
1416    private PartialSolution getPartialParentSolution(AstConcreteClafer clafer) {
1417        return getPartialSolution(clafer.getParent());
1418    }
1419
1420    private IrDomain[] getPartialInts(AstRef ref) {
1421        return analysis.getPartialInts(ref);
1422    }
1423
1424    private int getOffset(AstAbstractClafer sup, AstClafer sub) {
1425        int offset = 0;
1426        for (AstClafer cur = sub; !sup.equals(cur); cur = cur.getSuperClafer()) {
1427            if (!cur.hasSuperClafer()) {
1428                throw new AstException(sub + " is not a sub clafer of " + sup);
1429            }
1430            offset += analysis.getOffsets(cur.getSuperClafer()).getOffset(cur);
1431        }
1432        return offset;
1433    }
1434
1435    private Card getCard(AstConcreteClafer clafer) {
1436        return analysis.getCard(clafer);
1437    }
1438
1439    private Card getGlobalCard(AstClafer clafer) {
1440        return analysis.getGlobalCard(clafer);
1441    }
1442
1443    private Type getType(AstExpr expr) {
1444        return analysis.getType(expr);
1445    }
1446
1447    private AstClafer getCommonSupertype(AstExpr expr) {
1448        return analysis.getCommonSupertype(expr);
1449    }
1450}