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 (Seq (Form a))

Or (Seq (Form a))

nt :: Form a -> Form a

conj :: List f => f (Form a) -> Form a

disj :: List f => f (Form a) -> Form a

true :: Form a

false :: Form a

unique :: List f => f (Form a) -> Form a

runSat :: (Hashable b, Ord b) => Watch a -> [b] -> Sat a b c -> IO c

runSat1 :: (Ord a, Hashable a) => Watch a -> Sat1 a b -> IO b

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

solve :: (Ord a, Hashable a) => [Signed a] -> Sat1 a Bool

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

modelValue :: (Ord a, Hashable a) => a -> Sat1 a Bool

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

flatten :: (Ord a, Hashable a) => Form a -> Sat1 a (Seq (Seq Lit))

lit :: (Ord a, Hashable a) => Signed a -> Sat1 a Lit

var :: (Ord a, Hashable a) => a -> Sat1 a Lit