diff --git a/.travis.yml b/.travis.yml new file mode 100644 --- /dev/null +++ b/.travis.yml @@ -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 diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,11 @@ +ersatz-toysat +============= + +[![Build Status](https://secure.travis-ci.org/msakai/ersatz-toysat.png?branch=master)](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. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/ersatz-toysat.cabal b/ersatz-toysat.cabal new file mode 100644 --- /dev/null +++ b/ersatz-toysat.cabal @@ -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 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 diff --git a/examples/LICENSE b/examples/LICENSE new file mode 100644 --- /dev/null +++ b/examples/LICENSE @@ -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 diff --git a/examples/regexp-grid/Main.hs b/examples/regexp-grid/Main.hs new file mode 100644 --- /dev/null +++ b/examples/regexp-grid/Main.hs @@ -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]) diff --git a/examples/regexp-grid/RegexpGrid/Problem.hs b/examples/regexp-grid/RegexpGrid/Problem.hs new file mode 100644 --- /dev/null +++ b/examples/regexp-grid/RegexpGrid/Problem.hs @@ -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 diff --git a/examples/regexp-grid/RegexpGrid/Regexp.hs b/examples/regexp-grid/RegexpGrid/Regexp.hs new file mode 100644 --- /dev/null +++ b/examples/regexp-grid/RegexpGrid/Regexp.hs @@ -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" #-} diff --git a/examples/regexp-grid/RegexpGrid/Types.hs b/examples/regexp-grid/RegexpGrid/Types.hs new file mode 100644 --- /dev/null +++ b/examples/regexp-grid/RegexpGrid/Types.hs @@ -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 diff --git a/examples/sudoku/Main.hs b/examples/sudoku/Main.hs new file mode 100644 --- /dev/null +++ b/examples/sudoku/Main.hs @@ -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)) diff --git a/examples/sudoku/Sudoku/Cell.hs b/examples/sudoku/Sudoku/Cell.hs new file mode 100644 --- /dev/null +++ b/examples/sudoku/Sudoku/Cell.hs @@ -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) diff --git a/examples/sudoku/Sudoku/Problem.hs b/examples/sudoku/Sudoku/Problem.hs new file mode 100644 --- /dev/null +++ b/examples/sudoku/Sudoku/Problem.hs @@ -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] ] diff --git a/src/Ersatz/Solver/Toysat.hs b/src/Ersatz/Solver/Toysat.hs new file mode 100644 --- /dev/null +++ b/src/Ersatz/Solver/Toysat.hs @@ -0,0 +1,34 @@ +{-# OPTIONS_GHC -Wall #-} +-------------------------------------------------------------------- +-- | +-- Copyright : © Masahiro Sakai 2014 +-- License : BSD3 +-- Maintainer: Masahiro Sakai +-- 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)