001package org.clafer.choco.constraint.propagator; 002 003import org.clafer.common.Util; 004import solver.constraints.Propagator; 005import solver.constraints.PropagatorPriority; 006import solver.exception.ContradictionException; 007import solver.variables.BoolVar; 008import solver.variables.EventType; 009import util.ESat; 010 011/** 012 * 013 * @author jimmy 014 */ 015public class PropOne extends Propagator<BoolVar> { 016 017 public PropOne(BoolVar[] vars) { 018 super(vars, PropagatorPriority.BINARY, true); 019 } 020 021 @Override 022 public int getPropagationConditions(int vIdx) { 023 return EventType.INSTANTIATE.mask; 024 } 025 026 private void clearAllBut(int exclude) throws ContradictionException { 027 for (int i = 0; i < vars.length; i++) { 028 if (i != exclude) { 029 vars[i].setToFalse(aCause); 030 } 031 } 032 } 033 034 @Override 035 public void propagate(int evtmask) throws ContradictionException { 036 // The number of uninstantiated variables. 037 int count = 0; 038 BoolVar last = null; 039 for (int i = 0; i < vars.length; i++) { 040 BoolVar var = vars[i]; 041 if (var.instantiated()) { 042 if (var.getValue() == 1) { 043 clearAllBut(i); 044 return; 045 } 046 } else { 047 count++; 048 last = var; 049 } 050 } 051 // Every variable is false except for last. 052 if (count == 1) { 053 last.setToTrue(aCause); 054 } 055 if (count == 0) { 056 contradiction(vars[0], "All false."); 057 } 058 } 059 060 @Override 061 public void propagate(int idxVarInProp, int mask) throws ContradictionException { 062 assert EventType.isInstantiate(mask); 063 if (vars[idxVarInProp].getValue() == 1) { 064 clearAllBut(idxVarInProp); 065 } else { 066 propagate(mask); 067 } 068 } 069 070 @Override 071 public ESat isEntailed() { 072 int count = 0; 073 boolean allInstantiated = true; 074 for (BoolVar var : vars) { 075 if (var.instantiated()) { 076 if (var.getValue() == 1) { 077 count++; 078 if (count > 1) { 079 return ESat.FALSE; 080 } 081 } 082 } else { 083 allInstantiated = false; 084 } 085 } 086 return allInstantiated 087 ? (count == 1 ? ESat.TRUE : ESat.FALSE) : ESat.UNDEFINED; 088 } 089 090 @Override 091 public String toString() { 092 return "one(" + Util.commaSeparate(vars) + ")"; 093 } 094}