001package org.clafer.choco.constraint.propagator;
002
003import solver.constraints.Propagator;
004import solver.constraints.PropagatorPriority;
005import solver.exception.ContradictionException;
006import solver.variables.BoolVar;
007import solver.variables.EventType;
008import util.ESat;
009
010/**
011 *
012 * @author jimmy
013 */
014public class PropIfThenElse extends Propagator<BoolVar> {
015
016    private final BoolVar antecedent, consequent, alternative;
017
018    public PropIfThenElse(BoolVar antecedent, BoolVar consequent, BoolVar alternative) {
019        super(new BoolVar[]{antecedent, consequent, alternative}, PropagatorPriority.UNARY, true);
020        this.antecedent = antecedent;
021        this.consequent = consequent;
022        this.alternative = alternative;
023    }
024
025    private boolean isAntecedent(int idx) {
026        return idx == 0;
027    }
028
029    private boolean isConsequent(int idx) {
030        return idx == 1;
031    }
032
033    private boolean isAlternative(int idx) {
034        return idx == 2;
035    }
036
037    @Override
038    protected int getPropagationConditions(int vIdx) {
039        return EventType.INT_ALL_MASK();
040    }
041
042    @Override
043    public void propagate(int evtmask) throws ContradictionException {
044        if (antecedent.instantiated()) {
045            if (antecedent.getValue() == 1) {
046                consequent.setToTrue(aCause);
047            } else {
048                alternative.setToTrue(aCause);
049            }
050            setPassive();
051        } else if (consequent.instantiatedTo(1) && alternative.instantiatedTo(1)) {
052            setPassive();
053        } else {
054            if (consequent.instantiatedTo(0)) {
055                antecedent.setToFalse(aCause);
056                alternative.setToTrue(aCause);
057            }
058            if (alternative.instantiatedTo(0)) {
059                antecedent.setToTrue(aCause);
060                consequent.setToTrue(aCause);
061            }
062        }
063    }
064
065    @Override
066    public void propagate(int idxVarInProp, int mask) throws ContradictionException {
067        if (isAntecedent(idxVarInProp)) {
068            assert antecedent.instantiated();
069            if (antecedent.getValue() == 1) {
070                consequent.setToTrue(aCause);
071            } else {
072                alternative.setToTrue(aCause);
073            }
074            setPassive();
075        } else if (isConsequent(idxVarInProp)) {
076            assert consequent.instantiated();
077            if (consequent.getValue() == 0) {
078                antecedent.setToFalse(aCause);
079                alternative.setToTrue(aCause);
080            } else if (alternative.instantiatedTo(1)) {
081                setPassive();
082            }
083        } else {
084            assert isAlternative(idxVarInProp);
085            if (alternative.getValue() == 0) {
086                antecedent.setToTrue(aCause);
087                consequent.setToTrue(aCause);
088            } else if (consequent.instantiatedTo(1)) {
089                setPassive();
090            }
091        }
092    }
093
094    @Override
095    public ESat isEntailed() {
096        if (antecedent.instantiated()) {
097            return antecedent.getValue() == 1 ? consequent.getBooleanValue() : alternative.getBooleanValue();
098        }
099        if (consequent.instantiatedTo(1) && alternative.instantiatedTo(1)) {
100            return ESat.TRUE;
101        }
102        if (consequent.instantiatedTo(0) && alternative.instantiatedTo(0)) {
103            return ESat.FALSE;
104        }
105        return ESat.UNDEFINED;
106    }
107
108    @Override
109    public String toString() {
110        return "if " + antecedent + " then " + consequent + " else " + alternative;
111    }
112}