001package org.clafer.choco.constraint;
002
003import java.util.ArrayList;
004import java.util.Arrays;
005import java.util.List;
006import solver.constraints.Constraint;
007import solver.constraints.Propagator;
008import solver.constraints.PropagatorPriority;
009import solver.exception.ContradictionException;
010import solver.variables.EventType;
011import solver.variables.Variable;
012import util.ESat;
013import static util.ESat.TRUE;
014import static util.ESat.UNDEFINED;
015
016/**
017 * Boolean or. The difference between this constraint and the one provided by
018 * the library is that this one does not reify to boolean variables, thus it can
019 * be added after the search has started. The one provided in the library
020 * requires dynamic variable addition which is not supported.
021 *
022 * @author jimmy
023 */
024public class OrConstraint extends Constraint<Variable, Propagator<Variable>> {
025
026    public OrConstraint(Constraint... constraints) {
027        super(buildArray(constraints), constraints[0].getSolver());
028        setPropagators(new PropOr(vars, constraints));
029    }
030
031    private static Variable[] buildArray(Constraint... constraints) {
032        List<Variable> vars = new ArrayList<>();
033        for (Constraint constraint : constraints) {
034            vars.addAll(Arrays.asList(constraint.getVariables()));
035            for(Propagator propagator : constraint.getPropagators()) {
036                propagator.setReifiedSilent();
037            }
038        }
039        return vars.toArray(new Variable[vars.size()]);
040    }
041
042    private class PropOr extends Propagator<Variable> {
043
044        private final Constraint[] constraints;
045
046        protected PropOr(Variable[] vars, Constraint[] constraints) {
047            super(vars, PropagatorPriority.LINEAR, true);
048            this.constraints = constraints;
049        }
050
051        @Override
052        public int getPropagationConditions(int vIdx) {
053            return EventType.ALL_FINE_EVENTS.mask;
054        }
055
056        @Override
057        public void propagate(int evtmask) throws ContradictionException {
058            boolean allFalse = true;
059            for (Constraint constraint : constraints) {
060                switch (constraint.isSatisfied()) {
061                    case TRUE:
062                        setPassive();
063                        return;
064                    case UNDEFINED:
065                        allFalse = false;
066                        break;
067                }
068            }
069            if (allFalse) {
070                contradiction(vars[0], "All unsat.");
071            }
072        }
073
074        @Override
075        public void propagate(int idxVarInProp, int mask) throws ContradictionException {
076            forcePropagate(EventType.CUSTOM_PROPAGATION);
077        }
078
079        @Override
080        public ESat isEntailed() {
081            boolean allFalse = true;
082            for (Constraint constraint : constraints) {
083                switch (constraint.isSatisfied()) {
084                    case TRUE:
085                        return ESat.TRUE;
086                    case UNDEFINED:
087                        allFalse = false;
088                        break;
089                }
090            }
091            return allFalse ? ESat.FALSE : ESat.UNDEFINED;
092        }
093    }
094}