diff --git a/solver/src/main/java/org/chocosolver/solver/variables/IViewFactory.java b/solver/src/main/java/org/chocosolver/solver/variables/IViewFactory.java index 80029269fe..fbbf5b5d85 100644 --- a/solver/src/main/java/org/chocosolver/solver/variables/IViewFactory.java +++ b/solver/src/main/java/org/chocosolver/solver/variables/IViewFactory.java @@ -32,6 +32,7 @@ * A kind of factory relying on interface default implementation to allow (multiple) inheritance * * @author Jean-Guillaume FAGES + * @author Aditya Nikam */ public interface IViewFactory extends ISelf { @@ -128,16 +129,19 @@ default IntVar intView(int a, IntVar var, int b) { } if (var instanceof IntAffineView) { IntAffineView view = (IntAffineView) var; - int av = (view.p ? 1 : -1) * view.a * a; - int bv = a * view.b + b; + // Compose in long: flattening can overflow int even when every + // value the composed expression can take is well within range. + long av = (view.p ? 1L : -1L) * view.a * a; + long bv = (long) a * view.b + b; if (av == 1 && bv == 0) { return view.getVariable(); - } else { - return intView(av, view.getVariable(), bv); + } else if (fitsInt(av) && fitsInt(bv)) { + return intView((int) av, view.getVariable(), (int) bv); } - } else { - return new IntAffineView<>(var, a, b); + // Flattening would overflow, so stack a view on the view: its + // own coefficients are small enough to be applied one at a time. } + return new IntAffineView<>(var, a, b); } else { int lb, ub; if (a > 0) { @@ -167,6 +171,14 @@ default IntVar intView(int a, IntVar var, int b) { } } + /** + * @param value a value computed in long arithmetic + * @return {@code true} if value can be stored in an int without loss + */ + private static boolean fitsInt(long value) { + return value >= Integer.MIN_VALUE && value <= Integer.MAX_VALUE; + } + /** * Create a view based on var, i.e. view = |var| * diff --git a/solver/src/test/java/org/chocosolver/solver/variables/view/integer/IntAffineViewTest.java b/solver/src/test/java/org/chocosolver/solver/variables/view/integer/IntAffineViewTest.java index 29cc06ce97..53c0bce1ec 100644 --- a/solver/src/test/java/org/chocosolver/solver/variables/view/integer/IntAffineViewTest.java +++ b/solver/src/test/java/org/chocosolver/solver/variables/view/integer/IntAffineViewTest.java @@ -27,6 +27,7 @@ *
* * @author Charles Prud'homme + * @author Aditya Nikam * @since 06/10/2023 */ public class IntAffineViewTest { @@ -229,4 +230,30 @@ public void testViewAndReification(boolean lcg) { assertEquals(m.getSolver().getSolutionCount(), 2); assertEquals(m.getSolver().getFailCount(), 2); } + + @Test(groups = "1s", timeOut = 60000) + public void testNestedAffineViewOverflowKeepsSolution() { + Model m = new Model(); + IntVar x = m.intVar("x", 46_341, 46_342, false); + // Flattening (x - 46341) * 46341 gives b = 46341 * -46341, which does + // not fit in an int, although the product itself is at most 46341. + IntVar result = x.sub(46_341).mul(46_341).intVar(); + result.eq(0).post(); + assertEquals(m.getSolver().solve(), true); + assertEquals(x.getValue(), 46_341); + } + + @Test(groups = "1s", timeOut = 60000) + public void testNestedAffineViewOverflowRejectsInvalidSolution() { + Model m = new Model(); + IntVar x = m.intVar("x", 46_341, 46_342, false); + IntVar result = x.sub(46_341).mul(46_341).intVar(); + result.ne(0).post(); + m.getSolver().setSearch(inputOrderLBSearch(x)); + while (m.getSolver().solve()) { + assertEquals(x.getValue(), 46_342); + assertEquals(result.getValue(), 46_341); + } + assertEquals(m.getSolver().getSolutionCount(), 1); + } } \ No newline at end of file