Jukebox.Sat.Easy

Documentation

newtype Sat1 a b

Constructors

Sat1

Fields

• runSat1_ :: ReaderT Solver (ReaderT (Watch a) (StateT (Map a Lit) IO)) b

Instances

Monad (Sat1 a)

Defined in Jukebox.Sat.Easy

Methods

(>>=) :: Sat1 a a0 -> (a0 -> Sat1 a b) -> Sat1 a b

(>>) :: Sat1 a a0 -> Sat1 a b -> Sat1 a b

return :: a0 -> Sat1 a a0

fail :: String -> Sat1 a a0

Functor (Sat1 a)

Defined in Jukebox.Sat.Easy

Methods

fmap :: (a0 -> b) -> Sat1 a a0 -> Sat1 a b

(<$) :: a0 -> Sat1 a b -> Sat1 a a0

Applicative (Sat1 a)

Defined in Jukebox.Sat.Easy

Methods

pure :: a0 -> Sat1 a a0

(<*>) :: Sat1 a (a0 -> b) -> Sat1 a a0 -> Sat1 a b

liftA2 :: (a0 -> b -> c) -> Sat1 a a0 -> Sat1 a b -> Sat1 a c

(*>) :: Sat1 a a0 -> Sat1 a b -> Sat1 a b

(<*) :: Sat1 a a0 -> Sat1 a b -> Sat1 a a0

MonadIO (Sat1 a)

Defined in Jukebox.Sat.Easy

Methods

liftIO :: IO a0 -> Sat1 a a0

newtype Sat a b c

Constructors

Sat

Fields

• runSat_ :: ReaderT (Watch a) (StateT (Map b (SatState a)) IO) c

Instances

Monad (Sat a b)

Defined in Jukebox.Sat.Easy

Methods

(>>=) :: Sat a b a0 -> (a0 -> Sat a b b0) -> Sat a b b0

(>>) :: Sat a b a0 -> Sat a b b0 -> Sat a b b0

return :: a0 -> Sat a b a0

fail :: String -> Sat a b a0

Functor (Sat a b)

Defined in Jukebox.Sat.Easy

Methods

fmap :: (a0 -> b0) -> Sat a b a0 -> Sat a b b0

(<$) :: a0 -> Sat a b b0 -> Sat a b a0

Applicative (Sat a b)

Defined in Jukebox.Sat.Easy

Methods

pure :: a0 -> Sat a b a0

(<*>) :: Sat a b (a0 -> b0) -> Sat a b a0 -> Sat a b b0

liftA2 :: (a0 -> b0 -> c) -> Sat a b a0 -> Sat a b b0 -> Sat a b c

(*>) :: Sat a b a0 -> Sat a b b0 -> Sat a b b0

(<*) :: Sat a b a0 -> Sat a b b0 -> Sat a b a0

MonadIO (Sat a b)

Defined in Jukebox.Sat.Easy

Methods

liftIO :: IO a0 -> Sat a b a0

data SatState a

Constructors

SatState Solver (Map a Lit)

type Watch a = a -> Sat1 a ()

data Form a

Constructors

Lit (Signed a)

And [Form a]

Or [Form a]

nt :: Form a -> Form a

true :: Form a

false :: Form a

unique :: [Form a] -> Form a

runSat :: Ord b => Watch a -> [b] -> Sat a b c -> IO c

runSat1 :: Ord a => Watch a -> Sat1 a b -> IO b

atIndex :: (Ord a, Ord b) => b -> Sat1 a c -> Sat a b c

solve :: Ord a => [Signed a] -> Sat1 a Bool

model :: Ord a => Sat1 a (a -> Bool)

modelValue :: Ord a => a -> Sat1 a Bool

addForm :: Ord a => Form a -> Sat1 a ()

flatten :: Ord a => Form a -> Sat1 a [[Lit]]

lit :: Ord a => Signed a -> Sat1 a Lit

var :: Ord a => a -> Sat1 a Lit