jukebox-0.1.6: A first-order reasoning toolbox
Jukebox.HighSat
newtype Sat1 a b Source
Constructors
Fields
Instances
newtype Sat a b c Source
data SatState a Source
type Watch a = a -> Sat1 a () Source
data Form a Source
nt :: Form a -> Form a Source
conj :: List f => f (Form a) -> Form a Source
disj :: List f => f (Form a) -> Form a Source
true :: Form a Source
false :: Form a Source
unique :: List f => f (Form a) -> Form a Source
runSat :: (Hashable b, Ord b) => Watch a -> [b] -> Sat a b c -> IO c Source
runSat1 :: (Ord a, Hashable a) => Watch a -> Sat1 a b -> IO b Source
atIndex :: (Ord a, Hashable a, Ord b, Hashable b) => b -> Sat1 a c -> Sat a b c Source
solve :: (Ord a, Hashable a) => [Signed a] -> Sat1 a Bool Source
model :: (Ord a, Hashable a) => Sat1 a (a -> Bool) Source
modelValue :: (Ord a, Hashable a) => a -> Sat1 a Bool Source
addForm :: (Ord a, Hashable a) => Form a -> Sat1 a () Source
flatten :: (Ord a, Hashable a) => Form a -> Sat1 a (Seq (Seq Lit)) Source
lit :: (Ord a, Hashable a) => Signed a -> Sat1 a Lit Source
var :: (Ord a, Hashable a) => a -> Sat1 a Lit Source