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

Copyright(c) Levent Erkok
Safe HaskellNone



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.



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