(use-modules
  (srfi srfi-1)
  (srfi srfi-26)
  (ice-9 match)
  (sat solver)
  (sat helpers))

(define (get-value board vals col row)
  (1+
   (find
     (lambda (possible-value)
       (array-ref vals
                  (array-ref board col row possible-value)))
     (iota (biggest-value board)))))


(define (set-initial-value board col row val)
  (add-clause
    (list
      (array-ref board
                 col
                 row
                 (1- val)))))


(define (map-for-0-to n f)
  (map f (iota n)))


(define (make-row row board-size)
  (map-for-0-to
    board-size
    (cut cons <> row)))


(define (make-col col board-size)
  (map-for-0-to
    board-size
    (cut cons col <>)))


(define (rows board-size)
  (map-for-0-to
    board-size
    (cut make-row <> board-size)))


(define (cols board-size)
  (map-for-0-to
    board-size
    (cut make-col <> board-size)))


(define (make-box bcol brow box-size)
  (let ((l '()))
    (do ((icol 0 (1+ icol))) ((= icol box-size))
      (do ((irow 0 (1+ irow))) ((= irow box-size))
        (set! l (cons
                  (cons (+ (* box-size bcol) icol)
                        (+ (* box-size brow) irow))
                  l))))
    l))


(define (boxes board-size box-size)
  (let ((l '()))
    (do ((bcol 0 (1+ bcol))) ((= bcol 3))
      (do ((brow 0 (1+ brow))) ((= brow 3))
        (set! l (cons
                   (make-box bcol brow box-size)
                   l))
        ))
    l))


(define (biggest-value board)
  (1+ (match
    (array-shape board)
    (((_ _) (_ _) (_ max-value))
     max-value))))


(define (unique-values board coords-list)
  (for-each
    (lambda (n)
      (exactly-one-true
        (map
          (lambda (coord)
            (array-ref board (car coord) (cdr coord) n))
          coords-list)))
    (iota (biggest-value board))))


(define (all-unique-values board coord-lists)
  (for-each
    (cut unique-values board <>)
    coord-lists))


(define (make-board size)
  (let ((board (make-array #f size size size)))
    (array-map! board make-sat-variable)
    board))


(define (all-one-number board col row)
  (exactly-one-true
    (map
      (lambda (value)
        (array-ref board col row value))
      (iota (biggest-value board)))))


(let* ((board-size 9)
       (board (make-board board-size)))

  ;; The standard Sudoku rules
  (all-unique-values board (rows board-size))
  (all-unique-values board (cols board-size))
  (all-unique-values board (boxes board-size 3))

  ;; Each position contains exactly one number
  (do ((col 0 (1+ col))) ((= col board-size))
    (do ((row 0 (1+ row))) ((= row board-size))
      (all-one-number board col row)))

  ;; Initially specified values
  (set-initial-value board 0 0 4)
  (set-initial-value board 0 7 5)
  (set-initial-value board 0 8 1)

  (set-initial-value board 1 1 3)
  (set-initial-value board 1 3 2)

  (set-initial-value board 2 8 4)

  (set-initial-value board 3 2 7)
  (set-initial-value board 3 6 6)
  (set-initial-value board 3 7 2)

  (set-initial-value board 4 4 8)
  (set-initial-value board 4 5 1)

  (set-initial-value board 5 6 3)

  (set-initial-value board 6 0 8)
  (set-initial-value board 6 4 4)

  (set-initial-value board 7 3 6)
  (set-initial-value board 7 6 7)

  (set-initial-value board 8 0 5)

  (let ((vals (solve-sat)))
    (do ((row 0 (1+ row))) ((= row board-size))
      (do ((col 0 (1+ col))) ((= col board-size))
        (format #t "~a" (get-value board vals col row)))
      (newline))))