-
Notifications
You must be signed in to change notification settings - Fork 0
/
SetGame.hs
92 lines (72 loc) · 2.53 KB
/
SetGame.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
{-# Language TypeFamilies #-}
{-# Language DeriveGeneric #-}
module Main where
import Ersatz
import Booleans
import Control.Applicative
import Control.Monad (replicateM)
import GHC.Generics
import Prelude hiding (not, all, and, (&&), (||))
data Color = Red | Green | Blue deriving (Eq, Show, Enum)
data Shape = Oval | Squiggle | Chevron deriving (Eq, Show, Enum)
data Count = One | Two | Three deriving (Eq, Show, Enum)
data Fill = Solid | Hollow | Striped deriving (Eq, Show, Enum)
data Card = Card Color Shape Count Fill deriving (Show)
------------------------------------------------------------------------
data SCard = SCard { scardColor, scardShape, scardCount, scardFill :: Fin3 }
deriving Generic
instance Variable SCard
instance Equatable SCard
instance Codec SCard where
type Decoded SCard = Card
encode (Card a b c d) = SCard (aux a) (aux b) (aux c) (aux d)
where
aux :: Enum a => a -> Fin3
aux x = encode (fromEnum x)
decode sol (SCard a b c d) =
do a' <- decode sol a
b' <- decode sol b
c' <- decode sol c
d' <- decode sol d
return (Card (toEnum a') (toEnum b') (toEnum c') (toEnum d'))
------------------------------------------------------------------------
newtype Fin3 = Fin3 Bit2
deriving Generic
instance Variable Fin3 where
literally m =
do Bit2 a b <- literally m
return (Fin3 (Bit2 a (not a && b)))
instance Equatable Fin3
instance Codec Fin3 where
type Decoded Fin3 = Int
encode 0 = Fin3 (encode 0)
encode 1 = Fin3 (encode 1)
encode 2 = Fin3 (encode 2)
encode _ = error "Fin3.encode: out of range"
decode sol (Fin3 a) = fromIntegral <$> decode sol a
------------------------------------------------------------------------
match3 :: Equatable a => a -> a -> a -> Bit
match3 x y z = same || different
where
same = x === y && y === z && x === z
different = x /== y && y /== z && x /== z
goodSet :: (SCard, SCard, SCard) -> Bit
goodSet (c1,c2,c3) =
and [aux scardColor, aux scardShape, aux scardCount, aux scardFill]
where
aux sel = match3 (sel c1) (sel c2) (sel c3)
problem :: MonadSAT s m => m [(SCard, SCard, SCard)]
problem =
do cards <- replicateM 81 exists
assert (unique cards)
let sets = threes cards
assert (all goodSet sets)
return sets
main :: IO ()
main =
do Just sets <- getModel problem
mapM_ print sets
threes :: [a] -> [(a,a,a)]
threes (x:y:z:rest) = (x,y,z) : threes rest
threes [] = []
threes _ = error "threes: Expected length to be multiple of three"