Improved error messages when violating variable boundaries limits

[pafnucy]

Flatzinc variables that store product of array break integer limit. It would be better, if this issue was detected during flatzinc generation, not when running it. This way more understandable error message could be given.

Two students of Modelling Discrete Optimization encountered this error when experimenting with sum-product exercise and were confused by error given by minizinc:

Error: invalid integer literal in line no. 21
Error: syntax error, unexpected ':', expecting FZ_INT_LIT in line no. 21

minizinc code from student: source:

% MiniZinc program to solve the *Sum Prodcut Problem*
% from the "Basic modeling for discrete optimization" from coursera
% 
% Author: Michael J. Winckler
% Date:   26.10.2018
% 

set of int: DIGIT = 0..9;

par int: n;

array[1..n] of var DIGIT: sol;

constraint sum(sol) = product(sol);

constraint forall(i in 1..(n-1))(sol[i] <= sol[i+1]);

solve satisfy;

flatzinc output for parameter n=10:

array [1..2] of int: X_INTRODUCED_29_ = [1,-1];
var 0..9: X_INTRODUCED_0_;
var 0..9: X_INTRODUCED_1_;
var 0..9: X_INTRODUCED_2_;
var 0..9: X_INTRODUCED_3_;
var 0..9: X_INTRODUCED_4_;
var 0..9: X_INTRODUCED_5_;
var 0..9: X_INTRODUCED_6_;
var 0..9: X_INTRODUCED_7_;
var 0..9: X_INTRODUCED_8_;
var 0..9: X_INTRODUCED_9_;
var 0..90: X_INTRODUCED_10_ ::var_is_introduced :: is_defined_var;
var 0..81: X_INTRODUCED_20_ ::var_is_introduced :: is_defined_var;
var 0..729: X_INTRODUCED_21_ ::var_is_introduced :: is_defined_var;
var 0..6561: X_INTRODUCED_22_ ::var_is_introduced :: is_defined_var;
var 0..59049: X_INTRODUCED_23_ ::var_is_introduced :: is_defined_var;
var 0..531441: X_INTRODUCED_24_ ::var_is_introduced :: is_defined_var;
var 0..4782969: X_INTRODUCED_25_ ::var_is_introduced :: is_defined_var;
var 0..43046721: X_INTRODUCED_26_ ::var_is_introduced :: is_defined_var;
var 0..387420489: X_INTRODUCED_27_ ::var_is_introduced :: is_defined_var;
var 0..3486784401: X_INTRODUCED_28_ ::var_is_introduced :: is_defined_var;
array [1..10] of var int: sol:: output_array([1..10]) = [X_INTRODUCED_0_,X_INTRODUCED_1_,X_INTRODUCED_2_,X_INTRODUCED_3_,X_INTRODUCED_4_,X_INTRODUCED_5_,X_INTRODUCED_6_,X_INTRODUCED_7_,X_INTRODUCED_8_,X_INTRODUCED_9_];
constraint int_eq(X_INTRODUCED_10_,X_INTRODUCED_28_);
constraint int_lin_le(X_INTRODUCED_29_,[X_INTRODUCED_0_,X_INTRODUCED_1_],0);
constraint int_lin_le(X_INTRODUCED_29_,[X_INTRODUCED_1_,X_INTRODUCED_2_],0);
constraint int_lin_le(X_INTRODUCED_29_,[X_INTRODUCED_2_,X_INTRODUCED_3_],0);
constraint int_lin_le(X_INTRODUCED_29_,[X_INTRODUCED_3_,X_INTRODUCED_4_],0);
constraint int_lin_le(X_INTRODUCED_29_,[X_INTRODUCED_4_,X_INTRODUCED_5_],0);
constraint int_lin_le(X_INTRODUCED_29_,[X_INTRODUCED_5_,X_INTRODUCED_6_],0);
constraint int_lin_le(X_INTRODUCED_29_,[X_INTRODUCED_6_,X_INTRODUCED_7_],0);
constraint int_lin_le(X_INTRODUCED_29_,[X_INTRODUCED_7_,X_INTRODUCED_8_],0);
constraint int_lin_le(X_INTRODUCED_29_,[X_INTRODUCED_8_,X_INTRODUCED_9_],0);
constraint int_lin_eq([1,1,1,1,1,1,1,1,1,1,-1],[X_INTRODUCED_0_,X_INTRODUCED_1_,X_INTRODUCED_2_,X_INTRODUCED_3_,X_INTRODUCED_4_,X_INTRODUCED_5_,X_INTRODUCED_6_,X_INTRODUCED_7_,X_INTRODUCED_8_,X_INTRODUCED_9_,X_INTRODUCED_10_],0):: defines_var(X_INTRODUCED_10_);
constraint int_times(X_INTRODUCED_8_,X_INTRODUCED_9_,X_INTRODUCED_20_):: defines_var(X_INTRODUCED_20_);
constraint int_times(X_INTRODUCED_7_,X_INTRODUCED_20_,X_INTRODUCED_21_):: defines_var(X_INTRODUCED_21_);
constraint int_times(X_INTRODUCED_6_,X_INTRODUCED_21_,X_INTRODUCED_22_):: defines_var(X_INTRODUCED_22_);
constraint int_times(X_INTRODUCED_5_,X_INTRODUCED_22_,X_INTRODUCED_23_):: defines_var(X_INTRODUCED_23_);
constraint int_times(X_INTRODUCED_4_,X_INTRODUCED_23_,X_INTRODUCED_24_):: defines_var(X_INTRODUCED_24_);
constraint int_times(X_INTRODUCED_3_,X_INTRODUCED_24_,X_INTRODUCED_25_):: defines_var(X_INTRODUCED_25_);
constraint int_times(X_INTRODUCED_2_,X_INTRODUCED_25_,X_INTRODUCED_26_):: defines_var(X_INTRODUCED_26_);
constraint int_times(X_INTRODUCED_1_,X_INTRODUCED_26_,X_INTRODUCED_27_):: defines_var(X_INTRODUCED_27_);
constraint int_times(X_INTRODUCED_0_,X_INTRODUCED_27_,X_INTRODUCED_28_):: defines_var(X_INTRODUCED_28_);
solve  satisfy;

[Dekker1]

Although I agree that the error message currently generated should change. We currently do not have any way of reasoning about the limitations of the domains of variables within solvers. (Although MiniZinc does have it's own absolute values)

I think the best solution would be to ensure make sure that the solver generates an understandable error that the user can understand and reason about. It looks like in this case the solver used is Gecode. Could you confirm that this is the solver in question?

[lalithsuresh]

We're running into the same problem. And yes, the error is from Gecode.

When using Gecode:

Error: invalid integer literal in line no. 1
Error: syntax error, unexpected FZ_DOTDOT in line no. 1
=====ERROR=====

When using Chuffed:

=====ERROR=====

Here's the minizinc that produces this:

var int: x;

constraint x = 668145088 * 4;

output[show(x)]

[Dekker1]

This is indeed the same problem. Gecode actually does hint at the problem (Error: invalid integer literal in line no. 1, but we've discussed changing the error to be more understandable and to make sure gecode does not continue afterwards (so the second error doesn't show up)

For Chuffed the limits are set at -500000000..500000000, anything smaller or bigger will result in the error. Like Gecode, we need to improve the error message generated.

We are discussing adding these boundary limits to the solver configurations. This would possibly improve our ability to detect these problems during flattening and generating a better error message.

[RussAbbott]

I re-wrote the original program minimally and got a solution for n = 10 (but not n = 11).

set of int: DIGIT = 1..9;

par int: n;

array[1..n, 1..n] of var DIGIT: sol;

array [1..n] of var int: s;

constraint forall(i in 1..n)(s[i] == sum(sol[i, 1..i]));

array [1..n] of var int: p;

constraint forall(i in 1..n)(p[i] == product(sol[i, 1..i]));

constraint forall(i in 1..n) (s[i] == p[i]);

constraint forall(i, j, k in 1..n where j < k)(sol[i, j] <= sol[i, k]);

solve satisfy;

output ["(i): " ++ join(", ", [show(sol[i,j]) | j in 1..i]) ++ "\n" | i in 1..n];

Then, if the constraint constraint forall(i in 1..n) (s[i] == p[i]); is removed I get results up to n = 19. But at n=20 I get error

MiniZinc: arithmetic error: integer overflow

Why would that happen when sum is 20 and product is 1?

[RussAbbott]

In the previous program, if I force sol[i, j] == 1 with this constraint constraint forall(i, j in 1..n)(sol[i, j] == 1); everything is fine through n = 94. At n = 95, I get a pop-up error that says: "Unknown error while executing the MiniZinc interpreter."

It looks like something is seriously wrong.

[guidotack]

MiniZinc currently compiles the product expression separately and tries to infer bounds for the result. Since the compiler can't see that the result is bounded, it runs into this overflow (since all individual sol[i,j] are only bounded by 9). The only workaround is to decompose the product yourself and impose the extra constraints on the intermediate results. I can't reproduce the behaviour for n=95, please let us know which version of MiniZinc and which operating system you are using. My suspicion is that this is simply a stack overflow from the recursive definition of the product function. Try replacing product with my_product using this definition:

function var int: my_product(array[int] of var int: x) = 
  if length(x)=0 then 1 else
    let {
      array[int] of var int: xx = array1d(x);
      array[index_set(xx)] of var int: y;
      constraint y[1] = xx[1];
      constraint forall (i in 2..length(y)) (y[i]=y[i-1]*xx[i]);
    } in y[length(y)]
  endif;

Since you know the domain of each intermediate product, you can also pass that in as an additional argument to get rid of the overflow:

constraint forall(i in 1..n)(p[i] == my_product(sol[i, 1..i], 1..9*i));

function var int: my_product(array[int] of var int: x, set of int: d) = 
  if length(x)=0 then 1
  else
    let {
      array[int] of var int: xx = array1d(x);
      array[index_set(xx)] of var d: y;
      constraint y[1] = xx[1];
      constraint forall (i in 2..length(y)) (y[i]=y[i-1]*xx[i]);
    } in y[length(y)]
  endif;

[RussAbbott]

Your my_product function fixed the problem.

I'm using MiniZinc 2.3.2 running on Windows 10. Got the same result on two different Windows HP computers.

-- Russ Abbott Professor, Computer Science California State University, Los Angeles

On Fri, Nov 8, 2019 at 3:53 PM Guido Tack notifications@github.com wrote:

MiniZinc currently compiles the product expression separately and tries to infer bounds for the result. Since the compiler can't see that the result is bounded, it runs into this overflow (since all individual sol[i,j] are only bounded by 9). The only workaround is to decompose the product yourself and impose the extra constraints on the intermediate results. I can't reproduce the behaviour for n=95, please let us know which version of MiniZinc and which operating system you are using. My suspicion is that this is simply a stack overflow from the recursive definition of the product function. Try replacing product with my_product using this definition:

function var int: my_product(array[int] of var int: x) = if length(x)=0 then 1 else let { array[int] of var int: xx = array1d(x); array[index_set(xx)] of var int: y; constraint y[1] = xx[1]; constraint forall (i in 2..length(y)) (y[i]=y[i-1]*xx[i]); } in y[length(y)] endif;

Since you know the domain of each intermediate product, you can also pass that in as an additional argument to get rid of the overflow:

constraint forall(i in 1..n)(p[i] == my_product(sol[i, 1..i], 1..9*i));

function var int: my_product(array[int] of var int: x, set of int: d) = if length(x)=0 then 1 else let { array[int] of var int: xx = array1d(x); array[index_set(xx)] of var d: y; constraint y[1] = xx[1]; constraint forall (i in 2..length(y)) (y[i]=y[i-1]*xx[i]); } in y[length(y)] endif;

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/MiniZinc/libminizinc/issues/260?email_source=notifications&email_token=AAIOFGARIY4E2MK26KIQ2TTQSX3ZBA5CNFSM4GDJQFJ2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEDTWLDQ#issuecomment-552035726, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAIOFGESQUVDPCARG27EQITQSX3ZBANCNFSM4GDJQFJQ .