2.8.2: partial functions and undefined values: missing solution

[matsc-at-sics-se]

[Another facet of #760].

This is expected (warnings omitted):

$ cat /tmp/bug.mzn 
var {2}: A;
var {2}: B;
constraint
    (((((B - A) ^ -1) * 3) = 3) <-> false);
$ minizinc -a /tmp/bug.mzn 
A = 2;
B = 2;
----------
==========

But if I extend the domains, the solution A = B = 2 is lost:

$ cat /tmp/bug.mzn 
var {-2,2}: A;
var {-2,2}: B;
constraint
    (((((B - A) ^ -1) * 3) = 3) <-> false);
$ minizinc -a /tmp/bug.mzn 
A = 2;
B = -2;
----------
A = -2;
B = 2;
----------
==========

If I find more cases, I will add them to this issue.

[Dekker1]

Thank you for the issue report.

It seems something is going wrong when translating the <expr> = 3 expression. Because the top level is <expr> <-> false. It converts = into !=, removing the outer expression. However, since this now changes the Boolean context in which the partiality is captured into the root context, this causes the whole model to become unsatisfiable when A = B = 2.

This is easy to see if you add a few extra constraints:

var {-2,2}: A;
var {-2,2}: B;
constraint
    (((((B - A) ^ -1) * 3) = 3) <-> false);
    
constraint A = B;
constraint A = 2;

Which gets translated into:

array [1..1] of int: X_INTRODUCED_16_ = [3];
var 2..2: A:: output_var;
var -1..1: X_INTRODUCED_15_ ::var_is_introduced :: is_defined_var;
constraint int_div(1,1,X_INTRODUCED_15_):: defines_var(X_INTRODUCED_15_);
constraint int_lin_ne(X_INTRODUCED_16_,[X_INTRODUCED_15_],3);
solve  satisfy;

[matsc-at-sics-se]

This is likely the same issue. MiniZinc finds two solutions with B = 2, but there are two more with B = 0.

$ cat /tmp/latest.mzn 
var {0,2}: B;
var -3.. -2: C;
constraint (((((5 div 0) * C))=B) <-> false);
$ minizinc -a /tmp/latest.mzn 
B = 2;
C = -3;
----------
B = 2;
C = -2;
----------
==========