jukebox-0.1.2: 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 aSource
conj :: List f => f (Form a) -> Form aSource
disj :: List f => f (Form a) -> Form aSource
true :: Form aSource
false :: Form aSource
unique :: List f => f (Form a) -> Form aSource
runSat :: (Hashable b, Ord b) => Watch a -> [b] -> Sat a b c -> IO cSource
runSat1 :: (Ord a, Hashable a) => Watch a -> Sat1 a b -> IO bSource
atIndex :: (Ord a, Hashable a, Ord b, Hashable b) => b -> Sat1 a c -> Sat a b cSource
solve :: (Ord a, Hashable a) => [Signed a] -> Sat1 a BoolSource
model :: (Ord a, Hashable a) => Sat1 a (a -> Bool)Source
modelValue :: (Ord a, Hashable a) => a -> Sat1 a BoolSource
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 LitSource
var :: (Ord a, Hashable a) => a -> Sat1 a LitSource