#
# Hidato puzzle instances in Z3
#
# This file includes instances for the Hidato models:
# - hidato.py
# - hidato_table.py
# - hidato_function.py
#
# This Z3 model was written by Hakan Kjellerstrand (hakank@gmail.com)
# See also my Z3 page: http://hakank.org/z3/
# 

#
# models, a 0 indicates an open cell which number is not yet known.
#
instances = {

  "puzzle1" : [[6, 0, 9],
               [0, 2, 8],
               [1, 0, 0]],
  
  "puzzle2" : [[0, 44, 41, 0, 0, 0, 0],
               [0, 43, 0, 28, 29, 0, 0],
               [0, 1, 0, 0, 0, 33, 0],
               [0, 2, 25, 4, 34, 0, 36],
               [49, 16, 0, 23, 0, 0, 0],
               [0, 19, 0, 0, 12, 7, 0],
               [0, 0, 0, 14, 0, 0, 0]],

  # Problems from the book:
  # Gyora Bededek: "Hidato: 2000 Pure Logic Puzzles"
  # Problem 1 (Practice)
  "puzzle3" : [[0, 0, 20, 0, 0],
               [0, 0, 0, 16, 18],
               [22, 0, 15, 0, 0],
               [23, 0, 1, 14, 11],
               [0, 25, 0, 0, 12]],
  
  # problem 2 (Practice)  
  "puzzle4" : [[0, 0, 0, 0, 14],
               [0, 18, 12, 0, 0],
               [0, 0, 17, 4, 5],
               [0, 0, 7, 0, 0],
               [9, 8, 25, 1, 0]],
  
  # problem 3 (Beginner)  
  "puzzle5" : [[0, 26, 0, 0, 0, 18],
               [0, 0, 27, 0, 0, 19],
               [31, 23, 0, 0, 14, 0],
               [0, 33, 8, 0, 15, 1],
               [0, 0, 0, 5, 0, 0],
               [35, 36, 0, 10, 0, 0]],

  # Problem 15 (Intermediate)  
  "puzzle6" : [[64, 0, 0, 0, 0, 0, 0, 0],
               [1, 63, 0, 59, 15, 57, 53, 0],
               [0, 4, 0, 14, 0, 0, 0, 0],
               [3, 0, 11, 0, 20, 19, 0, 50],
               [0, 0, 0, 0, 22, 0, 48, 40],
               [9, 0, 0, 32, 23, 0, 0, 41],
               [27, 0, 0, 0, 36, 0, 46, 0],
               [28, 30, 0, 35, 0, 0, 0, 0]],

  #  Problem 156 (Master]
  "puzzle7" :  [[88, 0, 0,100, 0, 0,37,0, 0,34],
                [ 0,86, 0,96,41, 0, 0,36, 0, 0],
                [ 0,93,95,83, 0, 0, 0,31,47, 0],
                [ 0,91, 0, 0, 0, 0, 0,29, 0, 0],
                [11, 0, 0, 0, 0, 0, 0,45,51, 0],
                [ 0, 9, 5, 3, 1, 0, 0, 0, 0, 0],
                [ 0,13, 4, 0, 0, 0, 0, 0, 0, 0],
                [15, 0, 0,25, 0, 0,54,67, 0, 0],
                [ 0,17, 0,23, 0,60,59, 0,69, 0],
                [19, 0,21,62,63, 0, 0, 0, 0, 0]],


  # Problem 188 (Genius]
  "puzzle8" : [[  0,  0,134,  2,  4,  0,  0,  0,  0,  0,  0,  0],
               [136,  0,  0,  1,  0,  5,  6, 10,115,106,  0,  0],
               [139,  0,  0,124,  0,122,117,  0,  0,107,  0,  0],
               [  0,131,126,  0,123,  0,  0, 12,  0,  0,  0,103],
               [  0,  0,144,  0,  0,  0,  0,  0, 14,  0, 99,101],
               [  0,  0,129,  0, 23, 21,  0, 16, 65, 97, 96,  0],
               [ 30, 29, 25,  0,  0, 19,  0,  0,  0, 66, 94,  0],
               [ 32,  0,  0, 27, 57, 59, 60,  0,  0,  0,  0, 92],
               [  0, 40, 42,  0, 56, 58,  0,  0, 72,  0,  0,  0],
               [  0, 39,  0,  0,  0,  0, 78, 73, 71, 85, 69,  0],
               [ 35,  0,  0, 46, 53,  0,  0,  0, 80, 84,  0,  0],
               [ 36,  0, 45,  0,  0, 52, 51,  0,  0,  0,  0, 88]],


}