1 /* 2 * XplusYeqZ.java 3 * This file is part of JaCoP. 4 * <p> 5 * JaCoP is a Java Constraint Programming solver. 6 * <p> 7 * Copyright (C) 2000-2008 Krzysztof Kuchcinski and Radoslaw Szymanek 8 * <p> 9 * This program is free software: you can redistribute it and/or modify 10 * it under the terms of the GNU Affero General Public License as published by 11 * the Free Software Foundation, either version 3 of the License, or 12 * (at your option) any later version. 13 * <p> 14 * This program is distributed in the hope that it will be useful, 15 * but WITHOUT ANY WARRANTY; without even the implied warranty of 16 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the 17 * GNU Affero General Public License for more details. 18 * <p> 19 * Notwithstanding any other provision of this License, the copyright 20 * owners of this work supplement the terms of this License with terms 21 * prohibiting misrepresentation of the origin of this work and requiring 22 * that modified versions of this work be marked in reasonable ways as 23 * different from the original version. This supplement of the license 24 * terms is in accordance with Section 7 of GNU Affero General Public 25 * License version 3. 26 * <p> 27 * You should have received a copy of the GNU Affero General Public License 28 * along with this program. If not, see <http://www.gnu.org/licenses/>. 29 */ 30 31 package org.jacop.constraints; 32 33 import org.jacop.core.IntDomain; 34 import org.jacop.core.IntVar; 35 import org.jacop.core.Store; 36 37 import java.util.concurrent.atomic.AtomicInteger; 38 39 /** 40 * Constraint X + Y = Z 41 * <p> 42 * Bound consistency is used. 43 * 44 * @author Krzysztof Kuchcinski and Radoslaw Szymanek 45 * @version 4.8 46 */ 47 48 public class XplusYeqZ extends PrimitiveConstraint { 49 50 final static AtomicInteger idNumber = new AtomicInteger(0); 51 52 /** 53 * It specifies variable x in constraint x+y=z. 54 */ 55 final public IntVar x; 56 57 /** 58 * It specifies variable x in constraint x+y=z. 59 */ 60 final public IntVar y; 61 62 /** 63 * It specifies variable x in constraint x+y=z. 64 */ 65 final public IntVar z; 66 67 /** 68 * It constructs constraint X+Y=Z. 69 * 70 * @param x variable x. 71 * @param y variable y. 72 * @param z variable z. 73 */ XplusYeqZ(IntVar x, IntVar y, IntVar z)74 public XplusYeqZ(IntVar x, IntVar y, IntVar z) { 75 76 checkInputForNullness(new String[] {"x", "y", "z"}, new Object[] {x, y, z}); 77 78 numberId = idNumber.incrementAndGet(); 79 80 this.x = x; 81 this.y = y; 82 this.z = z; 83 84 checkForOverflow(); 85 86 setScope(x, y, z); 87 } 88 consistency(final Store store)89 @Override public void consistency(final Store store) { 90 91 do { 92 93 store.propagationHasOccurred = false; 94 95 if (x.singleton()) { 96 97 y.domain.inShift(store.level, y, z.domain, -x.value()); 98 z.domain.inShift(store.level, z, y.domain, x.value()); 99 100 } else if (y.singleton()) { 101 102 x.domain.inShift(store.level, x, z.domain, -y.value()); 103 z.domain.inShift(store.level, z, x.dom(), y.value()); 104 105 } else { 106 107 // for large domains (for example, Integer.MIN_VALUE..Integer.MAX_VALUE) uncomment three lines below, 108 // comment three lines after uncommented lines and checkForOverlow in the constructor 109 // x.domain.in(store.level, x, IntDomain.subtractInt(z.min(), y.max()), IntDomain.subtractInt(z.max(), y.min())); 110 // y.domain.in(store.level, y, IntDomain.subtractInt(z.min(), x.max()), IntDomain.subtractInt(z.max(), x.min())); 111 // z.domain.in(store.level, z, IntDomain.addInt(x.min(), y.min()), IntDomain.addInt(x.max(), y.max())); 112 113 x.domain.in(store.level, x, z.min() - y.max(), z.max() - y.min()); 114 y.domain.in(store.level, y, z.min() - x.max(), z.max() - x.min()); 115 z.domain.in(store.level, z, x.min() + y.min(), x.max() + y.max()); 116 } 117 118 } while (store.propagationHasOccurred); 119 120 } 121 checkForOverflow()122 void checkForOverflow() { 123 124 int sumMin = 0, sumMax = 0; 125 126 sumMin = Math.addExact(sumMin, x.min()); 127 sumMax = Math.addExact(sumMax, x.max()); 128 129 sumMin = Math.addExact(sumMin, y.min()); 130 sumMax = Math.addExact(sumMax, y.max()); 131 132 Math.subtractExact(sumMin, z.max()); 133 Math.subtractExact(sumMax, z.min()); 134 } 135 getDefaultNestedNotConsistencyPruningEvent()136 @Override protected int getDefaultNestedNotConsistencyPruningEvent() { 137 return IntDomain.BOUND; 138 } 139 140 getDefaultNestedConsistencyPruningEvent()141 @Override protected int getDefaultNestedConsistencyPruningEvent() { 142 return IntDomain.GROUND; 143 } 144 getDefaultNotConsistencyPruningEvent()145 @Override protected int getDefaultNotConsistencyPruningEvent() { 146 return IntDomain.GROUND; 147 } 148 getDefaultConsistencyPruningEvent()149 @Override public int getDefaultConsistencyPruningEvent() { 150 return IntDomain.BOUND; 151 } 152 notConsistency(final Store store)153 @Override public void notConsistency(final Store store) { 154 155 do { 156 157 store.propagationHasOccurred = false; 158 159 if (z.singleton() && y.singleton()) 160 x.domain.inComplement(store.level, x, z.min() - y.min()); 161 162 if (z.singleton() && x.singleton()) 163 y.domain.inComplement(store.level, y, z.min() - x.min()); 164 165 if (x.singleton() && y.singleton()) 166 z.domain.inComplement(store.level, z, x.min() + y.min()); 167 168 } while (store.propagationHasOccurred); 169 170 } 171 notSatisfied()172 @Override public boolean notSatisfied() { 173 IntDomain xDom = x.dom(), yDom = y.dom(), zDom = z.dom(); 174 return (xDom.max() + yDom.max() < zDom.min() || xDom.min() + yDom.min() > zDom.max()); 175 } 176 satisfied()177 @Override public boolean satisfied() { 178 179 // return (grounded() && x.value() + y.value() == z.value()); 180 int xMin = x.min(), yMin = y.min(), zMin = z.min(); 181 return x.singleton(xMin) && y.singleton(yMin) && z.singleton(zMin) && xMin + yMin == zMin; 182 } 183 toString()184 @Override public String toString() { 185 186 return id() + " : XplusYeqZ(" + x + ", " + y + ", " + z + " )"; 187 } 188 189 } 190