Records and checks

Each repeat iteration forms a record. Its fields become columns in the data; nested repeats add array levels. Record names let a check refer to one record’s fields together.

Read jobs and check machine use

Each job below has one operation per machine. The inner repeat reads a machine number and duration for each operation:

site/examples/tutorial/jobshop-checks.iris

n_jobs: 1..
n_machines: 1..
check n_jobs <= (gecode.int_max - 2) / 2 / n_machines "there are too many jobs and machines"
repeat n_jobs as jobs {
  each job
  repeat n_machines as steps {
    each step
    machine: 0..<n_machines
    duration: 0..
  }
}
check distinct(job.machine) "a job uses a machine twice; each job must use every machine once"
check sum(j in jobs: sum(j.duration)) <= gecode.int_max "the total duration is too large"

site/examples/tutorial/jobshop.txt

2 2
0 3 1 2
1 4 0 1

iris read site/examples/tutorial/jobshop-checks.iris site/examples/tutorial/jobshop.txt --dzn

n_jobs = 2;
n_machines = 2;
machine = [| 0, 1
  | 1, 0 |];
duration = [| 3, 2
  | 4, 1 |];

The data has machine and duration columns of depth 2. There are no record objects and no entries named job or jobs. as jobs names the record list; each job names its individual records. Place each first in its repeat.

See column construction and logical records.

Check a record or a collection

check distinct(job.machine) runs for each job. job.machine is that job’s machine array. A plain repeated field in a check can also denote one record’s field, rather than the whole stored column. This is why checks can identify a failing record without an explicit loop.

The final comprehension explicitly ranges over jobs, sums each duration array, and compares the instance total with gecode.int_max. For a whole-column calculation that should happen once, compute it with let before checking the result. Avoid relying on a repeated field’s ordinary expression meaning inside a check: the check’s record resolution can change it.

See record names and field access, comprehensions, and checks and failure witnesses.

Locate a failed record

The first job in this input uses machine 0 twice:

site/examples/guides/jobshop-invalid.txt

2 2
0 3 0 2
1 4 0 1

iris read site/examples/tutorial/jobshop-checks.iris site/examples/guides/jobshop-invalid.txt --dzn

site/examples/guides/jobshop-invalid.txt:2:1: check failed for record 1 of 'jobs': a job uses a machine twice; each job must use every machine once
     2 | 0 3 0 2
       | ^
spec: site/examples/tutorial/jobshop-checks.iris:12

E-CHECK-FAILED points at the saved start of the failing job. The record number in the message starts at 1; the canonical error’s record_path starts at 0, so this job has path [0]. A check without a record witness uses the current input cursor instead.

Checks stop at the first false condition. A hard evaluation error, such as an out-of-range array index, keeps its own error code. Guard optional data with defined and short-circuit operators before accessing it.

For the complete reader, including descriptions and named instances, see the job shop tutorial and library page.