ersatz-toysat (empty) → 0.2.0.0
raw patch · 14 files changed
+810/−0 lines, 14 filesdep +arraydep +basedep +containerssetup-changed
Dependencies added: array, base, containers, ersatz, ersatz-toysat, ghc-prim, lens, mtl, parsec, toysolver, transformers
Files
- .travis.yml +64/−0
- LICENSE +30/−0
- README.md +11/−0
- Setup.hs +2/−0
- ersatz-toysat.cabal +83/−0
- examples/LICENSE +39/−0
- examples/regexp-grid/Main.hs +38/−0
- examples/regexp-grid/RegexpGrid/Problem.hs +203/−0
- examples/regexp-grid/RegexpGrid/Regexp.hs +79/−0
- examples/regexp-grid/RegexpGrid/Types.hs +50/−0
- examples/sudoku/Main.hs +65/−0
- examples/sudoku/Sudoku/Cell.hs +28/−0
- examples/sudoku/Sudoku/Problem.hs +84/−0
- src/Ersatz/Solver/Toysat.hs +34/−0
+ .travis.yml view
@@ -0,0 +1,64 @@+# NB: don't set `language: haskell` here++# The following enables several GHC versions to be tested; often it's enough to test only against the last release in a major GHC version. Feel free to omit lines listings versions you don't need/want testing for.+env:+# - CABALVER=1.16 GHCVER=6.12.3+# - CABALVER=1.16 GHCVER=7.0.1+# - CABALVER=1.16 GHCVER=7.0.2+# - CABALVER=1.16 GHCVER=7.0.3+# - CABALVER=1.16 GHCVER=7.0.4+# - CABALVER=1.16 GHCVER=7.2.1+# - CABALVER=1.16 GHCVER=7.2.2+# - CABALVER=1.16 GHCVER=7.4.1+ - CABALVER=1.16 GHCVER=7.4.2+# - CABALVER=1.16 GHCVER=7.6.1+# - CABALVER=1.16 GHCVER=7.6.2+ - CABALVER=1.18 GHCVER=7.6.3+# - CABALVER=1.18 GHCVER=7.8.1 # see note about Alex/Happy for GHC >= 7.8+# - CABALVER=1.18 GHCVER=7.8.2+ - CABALVER=1.18 GHCVER=7.8.3+ - CABALVER=1.22 GHCVER=7.10.1+# - CABALVER=head GHCVER=head # see section about GHC HEAD snapshots++matrix:+ allow_failures:+ - env: CABALVER=1.22 GHCVER=7.10.1++# Note: the distinction between `before_install` and `install` is not important.+before_install:+ - travis_retry sudo add-apt-repository -y ppa:hvr/ghc+ - travis_retry sudo apt-get update+ - travis_retry sudo apt-get install cabal-install-$CABALVER ghc-$GHCVER # see note about happy/alex+ - export PATH=/opt/ghc/$GHCVER/bin:/opt/cabal/$CABALVER/bin:$PATH+ - |+ if [ $GHCVER = "head" ] || [ ${GHCVER%.*} = "7.8" ] || [ ${GHCVER%.*} = "7.10" ]; then+ travis_retry sudo apt-get install happy-1.19.4 alex-3.1.3+ export PATH=/opt/alex/3.1.3/bin:/opt/happy/1.19.4/bin:$PATH+ else+ travis_retry sudo apt-get install happy alex+ fi++install:+ - cabal --version+ - echo "$(ghc --version) [$(ghc --print-project-git-commit-id 2> /dev/null || echo '?')]"+ - travis_retry cabal update+ - cabal install --only-dependencies -fexamples --enable-tests --enable-benchmarks++# Here starts the actual work to be performed for the package under test; any command which exits with a non-zero exit code causes the build to fail.+script:+ - if [ -f configure.ac ]; then autoreconf -i; fi+ - cabal configure -fexamples --enable-tests --enable-benchmarks -v2 # -v2 provides useful information for debugging+ - cabal build # this builds all libraries and executables (including tests/benchmarks)+ - cabal test+ - cabal check+ - cabal sdist # tests that a source-distribution can be generated++# The following scriptlet checks that the resulting source distribution can be built & installed+ - export SRC_TGZ=$(cabal info . | awk '{print $2 ".tar.gz";exit}') ;+ cd dist/;+ if [ -f "$SRC_TGZ" ]; then+ cabal install --force-reinstalls "$SRC_TGZ";+ else+ echo "expected '$SRC_TGZ' not found";+ exit 1;+ fi
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2015, Masahiro Sakai++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * Redistributions in binary form must reproduce the above+ copyright notice, this list of conditions and the following+ disclaimer in the documentation and/or other materials provided+ with the distribution.++ * Neither the name of Masahiro Sakai nor the names of other+ contributors may be used to endorse or promote products derived+ from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+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.
+ README.md view
@@ -0,0 +1,11 @@+ersatz-toysat+=============++[](http://travis-ci.org/msakai/ersatz-toysat)++toysat driver as backend for ersatz++Examples+--------++The contents of `examples/` directory are copied from ersatz package and modified to use the toysat driver as backend.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ ersatz-toysat.cabal view
@@ -0,0 +1,83 @@+-- Initial ersatz-toysat.cabal generated by cabal init. For further documentation, see+-- http://haskell.org/cabal/users-guide/++name: ersatz-toysat+version: 0.2.0.0+synopsis: toysat driver as backend for ersatz+description: toysat driver as backend for ersatz+homepage: https://github.com/msakai/ersatz-toysat+license: BSD3+license-file: LICENSE+author: Masahiro Sakai+maintainer: masahiro.sakai@gmail.com+copyright: (c) 2014 Masahiro Sakai+category: Logic, Algorithms+build-type: Simple+extra-source-files: README.md, examples/LICENSE, .travis.yml+cabal-version: >=1.10++source-repository head+ type: git+ location: git://github.com/msakai/ersatz-toysat.git++flag examples+ description: Build examples+ default: False+ manual: True++library+ exposed-modules: Ersatz.Solver.Toysat+ build-depends:+ base >=4.5 && <4.9,+ array >= 0.4 && < 0.6,+ containers >= 0.4.2.1 && < 0.6,+ transformers == 0.3.*,+ ersatz >=0.2.6.1 && <0.3.0,+ toysolver >=0.2.0 && <0.3.0+ hs-source-dirs: src+ default-language: Haskell2010++executable ersatz-toysat-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,+ ersatz-toysat,+ lens,+ mtl,+ parsec >= 3.1 && < 3.2+ if impl(ghc >= 7.4 && < 7.6)+ build-depends: ghc-prim+ 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-toysat-sudoku+ -- description: An example program that solves a sudoku problem using Ersatz.+ if flag(examples)+ build-depends:+ array,+ base < 5,+ ersatz,+ ersatz-toysat,+ mtl+ if impl(ghc >= 7.4 && < 7.6)+ build-depends: ghc-prim+ else+ buildable: False+ default-language: Haskell2010+ main-is: Main.hs+ other-modules:+ Sudoku.Cell+ Sudoku.Problem+ ghc-options: -Wall+ hs-source-dirs: examples/sudoku
+ examples/LICENSE view
@@ -0,0 +1,39 @@+Copyright © 2010-2014 Edward Kmett+Copyright © 2013 Johan Kiviniemi++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are+met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * Redistributions in binary form must reproduce the above+ copyright notice, this list of conditions and the following+ disclaimer in the documentation and/or other materials provided+ with the distribution.++ * Neither the name of Edward Kmett nor the names of other+ contributors may be used to endorse or promote products derived+ from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+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
+ examples/regexp-grid/Main.hs view
@@ -0,0 +1,38 @@+module Main (main) where++import Control.Monad+import Data.List (intersperse)+import Data.Map (Map)+import qualified Data.Map as Map+import Ersatz+import Ersatz.Solver.Toysat++import RegexpGrid.Problem+import RegexpGrid.Types++main :: IO ()+main = do+ (res, msol) <- solveWith toysat problem+ when (res /= Satisfied) (fail (show res))+ case msol of+ Nothing -> fail "Sol was Nothing"+ Just sol ->+ mapM_ (putStrLn . ($ sol))+ [ line 6 P00 P06+ , line 5 P10 P17+ , line 4 P20 P28+ , line 3 P30 P39+ , line 2 P40 P4a+ , line 1 P50 P5b+ , line 0 P60 P6c+ , line 1 P70 P7b+ , line 2 P80 P8a+ , line 3 P90 P99+ , line 4 Pa0 Pa8+ , line 5 Pb0 Pb7+ , line 6 Pc0 Pc6+ ]++line :: Int -> Pos -> Pos -> Map Pos Char -> String+line spaces start end sol =+ replicate spaces ' ' ++ intersperse ' ' (map (sol Map.!) [start..end])
+ examples/regexp-grid/RegexpGrid/Problem.hs view
@@ -0,0 +1,203 @@+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TemplateHaskell #-}++-- | Generate an Ersatz problem definition for the regexp grid.++module RegexpGrid.Problem (problem) where++import Prelude hiding ((&&), (||), not, and, or, all, any)++import Control.Applicative+import Control.Monad.Reader+import Control.Monad.RWS.Strict+import Control.Lens+import Data.Foldable (asum)+import Data.Map (Map)+import qualified Data.Map as Map+import Data.Sequence (Seq)+import qualified Data.Sequence as Seq+import Ersatz++import RegexpGrid.Regexp+import RegexpGrid.Types++type ReBit = RWST () ReBitResult ReBitState []++-- | The state threaded through 'reBit'.+data ReBitState = ReBitState+ { _rbsFields :: Seq Field -- ^ The fields against whom to apply the regexp.+ , _rbsLastGroup :: Integer -- ^ The latest captured group.+ , _rbsGroups :: Map Integer (Seq Field) -- ^ The groups captured so far.+ }+ deriving Show++-- | The result value of 'reBit'.+data ReBitResult = ReBitResult+ { _rbrCurrentGroup :: Seq Field -- ^ The fields in the current group. Used by backreferences.+ , _rbrResultBit :: Bit -- ^ The accumulated result 'Bit'.+ }+ deriving Show++makeLenses ''ReBitState+makeLenses ''ReBitResult++instance Monoid ReBitResult where+ mempty = ReBitResult mempty true+ {-# INLINE mempty #-}+ ReBitResult fieldsA bitA `mappend` ReBitResult fieldsB bitB =+ ReBitResult (fieldsA <> fieldsB) (bitA && bitB)+ {-# INLINE mappend #-}++problem :: (Applicative m, MonadState s m, HasSAT s) => m (Map Pos Field)+problem = do+ -- Allocate a literal for each field.+ fieldMap <- Map.fromList <$> mapM (\pos -> (pos,) <$> exists) [minBound..]+ runReaderT problem' fieldMap+ return fieldMap++problem' :: (MonadState s m, HasSAT s) => ReaderT (Map Pos Field) m ()+problem' = do+ r [P00,P01,P02,P03,P04,P05,P06] ".*H.*H.*"+ r [P10,P11,P12,P13,P14,P15,P16,P17] "(DI|NS|TH|OM)*"+ r [P20,P21,P22,P23,P24,P25,P26,P27,P28] "F.*[AO].*[AO].*"+ r [P30,P31,P32,P33,P34,P35,P36,P37,P38,P39] "(O|RHH|MM)*"+ r [P40,P41,P42,P43,P44,P45,P46,P47,P48,P49,P4a] ".*"+ r [P50,P51,P52,P53,P54,P55,P56,P57,P58,P59,P5a,P5b] "C*MC(CCC|MM)*"+ r [P60,P61,P62,P63,P64,P65,P66,P67,P68,P69,P6a,P6b,P6c] "[^C]*[^R]*III.*"+ r [P70,P71,P72,P73,P74,P75,P76,P77,P78,P79,P7a,P7b] "(...?)\\1*"+ r [P80,P81,P82,P83,P84,P85,P86,P87,P88,P89,P8a] "([^X]|XCC)*"+ r [P90,P91,P92,P93,P94,P95,P96,P97,P98,P99] "(RR|HHH)*.?"+ r [Pa0,Pa1,Pa2,Pa3,Pa4,Pa5,Pa6,Pa7,Pa8] "N.*X.X.X.*E"+ r [Pb0,Pb1,Pb2,Pb3,Pb4,Pb5,Pb6,Pb7] "R*D*M*"+ r [Pc0,Pc1,Pc2,Pc3,Pc4,Pc5,Pc6] ".(C|HH)*"++ r [P00,P10,P20,P30,P40,P50,P60] "(ND|ET|IN)[^X]*"+ r [P01,P11,P21,P31,P41,P51,P61,P70] "[CHMNOR]*I[CHMNOR]*"+ r [P02,P12,P22,P32,P42,P52,P62,P71,P80] "P+(..)\\1.*"+ r [P03,P13,P23,P33,P43,P53,P63,P72,P81,P90] "(E|CR|MN)*"+ r [P04,P14,P24,P34,P44,P54,P64,P73,P82,P91,Pa0] "([^MC]|MM|CC)*"+ r [P05,P15,P25,P35,P45,P55,P65,P74,P83,P92,Pa1,Pb0] "[AM]*CM(RC)*R?"+ r [P06,P16,P26,P36,P46,P56,P66,P75,P84,P93,Pa2,Pb1,Pc0] ".*"+ r [P17,P27,P37,P47,P57,P67,P76,P85,P94,Pa3,Pb2,Pc1] ".*PRR.*DDC.*"+ r [P28,P38,P48,P58,P68,P77,P86,P95,Pa4,Pb3,Pc2] "(HHX|[^HX])*"+ r [P39,P49,P59,P69,P78,P87,P96,Pa5,Pb4,Pc3] "([^EMC]|EM)*"+ r [P4a,P5a,P6a,P79,P88,P97,Pa6,Pb5,Pc4] ".*OXR.*"+ r [P5b,P6b,P7a,P89,P98,Pa7,Pb6,Pc5] ".*LR.*RL.*"+ r [P6c,P7b,P8a,P99,Pa8,Pb7,Pc6] ".*SE.*UE.*"++ r [Pc0,Pb0,Pa0,P90,P80,P70,P60] ".*G.*V.*H.*"+ r [Pc1,Pb1,Pa1,P91,P81,P71,P61,P50] "[CR]*"+ r [Pc2,Pb2,Pa2,P92,P82,P72,P62,P51,P40] ".*XEXM*"+ r [Pc3,Pb3,Pa3,P93,P83,P73,P63,P52,P41,P30] ".*DD.*CCM.*"+ r [Pc4,Pb4,Pa4,P94,P84,P74,P64,P53,P42,P31,P20] ".*XHCR.*X.*"+ r [Pc5,Pb5,Pa5,P95,P85,P75,P65,P54,P43,P32,P21,P10] ".*(.)(.)(.)(.)\\4\\3\\2\\1.*"+ r [Pc6,Pb6,Pa6,P96,P86,P76,P66,P55,P44,P33,P22,P11,P00] ".*(IN|SE|HI)"+ r [Pb7,Pa7,P97,P87,P77,P67,P56,P45,P34,P23,P12,P01] "[^C]*MMM[^C]*"+ r [Pa8,P98,P88,P78,P68,P57,P46,P35,P24,P13,P02] ".*(.)C\\1X\\1.*"+ r [P99,P89,P79,P69,P58,P47,P36,P25,P14,P03] "[CEIMU]*OH[AEMOR]*"+ r [P8a,P7a,P6a,P59,P48,P37,P26,P15,P04] "(RX|[^R])*"+ r [P7b,P6b,P5a,P49,P38,P27,P16,P05] "[^M]*M[^M]*"+ r [P6c,P5b,P4a,P39,P28,P17,P06] "(S|MM|HHH)*"++r :: (MonadState s m, HasSAT s)+ => [Pos] -> String -> ReaderT (Map Pos Field) m ()+r poss regexpStr = do+ fieldMap <- ask+ let fields = (fieldMap Map.!) <$> Seq.fromList poss++ regexp <- either (fail . show) return+ $ parseRegexp "RegexpGrid.Problem" regexpStr++ lift . assert $ runReBit regexp fields++runReBit :: Regexp -> Seq Field -> Bit+runReBit regexp fields =+ or (evalRWST go () initState ^.. folded . _2 . rbrResultBit)+ where+ 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 ()++-- The end of the regexp. Nothing to do.+reBit Nil = return ()++-- Any character. Advance a field, assert just true.+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) = 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) = 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) = 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) = do+ asum (map reBit res)+ reBit next++-- Capture a group.+reBit (Group re' next) = do+ ((), 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)++ reBit next++-- Repetition {_,0}: Just skip to the next part of the regexp.+reBit (Repeat _ (Just 0) _ next) =+ reBit next++-- Repetition {0,_}: Branch to the alternatives:+-- • skip to the next part (zero instances)+-- • at least one instance ({1,_}).+reBit (Repeat 0 mj re' next) =+ reBit next <|> reBit (Repeat 1 mj re' next)++-- 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) = do+ reBit re'+ reBit (Repeat (i-1) (subtract 1 <$> mj) re' next)++-- Backreference.+reBit (Backreference n next) = do+ -- The fields of the group referred to.+ Just refFields <- use (rbsGroups . at n)+ -- Advance an equivalent number of fields.+ fields <- traverse (const nextField) refFields+ -- Assert that the field sequences match each other.+ tell $ ReBitResult fields (and (Seq.zipWith (===) refFields fields))+ reBit next++-- Advance a field and build a Bit based on it.+withNextField :: (Field -> Bit) -> ReBit ()+withNextField func = do+ f <- nextField+ tell $ ReBitResult (Seq.singleton f) (func f)++-- Advance a field.+nextField :: ReBit Field+nextField = do+ -- Pop the first field from the state. Fails if there are none left.+ Just (f, fs) <- preuse (rbsFields . _Cons)+ rbsFields .= fs+ return f
+ examples/regexp-grid/RegexpGrid/Regexp.hs view
@@ -0,0 +1,79 @@+-- | A parser for a subset of the regular expression syntax.++module RegexpGrid.Regexp (Regexp (..), parseRegexp) where++import Control.Applicative hiding ((<|>), many)+import Control.Monad+import Data.Char+import Text.Parsec++data Regexp = Nil+ | AnyCharacter Regexp+ | Character Char Regexp+ | Accept [Char] Regexp+ | Reject [Char] Regexp+ | Choice [Regexp] Regexp+ | Group Regexp Regexp+ | Repeat Integer (Maybe Integer) Regexp Regexp+ | Backreference Integer Regexp+ deriving Show++type REParser = Parsec String REState (Regexp -> Regexp)+type REState = Integer++parseRegexp :: SourceName -> String -> Either ParseError Regexp+parseRegexp = runParser (regexp <* eof) 0++regexp :: Parsec String REState Regexp+regexp = go <$> (items `sepBy` char '|')+ where+ go [] = Nil+ go [re] = re+ go res = Choice res Nil++items :: Parsec String REState Regexp+items = go <$> many (nonModifier >>= modifier)+ where+ go = ($ Nil) . foldr (.) id++nonModifier :: REParser+nonModifier = AnyCharacter <$ char '.'+ <|> group+ <|> characterClass+ <|> backreference+ <|> Character <$> nonSpecialChar++group :: REParser+group = Group <$> between (char '(') (char ')') go+ where+ go = modifyState (+1) *> regexp++backreference :: REParser+backreference = do+ _ <- char '\\'+ n <- fromIntegral . digitToInt <$> digit+ numGroups <- getState+ when (n == 0 || n > numGroups) $ invalid n+ return (Backreference n)+ where+ invalid n = fail ("Invalid backreference: " ++ show n)++characterClass :: REParser+characterClass = between (char '[') (char ']') go+ where+ go = Reject <$> (char '^' *> many1 nonSpecialChar)+ <|> Accept <$> many1 nonSpecialChar++nonSpecialChar :: Parsec String u Char+nonSpecialChar = noneOf "\\.[](){}|^$?*+" <?> "nonspecial"++modifier :: (Regexp -> Regexp) -> REParser+modifier re = Repeat 0 (Just 1) re' <$ char '?'+ <|> Repeat 0 Nothing re' <$ char '*'+ <|> Repeat 1 Nothing re' <$ char '+'+ <|> pure re+ where+ re' :: Regexp+ re' = re Nil++{-# ANN module "HLint: ignore Use String" #-}
+ examples/regexp-grid/RegexpGrid/Types.hs view
@@ -0,0 +1,50 @@+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DeriveDataTypeable #-}++module RegexpGrid.Types+( Pos (..)+, Field (..)+) where++import Control.Applicative+import Data.Char (chr, ord)+import Data.Typeable+import Ersatz+import GHC.Generics++data Pos = P00|P01|P02|P03|P04|P05|P06+ | P10|P11|P12|P13|P14|P15|P16|P17+ | P20|P21|P22|P23|P24|P25|P26|P27|P28+ | P30|P31|P32|P33|P34|P35|P36|P37|P38|P39+ | P40|P41|P42|P43|P44|P45|P46|P47|P48|P49|P4a+ | P50|P51|P52|P53|P54|P55|P56|P57|P58|P59|P5a|P5b+ | P60|P61|P62|P63|P64|P65|P66|P67|P68|P69|P6a|P6b|P6c+ | P70|P71|P72|P73|P74|P75|P76|P77|P78|P79|P7a|P7b+ | P80|P81|P82|P83|P84|P85|P86|P87|P88|P89|P8a+ | P90|P91|P92|P93|P94|P95|P96|P97|P98|P99+ | Pa0|Pa1|Pa2|Pa3|Pa4|Pa5|Pa6|Pa7|Pa8+ | Pb0|Pb1|Pb2|Pb3|Pb4|Pb5|Pb6|Pb7+ | Pc0|Pc1|Pc2|Pc3|Pc4|Pc5|Pc6+ deriving (Eq, Ord, Bounded, Enum, Read, Show)++-- 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.)+newtype Field = Field Bit5+ deriving (Show, Typeable, Generic)++instance Boolean Field+instance Variable Field+instance Equatable Field++instance Decoding Field where+ type Decoded Field = Char+ decode s (Field f) = chr . (+ origin) . fromIntegral <$> decode s f++instance Encoding Field where+ type Encoded Field = Char+ encode = Field . encode . fromIntegral . subtract origin . ord++-- Encode 0 as the character preceding A.+origin :: Int+origin = ord 'A' - 1
+ examples/sudoku/Main.hs view
@@ -0,0 +1,65 @@+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 Ersatz.Solver.Toysat++import Sudoku.Problem++main :: IO ()+main = do+ putStrLn "Problem:"+ putStr (render initValues)++ putStrLn "Solution:"+ (res, msol) <- solveWith toysat (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] ]
+ src/Ersatz/Solver/Toysat.hs view
@@ -0,0 +1,34 @@+{-# OPTIONS_GHC -Wall #-}+--------------------------------------------------------------------+-- |+-- Copyright : © Masahiro Sakai 2014+-- License : BSD3+-- Maintainer: Masahiro Sakai <masahiro.sakai@gmail.com>+-- Stability : experimental+-- Portability: portable+--+--------------------------------------------------------------------+module Ersatz.Solver.Toysat where++import Control.Monad+import Control.Monad.IO.Class+import Data.Array.IArray+import qualified Data.IntSet as IntSet+import qualified Data.IntMap as IntMap+import qualified Data.Set as Set+import Ersatz+import qualified ToySolver.SAT as ToySAT++toysat :: MonadIO m => Solver SAT m+toysat problem = liftIO $ do+ solver <- ToySAT.newSolver+ let nv = dimacsNumVariables problem+ ToySAT.newVars_ solver nv+ forM_ (Set.toList (dimacsClauses problem)) $ \clause -> do+ ToySAT.addClause solver (IntSet.toList clause)+ ret <- ToySAT.solve solver+ if ret then do+ model <- ToySAT.getModel solver+ return (Satisfied, IntMap.fromList (assocs model))+ else+ return (Unsatisfied, IntMap.empty)