001package org.clafer.compiler;
002
003import java.util.ArrayList;
004import java.util.Arrays;
005import java.util.List;
006import org.clafer.collection.Either;
007import org.clafer.collection.Pair;
008import org.clafer.common.Check;
009import org.clafer.instance.InstanceModel;
010import solver.ResolutionPolicy;
011import solver.Solver;
012import solver.constraints.ICF;
013import solver.exception.ContradictionException;
014import solver.objective.IntObjectiveManager;
015import solver.propagation.NoPropagationEngine;
016import solver.propagation.hardcoded.SevenQueuesPropagatorEngine;
017import solver.search.loop.monitors.IMonitorSolution;
018import solver.search.solution.Solution;
019import solver.variables.IntVar;
020import solver.variables.SetVar;
021import solver.variables.Variable;
022
023/**
024 *
025 * @author jimmy
026 */
027public class ClaferOptimizer implements ClaferSearch<Pair<Integer, InstanceModel>> {
028
029    public final Solver solver;
030    private final ClaferSolutionMap solutionMap;
031    private final boolean maximize;
032    private final Either<Integer, IntVar> score;
033    private boolean first = true;
034    private boolean more = true;
035    private boolean second = true;
036    private final Solution firstSolution = new Solution();
037
038    ClaferOptimizer(Solver solver, ClaferSolutionMap solutionMap,
039            boolean maximize, Either<Integer, IntVar> score) {
040        this.solver = Check.notNull(solver);
041        this.solutionMap = Check.notNull(solutionMap);
042        this.maximize = maximize;
043        this.score = Check.notNull(score);
044    }
045
046    public ClaferSolutionMap getSolutionMap() {
047        return solutionMap;
048    }
049
050    public boolean isMaximize() {
051        return maximize;
052    }
053
054    public boolean isMinimize() {
055        return !maximize;
056    }
057
058    @Override
059    public boolean find() {
060        if (!more) {
061            return false;
062        }
063        if (first) {
064            more &= solveFirst();
065            first = false;
066            return more;
067        }
068        more &= solveNext();
069        return more;
070    }
071
072    /*
073     * Implementation of multiple optimal search based on discussion here:
074     * https://github.com/chocoteam/choco3/issues/121.
075     */
076    private boolean solveFirst() {
077        if (score.isLeft()) {
078            return solver.findSolution();
079        }
080        IntVar scoreVar = score.getRight();
081        solver.getSearchLoop().setObjectivemanager(new IntObjectiveManager(
082                scoreVar,
083                maximize ? ResolutionPolicy.MAXIMIZE : ResolutionPolicy.MINIMIZE,
084                solver));
085        solver.getSearchLoop().plugSearchMonitor(new IMonitorSolution() {
086            private static final long serialVersionUID = 1L;
087
088            @Override
089            public void onSolution() {
090                if (first) {
091                    firstSolution.record(solver);
092                }
093            }
094        });
095        if (solver.getEngine() == NoPropagationEngine.SINGLETON) {
096            solver.set(new SevenQueuesPropagatorEngine(solver));
097        }
098        solver.getSearchLoop().getMeasures().setReadingTimeCount(System.nanoTime());
099        solver.getSearchLoop().launch(false);
100        if (!firstSolution.hasBeenFound()) {
101            return false;
102        }
103        try {
104            firstSolution.restore();
105        } catch (ContradictionException e) {
106            // Should never happen because the solution should not be contradictory.
107            throw new IllegalStateException(e);
108        }
109        return true;
110    }
111
112    private boolean solveNext() {
113        if (score.isLeft() || !second) {
114            return solver.nextSolution();
115        }
116        second = false;
117        IntVar scoreVar = score.getRight();
118        int best = scoreVar.getValue();
119        // TODO: forbid the current solution from happening again.                                                 
120        solver.getEngine().flush();
121        solver.getSearchLoop().reset();
122        solver.post(ICF.arithm(scoreVar, "=", best));
123        boolean next = solver.findSolution();
124        return next && duplicateSolution() ? solver.nextSolution() : next;
125    }
126
127    private boolean duplicateSolution() {
128        for (IntVar var : solutionMap.getIrSolution().getIntVars()) {
129            if ((var.getTypeAndKind() & Variable.CSTE) == 0) {
130                if (var.getValue() != firstSolution.getIntVal(var)) {
131                    return false;
132                }
133            }
134        }
135        for (SetVar var : solutionMap.getIrSolution().getSetVars()) {
136            if ((var.getTypeAndKind() & Variable.CSTE) == 0) {
137                if (!Arrays.equals(var.getValue(), firstSolution.getSetVal(var))) {
138                    return false;
139                }
140            }
141        }
142        return true;
143    }
144
145    /**
146     * @return the optimal value and the optimal instance
147     */
148    @Override
149    public Pair<Integer, InstanceModel> instance() {
150        return new Pair<>(
151                score.isLeft() ? score.getLeft() : score.getRight().getValue(),
152                solutionMap.getInstance());
153    }
154
155    @Override
156    public Pair<Integer, InstanceModel>[] allInstances() {
157        List<Pair<Integer, InstanceModel>> instances = new ArrayList<>();
158        while (find()) {
159            instances.add(instance());
160        }
161        @SuppressWarnings("unchecked")
162        Pair<Integer, InstanceModel>[] pairs = new Pair[instances.size()];
163        return instances.toArray(pairs);
164    }
165
166    @Override
167    public Solver getInternalSolver() {
168        return solver;
169    }
170}