A specification language for structured text formats

Iris describes the structure of a text format in a reader spec: which values a file contains, how they are laid out, how they are collected into arrays, and which conditions they must satisfy. From that one description, Iris reads each input into named, typed data, or rejects it with the input position and the reader-spec statement that failed.

The format library has reader specs for formats such as DIMACS CNF, TSPLIB and Sudoku. Iris began as the instance reader introduced in Gecode 6.5.0. Run a reader spec from the command line, call it from Rust, or try it in the playground.

Introduction Explore formats

A DIMACS file, its reader spec, and the data it reads.

Input

input.txt

Reader spec

dimacs-cnf.iris

format dimacs-cnf


 # SATLIB files end with "%" and "0"

 {
   # the terminating 0 is not stored
}

Data

typed entries

vars int

clauses int

clause int · depth 2

Focus or point to connect input, reader spec, and data. Select to keep a connection; Escape clears it.

All three clauses read; terminating zeros are consumed without being stored.

Examples from the format library

Choose a format to inspect its input, reader spec, and data. These examples run through the Iris command-line tool.

DIMACS CNF TSPLIB Nonogram Job shop Sudoku TSPTW

Zero terminators end each clause and are discarded from the data.

input spec.iris JSON dzn

three-variables · inputView full input

c Hand-made three-variable formula
p cnf 3 3
1 -2 0
2 3 -1 0
-3 0

three-variables · spec.irisView full reader spec

format dimacs-cnf

comment "c"
stop "%" # SATLIB files end with "%" and "0"
line "p cnf {vars:0..gecode.int_max} {clauses:0..}"
repeat clauses {
  list clause: -vars..vars until 0 # the terminating 0 is not stored
}

three-variables · JSONView full json

{"iris":"0.1","entries":[{"name":"vars","type":"int","depth":0,"value":3},{"name":"clauses","type":"int","depth":0,"value":3},{"name":"clause","type":"int","depth":2,"value":[[1,-2],[2,3,-1],[-3]]}]}

three-variables · dznView full dzn

vars = 3;
clauses = 3;
% clause: array[int] of tuple(array[int] of int)
clause = [([1, -2],), ([2, 3, -1],), ([-3],)];

Open in playground Download full case About DIMACS CNF

Read the inputRun from the repository root.

iris read formats/dimacs-cnf/dimacs-cnf.iris formats/dimacs-cnf/cases/three-variables/input.txt --dzn

vars = 3;
clauses = 3;
% clause: array[int] of tuple(array[int] of int)
clause = [([1, -2],), ([2, 3, -1],), ([-3],)];

Read succeeded

Coordinates remain coordinates; distance construction belongs to the host.

input spec.iris JSON dzn

euc-2d-five · inputView full input

NAME : handmade-euc-2d-five
TYPE : TSP
DIMENSION : 5
EDGE_WEIGHT_TYPE : EUC_2D
NODE_COORD_TYPE : TWOD_COORDS
NODE_COORD_SECTION
1 0 0
2 3 0
3 3 4
4 0 4
5 1.5 2
EOF

euc-2d-five · spec.irisView full reader spec

format tsplib

comment "COMMENT"
sections until "EOF" {
  "NAME : {name:rest}" optional
  "TYPE : {type:word}" optional
  "DIMENSION : {n:2..46340}"
  "EDGE_WEIGHT_TYPE : {edge_weight_type:word}" optional
  "EDGE_WEIGHT_FORMAT : {edge_weight_format:word}" optional
  "NODE_COORD_TYPE : {node_coord_type:word}" optional
  "DISPLAY_DATA_TYPE : {display_data_type:word}" optional
  "NODE_COORD_SECTION" optional {
    repeat n {
      node: int
      x: float
      y: float
    }
  }
  "EDGE_WEIGHT_SECTION" optional {
    if !defined(edge_weight_format) {
      let edge_weight_format = "FULL_MATRIX"
    }
    weight[n][n]: 0..gecode.int_max / n layout edge_weight_format
  }

Excerpt · View full reader spec

euc-2d-five · JSONView full json

{"iris":"0.1","entries":[{"name":"name","type":"string","depth":0,"value":"handmade-euc-2d-five"},{"name":"type","type":"string","depth":0,"value":"TSP"},{"name":"n","type":"int","depth":0,"value":5},{"name":"edge_weight_type","type":"string","depth":0,"value":"EUC_2D"},{"name":"node_coord_type","type":"string","depth":0,"value":"TWOD_COORDS"},{"name":"node","type":"int","depth":1,"value":[1,2,3,4,5]},{"name":"x","type":"float","depth":1,"value":[0,3,3,0,1.5]},{"name":"y","type":"float","depth":1,"value":[0,0,4,4,2]}]}

euc-2d-five · dznView full dzn

name = "handmade-euc-2d-five";
'type' = "TSP";
n = 5;
edge_weight_type = "EUC_2D";
node_coord_type = "TWOD_COORDS";
node = [1, 2, 3, 4, 5];
x = [0.0, 3.0, 3.0, 0.0, 1.5];
y = [0.0, 0.0, 4.0, 4.0, 2.0];

Open in playground Download full case About TSPLIB

Read the inputRun from the repository root.

iris read formats/tsplib/tsplib.iris formats/tsplib/cases/euc-2d-five/input.txt --dzn

name = "handmade-euc-2d-five";
'type' = "TSP";
n = 5;
edge_weight_type = "EUC_2D";
node_coord_type = "TWOD_COORDS";
node = [1, 2, 3, 4, 5];
x = [0.0, 3.0, 3.0, 0.0, 1.5];
y = [0.0, 0.0, 4.0, 4.0, 2.0];

Read succeeded

Row and column clues become ragged arrays, with one array per line.

input spec.iris JSON dzn

five-by-five · inputView full input

title "Hand-made X"
width 5
height 5
rows
1,1
1,1
1
1,1
1,1
columns
1,1
1,1
1
1,1
1,1

five-by-five · spec.irisView full reader spec

format nonogram

separators ","
sections skip other {
  "width {width:1..}"
  "height {height:1..}"
  "rows" {
    repeat height {
      list row: 0.. until eol
    }
  }
  "columns" {
    repeat width {
      list col: 0.. until eol
    }
  }
}

check height <= 1000000 / width "the board must have at most a million fields"
check size(row) == height && size(col) == width
  "the numbers of rows and columns differ from the board size"
check count(row) <= 1 || min(row) > 0 "a 0 must be the only clue of its row"
check count(col) <= 1 || min(col) > 0 "a 0 must be the only clue of its column"
check sum(row) + count(row) - 1 <= width "the clues of a row do not fit into the width of the board"

Excerpt · View full reader spec

five-by-five · JSONView full json

{"iris":"0.1","entries":[{"name":"width","type":"int","depth":0,"value":5},{"name":"height","type":"int","depth":0,"value":5},{"name":"row","type":"int","depth":2,"value":[[1,1],[1,1],[1],[1,1],[1,1]]},{"name":"col","type":"int","depth":2,"value":[[1,1],[1,1],[1],[1,1],[1,1]]}]}

five-by-five · dznView full dzn

width = 5;
height = 5;
% row: array[int] of tuple(array[int] of int)
row = [([1, 1],), ([1, 1],), ([1],), ([1, 1],), ([1, 1],)];
% col: array[int] of tuple(array[int] of int)
col = [([1, 1],), ([1, 1],), ([1],), ([1, 1],), ([1, 1],)];

Open in playground Download full case About Nonogram

Read the inputRun from the repository root.

iris read formats/nonogram/nonogram.iris formats/nonogram/cases/five-by-five/input.txt --dzn

width = 5;
height = 5;
% row: array[int] of tuple(array[int] of int)
row = [([1, 1],), ([1, 1],), ([1],), ([1, 1],), ([1, 1],)];
% col: array[int] of tuple(array[int] of int)
col = [([1, 1],), ([1, 1],), ([1],), ([1, 1],), ([1, 1],)];

Read succeeded

Each job’s operations yield machine and duration arrays.

input spec.iris JSON dzn

jsplib · inputView full input

# Hand-made JSPLIB style file
# Jobs and machines, then machine-duration pairs
3 3
0 3 2 2 1 4
1 2 0 1 2 3
2 4 1 3 0 2

jsplib · spec.irisView full reader spec

format jobshop

comment "#" "+++"
instances {
  sections skip other {
    "instance {name:word}" optional
    "{n_jobs:1..} {n_machines:1..}" last {
      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"
}

jsplib · JSONView full json

{"iris":"0.1","entries":[{"name":"n_jobs","type":"int","depth":0,"value":3},{"name":"n_machines","type":"int","depth":0,"value":3},{"name":"machine","type":"int","depth":2,"value":[[0,2,1],[1,0,2],[2,1,0]]},{"name":"duration","type":"int","depth":2,"value":[[3,2,4],[2,1,3],[4,3,2]]}]}

jsplib · dznView full dzn

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

Open in playground Download full case About Job shop

Read the inputRun from the repository root.

iris read formats/jobshop/jobshop.iris formats/jobshop/cases/jsplib/input.txt --dzn

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

Read succeeded

Blank cells become zero. Solving the puzzle belongs to the host.

input spec.iris JSON dzn

four-by-four · inputView full input

# size=4 box=2x2
1..4
.41.
.14.
4..1

four-by-four · spec.irisView full reader spec

format sudoku

instances {
  line "# size={n:1..} box={box_width:1..}x{box_height:1..}"
  cells[n][n]: alphabet "123456789ABCDEFGHIJKLMNOPQRSTUVWXYZ0" blank "."

  check box_width * box_height == n "boxes must tile the grid"
  check max(cells) <= n "a value is larger than the size of the grid"
}

four-by-four · JSONView full json

{"iris":"0.1","entries":[{"name":"n","type":"int","depth":0,"value":4},{"name":"box_width","type":"int","depth":0,"value":2},{"name":"box_height","type":"int","depth":0,"value":2},{"name":"cells","type":"int","depth":2,"value":[[1,0,0,4],[0,4,1,0],[0,1,4,0],[4,0,0,1]]}]}

four-by-four · dznView full dzn

n = 4;
box_width = 2;
box_height = 2;
cells = [| 1, 0, 0, 4
  | 0, 4, 1, 0
  | 0, 1, 4, 0
  | 4, 0, 0, 1 |];

Open in playground Download full case About Sudoku

Read the inputRun from the repository root.

iris read formats/sudoku/sudoku.iris formats/sudoku/cases/four-by-four/input.txt --dzn

n = 4;
box_width = 2;
box_height = 2;
cells = [| 1, 0, 0, 4
  | 0, 4, 1, 0
  | 0, 1, 4, 0
  | 4, 0, 0, 1 |];

Read succeeded

Travel times form a matrix; checks require ordered time windows.

input spec.iris JSON dzn

three-nodes · inputView full input

# Hand-made depot and two customers
3
0 2 4
3 0 2
4 3 0
0 20
2 8
5 12

three-nodes · spec.irisView full reader spec

format tsptw

comment "#"
n: 2..1000
dist[n][n]: 0..gecode.int_max / 2 / n

type time = 0..gecode.int_max / 2
repeat n as nodes {
  each node
  ready: time
  due: time
}

check node.ready <= node.due "the time window of a node is invalid"
check nodes[0].ready == 0 "the depot (node 0) must open at time 0"

three-nodes · JSONView full json

{"iris":"0.1","entries":[{"name":"n","type":"int","depth":0,"value":3},{"name":"dist","type":"int","depth":2,"value":[[0,2,4],[3,0,2],[4,3,0]]},{"name":"ready","type":"int","depth":1,"value":[0,2,5]},{"name":"due","type":"int","depth":1,"value":[20,8,12]}]}

three-nodes · dznView full dzn

n = 3;
dist = [| 0, 2, 4
  | 3, 0, 2
  | 4, 3, 0 |];
ready = [0, 2, 5];
due = [20, 8, 12];

Open in playground Download full case About TSPTW

Read the inputRun from the repository root.

iris read formats/tsptw/tsptw.iris formats/tsptw/cases/three-nodes/input.txt --dzn

n = 3;
dist = [| 0, 2, 4
  | 3, 0, 2
  | 4, 3, 0 |];
ready = [0, 2, 5];
due = [20, 8, 12];

Read succeeded

Invalid input

This file declares three variables but uses literal 4. Iris reports the input position and the reader-spec statement that rejected it.

literal-out-of-range · inputView full input

p cnf 3 1
1 4 0

E-EXPECTED-VALUE

Read rejectedRun from the repository root.

iris read formats/dimacs-cnf/dimacs-cnf.iris formats/dimacs-cnf/cases/literal-out-of-range/input.txt --dzn

formats/dimacs-cnf/cases/literal-out-of-range/input.txt:2:3: expected an int in -3..3, found '4'
     2 | 1 4 0
       |   ^
while reading: repeat [1 of 1] > clause
spec: formats/dimacs-cnf/dimacs-cnf.iris:7

Input rejected

Download error JSON Download full case