sbv-0.9.8: Symbolic Bit Vectors: Prove bit-precise program properties using SMT solvers.




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 = SWord32Source

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] -> SBoolSource

Checks that all elements in a list are within bounds

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

Get the diagonal of a square matrix

isMagic :: Board -> SBoolSource

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