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

Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

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

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