Great news—your understanding of this MiniZinc syntax is 100% correct! Let’s break down the original example step by step to confirm, and validate your fruit enum test case to make sure you’ve got this locked in.

First, let’s recap the key distinctions you nailed:

• set of int: DIGIT = 1..9: This defines a fixed collection (set) of integers from 1 to 9. It’s not a variable—it’s a type/scope used to index arrays or restrict variable values.
• array[DIGIT] of int: rods = [1,2,3,4,5,2,3,4,5]: The DIGIT set becomes the index range for the rods array. So rods[1] = 1, rods[2] = 2, ..., rods[9] = 5 (each index maps directly to the array’s elements in order).
• var 1..9: X: This creates a variable that can take any integer value between 1 and 9. It’s a dynamic value the solver will compute, unlike the fixed DIGIT set.

Let’s unpack the full context (even though you didn’t include the variable declarations, they’re implied in the course):
First, the course would have declared 5 variables like this:

var DIGIT: M1;
var DIGIT: M2;
var DIGIT: M3;
var DIGIT: M4;
var DIGIT: M5;

These variables represent unknown digits (1-9) the solver needs to find. Now let’s break the constraints:

Constraint 1: Sum of Rod Values #

constraint rods[M1] + rods[M2] + rods[M3] + rods[M4] + rods[M5] = 12;

Each Mi is a digit (1-9), so rods[Mi] pulls the pre-defined integer value from the rods array at index Mi. For example:

• If M1 = 6, rods[M1] = 2 (since the 6th element in rods is 2)
• If M2 = 5, rods[M2] = 5
  The solver must find values for M1-M5 where the sum of these pulled values equals 12.

Constraint 2: Numeric Equation #

constraint 2303 + M1 * 10 + 980 + M2 * 1000 + M3 = 301 + M4 * 1000 + M5 * 10;

This is a standard arithmetic equation where each Mi acts as a digit in a larger number:

• M2 * 1000 = M2 is the thousands place in a number
• M1 * 10 = M1 is the tens place
  When you compute both sides, they must be equal. For example, if M2=1, that term becomes 1000; if M5=7, that term becomes 70.

Let’s confirm your test case to reinforce the logic:

enum FRUIT = {apple, orange, banana};
array[FRUIT] of int: whatever = [4, 9834, -42];
var FRUIT: Opt1;

• FRUIT is an enumeration set (a fixed collection of named values)
• whatever[apple] = 4, whatever[orange] = 9834, whatever[banana] = -42 (indexed directly by the enum values)
• Opt1 is a variable that can take any of the three enum values. When you use whatever[Opt1] in a constraint, it dynamically uses the integer value tied to whatever enum value Opt1 takes (e.g., if Opt1 = banana, whatever[Opt1] = -42).

The only implicit detail you might not have spelled out is that when you declare a variable like var DIGIT: Mi, you’re automatically restricting Mi to values in the DIGIT set (1-9). This means the solver will never try values outside that range, which aligns with how the rods array is indexed (since rods only exists for indices 1-9).

Your understanding is solid—no deviations or missing pieces here!

内容的提问来源于stack exchange，提问作者MikeyB