ersatz 0.2.0.1 → 0.2.4
raw patch · 36 files changed
+525/−222 lines, 36 filesdep +parsecdep ~arraydep ~basedep ~containerssetup-changednew-component:exe:ersatz-regexp-gridnew-component:exe:ersatz-sudokubinary-added
Dependencies added: parsec
Dependency ranges changed: array, base, containers, lens, mtl, transformers
Files
- CHANGELOG.md +13/−0
- HLint.hs +1/−0
- LICENSE +9/−2
- README.md +53/−0
- Setup.lhs +15/−4
- ersatz.cabal +114/−20
- examples/regexp-grid/COPYING +0/−13
- examples/regexp-grid/Main.hs +1/−1
- examples/regexp-grid/RegexpGrid/Problem.hs +35/−33
- examples/regexp-grid/RegexpGrid/Types.hs +1/−1
- examples/regexp-grid/Setup.hs +0/−2
- examples/regexp-grid/regexp-grid.cabal +0/−22
- examples/sudoku/Main.hs +64/−0
- examples/sudoku/Sudoku/Cell.hs +28/−0
- examples/sudoku/Sudoku/Problem.hs +84/−0
- notes/SPOILER.html +15/−0
- notes/grid.pdf binary
- src/Ersatz.hs +1/−1
- src/Ersatz/Bit.hs +51/−42
- src/Ersatz/Bits.hs +9/−8
- src/Ersatz/Decoding.hs +2/−1
- src/Ersatz/Encoding.hs +1/−1
- src/Ersatz/Equatable.hs +2/−1
- src/Ersatz/Internal/Circuit.hs +0/−56
- src/Ersatz/Internal/Formula.hs +2/−1
- src/Ersatz/Internal/Literal.hs +2/−1
- src/Ersatz/Internal/Parser.hs +1/−1
- src/Ersatz/Internal/StableName.hs +1/−1
- src/Ersatz/Problem.hs +2/−1
- src/Ersatz/Solution.hs +2/−1
- src/Ersatz/Solver.hs +1/−1
- src/Ersatz/Solver/Common.hs +1/−1
- src/Ersatz/Solver/DepQBF.hs +3/−2
- src/Ersatz/Solver/Minisat.hs +3/−2
- src/Ersatz/Variable.hs +7/−1
- tests/doctests.hsc +1/−1
CHANGELOG.md view
@@ -1,3 +1,16 @@+0.2.3+-----+* SafeHaskell support++0.2.2+-----+* Added examples to the documentation.+* Made the examples build as `ersatz-sudoku` and `ersatz-regexp-grid`.++0.2.1+-----+* Added `examples/sudoku`, a sudoku solver.+ 0.2.0.1 ------- * Fixed an overly conservative bound on `containers`.
+ HLint.hs view
@@ -0,0 +1,1 @@+import "hint" HLint.Default
LICENSE view
@@ -1,5 +1,5 @@-Copyright (c) 2010-2013 Edward Kmett-Copyright (c) 2013 Johan Kiviniemi+Copyright © 2010-2013 Edward Kmett+Copyright © 2013 Johan Kiviniemi All rights reserved. @@ -30,3 +30,10 @@ THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.++----------------------------------------------------------------------++The puzzle in notes/grid.pdf was also made available to us for+distribution under the BSD3 license. This puzzle was written+for MIT Mystery Hunt 2013 by Dan Gulotta based on an idea by+Palmer Mebane. Copyright © 2013 Dan Gulotta
README.md view
@@ -59,6 +59,59 @@ Support is offered for decoding various Haskell datatypes from the solution provided by the SAT solver. +# Examples++Included are a couple of examples included with the distribution.+Neither are as fast as a dedicated solver for their respective+domains, but they showcase how you can solve real world problems+involving 10s or 100s of thousands of variables and constraints+with `ersatz`.++## sudoku++```+% time ersatz-sudoku+Problem:+┌───────┬───────┬───────┐+│ 5 3 │ 7 │ │+│ 6 │ 1 9 5 │ │+│ 9 8 │ │ 6 │+├───────┼───────┼───────┤+│ 8 │ 6 │ 3 │+│ 4 │ 8 3 │ 1 │+│ 7 │ 2 │ 6 │+├───────┼───────┼───────┤+│ 6 │ │ 2 8 │+│ │ 4 1 9 │ 5 │+│ │ 8 │ 7 9 │+└───────┴───────┴───────┘+Solution:+┌───────┬───────┬───────┐+│ 5 3 4 │ 6 7 8 │ 9 1 2 │+│ 6 7 2 │ 1 9 5 │ 3 4 8 │+│ 1 9 8 │ 3 4 2 │ 5 6 7 │+├───────┼───────┼───────┤+│ 8 5 9 │ 7 6 1 │ 4 2 3 │+│ 4 2 6 │ 8 5 3 │ 7 9 1 │+│ 7 1 3 │ 9 2 4 │ 8 5 6 │+├───────┼───────┼───────┤+│ 9 6 1 │ 5 3 7 │ 2 8 4 │+│ 2 8 7 │ 4 1 9 │ 6 3 5 │+│ 3 4 5 │ 2 8 6 │ 1 7 9 │+└───────┴───────┴───────┘+ersatz-sudoku 1,13s user 0,04s system 99% cpu 1,179 total+```++## regexp-grid++This solves the [regular crossword puzzle](https://github.com/ekmett/ersatz/raw/master/notes/grid.pdf) from the MIT mystery hunt.++> % time ersatz-regexp-grid++[SPOILER](notes/SPOILER.html)++> ersatz-regexp-grid 2,45s user 0,05s system 99% cpu 2,502 total+ Contact Information -------------------
Setup.lhs view
@@ -5,14 +5,15 @@ import Data.List ( nub ) import Data.Version ( showVersion )-import Distribution.Package ( PackageName(PackageName), PackageId, InstalledPackageId, packageVersion, packageName )+import Distribution.Package ( PackageName(PackageName), Package, PackageId, InstalledPackageId, packageVersion, packageName ) import Distribution.PackageDescription ( PackageDescription(), TestSuite(..) ) import Distribution.Simple ( defaultMainWithHooks, UserHooks(..), simpleUserHooks )-import Distribution.Simple.Utils ( rewriteFile, createDirectoryIfMissingVerbose)+import Distribution.Simple.Utils ( rewriteFile, createDirectoryIfMissingVerbose, copyFiles ) import Distribution.Simple.BuildPaths ( autogenModulesDir )-import Distribution.Simple.Setup ( BuildFlags(buildVerbosity), fromFlag)+import Distribution.Simple.Setup ( BuildFlags(buildVerbosity), Flag(..), fromFlag, HaddockFlags(haddockDistPref)) import Distribution.Simple.LocalBuildInfo ( withLibLBI, withTestLBI, LocalBuildInfo(), ComponentLocalBuildInfo(componentPackageDeps) )-import Distribution.Verbosity ( Verbosity)+import Distribution.Text ( display )+import Distribution.Verbosity ( Verbosity, normal ) import System.FilePath ( (</>) ) main :: IO ()@@ -20,7 +21,17 @@ { buildHook = \pkg lbi hooks flags -> do generateBuildModule (fromFlag (buildVerbosity flags)) pkg lbi buildHook simpleUserHooks pkg lbi hooks flags+ , postHaddock = \args flags pkg lbi -> do+ copyFiles normal (haddockOutputDir flags pkg) [("notes","SPOILER.html"), ("notes","grid.pdf")]+ postHaddock simpleUserHooks args flags pkg lbi }++haddockOutputDir :: Package p => HaddockFlags -> p -> FilePath+haddockOutputDir flags pkg = destDir where+ baseDir = case haddockDistPref flags of+ NoFlag -> "."+ Flag x -> x+ destDir = baseDir </> "doc" </> "html" </> display (packageName pkg) generateBuildModule :: Verbosity -> PackageDescription -> LocalBuildInfo -> IO () generateBuildModule verbosity pkg lbi = do
ersatz.cabal view
@@ -1,9 +1,10 @@ name: ersatz-version: 0.2.0.1+version: 0.2.4 license: BSD3 license-file: LICENSE author: Edward A. Kmett, Johan Kiviniemi maintainer: Edward A. Kmett <ekmett@gmail.com>+copyright: © 2010-2013 Edward Kmett, © 2013 Johan Kiviniemi stability: experimental homepage: http://github.com/ekmett/ersatz bug-reports: http://github.com/ekmett/ersatz/issues@@ -20,24 +21,71 @@ . > half_adder :: Bit -> Bit -> (Bit, Bit) > half_adder a b = (a `xor` b, a && b)-copyright: (c) 2010-2013 Edward Kmett, (c) 2013 Johan Kiviniemi+ .+ /Longer Examples/+ .+ Included are a couple of examples included with the distribution.+ Neither are as fast as a dedicated solver for their respective+ domains, but they showcase how you can solve real world problems+ involving 10s or 100s of thousands of variables and constraints+ with `ersatz`.+ .+ @ersatz-sudoku@+ .+ > % time ersatz-sudoku+ > Problem:+ > ┌───────┬───────┬───────┐+ > │ 5 3 │ 7 │ │+ > │ 6 │ 1 9 5 │ │+ > │ 9 8 │ │ 6 │+ > ├───────┼───────┼───────┤+ > │ 8 │ 6 │ 3 │+ > │ 4 │ 8 3 │ 1 │+ > │ 7 │ 2 │ 6 │+ > ├───────┼───────┼───────┤+ > │ 6 │ │ 2 8 │+ > │ │ 4 1 9 │ 5 │+ > │ │ 8 │ 7 9 │+ > └───────┴───────┴───────┘+ > Solution:+ > ┌───────┬───────┬───────┐+ > │ 5 3 4 │ 6 7 8 │ 9 1 2 │+ > │ 6 7 2 │ 1 9 5 │ 3 4 8 │+ > │ 1 9 8 │ 3 4 2 │ 5 6 7 │+ > ├───────┼───────┼───────┤+ > │ 8 5 9 │ 7 6 1 │ 4 2 3 │+ > │ 4 2 6 │ 8 5 3 │ 7 9 1 │+ > │ 7 1 3 │ 9 2 4 │ 8 5 6 │+ > ├───────┼───────┼───────┤+ > │ 9 6 1 │ 5 3 7 │ 2 8 4 │+ > │ 2 8 7 │ 4 1 9 │ 6 3 5 │+ > │ 3 4 5 │ 2 8 6 │ 1 7 9 │+ > └───────┴───────┴───────┘+ > ersatz-sudoku 1,13s user 0,04s system 99% cpu 1,179 total+ .+ @ersatz-regexp-grid@+ .+ This solves the \"regular crossword puzzle\" (<grid.pdf>) from the 2013 MIT mystery hunt.+ .+ > % time ersatz-regexp-grid+ .+ "SPOILER"+ .+ > ersatz-regexp-grid 2,45s user 0,05s system 99% cpu 2,502 total+ build-type: Custom cabal-version: >= 1.10-tested-with: GHC == 7.6.2+tested-with: GHC == 7.4.1, GHC == 7.6.2 extra-source-files:- AUTHORS.md- README.md- CHANGELOG.md .ghci .gitignore .travis.yml- examples/regexp-grid/COPYING- examples/regexp-grid/Main.hs- examples/regexp-grid/regexp-grid.cabal- examples/regexp-grid/RegexpGrid/Problem.hs- examples/regexp-grid/RegexpGrid/Regexp.hs- examples/regexp-grid/RegexpGrid/Types.hs- examples/regexp-grid/Setup.hs+ AUTHORS.md+ CHANGELOG.md+ HLint.hs+ README.md+ notes/SPOILER.html+ notes/grid.pdf notes/papers.md travis/cabal-apt-install travis/config@@ -104,6 +152,11 @@ type: git location: git://github.com/ekmett/ersatz.git +flag examples+ description: Build examples+ default: True+ manual: True+ library ghc-options: -Wall hs-source-dirs: src@@ -132,7 +185,6 @@ Ersatz.Decoding Ersatz.Equatable Ersatz.Encoding- Ersatz.Internal.Circuit Ersatz.Internal.Formula Ersatz.Internal.Literal Ersatz.Problem@@ -147,18 +199,60 @@ Ersatz.Internal.StableName Ersatz.Solver.Common ++executable ersatz-regexp-grid+ -- description: An example program that solves the regular expression crossword problem <http://www.coinheist.com/rubik/a_regular_crossword/> using Ersatz.+ if flag(examples)+ build-depends:+ base < 5,+ containers,+ ersatz,+ ghc-prim,+ lens,+ mtl,+ parsec >= 3.1 && < 3.2+ else+ buildable: False+ main-is: Main.hs+ other-modules:+ RegexpGrid.Problem+ RegexpGrid.Regexp+ RegexpGrid.Types+ default-language: Haskell2010+ ghc-options: -Wall+ hs-source-dirs: examples/regexp-grid++executable ersatz-sudoku+ -- description: An example program that solves a sudoku problem using Ersatz.+ if flag(examples)+ build-depends:+ array,+ base < 5,+ ersatz,+ ghc-prim,+ mtl+ else+ buildable: False+ default-language: Haskell2010+ main-is: Main.hs+ other-modules:+ Sudoku.Cell+ Sudoku.Problem+ ghc-options: -Wall+ hs-source-dirs: examples/sudoku+ test-suite properties type: exitcode-stdio-1.0 ghc-options: -Wall default-language: Haskell2010 build-depends:- ersatz,- base >= 4 && < 6,- mtl >= 1.1 && < 2.2,- transformers == 0.3.*,- containers >= 0.2.0.1,- array >= 0.2 && < 0.5,+ array,+ base < 5,+ containers, data-reify >= 0.5 && < 0.7,+ ersatz,+ mtl,+ transformers, test-framework >= 0.2.4 && < 0.9, test-framework-quickcheck >= 0.2.4 && < 0.4, test-framework-hunit >= 0.2.4 && < 0.4,
− examples/regexp-grid/COPYING
@@ -1,13 +0,0 @@-© 2013 Johan Kiviniemi <devel@johan.kiviniemi.name>--Permission to use, copy, modify, and/or distribute this software for any-purpose with or without fee is hereby granted, provided that the above-copyright notice and this permission notice appear in all copies.--THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES-WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF-MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR-ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES-WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN-ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF-OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
examples/regexp-grid/Main.hs view
@@ -1,4 +1,4 @@-module Main where+module Main (main) where import Control.Monad import Data.List (intersperse)
examples/regexp-grid/RegexpGrid/Problem.hs view
@@ -6,16 +6,14 @@ module RegexpGrid.Problem (problem) where import Prelude hiding ((&&), (||), not, and, or, all, any)-import qualified Prelude as P import Control.Applicative import Control.Monad.Reader-import Control.Monad.State+import Control.Monad.RWS.Strict import Control.Lens import Data.Foldable (asum) import Data.Map (Map) import qualified Data.Map as Map-import Data.Monoid import Data.Sequence (Seq) import qualified Data.Sequence as Seq import Ersatz@@ -23,7 +21,7 @@ import RegexpGrid.Regexp import RegexpGrid.Types -type ReBit = StateT ReBitState []+type ReBit = RWST () ReBitResult ReBitState [] -- | The state threaded through 'reBit'. data ReBitState = ReBitState@@ -32,7 +30,6 @@ , _rbsGroups :: Map Integer (Seq Field) -- ^ The groups captured so far. } deriving Show-makeLenses ''ReBitState -- | The result value of 'reBit'. data ReBitResult = ReBitResult@@ -40,6 +37,8 @@ , _rbrResultBit :: Bit -- ^ The accumulated result 'Bit'. } deriving Show++makeLenses ''ReBitState makeLenses ''ReBitResult instance Monoid ReBitResult where@@ -112,53 +111,56 @@ lift . assert $ runReBit regexp fields runReBit :: Regexp -> Seq Field -> Bit-runReBit regexp fields = or (evalStateT go (ReBitState fields 0 Map.empty))+runReBit regexp fields =+ or (evalRWST go () initState ^.. folded . _2 . rbrResultBit) where- go = view rbrResultBit <$> reBit regexp <* endOfFields+ initState = ReBitState fields 0 Map.empty++ go = reBit regexp <* endOfFields -- Make sure all the fields have been consumed. endOfFields = guard . Seq.null =<< use rbsFields -reBit :: Regexp -> ReBit ReBitResult+reBit :: Regexp -> ReBit () -- The end of the regexp. Nothing to do.-reBit Nil = pure mempty+reBit Nil = return () -- Any character. Advance a field, assert just true.-reBit (AnyCharacter next) =- mappend <$> withNextField (const true)- <*> reBit next+reBit (AnyCharacter next) = do+ withNextField $ const true+ reBit next -- The character c. Advance a field and assert that it matches c.-reBit (Character c next) =- mappend <$> withNextField (\f -> f === encode c)- <*> reBit next+reBit (Character c next) = do+ withNextField $ \f -> f === encode c+ reBit next -- The character group cs. Advance a field and assert that it matches any one -- of cs.-reBit (Accept cs next) =- mappend <$> withNextField (\f -> any (\c -> f === encode c) cs)- <*> reBit next+reBit (Accept cs next) = do+ withNextField $ \f -> any (\c -> f === encode c) cs+ reBit next -- The character group ^cs. Advance a field and assert that it does not match -- any of cs.-reBit (Reject cs next) =- mappend <$> withNextField (\f -> all (\c -> f /== encode c) cs)- <*> reBit next+reBit (Reject cs next) = do+ withNextField $ \f -> all (\c -> f /== encode c) cs+ reBit next -- A choice of regexps. The 'Alternative' sum of all of them.-reBit (Choice res next) =- mappend <$> asum (map reBit res)- <*> reBit next+reBit (Choice res next) = do+ asum (map reBit res)+ reBit next -- Capture a group. reBit (Group re' next) = do- groupResult <- reBit re'+ ((), groupResult) <- listen (reBit re') -- Allocate a new group ID and add the group to the group map. gid <- rbsLastGroup <+= 1 rbsGroups . at gid ?= (groupResult ^. rbrCurrentGroup) - mappend groupResult <$> reBit next+ reBit next -- Repetition {_,0}: Just skip to the next part of the regexp. reBit (Repeat _ (Just 0) _ next) =@@ -172,9 +174,9 @@ -- Repetition {i,j} where i > 0 and j > 0: At least one instance followed by -- {i−1,j−1}.-reBit (Repeat i mj re' next) =- mappend <$> reBit re'- <*> reBit (Repeat (i-1) (subtract 1 <$> mj) re' next)+reBit (Repeat i mj re' next) = do+ reBit re'+ reBit (Repeat (i-1) (subtract 1 <$> mj) re' next) -- Backreference. reBit (Backreference n next) = do@@ -183,14 +185,14 @@ -- Advance an equivalent number of fields. fields <- traverse (const nextField) refFields -- Assert that the field sequences match each other.- let this = ReBitResult fields $ and (Seq.zipWith (===) refFields fields)- mappend this <$> reBit next+ tell $ ReBitResult fields (and (Seq.zipWith (===) refFields fields))+ reBit next -- Advance a field and build a Bit based on it.-withNextField :: (Field -> Bit) -> ReBit ReBitResult+withNextField :: (Field -> Bit) -> ReBit () withNextField func = do f <- nextField- return $ ReBitResult (Seq.singleton f) (func f)+ tell $ ReBitResult (Seq.singleton f) (func f) -- Advance a field. nextField :: ReBit Field
examples/regexp-grid/RegexpGrid/Types.hs view
@@ -30,7 +30,7 @@ -- 5 bits are enough for A–Z. (The subset of the alphabet used by the regexps -- also requires 5 bits. For simplicity, just use the full alphabet.)-data Field = Field Bit5+newtype Field = Field Bit5 deriving (Show, Typeable, Generic) instance Boolean Field
− examples/regexp-grid/Setup.hs
@@ -1,2 +0,0 @@-import Distribution.Simple-main = defaultMain
− examples/regexp-grid/regexp-grid.cabal
@@ -1,22 +0,0 @@-name: regexp-grid-version: 0.1-license-file: COPYING-author: Johan Kiviniemi-maintainer: Johan Kiviniemi <devel@johan.kiviniemi.name>-copyright: © 2013 Johan Kiviniemi-build-type: Simple-cabal-version: >= 1.8-synopsis: A solver for the regular expression crossword problem-description:- An example program that solves the regular expression crossword problem- <http://www.coinheist.com/rubik/a_regular_crossword/> using Ersatz.--executable regexp-grid- main-is: Main.hs- build-depends: base == 4.6.*- , containers == 0.5.*- , ersatz == 0.2.*- , lens == 3.8.*- , mtl == 2.1.*- , parsec == 3.1.*- ghc-options: -Wall
+ examples/sudoku/Main.hs view
@@ -0,0 +1,64 @@+module Main (main) where++import Prelude hiding ((&&), (||), not, and, or, all, any)++import Control.Applicative+import Control.Monad+import Data.Array (Array, (!))+import qualified Data.Array as Array+import Data.List+import Data.Word+import Ersatz++import Sudoku.Problem++main :: IO ()+main = do+ putStrLn "Problem:"+ putStr (render initValues)++ putStrLn "Solution:"+ (res, msol) <- solveWith cryptominisat (problem initValues)+ when (res /= Satisfied) (fail (show res))+ case msol of+ Just sol -> putStr (render sol)+ _ -> fail ("sol was " ++ show msol)++initValues :: Array (Word8,Word8) Word8+initValues =+ -- From https://en.wikipedia.org/w/index.php?title=Sudoku&oldid=543290082+ Array.listArray range+ [ 5, 3, 0, 0, 7, 0, 0, 0, 0+ , 6, 0, 0, 1, 9, 5, 0, 0, 0+ , 0, 9, 8, 0, 0, 0, 0, 6, 0+ , 8, 0, 0, 0, 6, 0, 0, 0, 3+ , 4, 0, 0, 8, 0, 3, 0, 0, 1+ , 7, 0, 0, 0, 2, 0, 0, 0, 6+ , 0, 6, 0, 0, 0, 0, 2, 8, 0+ , 0, 0, 0, 4, 1, 9, 0, 0, 5+ , 0, 0, 0, 0, 8, 0, 0, 7, 9+ ]++render :: Array (Word8,Word8) Word8 -> String+render sol = unlines . renderGroups top divider bottom+ $ map (renderLine sol) [0..8]+ where+ top = bar "┌" "───────" "┬" "┐"+ divider = bar "├" "───────" "┼" "┤"+ bottom = bar "└" "───────" "┴" "┘"++ bar begin fill middle end =+ begin ++ intercalate middle (replicate 3 fill) ++ end++renderLine :: Array (Word8,Word8) Word8 -> Word8 -> String+renderLine sol y = unwords . renderGroups "│" "│" "│"+ $ map (\x -> showN (sol ! (y,x))) [0..8]+ where+ showN n | 1 <= n && n <= 9 = show n+ | otherwise = " "++renderGroups :: a -> a -> a -> [a] -> [a]+renderGroups begin middle end values =+ [begin] ++ intercalate [middle] (chunks 3 values) ++ [end]+ where+ chunks n = unfoldr $ \xs -> splitAt n xs <$ guard (not (null xs))
+ examples/sudoku/Sudoku/Cell.hs view
@@ -0,0 +1,28 @@+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DeriveDataTypeable #-}++module Sudoku.Cell (Cell(..)) where++import Prelude hiding ((&&), (||), not, and, or, all, any)++import Data.Typeable (Typeable)+import Data.Word+import Ersatz+import GHC.Generics++newtype Cell = Cell Bit4+ deriving (Show, Typeable, Generic)++instance Boolean Cell+instance Variable Cell+instance Equatable Cell++instance Decoding Cell where+ type Decoded Cell = Word8+ decode s (Cell b) = decode s b++instance Encoding Cell where+ type Encoded Cell = Word8+ encode n | 1 <= n && n <= 9 = Cell (encode n)+ | otherwise = error ("Cell encode: invalid value " ++ show n)
+ examples/sudoku/Sudoku/Problem.hs view
@@ -0,0 +1,84 @@+module Sudoku.Problem (problem, range) where++import Prelude hiding ((&&), (||), not, and, or, all, any)++import Control.Applicative+import Control.Monad.Reader+import Control.Monad.State+import Data.Array (Array, (!))+import qualified Data.Array as Array+import Data.Word+import Ersatz++import Sudoku.Cell++type Index = (Word8,Word8)++type Grid = Array Index Cell++data Env = Env { envCellArray :: Grid -- ^ The puzzle.+ , envValues :: [Cell] -- ^ The possible values for any cell.+ }+ deriving Show++problem :: (Applicative m, MonadState s m, HasSAT s)+ => Array Index Word8 -> m Grid+problem initValues = do+ cellArray <- Array.listArray range+ <$> replicateM (Array.rangeSize range) exists++ runReaderT problem' $ Env cellArray (map encode [1..9])++ -- Assert all initial values.+ forM_ (Array.assocs initValues) $ \(idx, val) ->+ when (1 <= val && val <= 9) $+ assert $ (cellArray ! idx) === encode val++ return cellArray++problem' :: (MonadState s m, HasSAT s) => ReaderT Env m ()+problem' = do+ legalValues+ mapM_ allDifferent (subsquares ++ horizontal ++ vertical)++-- | Assert that each cell must have one of the legal values.+legalValues :: (MonadState s m, HasSAT s) => ReaderT Env m ()+legalValues = mapM_ legalValue . Array.elems =<< asks envCellArray+ where+ legalValue cell = do+ values <- asks envValues+ assert $ any (cell ===) values++-- | Assert that each cell in a group must have a different value.+allDifferent :: (MonadState s m, HasSAT s)+ => [(Word8,Word8)] -> ReaderT Env m ()+allDifferent indices = do+ cellArray <- asks envCellArray+ let pairs = [ (cellArray ! a, cellArray ! b)+ | a <- indices, b <- indices, a /= b+ ]+ forM_ pairs $ \(cellA, cellB) -> assert (cellA /== cellB)++-- | The valid index range for the grid.+range :: (Index,Index)+range = ((0,0),(8,8))++subsquares, horizontal, vertical :: [[Index]]++-- | The index group for each subsquare.+subsquares = do+ sqY <- [0..2]+ sqX <- [0..2]+ let top = 3*sqY+ left = 3*sqX+ return [ (y,x) | y <- [top..top+2], x <- [left..left+2] ]++-- | The index group for each line.+horizontal = do+ line <- [0..8]+ return [ (line,x) | x <- [0..8] ]++-- | The index group for each column.+vertical = do+ column <- [0..8]+ return [ (y,column) | y <- [0..8] ]
+ notes/SPOILER.html view
@@ -0,0 +1,15 @@+<html><head><title>Spoiler for regexp-grid</title></head><body><pre>+ N H P E H A S+ D I O M O M T H+ F O X N X A X P H+ M M O M M M M R H H+ M C X N M M C R X E M+ C M C C C C M M M M M M+H R X R C M I I I H X L S+ O R E O R E O R E O R E+ V C X C C H H M X C C+ R R R R H H H R R U+ N C X D X E X L E+ R R D D M M M M+ G C C H H C C+</pre></body></html>
+ notes/grid.pdf view
binary file changed (absent → 21661 bytes)
src/Ersatz.hs view
@@ -1,6 +1,6 @@ -------------------------------------------------------------------- -- |--- Copyright : (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013+-- Copyright : © Edward Kmett 2010-2013, Johan Kiviniemi 2013 -- License : BSD3 -- Maintainer: Edward Kmett <ekmett@gmail.com> -- Stability : experimental
src/Ersatz/Bit.hs view
@@ -7,11 +7,11 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE UndecidableInstances #-}-+{-# LANGUAGE Trustworthy #-} {-# OPTIONS_HADDOCK not-home #-} -------------------------------------------------------------------- -- |--- Copyright : (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013+-- Copyright : © Edward Kmett 2010-2013, Johan Kiviniemi 2013 -- License : BSD3 -- Maintainer: Edward Kmett <ekmett@gmail.com> -- Stability : experimental@@ -31,12 +31,11 @@ import Control.Monad.State import Data.Foldable (Foldable, toList) import qualified Data.Foldable as Foldable-import Data.Sequence ((<|), (|>), (><))+import Data.Sequence (Seq, (<|), (|>), (><)) import qualified Data.Sequence as Seq import Data.Typeable import Ersatz.Decoding import Ersatz.Encoding-import Ersatz.Internal.Circuit import Ersatz.Internal.Formula import Ersatz.Internal.Literal import Ersatz.Internal.StableName@@ -54,66 +53,76 @@ -- | A 'Bit' provides a reference to a possibly indeterminate boolean -- value that can be determined by an external SAT solver.-newtype Bit = Bit (Circuit Bit)+data Bit+ = And (Seq Bit)+ | Or (Seq Bit)+ | Xor Bit Bit+ | Mux Bit Bit Bit+ | Not Bit+ | Var !Literal deriving (Show, Typeable) instance Boolean Bit where -- improve the stablemap this way bool True = true bool False = false- true = Bit (Var literalTrue)- false = Bit (Var literalFalse)+ true = Var literalTrue+ false = Var literalFalse - a@(Bit (Var (Literal (-1)))) && _ = a- _ && b@(Bit (Var (Literal (-1)))) = b- a && Bit (Var (Literal 1)) = a- Bit (Var (Literal 1)) && b = b- Bit (And as) && Bit (And bs) = Bit (And (as >< bs))- Bit (And as) && b = Bit (And (as |> b))- a && Bit (And bs) = Bit (And (a <| bs))- a && b = Bit (And (a <| b <| Seq.empty))+ a@(Var (Literal (-1))) && _ = a+ _ && b@(Var (Literal (-1))) = b+ a && Var (Literal 1) = a+ Var (Literal 1) && b = b+ And as && And bs = And (as >< bs)+ And as && b = And (as |> b)+ a && And bs = And (a <| bs)+ a && b = And (a <| b <| Seq.empty) - a || Bit (Var (Literal (-1))) = a- Bit (Var (Literal (-1))) || b = b- a@(Bit (Var (Literal 1))) || _ = a- _ || b@(Bit (Var (Literal 1))) = b- Bit (Or as) || Bit (Or bs) = Bit (Or (as >< bs))- Bit (Or as) || b = Bit (Or (as |> b))- a || Bit (Or bs) = Bit (Or (a <| bs))- a || b = Bit (Or (a <| b <| Seq.empty))+ a || Var (Literal (-1)) = a+ Var (Literal (-1)) || b = b - not (Bit (Not c)) = c- not (Bit (Var l)) = Bit (Var (negateLiteral l))- not c = Bit (Not c)+ a@(Var (Literal 1)) || _ = a+ _ || b@(Var (Literal 1)) = b - a `xor` Bit (Var (Literal (-1))) = a- Bit (Var (Literal (-1))) `xor` b = b- a `xor` Bit (Var (Literal 1)) = not a- Bit (Var (Literal 1)) `xor` b = not b- a `xor` b = Bit (Xor a b)+ Or as || Or bs = Or (as >< bs)+ Or as || b = Or (as |> b)+ a || Or bs = Or (a <| bs)+ a || b = Or (a <| b <| Seq.empty) + not (Not c) = c+ not (Var l) = Var (negateLiteral l)+ not c = Not c++ a `xor` Var (Literal (-1)) = a+ Var (Literal (-1)) `xor` b = b+ a `xor` Var (Literal 1) = not a+ Var (Literal 1) `xor` b = not b+ a `xor` b = Xor a b+ and = Foldable.foldl' (&&) true or = Foldable.foldl' (||) false all p = Foldable.foldl' (\res b -> res && p b) true any p = Foldable.foldl' (\res b -> res || p b) false - choose f _ (Bit (Var (Literal (-1)))) = f- choose _ t (Bit (Var (Literal 1))) = t- choose f t s = Bit (Mux f t s)+ choose f _ (Var (Literal (-1))) = f+ choose _ t (Var (Literal 1)) = t+ choose f t s = Mux f t s instance Variable Bit where- exists = liftM (Bit . Var) exists- forall = liftM (Bit . Var) forall+ exists = liftM Var exists+#ifndef HLINT+ forall = liftM Var forall+#endif -- a Bit you don't assert is actually a boolean function that you can evaluate later after compilation instance Decoding Bit where type Decoded Bit = Bool- decode sol b@(Bit c) + decode sol b = solutionStableName sol (unsafePerformIO (makeStableName' b)) -- The StableName didn’t have an associated literal with a solution, -- recurse to compute the value.- <|> case c of+ <|> case b of And cs -> andMaybeBools . toList $ decode sol <$> cs Or cs -> orMaybeBools . toList $ decode sol <$> cs Xor x y -> xor <$> decode sol x <*> decode sol y@@ -158,10 +167,10 @@ -- | Convert a 'Bit' to a 'Literal'. runBit :: (MonadState s m, HasSAT s) => Bit -> m Literal-runBit (Bit (Not c)) = negateLiteral `liftM` runBit c-runBit (Bit (Var l)) = return l-runBit b@(Bit c) = generateLiteral b $ \out ->- assertFormula =<< case c of+runBit (Not c) = negateLiteral `liftM` runBit c+runBit (Var l) = return l+runBit b = generateLiteral b $ \out ->+ assertFormula =<< case b of And bs -> formulaAnd out `liftM` mapM runBit (toList bs) Or bs -> formulaOr out `liftM` mapM runBit (toList bs) Xor x y -> liftM2 (formulaXor out) (runBit x) (runBit y)
src/Ersatz/Bits.hs view
@@ -1,9 +1,10 @@ {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE Safe #-} -------------------------------------------------------------------- -- |--- Copyright : (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013+-- Copyright : © Edward Kmett 2010-2013, Johan Kiviniemi 2013 -- License : BSD3 -- Maintainer: Edward Kmett <ekmett@gmail.com> -- Stability : experimental@@ -31,19 +32,19 @@ -- | A container of 1 'Bit' that 'encode's from and 'decode's to 'Word8' newtype Bit1 = Bit1 Bit deriving (Show,Typeable,Generic) -- | A container of 2 'Bit's that 'encode's from and 'decode's to 'Word8'-data Bit2 = Bit2 Bit Bit deriving (Show,Typeable,Generic)+data Bit2 = Bit2 !Bit !Bit deriving (Show,Typeable,Generic) -- | A container of 3 'Bit's that 'encode's from and 'decode's to 'Word8'-data Bit3 = Bit3 Bit Bit Bit deriving (Show,Typeable,Generic)+data Bit3 = Bit3 !Bit !Bit !Bit deriving (Show,Typeable,Generic) -- | A container of 4 'Bit's that 'encode's from and 'decode's to 'Word8'-data Bit4 = Bit4 Bit Bit Bit Bit deriving (Show,Typeable,Generic)+data Bit4 = Bit4 !Bit !Bit !Bit !Bit deriving (Show,Typeable,Generic) -- | A container of 5 'Bit's that 'encode's from and 'decode's to 'Word8'-data Bit5 = Bit5 Bit Bit Bit Bit Bit deriving (Show,Typeable,Generic)+data Bit5 = Bit5 !Bit !Bit !Bit !Bit !Bit deriving (Show,Typeable,Generic) -- | A container of 6 'Bit's that 'encode's from and 'decode's to 'Word8'-data Bit6 = Bit6 Bit Bit Bit Bit Bit Bit deriving (Show,Typeable,Generic)+data Bit6 = Bit6 !Bit !Bit !Bit !Bit !Bit !Bit deriving (Show,Typeable,Generic) -- | A container of 7 'Bit's that 'encode's from and 'decode's to 'Word8'-data Bit7 = Bit7 Bit Bit Bit Bit Bit Bit Bit deriving (Show,Typeable,Generic)+data Bit7 = Bit7 !Bit !Bit !Bit !Bit !Bit !Bit !Bit deriving (Show,Typeable,Generic) -- | A container of 8 'Bit's that 'encode's from and 'decode's to 'Word8'-data Bit8 = Bit8 Bit Bit Bit Bit Bit Bit Bit Bit deriving (Show,Typeable,Generic)+data Bit8 = Bit8 !Bit !Bit !Bit !Bit !Bit !Bit !Bit !Bit deriving (Show,Typeable,Generic) instance Boolean Bit1 instance Boolean Bit2
src/Ersatz/Decoding.hs view
@@ -1,8 +1,9 @@ {-# LANGUAGE Rank2Types #-} {-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE Safe #-} -------------------------------------------------------------------- -- |--- Copyright : (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013+-- Copyright : © Edward Kmett 2010-2013, Johan Kiviniemi 2013 -- License : BSD3 -- Maintainer: Edward Kmett <ekmett@gmail.com> -- Stability : experimental
src/Ersatz/Encoding.hs view
@@ -2,7 +2,7 @@ {-# LANGUAGE TypeFamilies #-} -------------------------------------------------------------------- -- |--- Copyright : (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013+-- Copyright : © Edward Kmett 2010-2013, Johan Kiviniemi 2013 -- License : BSD3 -- Maintainer: Edward Kmett <ekmett@gmail.com> -- Stability : experimental
src/Ersatz/Equatable.hs view
@@ -7,11 +7,12 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE Safe #-} {-# OPTIONS_HADDOCK not-home #-} -------------------------------------------------------------------- -- |--- Copyright : (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013+-- Copyright : © Edward Kmett 2010-2013, Johan Kiviniemi 2013 -- License : BSD3 -- Maintainer: Edward Kmett <ekmett@gmail.com> -- Stability : experimental
− src/Ersatz/Internal/Circuit.hs
@@ -1,56 +0,0 @@-{-# LANGUAGE DeriveDataTypeable #-}------------------------------------------------------------------------ |--- Copyright : (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013--- License : BSD3--- Maintainer: Edward Kmett <ekmett@gmail.com>--- Stability : experimental--- Portability: non-portable-------------------------------------------------------------------------module Ersatz.Internal.Circuit- ( Circuit(..)- ) where--import Control.Applicative-import Data.Foldable (Foldable, foldMap)-import Data.Monoid-import Data.Sequence (Seq)-import Data.Traversable (Traversable, traverse)-import Data.Typeable-import Ersatz.Internal.Literal---- | This is used to observe the directed graph with sharing of how multiple--- 'Ersatz.Bit.Bit' values are related.-data Circuit c- = And (Seq c)- | Or (Seq c)- | Xor c c- | Mux c c c -- ^ False branch, true branch, predicate/selector branch- | Not c- | Var !Literal- deriving (Show, Typeable)--instance Functor Circuit where- fmap f (And as) = And (fmap f as)- fmap f (Or as) = Or (fmap f as)- fmap f (Xor a b) = Xor (f a) (f b)- fmap f (Mux a b c) = Mux (f a) (f b) (f c)- fmap f (Not a) = Not (f a)- fmap _ (Var l) = Var l--instance Foldable Circuit where- foldMap f (And as) = foldMap f as- foldMap f (Or as) = foldMap f as- foldMap f (Xor a b) = f a <> f b- foldMap f (Mux a b c) = f a <> f b <> f c- foldMap f (Not a) = f a- foldMap _ Var{} = mempty--instance Traversable Circuit where- traverse f (And as) = And <$> traverse f as- traverse f (Or as) = Or <$> traverse f as- traverse f (Xor a b) = Xor <$> f a <*> f b- traverse f (Mux a b c) = Mux <$> f a <*> f b <*> f c- traverse f (Not a) = Not <$> f a- traverse _ (Var l) = pure (Var l)
src/Ersatz/Internal/Formula.hs view
@@ -6,11 +6,12 @@ {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE Trustworthy #-} {-# OPTIONS_HADDOCK not-home #-} -------------------------------------------------------------------- -- |--- Copyright : (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013+-- Copyright : © Edward Kmett 2010-2013, Johan Kiviniemi 2013 -- License : BSD3 -- Maintainer: Edward Kmett <ekmett@gmail.com> -- Stability : experimental
src/Ersatz/Internal/Literal.hs view
@@ -1,7 +1,8 @@ {-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE Trustworthy #-} -------------------------------------------------------------------- -- |--- Copyright : (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013+-- Copyright : © Edward Kmett 2010-2013, Johan Kiviniemi 2013 -- License : BSD3 -- Maintainer: Edward Kmett <ekmett@gmail.com> -- Stability : experimental
src/Ersatz/Internal/Parser.hs view
@@ -1,6 +1,6 @@ -------------------------------------------------------------------- -- |--- Copyright : (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013+-- Copyright : © Edward Kmett 2010-2013, Johan Kiviniemi 2013 -- License : BSD3 -- Maintainer: Edward Kmett <ekmett@gmail.com> -- Stability : experimental
src/Ersatz/Internal/StableName.hs view
@@ -1,7 +1,7 @@ {-# OPTIONS_HADDOCK not-home #-} -------------------------------------------------------------------- -- |--- Copyright : (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013+-- Copyright : © Edward Kmett 2010-2013, Johan Kiviniemi 2013 -- License : BSD3 -- Maintainer: Edward Kmett <ekmett@gmail.com> -- Stability : experimental
src/Ersatz/Problem.hs view
@@ -11,11 +11,12 @@ {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE Trustworthy #-} {-# OPTIONS_HADDOCK not-home #-} -------------------------------------------------------------------- -- |--- Copyright : (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013+-- Copyright : © Edward Kmett 2010-2013, Johan Kiviniemi 2013 -- License : BSD3 -- Maintainer: Edward Kmett <ekmett@gmail.com> -- Stability : experimental
src/Ersatz/Solution.hs view
@@ -1,9 +1,10 @@ {-# LANGUAGE Rank2Types #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE ImpredicativeTypes #-}+{-# LANGUAGE Trustworthy #-} -- Safe if lens is Safe -------------------------------------------------------------------- -- |--- Copyright : (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013+-- Copyright : © Edward Kmett 2010-2013, Johan Kiviniemi 2013 -- License : BSD3 -- Maintainer: Edward Kmett <ekmett@gmail.com> -- Stability : experimental
src/Ersatz/Solver.hs view
@@ -1,6 +1,6 @@ -------------------------------------------------------------------- -- |--- Copyright : (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013+-- Copyright : © Edward Kmett 2010-2013, Johan Kiviniemi 2013 -- License : BSD3 -- Maintainer: Edward Kmett <ekmett@gmail.com> -- Stability : experimental
src/Ersatz/Solver/Common.hs view
@@ -1,6 +1,6 @@ -------------------------------------------------------------------- -- |--- Copyright : (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013+-- Copyright : © Edward Kmett 2010-2013, Johan Kiviniemi 2013 -- License : BSD3 -- Maintainer: Edward Kmett <ekmett@gmail.com> -- Stability : experimental
src/Ersatz/Solver/DepQBF.hs view
@@ -1,6 +1,7 @@+{-# LANGUAGE Trustworthy #-} -------------------------------------------------------------------- -- |--- Copyright : (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013+-- Copyright : © Edward Kmett 2010-2013, Johan Kiviniemi 2013 -- License : BSD3 -- Maintainer: Edward Kmett <ekmett@gmail.com> -- Stability : experimental@@ -12,7 +13,7 @@ , depqbfPath ) where -import Blaze.ByteString.Builder+import Blaze.ByteString.Builder -- not Trustworthy import Control.Monad.IO.Class import qualified Data.ByteString as BS import Ersatz.Problem
src/Ersatz/Solver/Minisat.hs view
@@ -1,6 +1,7 @@+{-# LANGUAGE Trustworthy #-} -------------------------------------------------------------------- -- |--- Copyright : (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013+-- Copyright : © Edward Kmett 2010-2013, Johan Kiviniemi 2013 -- License : BSD3 -- Maintainer: Edward Kmett <ekmett@gmail.com> -- Stability : experimental@@ -13,7 +14,7 @@ , minisatPath ) where -import Blaze.ByteString.Builder+import Blaze.ByteString.Builder -- not Trustworthy import Control.Applicative import Control.Exception (IOException, handle) import Control.Monad
src/Ersatz/Variable.hs view
@@ -5,7 +5,7 @@ {-# LANGUAGE UndecidableInstances #-} -------------------------------------------------------------------- -- |--- Copyright : (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013+-- Copyright : © Edward Kmett 2010-2013, Johan Kiviniemi 2013 -- License : BSD3 -- Maintainer: Edward Kmett <ekmett@gmail.com> -- Stability : experimental@@ -36,7 +36,9 @@ instance Variable a => GVariable (K1 i a) where gexists = liftM K1 exists+#ifndef HLINT gforall = liftM K1 forall+#endif instance GVariable f => GVariable (M1 i c f) where gexists = liftM M1 gexists@@ -46,7 +48,9 @@ -- for any type that is an instance of 'Generic'. class Variable t where exists :: (MonadState s m, HasSAT s) => m t+#ifndef HLINT forall :: (MonadState s m, HasQSAT s) => m t+#endif #ifndef HLINT default exists :: (MonadState s m, HasSAT s, Generic t, GVariable (Rep t)) => m t@@ -58,7 +62,9 @@ instance Variable Literal where exists = literalExists+#ifndef HLINT forall = literalForall+#endif instance (Variable a, Variable b) => Variable (a,b) instance (Variable a, Variable b, Variable c) => Variable (a,b,c)
tests/doctests.hsc view
@@ -3,7 +3,7 @@ ----------------------------------------------------------------------------- -- | -- Module : Main (doctests)--- Copyright : (C) 2012-13 Edward Kmett+-- Copyright : © 2012-2013 Edward Kmett -- License : BSD-style (see the file LICENSE) -- Maintainer : Edward Kmett <ekmett@gmail.com> -- Stability : provisional