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

Portabilityportable
Stabilityexperimental
Maintainererkokl@gmail.com

Data.SBV.Examples.Puzzles.NQueens

Description

Synopsis

Documentation

type Solution = [SWord8]Source

A solution is a sequence of row-numbers where queens should be placed

isValid :: Int -> Solution -> SBoolSource

Checks that a given solution of n-queens is valid, i.e., no queen captures any other.

nQueens :: Int -> IO ()Source

Given n, it solves the n-queens puzzle, printing all possible solutions.