Join GitHub today
GitHub is home to over 28 million developers working together to host and review code, manage projects, and build software together.Sign up
Compilation of xorall in reification context seems to be wrong #146
In the parity-learning problem (part of the MiniZinc benchmarks library), we have the following constraint:
This constraint translates to s bool_array_xor constraints like this one for s = 1 in the 44_22_5.3 instance,:
So I expected to find X_INTRODUCED_22 (or some variable equal to it) in X_INTRODUCED_200 but it is not there.
In fact it seems that all the computed_parities end up as unconstrained search variables.
(I am using MiniZinc 2.0.14.)
The annotation is indeed misleading, but as far as I can see the compilation is correct. The negation of X_22 is X_199, which appears in X_200. I'll look into a fix for the spurious defines_var annotation on the xor, it should really say defines_var(X_INTRODUCED_199).
Guido, this is the negation constraint you referred to:
So we would end up with two constraints defining X_INTRODUCED_199 which is clearly not the dataflow intended by the model author. I would rather expect to see:
Btw, I wonder why there is no array_bool_xor/2 constraint.
That's the constraint. As I said earlier, the annotations are currently not generated correctly. The negation should define X_22, not X_199.
You can try out the fix I just pushed by replacing the definition of xorall_reif in builtins.mzn with the following: