[BUG] MiniZinc/Choco 240130, `c90bf40a9`, `^`, missing solutions

[matsc-at-sics-se]

$ cat /tmp/latest.mzn
include "globals.mzn";
var {-2,0}: A;
constraint
    2 ^ (((-1 ^ A) * -3) - -2) != -2;
matsc@teterev:~/sicstus4$ minizinc -a /tmp/latest.mzn
A = -2;
----------
A = 0;
----------
==========
matsc@teterev:~/sicstus4$ minizinc -a --solver choco /tmp/latest.mzn
%% Choco 240130
=====UNSATISFIABLE=====

[cprudhom]

Once again, thank you for the bug reporting.

[matsc-at-sics-se]

Charles, I take it back! IMHO, this is a MiniZinc compiler bug. The constraint should fail.

Why? Assume A = -2. Then

2 ^ (((-1 ^ A) * -3) - -2) != -2; -->
2 ^ ((1 * -3) - -2) != -2; -->
2 ^ (-3 - -2) != -2; -->
2 ^ -1 != -2; 

But 2 ^ -1 does not evaluate to an integer. ^ is a partial function. In MiniZinc, such undefinedness is supposed to "bubble up" and fail the closest Boolean context, i.e., the != constraint. The same thing happens for A = 0.

The story changes if you consider:

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

Now, the undefinedness should bubble up and falsify the = constraint, i.e., it should simplify to

false <-> false;

and two solutions are expected, but Choco reports none.

[cprudhom]

Thank you for the details. I found where the issue came from, by reducing the model. Such power constraint are encoded as table constraint in choco and it appears that negative exponent were not correctly managed. That is fixed now and ready to be pushed.