A quick Sentient program to solve a sudoku posted in a tweet

miracle-sudoku-tweet-solver.snt

# A quick Sentient program to solve the sudoku posted in this tweet:
# https://twitter.com/crypticcracking/status/1293897459912056833

function main () {
  array9<array9<int5>> sudoku;

  sudoku.each(function (row) {
    invariant row.uniq?;

    invariant row.all?(function (n) {
      return n.between?(1, 9);
    });
  });

  sudoku.transpose.each(function (column) {
    invariant column.uniq?;
  });

  sudoku.boxes.each(function (box) {
    invariant box.uniq?;
  });

  invariant sudoku[0][3].even?;
  invariant sudoku[1][2].odd?;
  invariant sudoku[2][1].even?;
  invariant sudoku[3][0].odd?;

  invariant sudoku[0][7].even?;
  invariant sudoku[1][6].odd?;
  invariant sudoku[2][5].even?;
  invariant sudoku[3][4].odd?;
  invariant sudoku[4][3].even?;
  invariant sudoku[5][2].odd?;
  invariant sudoku[6][1].even?;
  invariant sudoku[7][0].odd?;

  invariant sudoku[3][8].odd?;
  invariant sudoku[4][7].even?;
  invariant sudoku[5][6].odd?;
  invariant sudoku[6][5].even?;
  invariant sudoku[7][4].odd?;
  invariant sudoku[8][3].even?;

  invariant sudoku[1][0] +
            sudoku[2][1] +
            sudoku[3][2] +
            sudoku[4][3] +
            sudoku[5][4] +
            sudoku[6][5] +
            sudoku[7][6] +
            sudoku[8][7] == 56;

  invariant sudoku[3][0] +
            sudoku[4][1] +
            sudoku[5][2] +
            sudoku[6][3] +
            sudoku[7][4] +
            sudoku[8][5] == 18;

  invariant sudoku[0][6] +
            sudoku[1][7] +
            sudoku[2][8] == 11;

  invariant sudoku[0][3] +
            sudoku[1][4] +
            sudoku[2][5] +
            sudoku[3][6] +
            sudoku[4][7] +
            sudoku[5][8] == 24;

  invariant sudoku[0][5] +
            sudoku[1][4] +
            sudoku[2][3] +
            sudoku[3][2] +
            sudoku[4][1] +
            sudoku[5][0] == 45;

  invariant sudoku[8][2] +
            sudoku[7][3] +
            sudoku[6][4] +
            sudoku[5][5] +
            sudoku[4][6] +
            sudoku[3][7] +
            sudoku[2][8] == 25;

  invariant sudoku[8][6] +
            sudoku[7][7] +
            sudoku[6][8] == 8;

  expose sudoku;
};

function boxes (sudoku) {
  boxes = [];

  3.times(function^ (i) {
    3.times(function^ (j) {
      boxes = boxes.push(sudoku.box(i, j));
    });
  });

  return boxes;
};

function box (sudoku, i, j) {
  cells = [];

  x = i * 3;
  y = j * 3;

  3.times(function^ (i) {
    3.times(function^ (j) {
      cells = cells.push(sudoku[x + i][y + j]);
    });
  });

  return cells;
};

main();