sbv-5.14: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | None
Language | Haskell2010

Data.SBV.Examples.Puzzles.MagicSquare

Description

Solves the magic-square puzzle. An NxN magic square is one where all entries are filled with numbers from 1 to NxN such that sums of all rows, columns and diagonals is the same.

Synopsis

- type Elem = SWord32
- type Row = [Elem]
- type Board = [Row]
- check :: Elem -> Elem -> [Elem] -> SBool
- diag :: [[a]] -> [a]
- isMagic :: Board -> SBool
- chunk :: Int -> [a] -> [[a]]
- magic :: Int -> IO ()

# Documentation

type Elem = SWord32 Source #

Use 32-bit words for elements.

type Row = [Elem] Source #

A row is a list of elements

type Board = [Row] Source #

The puzzle board is a list of rows

check :: Elem -> Elem -> [Elem] -> SBool Source #

Checks that all elements in a list are within bounds

diag :: [[a]] -> [a] Source #

Get the diagonal of a square matrix

isMagic :: Board -> SBool Source #

Test if a given board is a magic square

chunk :: Int -> [a] -> [[a]] Source #

Group a list of elements in the sublists of length `i`

magic :: Int -> IO () Source #

Given `n`, magic `n` prints all solutions to the `nxn` magic square problem