In the solution of the Zebra puzzle (http://rosettacode.org/wiki/Zebra_puzzle#MiniZinc) there's a constraint stating that one of the pets must be a zebra:
var 1..5: n;
constraint Gz[n]=Zebra;
Has the expression below a different meaning? They yield different results.
constraint exists(n in 1..5)(Gz[n]=Zebra);
These constraints are indeed equivalent. There is however a different in the way MiniZinc will translate these constraint for the solver.
The first option will be translated as a element constraint:
var 1..5: n;
constraint array_int_element(n, Gz, Zebra);
While the second one will result in an big clause constraint:
constraint bool_clause([Gz[1]=Zebra, Gz[2]=Zebra, Gz[3]=Zebra, Gz[3]=Zebra, Gz[5]=Zebra], [])
Although the constraints are equivalent it might depend on the solver which form will be more efficient during solving.
A better approach is to use the global count_leq(array [int] of var int: x, int: y, int: c) which enforces c to be less or equal to the number of occurences of y in x. Expressing the constraint as:
include "count_leq.mzn";
constraint count_leq(Gz, Zebra, 1);
directly conveys the meaning of the constraint and allows the solver used to use whichever form of the constraint would be best suited for its solving mechanism
If the declaration var 1..5: n is removed, then there is no global n that can be used in the output section, and this will yield an error: MiniZinc: type error: undefined identifier n'`.
It you keep var 1..5: n then the variable n in the exists loop don't have any effect of the global defined variable n, with the result that (the global) n will take any of the values 1..5 (which is shown if all solutions are printed).