Jukebox.HighSat

Documentation

newtype Sat1 a b

Constructors

Sat1

Fields

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

Instances

Monad (Sat1 a)

Functor (Sat1 a)

Applicative (Sat1 a)

MonadIO (Sat1 a)

newtype Sat a b c

Constructors

Sat

Fields

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

Instances

Monad (Sat a b)

Functor (Sat a b)

Applicative (Sat a b)

MonadIO (Sat a b)

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