Source code

001package org.clafer.compiler;
002
003import java.util.ArrayList;
004import java.util.HashSet;
005import java.util.List;
006import java.util.Set;
007import org.clafer.ast.AstAbstractClafer;
008import org.clafer.ast.AstClafer;
009import org.clafer.ast.AstConcreteClafer;
010import org.clafer.ast.AstModel;
011import org.clafer.ast.AstRef;
012import org.clafer.ast.AstUtil;
013import org.clafer.ast.analysis.UnsatAnalyzer;
014import org.clafer.ast.compiler.AstCompiler;
015import org.clafer.ast.compiler.AstSolutionMap;
016import org.clafer.choco.constraint.Constraints;
017import org.clafer.collection.Either;
018import org.clafer.collection.Maybe;
019import org.clafer.common.Util;
020import org.clafer.graph.GraphUtil;
021import org.clafer.graph.KeyGraph;
022import org.clafer.graph.Vertex;
023import org.clafer.ir.IrIntConstant;
024import org.clafer.ir.IrIntVar;
025import org.clafer.ir.IrModule;
026import org.clafer.ir.IrSetConstant;
027import org.clafer.ir.IrSetVar;
028import org.clafer.ir.compiler.IrCompiler;
029import org.clafer.ir.compiler.IrSolutionMap;
030import org.clafer.objective.Objective;
031import org.clafer.scope.Scopable;
032import org.clafer.scope.Scope;
033import org.clafer.scope.ScopeBuilder;
034import solver.Solver;
035import solver.constraints.Constraint;
036import solver.constraints.ICF;
037import solver.search.loop.monitors.IMonitorSolution;
038import solver.search.strategy.IntStrategyFactory;
039import solver.search.strategy.SetStrategyFactory;
040import solver.search.strategy.strategy.AbstractStrategy;
041import solver.search.strategy.strategy.StrategiesSequencer;
042import solver.variables.IntVar;
043import solver.variables.SetVar;
044
045/**
046 * Compiles from AST -> Choco
047 *
048 * @author jimmy
049 */
050public class ClaferCompiler {
051
052    private ClaferCompiler() {
053    }
054
055    private static SetVar[] getSetVars(AstModel model, ClaferSolutionMap map) {
056        KeyGraph<AstClafer> dependency = new KeyGraph<>();
057        for (AstAbstractClafer abstractClafer : model.getAbstracts()) {
058            Vertex<AstClafer> node = dependency.getVertex(abstractClafer);
059            for (AstClafer sub : abstractClafer.getSubs()) {
060                node.addNeighbour(dependency.getVertex(sub));
061            }
062            if (abstractClafer.hasRef()) {
063                node.addNeighbour(dependency.getVertex(abstractClafer.getRef().getTargetType()));
064            }
065        }
066        for (AstConcreteClafer concreteClafer : AstUtil.getConcreteClafers(model)) {
067            Vertex<AstClafer> node = dependency.getVertex(concreteClafer);
068            if (concreteClafer.hasParent()) {
069                node.addNeighbour(dependency.getVertex(concreteClafer.getParent()));
070            }
071            if (concreteClafer.hasRef()) {
072                node.addNeighbour(dependency.getVertex(concreteClafer.getRef().getTargetType()));
073            }
074        }
075        List<SetVar> vars = new ArrayList<>();
076        for (Set<AstClafer> component : GraphUtil.computeStronglyConnectedComponents(dependency)) {
077            for (AstClafer clafer : component) {
078                if (clafer instanceof AstConcreteClafer) {
079                    for (IrSetVar setVar : map.getAstSolution().getSiblingVars(clafer)) {
080                        if (!(setVar instanceof IrSetConstant)) {
081                            Either<int[], SetVar> var = map.getIrSolution().getSetVar(setVar);
082                            if (var.isRight()) {
083                                vars.add(var.getRight());
084                            }
085                        }
086                    }
087                }
088            }
089        }
090        return vars.toArray(new SetVar[vars.size()]);
091    }
092
093    private static IntVar[] getIntVars(AstModel model, ClaferSolutionMap map) {
094        List<IntVar> vars = new ArrayList<>();
095        for (AstClafer clafer : AstUtil.getClafers(model)) {
096            if (clafer.hasRef()) {
097                for (IrIntVar intVar : map.getAstSolution().getRefVars(clafer.getRef())) {
098                    if (!(intVar instanceof IrIntConstant)) {
099                        Either<Integer, IntVar> var = map.getIrSolution().getIntVar(intVar);
100                        if (var.isRight()) {
101                            vars.add(var.getRight());
102                        }
103                    }
104                }
105            }
106        }
107        return vars.toArray(new IntVar[vars.size()]);
108    }
109
110    @SafeVarargs
111    private static void set(Solver solver, Maybe<? extends AbstractStrategy>... strategies) {
112        AbstractStrategy<?>[] strats = Maybe.filterJust(strategies);
113        if (strats.length == 0) {
114            solver.set(IntStrategyFactory.random(new IntVar[0], 0));
115        } else {
116            solver.set(new StrategiesSequencer(solver.getEnvironment(), strats));
117        }
118    }
119
120    private static Maybe<? extends AbstractStrategy<SetVar>> setStrategy(SetVar[] vars, ClaferOptions options) {
121        if (vars.length == 0) {
122            return Maybe.nothing();
123        }
124        if (options.isPreferSmallerInstances()) {
125            return Maybe.just(SetStrategyFactory.remove_first(vars));
126        }
127        return Maybe.just(SetStrategyFactory.force_first(vars));
128    }
129
130    private static Maybe<AbstractStrategy<IntVar>> firstFailInDomainMax(IntVar[] vars) {
131        if (vars.length == 0) {
132            return Maybe.nothing();
133        }
134        return Maybe.just(IntStrategyFactory.firstFail_InDomainMax(vars));
135    }
136
137    private static Maybe<AbstractStrategy<IntVar>> firstFailInDomainMin(IntVar[] vars) {
138        if (vars.length == 0) {
139            return Maybe.nothing();
140        }
141        return Maybe.just(IntStrategyFactory.firstFail_InDomainMin(vars));
142    }
143
144    public static ClaferSolver compile(AstModel in, Scopable scope) {
145        return compile(in, scope, ClaferOptions.Default);
146    }
147
148    public static ClaferSolver compile(AstModel in, Scopable scope, ClaferOptions options) {
149        Solver solver = new Solver();
150        IrModule module = new IrModule();
151
152        AstSolutionMap astSolution = AstCompiler.compile(in, scope.toScope(), module,
153                options.isFullSymmetryBreaking());
154        IrSolutionMap irSolution = IrCompiler.compile(module, solver, options.isFullOptimizations());
155        ClaferSolutionMap solution = new ClaferSolutionMap(astSolution, irSolution);
156
157        set(solver,
158                setStrategy(getSetVars(in, solution), options),
159                firstFailInDomainMin(getIntVars(in, solution)));
160        return new ClaferSolver(solver, solution);
161    }
162
163    public static ClaferOptimizer compile(AstModel in, Scopable scope, Objective objective) {
164        return compile(in, scope, objective, ClaferOptions.Default);
165    }
166
167    public static ClaferOptimizer compile(AstModel in, Scopable scope, Objective objective, ClaferOptions options) {
168        Solver solver = new Solver();
169        IrModule module = new IrModule();
170
171        AstSolutionMap astSolution = AstCompiler.compile(
172                in, scope.toScope(), objective, module,
173                options.isFullSymmetryBreaking());
174        IrSolutionMap irSolution = IrCompiler.compile(module, solver, options.isFullOptimizations());
175        ClaferSolutionMap solution = new ClaferSolutionMap(astSolution, irSolution);
176
177        Either<Integer, IntVar> objectiveVar = irSolution.getIntVar(astSolution.getObjectiveVar(objective));
178        IntVar[] objectiveVars = objectiveVar.isLeft() ? new IntVar[0] : new IntVar[]{objectiveVar.getRight()};
179
180        set(solver,
181                setStrategy(getSetVars(in, solution), options),
182                objective.isMaximize()
183                ? firstFailInDomainMax(objectiveVars)
184                : firstFailInDomainMin(objectiveVars),
185                firstFailInDomainMin(getIntVars(in, solution)));
186        return new ClaferOptimizer(solver, solution, objective.isMaximize(), objectiveVar);
187    }
188
189    public static ClaferUnsat compileUnsat(AstModel in, Scopable scope) {
190        return compileUnsat(in, scope.toScope(), ClaferOptions.Default);
191    }
192
193    public static ClaferUnsat compileUnsat(AstModel in, Scopable scope, ClaferOptions options) {
194        Solver solver = new Solver();
195        IrModule module = new IrModule();
196
197        AstSolutionMap astSolution = AstCompiler.compile(in, scope.toScope(), module,
198                Util.cons(new UnsatAnalyzer(), AstCompiler.DefaultAnalyzers),
199                options.isFullSymmetryBreaking());
200        IrSolutionMap irSolution = IrCompiler.compile(module, solver, options.isFullOptimizations());
201        ClaferSolutionMap solution = new ClaferSolutionMap(astSolution, irSolution);
202
203        set(solver,
204                firstFailInDomainMax(Either.filterRight(irSolution.getBoolVars(astSolution.getSoftVars()))),
205                setStrategy(getSetVars(in, solution), options),
206                firstFailInDomainMin(getIntVars(in, solution)));
207        return new ClaferUnsat(solver, solution);
208    }
209
210    public static ClaferSolver compilePartial(AstModel in, ScopeBuilder scope, AstConcreteClafer... concretize) {
211        return compilePartial(in, scope.toScope(), concretize);
212    }
213
214    public static ClaferSolver compilePartial(AstModel in, Scope scope, AstConcreteClafer... concretize) {
215        final Set<AstConcreteClafer> transitiveConcretize = new HashSet<>();
216        for (AstConcreteClafer clafer : concretize) {
217            concretize(clafer, transitiveConcretize);
218        }
219        final ClaferSolver solver = compile(in, scope);
220        final List<IntVar> intVars = new ArrayList<>();
221        final List<SetVar> setVars = new ArrayList<>();
222        for (AstConcreteClafer clafer : transitiveConcretize) {
223            IrSetVar[] siblingVars = solver.getSolutionMap().getAstSolution().getSiblingVars(clafer);
224            for (IrSetVar siblingVar : siblingVars) {
225                Either<int[], SetVar> var = solver.getSolutionMap().getIrSolution().getSetVar(siblingVar);
226                if (var.isRight()) {
227                    setVars.add(var.getRight());
228                }
229            }
230            AstRef ref = AstUtil.getInheritedRef(clafer);
231            if (ref != null) {
232                IrIntVar[] refVars = solver.getSolutionMap().getAstSolution().getRefVars(ref);
233                for (IrIntVar refVar : refVars) {
234                    Either<Integer, IntVar> var = solver.getSolutionMap().getIrSolution().getIntVar(refVar);
235                    if (var.isRight()) {
236                        intVars.add(var.getRight());
237                    }
238                }
239            }
240        }
241        solver.getInternalSolver().getSearchLoop().plugSearchMonitor(new IMonitorSolution() {
242            private static final long serialVersionUID = 1L;
243
244            @Override
245            public void onSolution() {
246                List<Constraint> constraints = new ArrayList<>();
247                for (IntVar var : intVars) {
248                    constraints.add(ICF.arithm(var, "!=", var.getValue()));
249                }
250                for (SetVar var : setVars) {
251                    constraints.add(Constraints.notEqual(var, var.getValue()));
252                }
253                solver.getInternalSolver().postCut(Constraints.or(
254                        constraints.toArray(new Constraint[constraints.size()])));
255            }
256        });
257        return solver;
258    }
259
260    private static void concretize(AstClafer clafer, Set<AstConcreteClafer> concretize) {
261        if (clafer instanceof AstAbstractClafer) {
262            concretize((AstAbstractClafer) clafer, concretize);
263        } else {
264            concretize((AstConcreteClafer) clafer, concretize);
265        }
266    }
267
268    private static void concretize(AstConcreteClafer clafer, Set<AstConcreteClafer> concretize) {
269        if (!AstUtil.isRoot(clafer) && concretize.add(clafer)) {
270            concretize(clafer.getParent(), concretize);
271            concretize(clafer.getSuperClafer(), concretize);
272        }
273    }
274
275    private static void concretize(AstAbstractClafer clafer, Set<AstConcreteClafer> concretize) {
276        if (!AstUtil.isTypeRoot(clafer)) {
277            for (AstClafer sub : clafer.getSubs()) {
278                concretize(sub, concretize);
279            }
280        }
281    }
282}