2.8.0: inconsistent behavior of partial functions and undefined values

[matsc-at-sics-se]

This behavior is consistent with the relational semantics [Section 2.2.7 of the Handbook]: division by zero gets silently treated as falsehood:

$ cat /tmp/foo.mzn
var -1 .. 1: D :: output_var;
var -1 .. 1: Q :: output_var = -1 div D;
$ minizinc -a /tmp/foo.mzn
D = -1;
----------
D = 1;
----------
==========

But if you narrow the domain of D to 0..0, the falsehood is not silent any more:

$ cat /tmp/foo.mzn
var  0 .. 0: D :: output_var;
var -1 .. 1: Q :: output_var = -1 div D;$ minizinc -a /tmp/foo.mzn
$ minizinc -a /tmp/foo.mzn
Warning: undefined result becomes false in Boolean context
  (division by zero)
/tmp/foo.mzn:2.1-28
  in variable declaration for 'Q'
  in binary 'div' operator expression
  in binary 'div' operator expression

Warning: model inconsistency detected
/tmp/foo.mzn:2.1-28
  in variable declaration for 'Q'
  in binary 'div' operator expression

=====UNSATISFIABLE=====

So in the first case it's silent, in the second case it's verbose. This is a bit inconsistent. The verbosity can get in the way. Please provide a way to turn off warnings.

Another odd thing: D and Q were annotated :: output_var but only D was output. Why?

Another example:

$ cat /tmp/foo.mzn 
var bool: P;
var  0 .. 1: D :: output_var;
var -1 .. 1: Q = if P then 1 else -1 div D endif  :: output_var;
output ["P = \(P);\n"];
output ["D = \(D);\n"];
output ["Q = \(Q);\n"];
$ minizinc -a /tmp/foo.mzn
P = true;
D = 0;
Q = 1;
----------
P = false;
D = 1;
Q = -1;
----------
P = true;
D = 1;
Q = 1;
----------
==========

Note the solution with D = 0 for which the constraint Q = if P then 1 else -1 div D endif contains a division by zero. Says Section 2.2.7: any undefinedness “bubbles up” to the closest Boolean context and becomes false there.
Apparently, the if-then-else-endif integer expression does not behave as a partial function in this respect. I did not expect a solution for D = 0.

Another example:

$ cat /tmp/foo.mzn
var -2.. -2 union 1..1: A;
constraint
    (((abs(A) - ((1 div 1) mod 0))=1) <-> false);
$ minizinc -a /tmp/foo.mzn
Error: result of evaluation is undefined: division by zero
/tmp/foo.mzn:3.6-47
  in binary '<->' operator expression
  in binary '=' operator expression
  in binary '-' operator expression
  in binary 'mod' operator expression

I expected the division by zero to bubble up, effectively turning the constraint into false <-> false. I expected to get two solutions but got none.

[Dekker1]

First regarding the output annotations, the correct annotation is :: output and you have to annotate the declaration (so it should be placed before the = ...;). :: output_var is a FlatZinc annotation for the solver, but not one the compiler will process, so it should not be used in models.

The reason why the first model does not give a warning, and the second does. Is because the compiler has realised that the divisor is par and will take a value that will trigger the relational semantics. I suppose it is just that we as the developers expect that in par cases this is usually unexpected.

Although the difference between par and var might be unexpected, it should be noted that the same warning system is used for other functions that can trigger the relational semantics as well. For example, the following model will work without warning giving a single solution, but if you change the domain to 0..0 (making i par), then if also gives these warnings.

array[1..4] of var int: a = set2array(1..4);
var 0..1: i;
any: x ::output = a[I];

Finally for the last model, if-then-else has a special relationship with the relational sementics (as noted in the handbook):

In order to “guard” against partiality, we can use conditional statements like if y=0 then 0 else x div y endif, or if i in index_set(x) then x[i] else 0 endif, which define a default value for the cases where the expression is undefined.

This effectively means that if one side becomes undefined, the semantics are that a different branch of the if-then-else expression must have been selected. So for example in this case an additional constraint would be enforced that (D=0) -> P

[Dekker1]

Actually rereading that comment from the handbook, this doesn't actually say what I then explained underneath. However, my explanation is certainly the semantics as I understand it, where the if-then-else expression is really a seperate expression that interacts with relational semantics (picking a defined branch), and should not be seen as a function.

We should update the handbook to include an explanation of this behaviour.

[matsc-at-sics-se]

My last model does not contain if-then-else, it contains mod.

[Dekker1]

Sorry, I missed that last model yesterday. That one certainly seems like a bug to me. A slightly smaller variant:

var 1..2: x;
constraint ( ( (x - 1 mod 0) = 1) <-> false);

Somehow having the variable x is important, otherwise the expression is evaluated correctly.

[Dekker1]

I found the problem in this final model. It seems that aggregation of linear expressions did not yet account for undefined expressions. A fix for this problem should be merged soon to the develop branch.

I think I also forgot to mention that if you want to avoid the generation of the warnings, then you can annotate known partial expressions with ::maybe_partial.