-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | A first-order reasoning toolbox
--   
--   Jukebox is a suite of tools for transforming problems in first-order
--   logic. It reads problems in TPTP (FOF and TFF) format.
--   
--   Currently it can translate typed problems to untyped (by efficiently
--   encoding types) and clausify problems (both typed and untyped).
@package jukebox
@version 0.1.5

module Jukebox.Sat
data Solver :: *
newSolver :: IO Solver
deleteSolver :: Solver -> IO ()
data Lit :: *
neg :: Lit -> Lit
false :: Lit
true :: Lit
class SatSolver s
getSolver :: SatSolver s => s -> Solver
newLit :: SatSolver s => s -> IO Lit
addClause :: SatSolver s => s -> [Lit] -> IO ()
solve :: SatSolver s => s -> [Lit] -> IO Bool
conflict :: SatSolver s => s -> IO [Lit]
modelValue :: SatSolver s => s -> Lit -> IO (Maybe Bool)
value :: SatSolver s => s -> Lit -> IO (Maybe Bool)
instance Jukebox.Sat.SatSolver MiniSat.Solver

module Jukebox.SatMin
solveLocalMin :: SatSolver s => s -> [Lit] -> [Lit] -> IO Bool
localMin :: SatSolver s => s -> [Lit] -> Lit -> [Lit] -> IO ()

module Jukebox.Sat3
data Lit3
Lit3 :: Lit -> Lit -> Lit3
[isFalse] :: Lit3 -> Lit
[isTrue] :: Lit3 -> Lit
false3 :: Lit3
true3 :: Lit3
bottom3 :: Lit3
neg3 :: Lit3 -> Lit3
newLit3 :: SatSolver s => s -> IO Lit3
newLit2 :: SatSolver s => s -> IO Lit3
modelValue3 :: SatSolver s => s -> Lit3 -> IO (Maybe Bool)
value3 :: SatSolver s => s -> Lit3 -> IO (Maybe Bool)
val3 :: (Lit -> IO (Maybe Bool)) -> Lit3 -> IO (Maybe Bool)

module Jukebox.SatEq
data SolverEq
SolverEq :: Solver -> IORef Int -> IORef (Map (Elt, Elt) Lit3) -> IORef (Maybe (Map Elt Elt)) -> SolverEq
[satSolver] :: SolverEq -> Solver
[counter] :: SolverEq -> IORef Int
[table] :: SolverEq -> IORef (Map (Elt, Elt) Lit3)
[model] :: SolverEq -> IORef (Maybe (Map Elt Elt))
newSolverEq :: Solver -> IO SolverEq
class SatSolver s => EqSolver s
getSolverEq :: EqSolver s => s -> SolverEq
newtype Elt
Elt :: Int -> Elt
newElt :: EqSolver s => s -> IO Elt
equal :: EqSolver s => s -> Elt -> Elt -> IO Lit3
solveEq :: EqSolver s => s -> [Lit] -> IO Bool
modelRep :: EqSolver s => s -> Elt -> IO (Maybe Elt)
instance GHC.Classes.Ord Jukebox.SatEq.Elt
instance GHC.Classes.Eq Jukebox.SatEq.Elt
instance Jukebox.Sat.SatSolver Jukebox.SatEq.SolverEq
instance Jukebox.SatEq.EqSolver Jukebox.SatEq.SolverEq
instance GHC.Show.Show Jukebox.SatEq.Elt

module Jukebox.TPTP.Lexer
scan :: ByteString -> TokenStream
data Pos
Pos :: {-# UNPACK #-} !Word -> {-# UNPACK #-} !Word -> Pos
data Token
Atom :: !Keyword -> !ByteString -> Token
[keyword] :: Token -> !Keyword
[name] :: Token -> !ByteString
Defined :: !Defined -> Token
[defined] :: Token -> !Defined
Var :: !ByteString -> Token
[name] :: Token -> !ByteString
DistinctObject :: !ByteString -> Token
[name] :: Token -> !ByteString
Number :: !Integer -> Token
[value] :: Token -> !Integer
Punct :: !Punct -> Token
[kind] :: Token -> !Punct
Eof :: Token
Error :: Token
data Punct
LParen :: Punct
RParen :: Punct
LBrack :: Punct
RBrack :: Punct
Comma :: Punct
Dot :: Punct
Or :: Punct
And :: Punct
Not :: Punct
Iff :: Punct
Implies :: Punct
Follows :: Punct
Xor :: Punct
Nor :: Punct
Nand :: Punct
Eq :: Punct
Neq :: Punct
ForAll :: Punct
Exists :: Punct
Let :: Punct
LetTerm :: Punct
Colon :: Punct
Times :: Punct
Plus :: Punct
FunArrow :: Punct
Lambda :: Punct
Apply :: Punct
ForAllLam :: Punct
ExistsLam :: Punct
DependentProduct :: Punct
DependentSum :: Punct
Some :: Punct
The :: Punct
Subtype :: Punct
SequentArrow :: Punct
data Defined
DTrue :: Defined
DFalse :: Defined
DEqual :: Defined
DDistinct :: Defined
DItef :: Defined
DItet :: Defined
DO :: Defined
DI :: Defined
DTType :: Defined
data Keyword
Normal :: Keyword
Thf :: Keyword
Tff :: Keyword
Fof :: Keyword
Cnf :: Keyword
Axiom :: Keyword
Hypothesis :: Keyword
Definition :: Keyword
Assumption :: Keyword
Lemma :: Keyword
Theorem :: Keyword
Conjecture :: Keyword
NegatedConjecture :: Keyword
Question :: Keyword
Plain :: Keyword
FiDomain :: Keyword
FiHypothesis :: Keyword
FiPredicates :: Keyword
Type :: Keyword
Unknown :: Keyword
Include :: Keyword
data TokenStream
At :: {-# UNPACK #-} !Pos -> !Contents -> TokenStream
data Contents
Cons :: !Token -> TokenStream -> Contents
instance GHC.Classes.Ord Jukebox.TPTP.Lexer.Punct
instance GHC.Classes.Eq Jukebox.TPTP.Lexer.Punct
instance GHC.Classes.Ord Jukebox.TPTP.Lexer.Defined
instance GHC.Classes.Eq Jukebox.TPTP.Lexer.Defined
instance GHC.Classes.Ord Jukebox.TPTP.Lexer.Keyword
instance GHC.Classes.Eq Jukebox.TPTP.Lexer.Keyword
instance GHC.Show.Show Jukebox.TPTP.Lexer.Pos
instance GHC.Show.Show Jukebox.TPTP.Lexer.Keyword
instance GHC.Show.Show Jukebox.TPTP.Lexer.Defined
instance GHC.Show.Show Jukebox.TPTP.Lexer.Punct
instance GHC.Base.Functor Jukebox.TPTP.Lexer.AlexLastAcc

module Jukebox.TPTP.Parsec
newtype Parsec a b
Parsec :: (forall c. (b -> Reply a c -> a -> Reply a c) -> Reply a c -> a -> Reply a c) -> Parsec a b
[runParsec] :: Parsec a b -> forall c. (b -> Reply a c -> a -> Reply a c) -> Reply a c -> a -> Reply a c
type Reply a b = [String] -> Result (Position a) b
data Result a b
Ok :: a -> b -> Result a b
Error :: a -> String -> Result a b
Expected :: a -> [String] -> Result a b
parseError :: [String] -> Parsec a b
fatalError :: Stream a c => String -> Parsec a b
nonempty :: Parsec a b -> Parsec a b
skipSome :: Parsec a b -> Parsec a ()
skipMany :: Parsec a b -> Parsec a ()
(<?>) :: Parsec a b -> String -> Parsec a b
between :: Parsec a b -> Parsec a c -> Parsec a d -> Parsec a d
sepBy1 :: Parsec a b -> Parsec a c -> Parsec a [b]
run_ :: Stream a c => Parsec a b -> a -> Result (Position a) b
run :: Stream a c => (Position a -> [String]) -> Parsec a b -> a -> (Position a, Either [String] b)
expected :: [String] -> [String] -> [String]
class Stream a b | a -> b where type family Position a
primToken :: Stream a b => a -> (a -> b -> c) -> c -> (String -> c) -> c
position :: Stream a b => a -> Position a
next :: Stream a b => Parsec a b
cut :: Stream a b => Parsec a ()
cut' :: Stream a b => Parsec a c -> Parsec a c
satisfy :: Stream a b => (b -> Bool) -> Parsec a b
eof :: Stream a b => Parsec a ()
data UserState state stream
UserState :: !state -> !stream -> UserState state stream
[userState] :: UserState state stream -> !state
[userStream] :: UserState state stream -> !stream
getState :: Parsec (UserState state a) state
putState :: state -> Parsec (UserState state a) ()
instance GHC.Base.Functor (Jukebox.TPTP.Parsec.Parsec a)
instance GHC.Base.Monad (Jukebox.TPTP.Parsec.Parsec a)
instance GHC.Base.MonadPlus (Jukebox.TPTP.Parsec.Parsec a)
instance GHC.Base.Applicative (Jukebox.TPTP.Parsec.Parsec a)
instance GHC.Base.Alternative (Jukebox.TPTP.Parsec.Parsec a)
instance Jukebox.TPTP.Parsec.Stream a b => Jukebox.TPTP.Parsec.Stream (Jukebox.TPTP.Parsec.UserState state a) b

module Jukebox.ProgressBar
data ProgressBar
ProgressBar :: IO () -> (String -> IO ()) -> IO () -> ProgressBar
[tick] :: ProgressBar -> IO ()
[enter] :: ProgressBar -> String -> IO ()
[leave] :: ProgressBar -> IO ()
tickOnRead :: ProgressBar -> ByteString -> IO ByteString
withProgressBar :: (ProgressBar -> IO a) -> IO a

module Jukebox.Options
data Annotated d p a
Annotated :: d -> p a -> Annotated d p a
[descr] :: Annotated d p a -> d
[parser] :: Annotated d p a -> p a
type ArgParser = Annotated ArgDesc SeqParser
type ArgDesc = String
data SeqParser a
SeqParser :: Int -> ([String] -> Either Error a) -> SeqParser a
[args] :: SeqParser a -> Int
[consume] :: SeqParser a -> [String] -> Either Error a
arg :: ArgDesc -> String -> (String -> Maybe a) -> ArgParser a
argNum :: (Read a, Num a) => ArgParser a
argFile :: ArgParser FilePath
argFiles :: ArgParser [FilePath]
argName :: ArgParser FilePath
argNums :: ArgParser [Int]
argOption :: [String] -> ArgParser String
argList :: [String] -> ArgParser [String]
argUsage :: ExitCode -> [String] -> ArgParser a
type OptionParser = Annotated [Flag] ParParser
data ParParser a
ParParser :: IO a -> ([String] -> ParseResult a) -> ParParser a
[val] :: ParParser a -> IO a
[peek] :: ParParser a -> [String] -> ParseResult a
data ParseResult a
Yes :: Int -> (ParParser a) -> ParseResult a
No :: (ParParser a) -> ParseResult a
Error :: Error -> ParseResult a
data Error
Mistake :: String -> Error
Usage :: ExitCode -> [String] -> Error
runPar :: ParParser a -> [String] -> Either Error (IO a)
awaitP :: (String -> Bool) -> a -> (String -> [String] -> ParseResult a) -> ParParser a
await :: String -> a -> ([String] -> ParseResult a) -> ParParser a
data Flag
Flag :: String -> String -> [String] -> String -> Flag
[flagName] :: Flag -> String
[flagGroup] :: Flag -> String
[flagHelp] :: Flag -> [String]
[flagArgs] :: Flag -> String
flag :: String -> [String] -> a -> ArgParser a -> OptionParser a
manyFlags :: String -> [String] -> ArgParser a -> OptionParser [a]
filenames :: OptionParser [String]
io :: IO a -> OptionParser a
bool :: String -> [String] -> OptionParser Bool
inGroup :: String -> OptionParser a -> OptionParser a
type ToolParser = Annotated [Tool] PrefixParser
data Tool
Tool :: String -> String -> String -> String -> Tool
[toolProgName] :: Tool -> String
[toolName] :: Tool -> String
[toolVersion] :: Tool -> String
[toolHelp] :: Tool -> String
newtype PrefixParser a
PrefixParser :: (String -> Maybe (Tool, ParParser a)) -> PrefixParser a
runPref :: PrefixParser a -> [String] -> Either Error (IO a)
tool :: Tool -> OptionParser a -> ToolParser a
getEffectiveArgs :: ToolParser a -> IO [String]
parseCommandLine :: Tool -> ToolParser a -> IO a
printHelp :: ExitCode -> [String] -> IO a
argError :: Tool -> String -> [String]
usageTool :: Tool -> String -> [String] -> String -> ToolParser a
versionTool :: Tool -> ToolParser a
helpTool :: Tool -> ToolParser a -> ToolParser a
help :: Tool -> OptionParser a -> [String]
greeting :: Tool -> String
usage :: Tool -> String -> [String]
justify :: String -> [String] -> [String]
instance GHC.Show.Show Jukebox.Options.Flag
instance GHC.Classes.Eq Jukebox.Options.Flag
instance GHC.Base.Functor p => GHC.Base.Functor (Jukebox.Options.Annotated d p)
instance (GHC.Base.Monoid d, GHC.Base.Applicative p) => GHC.Base.Applicative (Jukebox.Options.Annotated d p)
instance (GHC.Base.Monoid d, GHC.Base.Monoid (p a)) => GHC.Base.Monoid (Jukebox.Options.Annotated d p a)
instance GHC.Base.Functor Jukebox.Options.SeqParser
instance GHC.Base.Applicative Jukebox.Options.SeqParser
instance GHC.Base.Functor Jukebox.Options.ParParser
instance GHC.Base.Applicative Jukebox.Options.ParParser
instance GHC.Base.Functor Jukebox.Options.ParseResult
instance GHC.Base.Applicative Jukebox.Options.ParseResult
instance GHC.Base.Functor Jukebox.Options.PrefixParser
instance GHC.Base.Monoid (Jukebox.Options.PrefixParser a)

module Jukebox.TPTP.FindFile
findFile :: [FilePath] -> FilePath -> IO (Maybe FilePath)
findFileTPTP :: [FilePath] -> FilePath -> IO (Maybe FilePath)
getTPTPDirs :: IO [FilePath]
findFileFlags :: Annotated [Flag] ParParser [[Char]]

module Jukebox.Map
type Map a b = HashMap a b
fromList :: (Eq k, Hashable k) => [(k, v)] -> HashMap k v
toList :: HashMap k v -> [(k, v)]
insertWith :: (Eq k, Hashable k) => (v -> v -> v) -> k -> v -> HashMap k v -> HashMap k v
empty :: HashMap k v
findWithDefault :: (Eq k, Hashable k) => v -> k -> HashMap k v -> v
lookup :: (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
insert :: (Eq k, Hashable k) => k -> v -> HashMap k v -> HashMap k v
delete :: (Eq k, Hashable k) => k -> HashMap k v -> HashMap k v
elems :: HashMap k v -> [v]
union :: (Eq k, Hashable k) => HashMap k v -> HashMap k v -> HashMap k v
intersection :: (Eq k, Hashable k) => HashMap k v -> HashMap k w -> HashMap k v
null :: HashMap k v -> Bool
(!) :: (Eq k, Hashable k) => HashMap k v -> k -> v
member :: (Eq k, Hashable k) => k -> HashMap k v -> Bool
(\\) :: (Eq k, Hashable k) => HashMap k v1 -> HashMap k v -> HashMap k v1

module Jukebox.UnionFind
type UF a = State (S a)
data Replacement a
(:>) :: a -> a -> Replacement a
(=:=) :: (Hashable a, Ord a) => a -> a -> UF a (Maybe (Replacement a))
rep :: (Hashable a, Ord a) => a -> UF a a
evalUF :: S a -> UF a b -> b
execUF :: S a -> UF a b -> S a
runUF :: S a -> UF a b -> (b, S a)
type S a = Map a a
isRep :: (Hashable a, Ord a) => a -> UF a Bool
initial :: S a
reps :: (Hashable a, Ord a) => UF a (a -> a)

module Jukebox.Seq
data Seq a
Append :: (Seq a) -> (Seq a) -> Seq a
Unit :: a -> Seq a
Nil :: Seq a
class List f
fromList :: List f => f a -> Seq a
toList :: List f => f a -> [a]
appendA :: Seq a -> Seq a -> Seq a
cons :: a -> Seq a -> Seq a
snoc :: Seq a -> a -> Seq a
append :: (List f, List g) => f a -> g a -> Seq a
concat :: (List f, List g) => f (g a) -> Seq a
concatMap :: (List f, List g) => (a -> g b) -> f a -> Seq b
concatMapA :: (a -> Seq b) -> Seq a -> Seq b
fold :: (b -> b -> b) -> (a -> b) -> b -> Seq a -> b
unique :: (Ord a, Hashable a, List f) => f a -> [a]
length :: Seq a -> Int
mapM :: Monad m => (a -> m b) -> Seq a -> m (Seq b)
mapM_ :: Monad m => (a -> m ()) -> Seq a -> m ()
sequence :: Monad m => Seq (m a) -> m (Seq a)
instance Jukebox.Seq.List []
instance Jukebox.Seq.List Jukebox.Seq.Seq
instance GHC.Show.Show a => GHC.Show.Show (Jukebox.Seq.Seq a)
instance GHC.Base.Functor Jukebox.Seq.Seq
instance GHC.Base.Applicative Jukebox.Seq.Seq
instance GHC.Base.Monad Jukebox.Seq.Seq
instance GHC.Base.Alternative Jukebox.Seq.Seq
instance GHC.Base.MonadPlus Jukebox.Seq.Seq
instance GHC.Base.Monoid (Jukebox.Seq.Seq a)

module Jukebox.Utils
usort :: Ord a => [a] -> [a]
merge :: Ord a => [a] -> [a] -> [a]
nub :: (List f, Ord a, Hashable a) => f a -> [a]
popen :: FilePath -> [String] -> ByteString -> IO (ExitCode, ByteString)

module Jukebox.Name
data Name
uniqueId :: Name -> Int64
base :: Name -> ByteString
stringBaseName :: Named a => a -> String
unsafeMakeName :: Int64 -> ByteString -> Name
data (:::) a b
(:::) :: !a -> !b -> (:::) a b
lhs :: (a ::: b) -> a
rhs :: (a ::: b) -> b
class Named a where baseName = base . name
name :: Named a => a -> Name
baseName :: Named a => a -> ByteString
data Closed a
close :: Closed a -> (a -> NameM b) -> Closed b
close_ :: Closed a -> NameM b -> Closed b
closedIO :: Closed (IO a) -> IO (Closed a)
open :: Closed a -> a
closed0 :: Closed ()
stdNames :: Closed [Name]
nameO :: Name
nameI :: Name
data NameM a
newName :: Named a => a -> NameM Name
unsafeClose :: Int64 -> a -> Closed a
maxIndex :: Closed a -> Int64
supply :: (Closed () -> Closed a) -> NameM a
uniquify :: [Name] -> (Name -> ByteString)
instance GHC.Base.Monad Jukebox.Name.NameM
instance GHC.Base.Applicative Jukebox.Name.NameM
instance GHC.Base.Functor Jukebox.Name.NameM
instance (GHC.Show.Show a, GHC.Show.Show b) => GHC.Show.Show (a Jukebox.Name.::: b)
instance GHC.Classes.Eq Jukebox.Name.Name
instance GHC.Classes.Ord Jukebox.Name.Name
instance Data.Hashable.Class.Hashable Jukebox.Name.Name
instance GHC.Show.Show Jukebox.Name.Name
instance Jukebox.Name.Named Data.ByteString.Internal.ByteString
instance Jukebox.Name.Named [GHC.Types.Char]
instance Jukebox.Name.Named Jukebox.Name.Name
instance Jukebox.Name.Named a => GHC.Classes.Eq (a Jukebox.Name.::: b)
instance Jukebox.Name.Named a => GHC.Classes.Ord (a Jukebox.Name.::: b)
instance Jukebox.Name.Named a => Data.Hashable.Class.Hashable (a Jukebox.Name.::: b)
instance Jukebox.Name.Named a => Jukebox.Name.Named (a Jukebox.Name.::: b)
instance GHC.Base.Functor Jukebox.Name.Closed

module Jukebox.NameMap
type NameMap a = Map Int64 a
lookup :: Name -> NameMap a -> Maybe a
lookup_ :: Named a => a -> NameMap b -> b
insert :: Named a => a -> NameMap a -> NameMap a
member :: Named a => a -> NameMap a -> Bool
delete :: Named a => a -> NameMap a -> NameMap a
(!) :: NameMap a -> Name -> a
fromList :: (List f, Named a) => f a -> NameMap a
toList :: NameMap a -> [a]
singleton :: Named a => a -> NameMap a

module Jukebox.Form
debugging :: Bool
data DomainSize
Finite :: Int -> DomainSize
Infinite :: DomainSize
data Type
O :: Type
Type :: {-# UNPACK #-} !Name -> DomainSize -> DomainSize -> Type
[tname] :: Type -> {-# UNPACK #-} !Name
[tmonotone] :: Type -> DomainSize
[tsize] :: Type -> DomainSize
data FunType
FunType :: [Type] -> Type -> FunType
[args] :: FunType -> [Type]
[res] :: FunType -> Type
typeMaybeName :: Type -> Maybe Name
class Typed a
typ :: Typed a => a -> Type
type Variable = Name ::: Type
type Function = Name ::: FunType
data Term
Var :: Variable -> Term
(:@:) :: Function -> [Term] -> Term
newSymbol :: Named a => a -> b -> NameM (Name ::: b)
newFunction :: Named a => a -> [Type] -> Type -> NameM Function
newType :: Named a => a -> NameM Type
funArgs :: Function -> [Type]
arity :: Function -> Int
size :: Term -> Int
data Atomic
(:=:) :: Term -> Term -> Atomic
Tru :: Term -> Atomic
normAtomic :: Atomic -> Either (Term, Term) Term
data Signed a
Pos :: a -> Signed a
Neg :: a -> Signed a
type Literal = Signed Atomic
neg :: Signed a -> Signed a
the :: Signed a -> a
pos :: Signed a -> Bool
signForm :: Signed a -> Form -> Form
data Form
Literal :: Literal -> Form
Not :: Form -> Form
And :: (Seq Form) -> Form
Or :: (Seq Form) -> Form
Equiv :: Form -> Form -> Form
ForAll :: {-# UNPACK #-} !(Bind Form) -> Form
Exists :: {-# UNPACK #-} !(Bind Form) -> Form
Connective :: Connective -> Form -> Form -> Form
data Connective
Implies :: Connective
Follows :: Connective
Xor :: Connective
Nor :: Connective
Nand :: Connective
connective :: Connective -> Form -> Form -> Form
data Bind a
Bind :: (NameMap Variable) -> a -> Bind a
true :: Form
false :: Form
isTrue :: Form -> Bool
isFalse :: Form -> Bool
nt :: Form -> Form
(.=>.) :: Form -> Form -> Form
(.=.) :: Term -> Term -> Form
(/\) :: Form -> Form -> Form
(\/) :: Form -> Form -> Form
closeForm :: Form -> Form
conj :: List f => f Form -> Form
disj :: List f => f Form -> Form
positive :: Form -> Form
notInwards :: Form -> Form
simple :: Form -> Form
simplify :: Form -> Form
type CNF = Closed Obligs
data Obligs
Obligs :: [Input Clause] -> [[Input Clause]] -> String -> String -> Obligs
[axioms] :: Obligs -> [Input Clause]
[conjectures] :: Obligs -> [[Input Clause]]
[satisfiable] :: Obligs -> String
[unsatisfiable] :: Obligs -> String
toObligs :: [Input Clause] -> [[Input Clause]] -> Obligs
newtype Clause
Clause :: (Bind [Literal]) -> Clause
clause :: List f => f (Signed Atomic) -> Clause
toForm :: Clause -> Form
toLiterals :: Clause -> [Literal]
type Tag = ByteString
data Kind
Axiom :: Kind
Conjecture :: Kind
Question :: Kind
data Answer
Satisfiable :: Answer
Unsatisfiable :: Answer
NoAnswer :: NoAnswerReason -> Answer
data NoAnswerReason
GaveUp :: NoAnswerReason
Timeout :: NoAnswerReason
data Input a
Input :: Tag -> Kind -> a -> Input a
[tag] :: Input a -> Tag
[kind] :: Input a -> Kind
[what] :: Input a -> a
type Problem a = Closed [Input a]
data TypeOf a
Form :: TypeOf Form
Clause_ :: TypeOf Clause
Term :: TypeOf Term
Atomic :: TypeOf Atomic
Signed :: TypeOf (Signed a)
Bind_ :: TypeOf (Bind a)
List :: TypeOf [a]
Seq :: TypeOf (Seq a)
Input_ :: TypeOf (Input a)
Obligs_ :: TypeOf Obligs
class Symbolic a
typeOf :: Symbolic a => a -> TypeOf a
data Rep a
Const :: !a -> Rep a
Unary :: (a -> b) -> a -> Rep b
Binary :: (a -> b -> c) -> a -> b -> Rep c
rep :: Symbolic a => a -> Rep a
class Unpack a
rep' :: Unpack a => a -> Rep a
recursively :: Symbolic a => (forall a. Symbolic a => a -> a) -> a -> a
recursivelyM :: (Monad m, Symbolic a) => (forall a. Symbolic a => a -> m a) -> a -> m a
collect :: (Symbolic a, Monoid b) => (forall a. Symbolic a => a -> b) -> a -> b
type Subst = NameMap (Name ::: Term)
ids :: Subst
(|=>) :: Named a => a -> Term -> Subst
(|+|) :: Subst -> Subst -> Subst
subst :: Symbolic a => Subst -> a -> a
free :: Symbolic a => a -> NameMap Variable
ground :: Symbolic a => a -> Bool
bind :: Symbolic a => a -> Bind a
termsAndBinders :: Symbolic a => (Term -> Seq b) -> (forall a. Symbolic a => Bind a -> Seq b) -> a -> Seq b
names :: Symbolic a => a -> [Name]
types :: Symbolic a => a -> [Type]
types' :: Symbolic a => a -> [Type]
terms :: Symbolic a => a -> [Term]
vars :: Symbolic a => a -> [Variable]
functions :: Symbolic a => a -> [Function]
isFof :: Symbolic a => a -> Bool
uniqueNames :: Symbolic a => a -> NameM a
force :: Symbolic a => a -> a
check :: Symbolic a => a -> a
checkBinder :: NameMap Variable -> Subst -> Subst
type ShareState = (NameMap Type, NameMap Variable, NameMap Function)
share :: Symbolic a => a -> a
mapType :: Symbolic a => (Type -> Type) -> a -> a
instance GHC.Classes.Ord Jukebox.Form.Answer
instance GHC.Classes.Eq Jukebox.Form.Answer
instance GHC.Show.Show Jukebox.Form.NoAnswerReason
instance GHC.Classes.Ord Jukebox.Form.NoAnswerReason
instance GHC.Classes.Eq Jukebox.Form.NoAnswerReason
instance GHC.Classes.Ord Jukebox.Form.Kind
instance GHC.Classes.Eq Jukebox.Form.Kind
instance GHC.Classes.Ord a => GHC.Classes.Ord (Jukebox.Form.Signed a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Jukebox.Form.Signed a)
instance GHC.Show.Show a => GHC.Show.Show (Jukebox.Form.Signed a)
instance GHC.Classes.Ord Jukebox.Form.Term
instance GHC.Classes.Eq Jukebox.Form.Term
instance GHC.Classes.Eq Jukebox.Form.FunType
instance GHC.Show.Show Jukebox.Form.DomainSize
instance GHC.Classes.Ord Jukebox.Form.DomainSize
instance GHC.Classes.Eq Jukebox.Form.DomainSize
instance GHC.Classes.Eq Jukebox.Form.Type
instance GHC.Classes.Ord Jukebox.Form.Type
instance Data.Hashable.Class.Hashable Jukebox.Form.Type
instance Jukebox.Name.Named Jukebox.Form.Type
instance Jukebox.Form.Typed Jukebox.Form.Type
instance Jukebox.Form.Typed Jukebox.Form.FunType
instance Jukebox.Form.Typed b => Jukebox.Form.Typed (a Jukebox.Name.::: b)
instance Data.Hashable.Class.Hashable Jukebox.Form.Term
instance Jukebox.Name.Named Jukebox.Form.Term
instance Jukebox.Form.Typed Jukebox.Form.Term
instance GHC.Classes.Eq Jukebox.Form.Atomic
instance GHC.Classes.Ord Jukebox.Form.Atomic
instance Data.Hashable.Class.Hashable Jukebox.Form.Atomic
instance Data.Hashable.Class.Hashable a => Data.Hashable.Class.Hashable (Jukebox.Form.Signed a)
instance GHC.Base.Functor Jukebox.Form.Signed
instance GHC.Show.Show Jukebox.Form.Answer
instance GHC.Base.Functor Jukebox.Form.Input
instance Jukebox.Form.Symbolic Jukebox.Form.Form
instance Jukebox.Form.Symbolic Jukebox.Form.Clause
instance Jukebox.Form.Symbolic Jukebox.Form.Term
instance Jukebox.Form.Symbolic Jukebox.Form.Atomic
instance Jukebox.Form.Symbolic a => Jukebox.Form.Symbolic (Jukebox.Form.Signed a)
instance Jukebox.Form.Symbolic a => Jukebox.Form.Symbolic (Jukebox.Form.Bind a)
instance Jukebox.Form.Symbolic a => Jukebox.Form.Symbolic [a]
instance Jukebox.Form.Symbolic a => Jukebox.Form.Symbolic (Jukebox.Seq.Seq a)
instance Jukebox.Form.Symbolic a => Jukebox.Form.Symbolic (Jukebox.Form.Input a)
instance Jukebox.Form.Symbolic Jukebox.Form.Obligs
instance Jukebox.Form.Unpack Jukebox.Form.Form
instance Jukebox.Form.Unpack Jukebox.Form.Clause
instance Jukebox.Form.Unpack Jukebox.Form.Term
instance Jukebox.Form.Unpack Jukebox.Form.Atomic
instance Jukebox.Form.Symbolic a => Jukebox.Form.Unpack (Jukebox.Form.Signed a)
instance Jukebox.Form.Symbolic a => Jukebox.Form.Unpack (Jukebox.Form.Bind a)
instance Jukebox.Form.Symbolic a => Jukebox.Form.Unpack [a]
instance Jukebox.Form.Symbolic a => Jukebox.Form.Unpack (Jukebox.Seq.Seq a)
instance Jukebox.Form.Symbolic a => Jukebox.Form.Unpack (Jukebox.Form.Input a)
instance Jukebox.Form.Unpack Jukebox.Form.Obligs

module Jukebox.TPTP.Print
prettyShow :: Pretty a => a -> String
chattyShow :: Pretty a => a -> String
prettyFormula :: (Pretty a, Symbolic a) => a -> String
prettyProblem :: (Symbolic a, Pretty a) => String -> Level -> Problem a -> Doc
data Level
Normal :: Level
Chatty :: Level
class Pretty a
instance GHC.Classes.Ord Jukebox.TPTP.Print.Level
instance GHC.Classes.Eq Jukebox.TPTP.Print.Level
instance Jukebox.TPTP.Print.Pretty Jukebox.Name.Name
instance Jukebox.TPTP.Print.Pretty Jukebox.Form.Type
instance GHC.Show.Show Jukebox.Form.Type
instance GHC.Show.Show Jukebox.TPTP.Lexer.Token
instance Jukebox.TPTP.Print.Pretty Jukebox.Form.FunType
instance GHC.Show.Show Jukebox.Form.FunType
instance Jukebox.TPTP.Print.Pretty [Jukebox.Form.Type]
instance (Jukebox.Form.Symbolic a, Jukebox.TPTP.Print.Pretty a) => GHC.Show.Show (Jukebox.Form.Problem a)
instance Jukebox.TPTP.Print.Pretty a => Jukebox.TPTP.Print.Pretty (Jukebox.Form.Input a)
instance Jukebox.TPTP.Print.Pretty a => GHC.Show.Show (Jukebox.Form.Input a)
instance Jukebox.TPTP.Print.Pretty Jukebox.Form.Term
instance Jukebox.TPTP.Print.Pretty [Jukebox.Form.Term]
instance GHC.Show.Show Jukebox.Form.Term
instance Jukebox.TPTP.Print.Pretty Jukebox.Form.Atomic
instance GHC.Show.Show Jukebox.Form.Atomic
instance Jukebox.TPTP.Print.Pretty Jukebox.Form.Clause
instance GHC.Show.Show Jukebox.Form.Clause
instance Jukebox.TPTP.Print.Pretty Jukebox.Form.Form
instance GHC.Show.Show Jukebox.Form.Form
instance GHC.Show.Show Jukebox.Form.Connective
instance GHC.Show.Show Jukebox.Form.Kind

module Jukebox.HighSat
newtype Sat1 a b
Sat1 :: ReaderT Solver (ReaderT (Watch a) (StateT (Map a Lit) IO)) b -> Sat1 a b
[runSat1_] :: Sat1 a b -> ReaderT Solver (ReaderT (Watch a) (StateT (Map a Lit) IO)) b
newtype Sat a b c
Sat :: ReaderT (Watch a) (StateT (Map b (SatState a)) IO) c -> Sat a b c
[runSat_] :: Sat a b c -> ReaderT (Watch a) (StateT (Map b (SatState a)) IO) c
data SatState a
SatState :: Solver -> (Map a Lit) -> SatState a
type Watch a = a -> Sat1 a ()
data Form a
Lit :: (Signed a) -> Form a
And :: (Seq (Form a)) -> Form a
Or :: (Seq (Form a)) -> 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
instance Control.Monad.IO.Class.MonadIO (Jukebox.HighSat.Sat a b)
instance GHC.Base.Monad (Jukebox.HighSat.Sat a b)
instance GHC.Base.Applicative (Jukebox.HighSat.Sat a b)
instance GHC.Base.Functor (Jukebox.HighSat.Sat a b)
instance Control.Monad.IO.Class.MonadIO (Jukebox.HighSat.Sat1 a)
instance GHC.Base.Monad (Jukebox.HighSat.Sat1 a)
instance GHC.Base.Applicative (Jukebox.HighSat.Sat1 a)
instance GHC.Base.Functor (Jukebox.HighSat.Sat1 a)

module Jukebox.InferTypes
type Function' = Name ::: ([Type'], Type')
type Variable' = Name ::: Type'
type Type' = Name ::: Type
inferTypes :: [Input Clause] -> NameM ([Input Clause], Type -> Type)
solve :: NameMap Function' -> NameMap Variable' -> [Input Clause] -> ([Input Clause], Name -> Name)
generate :: NameMap Function' -> NameMap Variable' -> [Input Clause] -> UF Name ()

module Jukebox.Monotonox.Monotonicity
data Extension
TrueExtend :: Extension
FalseExtend :: Extension
CopyExtend :: Extension
data Var
FalseExtended :: Function -> Var
TrueExtended :: Function -> Var
annotateMonotonicity :: Problem Clause -> IO (Problem Clause)
monotone :: [Clause] -> IO (NameMap (Type ::: Maybe (NameMap (Function ::: Extension))))
fromModel :: [Function] -> Type -> (Var -> Bool) -> NameMap (Function ::: Extension)
extension :: Function -> (Var -> Bool) -> Extension
clause :: [Literal] -> Sat Var Type ()
literal :: [Literal] -> Literal -> Sat Var Type ()
safe :: [Literal] -> Term -> Form Var
guards :: Literal -> Variable -> Form Var
instance GHC.Classes.Ord Jukebox.Monotonox.Monotonicity.Var
instance GHC.Classes.Eq Jukebox.Monotonox.Monotonicity.Var
instance GHC.Show.Show Jukebox.Monotonox.Monotonicity.Extension
instance Data.Hashable.Class.Hashable Jukebox.Monotonox.Monotonicity.Var

module Jukebox.TPTP.ClauseParser
data ParseState
MkState :: ![Input Form] -> !(Map ByteString Type) -> !(Map ByteString (Name ::: FunType)) -> !(Map ByteString (Name ::: Type)) -> Type -> !(Closed ()) -> ParseState
type Parser = Parsec ParsecState
type ParsecState = UserState ParseState TokenStream
data IncludeStatement
Include :: ByteString -> (Maybe [Tag]) -> IncludeStatement
initialState :: ParseState
testParser :: Parser a -> String -> Either [String] a
getProblem :: Parser [Input Form]
keyword' :: Stream a Token => (Keyword -> Bool) -> Parsec a Token
keyword :: Stream a Token => Keyword -> Parsec a Token
punct' :: Stream a Token => (Punct -> Bool) -> Parsec a Token
punct :: Stream a Token => Punct -> Parsec a Token
defined' :: Stream a Token => (Defined -> Bool) -> Parsec a Defined
defined :: Stream a Token => Defined -> Parsec a Defined
variable :: Parsec ParsecState ByteString
number :: Parsec ParsecState Integer
atom :: Parsec ParsecState ByteString
parens :: Parser a -> Parser a
bracks :: Parser a -> Parser a
binExpr :: Parser a -> Parser (a -> a -> Parser a) -> Parser a
section :: (Tag -> Bool) -> Parser (Maybe IncludeStatement)
input :: (Tag -> Bool) -> Parser ()
kind :: Parser (Tag -> Form -> Input Form)
tag :: Parser Tag
include :: Parser IncludeStatement
newFormula :: Input Form -> Parser ()
newNameFrom :: Named a => Closed () -> a -> (Closed (), Name)
findType :: ByteString -> Parser Type
newFunction :: ByteString -> FunType -> Parser (Name ::: FunType)
applyFunction :: ByteString -> [Term] -> Type -> Parser Term
typeError :: Stream a c => (:::) Name FunType -> [Term] -> Parsec a b
lookupFunction :: FunType -> ByteString -> Parser (Name ::: FunType)
individual :: Parser Type
cnf :: Parser Form
tff :: Parser Form
fof :: Parser Form
data Thing
Apply :: !ByteString -> ![Term] -> Thing
Term :: !Term -> Thing
Formula :: !Form -> Thing
class TermLike a
fromThing :: TermLike a => Thing -> Parser a
var :: (TermLike a, ?ctx :: Maybe (Map ByteString Variable)) => Parser a
parser :: (TermLike a, ?binder :: Parser Variable, ?ctx :: Maybe (Map ByteString Variable)) => Parser a
class TermLike a => FormulaLike a
fromFormula :: FormulaLike a => Form -> a
term :: (?binder :: Parser Variable, ?ctx :: Maybe (Map ByteString Variable), TermLike a) => Parser a
literal :: (?binder :: Parser Variable, ?ctx :: Maybe (Map ByteString Variable), FormulaLike a) => Parser a
unitary :: (?binder :: Parser Variable, ?ctx :: Maybe (Map ByteString Variable), FormulaLike a) => Parser a
quantified :: (?binder :: Parser Variable, ?ctx :: Maybe (Map ByteString Variable), FormulaLike a) => Parser a
formula :: (?binder :: Parser Variable, ?ctx :: Maybe (Map ByteString Variable), FormulaLike a) => Parser a
varDecl :: Bool -> Parser Variable
type_ :: Parser Type
data Type_
TType :: Type_
Fun :: [Type] -> Type -> Type_
Prod :: [Type] -> Type_
prod :: Type_ -> Type_ -> Parser Type_
arrow :: Type_ -> Type_ -> Parser Type_
leaf :: Parser Type_
compoundType :: Parser Type_
typeDeclaration :: Parser ()
instance GHC.Show.Show Jukebox.TPTP.ClauseParser.IncludeStatement
instance Jukebox.TPTP.Parsec.Stream Jukebox.TPTP.Lexer.TokenStream Jukebox.TPTP.Lexer.Token
instance GHC.Show.Show Jukebox.TPTP.ClauseParser.Thing
instance Jukebox.TPTP.ClauseParser.TermLike Jukebox.Form.Form
instance Jukebox.TPTP.ClauseParser.TermLike Jukebox.Form.Term
instance Jukebox.TPTP.ClauseParser.TermLike Jukebox.TPTP.ClauseParser.Thing
instance Jukebox.TPTP.ClauseParser.FormulaLike Jukebox.Form.Form
instance Jukebox.TPTP.ClauseParser.FormulaLike Jukebox.TPTP.ClauseParser.Thing

module Jukebox.TPTP.ParseSnippet
tff :: [(String, Type)] -> [(String, Function)] -> String -> NameM Form
cnf :: [(String, Type)] -> [(String, Function)] -> String -> NameM Form
form :: Parsec (UserState ParseState TokenStream) a -> [(String, Type)] -> [(String, (:::) Name FunType)] -> [Char] -> NameM a
form' :: Parsec (UserState ParseState TokenStream) b -> [(String, Type)] -> [(String, (:::) Name FunType)] -> [Char] -> Closed () -> Closed b

module Jukebox.Provers.E
data EFlags
EFlags :: String -> Maybe Int -> Maybe Int -> EFlags
[eprover] :: EFlags -> String
[timeout] :: EFlags -> Maybe Int
[memory] :: EFlags -> Maybe Int
eflags :: OptionParser EFlags
mangleAnswer :: Symbolic a => a -> NameM a
runE :: (Pretty a, Symbolic a) => EFlags -> Problem a -> IO (Either Answer [Term])
extractAnswer :: Symbolic a => a -> String -> Either Answer [Term]

module Jukebox.Provers.SPASS
data SPASSFlags
SPASSFlags :: String -> Maybe Int -> Bool -> SPASSFlags
[spass] :: SPASSFlags -> String
[timeout] :: SPASSFlags -> Maybe Int
[sos] :: SPASSFlags -> Bool
spassFlags :: OptionParser SPASSFlags
runSPASS :: (Pretty a, Symbolic a) => SPASSFlags -> Problem a -> IO Answer
extractAnswer :: String -> Answer

module Jukebox.TPTP.ParseProblem
parseProblem :: [FilePath] -> FilePath -> IO (Either String (Problem Form))
parseProblemWith :: (FilePath -> IO (Maybe FilePath)) -> ProgressBar -> FilePath -> IO (Either String (Problem Form))

module Jukebox.Clausify
newtype ClausifyFlags
ClausifyFlags :: Bool -> ClausifyFlags
[splitting] :: ClausifyFlags -> Bool
clausifyFlags :: OptionParser ClausifyFlags
clausify :: ClausifyFlags -> Problem Form -> CNF
split :: Form -> [Form]
clausForm :: ByteString -> Form -> M [Input Clause]
miniscope :: Form -> M Form
forAll :: NameMap Variable -> Form -> M Form
forAllOr :: NameMap Variable -> [(Form, NameMap Variable)] -> M Form
removeEquiv :: Form -> M [Form]
removeEquivAux :: Bool -> Form -> M (Seq Form, Form, Form)
makeCopyable :: Bool -> Form -> Form -> M (Seq Form, Form, Form)
removeExists :: Form -> M Form
removeExpensiveOr :: Form -> M [Form]
type Cost = (Integer, Integer)
unitCost :: Cost
andCost :: [Cost] -> Cost
orCost :: [Cost] -> Cost
removeExpensiveOrAux :: Form -> M (Seq Form, Form, Cost)
makeOr :: [(Form, Cost)] -> M (Seq Form, Form, Cost)
cnf :: Form -> Seq (Seq Literal)
cross :: Seq (Seq (Seq Literal)) -> Seq (Seq Literal)
simplifyCNF :: Seq [Literal] -> [[Literal]]
type M = ReaderT Tag (StateT Int NameM)
run :: M a -> NameM a
skolemName :: Named a => String -> a -> M Name
nextSk :: M Int
withName :: Tag -> M a -> M a
getName :: M Tag
skolem :: Variable -> NameMap Variable -> M Term
literal :: String -> NameMap Variable -> M Atomic
instance GHC.Show.Show Jukebox.Clausify.ClausifyFlags

module Jukebox.GuessModel
data Universe
Peano :: Universe
Trees :: Universe
universe :: Universe -> Type -> NameM ([Function], [Form])
peano :: Type -> NameM ([Function], [Form])
trees :: Type -> NameM ([Function], [Form])
guessModel :: [String] -> Universe -> Problem Form -> Problem Form
ind :: Symbolic a => a -> Type
function :: [Function] -> Function -> Bool -> Function -> NameM [Form]
rhss :: [Function] -> [Term] -> Function -> Bool -> Form -> [Form]
cases :: [Function] -> [Type] -> NameM [[Term]]
cases1 :: [Function] -> Type -> NameM [Term]

module Jukebox.Monotonox.ToFOF
data Scheme
Scheme :: (Type -> NameM Function) -> ((Type -> Bool) -> (Type -> Function) -> Scheme1) -> Scheme
[makeFunction] :: Scheme -> Type -> NameM Function
[scheme1] :: Scheme -> (Type -> Bool) -> (Type -> Function) -> Scheme1
data Scheme1
Scheme1 :: (Bind Form -> Form) -> (Bind Form -> Form) -> (Term -> Term -> Form) -> (Function -> NameM Form) -> (Type -> NameM Form) -> Scheme1
[forAll] :: Scheme1 -> Bind Form -> Form
[exists] :: Scheme1 -> Bind Form -> Form
[equals] :: Scheme1 -> Term -> Term -> Form
[funcAxiom] :: Scheme1 -> Function -> NameM Form
[typeAxiom] :: Scheme1 -> Type -> NameM Form
guard :: Scheme1 -> (Type -> Bool) -> Input Form -> Input Form
translate :: Scheme -> (Type -> Bool) -> Problem Form -> Problem Form
translate1 :: Scheme -> (Type -> Bool) -> Problem Form -> Problem Form
tagsFlags :: OptionParser Bool
tags :: Bool -> Scheme
tags1 :: Bool -> (Type -> Bool) -> (Type -> Function) -> Scheme1
tagsAxiom :: Bool -> (Type -> Bool) -> (Type -> Function) -> Function -> NameM Form
tagsExists :: (Type -> Bool) -> Type -> Function -> NameM Form
guards :: Scheme
guards1 :: (Type -> Bool) -> (Type -> Function) -> Scheme1
naked :: Symbolic a => Bool -> Variable -> a -> Bool
guardsAxiom :: (Type -> Bool) -> (Type -> Function) -> Function -> NameM Form
guardsTypeAxiom :: (Type -> Bool) -> (Type -> Function) -> Type -> NameM Form

module Jukebox.Toolbox
data GlobalFlags
GlobalFlags :: Bool -> GlobalFlags
[quiet] :: GlobalFlags -> Bool
globalFlags :: OptionParser GlobalFlags
(=>>=) :: (Monad m, Applicative f) => f (a -> m b) -> f (b -> m c) -> f (a -> m c)
(=>>) :: (Monad m, Applicative f) => f (m a) -> f (m b) -> f (m b)
greetingBox :: Tool -> OptionParser (IO ())
greetingBoxIO :: Tool -> GlobalFlags -> IO ()
allFilesBox :: OptionParser ((FilePath -> IO ()) -> IO ())
allFiles :: (FilePath -> IO ()) -> [FilePath] -> IO ()
parseProblemBox :: OptionParser (FilePath -> IO (Problem Form))
parseProblemIO :: [FilePath] -> FilePath -> IO (Problem Form)
withString :: (Symbolic a, Pretty a) => String -> (Problem Form -> IO (Problem a)) -> String -> IO String
encodeString :: String -> IO String
clausifyBox :: OptionParser (Problem Form -> IO CNF)
clausifyIO :: GlobalFlags -> ClausifyFlags -> Problem Form -> IO CNF
toFofBox :: OptionParser (Problem Form -> IO (Problem Form))
oneConjectureBox :: OptionParser (CNF -> IO (Problem Clause))
oneConjecture :: CNF -> IO (Problem Clause)
toFofIO :: GlobalFlags -> (Problem Form -> IO CNF) -> Scheme -> Problem Form -> IO (Problem Form)
schemeBox :: OptionParser Scheme
monotonicityBox :: OptionParser (Problem Clause -> IO String)
monotonicity :: GlobalFlags -> Problem Clause -> IO String
annotateMonotonicityBox :: OptionParser (Problem Clause -> IO (Problem Clause))
prettyPrintBox :: (Symbolic a, Pretty a) => OptionParser (Problem a -> IO ())
prettyFormIO :: (Symbolic a, Pretty a) => GlobalFlags -> (String -> IO ()) -> Problem a -> IO ()
prettyClauseBox :: OptionParser (Problem Clause -> IO ())
prettyPrintIO :: (Symbolic a, Pretty a) => GlobalFlags -> String -> (String -> IO ()) -> Problem a -> IO ()
writeFileBox :: OptionParser (String -> IO ())
guessModelBox :: OptionParser (Problem Form -> IO (Problem Form))
guessModelIO :: [String] -> Universe -> Problem Form -> IO (Problem Form)
allObligsBox :: OptionParser ((Problem Clause -> IO Answer) -> Closed Obligs -> IO ())
allObligsIO :: (Closed [Input Clause] -> IO Answer) -> Closed Obligs -> IO ()
inferBox :: OptionParser (Problem Clause -> IO (Problem Clause, Type -> Type))
printInferredBox :: OptionParser ((Problem Clause, Type -> Type) -> IO (Problem Clause))
equinoxBox :: OptionParser (Problem Clause -> IO Answer)
instance GHC.Show.Show Jukebox.Toolbox.GlobalFlags