jukebox-0.2.15: A first-order reasoning toolbox
Jukebox.HighSat
newtype Sat1 a b Source #
Constructors
Fields
Instances
Methods
(>>=) :: Sat1 a a -> (a -> Sat1 a b) -> Sat1 a b #
(>>) :: Sat1 a a -> Sat1 a b -> Sat1 a b #
return :: a -> Sat1 a a #
fail :: String -> Sat1 a a #
fmap :: (a -> b) -> Sat1 a a -> Sat1 a b #
(<$) :: a -> Sat1 a b -> Sat1 a a #
pure :: a -> Sat1 a a #
(<*>) :: Sat1 a (a -> b) -> Sat1 a a -> Sat1 a b #
(*>) :: Sat1 a a -> Sat1 a b -> Sat1 a b #
(<*) :: Sat1 a a -> Sat1 a b -> Sat1 a a #
liftIO :: IO a -> Sat1 a a #
newtype Sat a b c Source #
(>>=) :: Sat a b a -> (a -> Sat a b b) -> Sat a b b #
(>>) :: Sat a b a -> Sat a b b -> Sat a b b #
return :: a -> Sat a b a #
fail :: String -> Sat a b a #
fmap :: (a -> b) -> Sat a b a -> Sat a b b #
(<$) :: a -> Sat a b b -> Sat a b a #
pure :: a -> Sat a b a #
(<*>) :: Sat a b (a -> b) -> Sat a b a -> Sat a b b #
(*>) :: Sat a b a -> Sat a b b -> Sat a b b #
(<*) :: Sat a b a -> Sat a b b -> Sat a b a #
liftIO :: IO a -> Sat a b a #
data SatState a Source #
type Watch a = a -> Sat1 a () Source #
data Form a Source #
nt :: Form a -> Form a Source #
true :: Form a Source #
false :: Form a Source #
unique :: [Form a] -> Form a Source #
runSat :: Ord b => Watch a -> [b] -> Sat a b c -> IO c Source #
runSat1 :: Ord a => Watch a -> Sat1 a b -> IO b Source #
atIndex :: (Ord a, Ord b) => b -> Sat1 a c -> Sat a b c Source #
solve :: Ord a => [Signed a] -> Sat1 a Bool Source #
model :: Ord a => Sat1 a (a -> Bool) Source #
modelValue :: Ord a => a -> Sat1 a Bool Source #
addForm :: Ord a => Form a -> Sat1 a () Source #
flatten :: Ord a => Form a -> Sat1 a [[Lit]] Source #
lit :: Ord a => Signed a -> Sat1 a Lit Source #
var :: Ord a => a -> Sat1 a Lit Source #