-- 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.5

module Jukebox.Name
data Name
Fixed :: !FixedName -> Maybe String -> Name
Unique :: {-# UNPACK #-} !Int64 -> {-# UNPACK #-} !Symbol -> Maybe String -> Renamer -> Name
Variant :: !Name -> ![Name] -> Renamer -> Name
data FixedName
Basic :: {-# UNPACK #-} !Symbol -> FixedName
Overloaded :: {-# UNPACK #-} !Symbol -> {-# UNPACK #-} !Symbol -> FixedName
Integer :: !Integer -> FixedName
Rational :: !Rational -> FixedName
Real :: !Rational -> FixedName
type Renamer = String -> Int -> Renaming
data Renaming
Renaming :: [String] -> String -> Renaming
base :: Named a => a -> String
label :: Named a => a -> Maybe String
hasLabel :: Named a => String -> a -> Bool
withMaybeLabel :: Maybe String -> Name -> Name
withLabel :: String -> Name -> Name
renamer :: Named a => a -> Renamer
defaultRenamer :: Renamer
withRenamer :: Name -> Renamer -> Name
compareName :: Name -> Either FixedName (Either Int64 (Name, [Name]))
class Named a
name :: Named a => a -> Name
allNames :: Named a => a -> [Name]
variant :: (Named a, Named b) => a -> [b] -> Name
unvariant :: Name -> Maybe (Name, [Name])
data a ::: b
(:::) :: a -> b -> (:::) a b
lhs :: (a ::: b) -> a
rhs :: (a ::: b) -> b
newtype NameM a
NameM :: State Int64 a -> NameM a
[unNameM] :: NameM a -> State Int64 a
runNameM :: [Name] -> NameM a -> a
newName :: Named a => a -> NameM Name
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.Ord Jukebox.Name.FixedName
instance GHC.Classes.Eq Jukebox.Name.FixedName
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 => Jukebox.Name.Named (a Jukebox.Name.::: b)
instance Jukebox.Name.Named [GHC.Types.Char]
instance Jukebox.Name.Named Data.Symbol.Unsafe.Symbol
instance Jukebox.Name.Named GHC.Integer.Type.Integer
instance Jukebox.Name.Named GHC.Types.Int
instance Jukebox.Name.Named Jukebox.Name.Name
instance GHC.Classes.Eq Jukebox.Name.Name
instance GHC.Classes.Ord Jukebox.Name.Name
instance GHC.Show.Show Jukebox.Name.Name
instance GHC.Show.Show Jukebox.Name.FixedName

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 [String] SeqParser
data SeqParser a
SeqParser :: Int -> ([String] -> Either Error a) -> SeqParser a
[args] :: SeqParser a -> Int
[consume] :: SeqParser a -> [String] -> Either Error a
arg :: String -> String -> (String -> Maybe a) -> ArgParser a
argNum :: (Read a, Num a) => ArgParser a
argFile :: ArgParser FilePath
argFiles :: ArgParser [FilePath]
argName :: ArgParser String
argNums :: ArgParser [Int]
argOption :: [(String, a)] -> ArgParser a
argList :: [String] -> ArgParser [String]
argOptionWith :: String -> String -> String -> [String] -> (String -> Maybe a) -> ArgParser a
argUsage :: ExitCode -> [String] -> ArgParser a
type OptionParser = Annotated [Flag] ParParser
data Flag
Flag :: String -> String -> FlagMode -> [String] -> String -> Flag
[flagName] :: Flag -> String
[flagGroup] :: Flag -> String
[flagMode] :: Flag -> FlagMode
[flagHelp] :: Flag -> [String]
[flagArgs] :: Flag -> String
data FlagMode
NormalMode :: FlagMode
ExpertMode :: FlagMode
HiddenMode :: FlagMode
flagExpert :: Flag -> Bool
data ParParser a
ParParser :: Either Error (IO a) -> ([String] -> ParseResult a) -> ParParser a
[val] :: ParParser a -> Either Error (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)
await :: (String -> Bool) -> Either Error a -> (String -> [String] -> ParseResult a) -> ParParser a
primFlag :: String -> [String] -> (String -> Bool) -> (a -> a -> Either Error a) -> a -> ArgParser (String -> a) -> OptionParser a
flag :: String -> [String] -> a -> ArgParser a -> OptionParser a
manyFlags :: String -> [String] -> ArgParser a -> OptionParser [a]
bool :: String -> [String] -> Bool -> OptionParser Bool
filenames :: OptionParser [String]
io :: IO a -> OptionParser a
inGroup :: String -> OptionParser a -> OptionParser a
expert :: OptionParser a -> OptionParser a
hidden :: OptionParser a -> OptionParser a
version :: String -> OptionParser a -> OptionParser a
printHelp :: ExitCode -> [String] -> IO a
printError :: String -> String -> IO a
help :: String -> String -> OptionParser a -> OptionParser a
usageText :: String -> String -> [String]
helpText :: Bool -> String -> String -> OptionParser a -> [String]
justify :: String -> [String] -> [String]
parseCommandLine :: String -> OptionParser a -> IO a
parseCommandLineWithExtraArgs :: [String] -> String -> OptionParser a -> IO a
parseCommandLineWithArgs :: String -> [String] -> String -> OptionParser a -> IO a
instance GHC.Show.Show Jukebox.Options.Flag
instance GHC.Classes.Eq Jukebox.Options.Flag
instance GHC.Show.Show Jukebox.Options.FlagMode
instance GHC.Classes.Eq Jukebox.Options.FlagMode
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 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.Semigroup d, GHC.Base.Monoid d, GHC.Base.Semigroup (p a), GHC.Base.Monoid (p a)) => GHC.Base.Monoid (Jukebox.Options.Annotated d p a)
instance (GHC.Base.Semigroup d, GHC.Base.Semigroup (p a)) => GHC.Base.Semigroup (Jukebox.Options.Annotated d p a)

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.Sat.Minimise
solveLocalMin :: SatSolver s => s -> [Lit] -> [Lit] -> IO Bool
localMin :: SatSolver s => s -> [Lit] -> Lit -> [Lit] -> IO ()

module Jukebox.Sat.ThreeValued
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.Sat.Equality
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.Sat.Equality.Elt
instance GHC.Classes.Eq Jukebox.Sat.Equality.Elt
instance Jukebox.Sat.Equality.EqSolver Jukebox.Sat.Equality.SolverEq
instance Jukebox.Sat.SatSolver Jukebox.Sat.Equality.SolverEq
instance GHC.Show.Show Jukebox.Sat.Equality.Elt

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

module Jukebox.TPTP.Lexer
scan :: String -> TokenStream
data Pos
Pos :: {-# UNPACK #-} !Word -> {-# UNPACK #-} !Word -> Pos
data Token
Atom :: !Keyword -> {-# UNPACK #-} !Symbol -> Token
[keyword] :: Token -> !Keyword
[tokenName] :: Token -> {-# UNPACK #-} !Symbol
Defined :: !Defined -> Token
[defined] :: Token -> !Defined
Var :: {-# UNPACK #-} !Symbol -> Token
[tokenName] :: Token -> {-# UNPACK #-} !Symbol
DistinctObject :: {-# UNPACK #-} !Symbol -> Token
[tokenName] :: Token -> {-# UNPACK #-} !Symbol
Number :: !Integer -> Token
[value] :: Token -> !Integer
Rational :: !Rational -> Token
[ratValue] :: Token -> !Rational
Real :: !Rational -> Token
[ratValue] :: Token -> !Rational
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
Other :: {-# UNPACK #-} !Symbol -> Punct
showPunct :: Punct -> Symbol
data Defined
DTrue :: Defined
DFalse :: Defined
DDistinct :: Defined
DItef :: Defined
DItet :: Defined
DO :: Defined
DI :: Defined
DTType :: Defined
data Keyword
Normal :: Keyword
Thf :: Keyword
Tff :: Keyword
Fof :: Keyword
Tcf :: 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.Punct
instance GHC.Show.Show Jukebox.TPTP.Lexer.Defined
instance GHC.Show.Show Jukebox.TPTP.Lexer.Keyword

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
infix 0 <?>
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) ()
getPosition :: Stream a b => Parsec a (Position a)
instance Jukebox.TPTP.Parsec.Stream a b => Jukebox.TPTP.Parsec.Stream (Jukebox.TPTP.Parsec.UserState state a) b
instance GHC.Base.Functor (Jukebox.TPTP.Parsec.Parsec a)
instance GHC.Base.Monad (Jukebox.TPTP.Parsec.Parsec a)
instance Control.Monad.Fail.MonadFail (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)

module Jukebox.UnionFind
type UF a = State (S a)
data Replacement a
(:>) :: a -> a -> Replacement a
(=:=) :: Ord a => a -> a -> UF a (Maybe (Replacement a))
rep :: 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 :: Ord a => a -> UF a Bool
initial :: S a
reps :: Ord a => UF a (a -> a)

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

module Jukebox.Form
debugging :: Bool
data Type
O :: Type
Type :: !Name -> Type
[tname] :: Type -> !Name
indType :: Type
intType :: Type
ratType :: Type
realType :: Type
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
infix 8 :=:
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 :: [Form] -> Form
Or :: [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 :: Set 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
positive :: Form -> Form
notInwards :: Form -> Form
simple :: Form -> Form
simplify :: Form -> Form
data CNF
CNF :: [Input Clause] -> [[Input Clause]] -> (Maybe Model -> Answer) -> (Maybe CNFRefutation -> Answer) -> CNF
[axioms] :: CNF -> [Input Clause]
[conjectures] :: CNF -> [[Input Clause]]
[satisfiable] :: CNF -> Maybe Model -> Answer
[unsatisfiable] :: CNF -> Maybe CNFRefutation -> Answer
toCNF :: [Input Clause] -> [[Input Clause]] -> CNF
newtype Clause
Clause :: Bind [Literal] -> Clause
clause :: [Literal] -> Clause
toForm :: Clause -> Form
toLiterals :: Clause -> [Literal]
toClause :: Form -> Maybe Clause
type Tag = String
data Kind
Ax :: AxKind -> Kind
Conj :: ConjKind -> Kind
data AxKind
Axiom :: AxKind
Hypothesis :: AxKind
Definition :: AxKind
Assumption :: AxKind
Lemma :: AxKind
TheoremKind :: AxKind
NegatedConjecture :: AxKind
data ConjKind
Conjecture :: ConjKind
Question :: ConjKind
data Answer
Sat :: SatReason -> Maybe Model -> Answer
Unsat :: UnsatReason -> Maybe CNFRefutation -> Answer
NoAnswer :: NoAnswerReason -> Answer
data NoAnswerReason
GaveUp :: NoAnswerReason
Timeout :: NoAnswerReason
data SatReason
Satisfiable :: SatReason
CounterSatisfiable :: SatReason
data UnsatReason
Unsatisfiable :: UnsatReason
Theorem :: UnsatReason
type Model = [String]
type CNFRefutation = [String]
explainAnswer :: Answer -> String
answerSZS :: Answer -> [String]
answerJustification :: Answer -> Maybe [String]
data Input a
Input :: Tag -> Kind -> InputSource -> a -> Input a
[tag] :: Input a -> Tag
[kind] :: Input a -> Kind
[source] :: Input a -> InputSource
[what] :: Input a -> a
data InputSource
Unknown :: InputSource
FromFile :: String -> Int -> InputSource
Inference :: String -> String -> [Input Form] -> InputSource
type Problem a = [Input a]
data TypeOf a
[Form] :: TypeOf Form
[Clause_] :: TypeOf Clause
[Term] :: TypeOf Term
[Atomic] :: TypeOf Atomic
[Signed] :: (Symbolic a, Symbolic (Signed a)) => TypeOf (Signed a)
[Bind_] :: (Symbolic a, Symbolic (Bind a)) => TypeOf (Bind a)
[List] :: (Symbolic a, Symbolic [a]) => TypeOf [a]
[Input_] :: (Symbolic a, Symbolic (Input a)) => TypeOf (Input a)
[CNF_] :: TypeOf CNF
class Symbolic a
typeOf :: Symbolic a => a -> TypeOf a
data Rep a
[Const] :: !a -> Rep a
[Unary] :: Symbolic a => (a -> b) -> a -> Rep b
[Binary] :: (Symbolic a, Symbolic b) => (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 = Map Variable Term
ids :: Subst
(|=>) :: Variable -> Term -> Subst
(|+|) :: Subst -> Subst -> Subst
subst :: Symbolic a => Subst -> a -> a
free :: Symbolic a => a -> Set Variable
ground :: Symbolic a => a -> Bool
bind :: Symbolic a => a -> Bind a
termsAndBinders :: forall a b. Symbolic a => (Term -> DList b) -> (forall a. Symbolic a => Bind a -> [b]) -> a -> [b]
names :: Symbolic a => a -> [Name]
run :: Symbolic a => a -> (a -> NameM b) -> b
run_ :: Symbolic a => a -> NameM b -> b
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]
funOcc :: Symbolic a => Function -> a -> Int
funsOcc :: Symbolic a => a -> Map Function Int
isFof :: Symbolic a => a -> Bool
eraseTypes :: Symbolic a => a -> a
uniqueNames :: Symbolic a => a -> NameM a
force :: Symbolic a => a -> a
check :: Symbolic a => a -> a
checkBinder :: Set Variable -> Subst -> Subst
mapName :: Symbolic a => (Name -> Name) -> a -> a
mapType :: Symbolic a => (Type -> Type) -> a -> a
instance Data.Traversable.Traversable Jukebox.Form.Input
instance Data.Foldable.Foldable Jukebox.Form.Input
instance GHC.Base.Functor Jukebox.Form.Input
instance GHC.Classes.Ord Jukebox.Form.Answer
instance GHC.Classes.Eq Jukebox.Form.Answer
instance GHC.Show.Show Jukebox.Form.UnsatReason
instance GHC.Classes.Ord Jukebox.Form.UnsatReason
instance GHC.Classes.Eq Jukebox.Form.UnsatReason
instance GHC.Show.Show Jukebox.Form.SatReason
instance GHC.Classes.Ord Jukebox.Form.SatReason
instance GHC.Classes.Eq Jukebox.Form.SatReason
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 Jukebox.Form.ConjKind
instance GHC.Classes.Eq Jukebox.Form.ConjKind
instance GHC.Classes.Ord Jukebox.Form.AxKind
instance GHC.Classes.Eq Jukebox.Form.AxKind
instance GHC.Classes.Ord Jukebox.Form.Form
instance GHC.Classes.Eq Jukebox.Form.Form
instance GHC.Classes.Ord a => GHC.Classes.Ord (Jukebox.Form.Bind a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Jukebox.Form.Bind a)
instance GHC.Classes.Ord Jukebox.Form.Connective
instance GHC.Classes.Eq Jukebox.Form.Connective
instance Data.Traversable.Traversable Jukebox.Form.Signed
instance Data.Foldable.Foldable Jukebox.Form.Signed
instance GHC.Base.Functor Jukebox.Form.Signed
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.Ord Jukebox.Form.FunType
instance GHC.Classes.Eq Jukebox.Form.FunType
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.Form.Input a)
instance Jukebox.Form.Unpack Jukebox.Form.CNF
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.Form.Input a)
instance Jukebox.Form.Symbolic Jukebox.Form.CNF
instance GHC.Show.Show Jukebox.Form.Answer
instance GHC.Classes.Eq Jukebox.Form.Atomic
instance GHC.Classes.Ord Jukebox.Form.Atomic
instance Jukebox.Name.Named Jukebox.Form.Term
instance Jukebox.Form.Typed Jukebox.Form.Term
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 GHC.Classes.Eq Jukebox.Form.Type
instance GHC.Classes.Ord Jukebox.Form.Type
instance Jukebox.Name.Named Jukebox.Form.Type

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


-- | Encodes Horn problems as unit equalities.
module Jukebox.Tools.HornToUnit
data HornFlags
HornFlags :: Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Encoding -> HornFlags
[allowConjunctiveConjectures] :: HornFlags -> Bool
[allowDisjunctiveConjectures] :: HornFlags -> Bool
[allowNonGroundConjectures] :: HornFlags -> Bool
[allowCompoundConjectures] :: HornFlags -> Bool
[dropNonHorn] :: HornFlags -> Bool
[passivise] :: HornFlags -> Bool
[multi] :: HornFlags -> Bool
[smaller] :: HornFlags -> Bool
[encoding] :: HornFlags -> Encoding
data Encoding
Symmetric :: Encoding
Asymmetric1 :: Encoding
Asymmetric2 :: Encoding
Asymmetric3 :: Encoding
hornFlags :: OptionParser HornFlags
hornToUnit :: HornFlags -> Problem Clause -> IO (Either (Input Clause) (Either Answer (Problem Clause)))
eliminatePredicates :: Problem Clause -> Problem Clause
eliminateMultiplePreconditions :: HornFlags -> Problem Clause -> Problem Clause
eliminateUnsuitableConjectures :: HornFlags -> Problem Clause -> Problem Clause
eliminateHornClauses :: HornFlags -> Problem Clause -> Either (Input Clause) (Problem Clause)
encodeTypesSmartly :: Problem Clause -> IO (Either Answer (Problem Clause -> Problem Clause))
hasSizeOneModel :: Problem Clause -> IO Bool
instance GHC.Show.Show Jukebox.Tools.HornToUnit.HornFlags
instance GHC.Show.Show Jukebox.Tools.HornToUnit.Encoding
instance GHC.Classes.Eq Jukebox.Tools.HornToUnit.Encoding

module Jukebox.Tools.Clausify
newtype ClausifyFlags
ClausifyFlags :: Bool -> ClausifyFlags
[splitting] :: ClausifyFlags -> Bool
clausifyFlags :: OptionParser ClausifyFlags
clausify :: ClausifyFlags -> Problem Form -> CNF
split :: Form -> [Form]
clausForm :: AxKind -> Input Form -> M [Input Clause]
miniscope :: Form -> M Form
forAll :: Set Variable -> Form -> M Form
forAllOr :: Set Variable -> [(Form, Set Variable)] -> M Form
removeEquiv :: Form -> M [Form]
removeEquivAux :: Bool -> Form -> M ([Form], Form, Form)
makeCopyable :: Bool -> Form -> Form -> M ([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 ([Form], Form, Cost)
makeOr :: [(Form, Cost)] -> M ([Form], Form, Cost)
cnf :: Form -> [[Literal]]
cross :: [[[Literal]]] -> [[Literal]]
simplifyCNF :: [[Literal]] -> [[Literal]]
type M = ReaderT Tag NameM
run :: M a -> NameM a
skolemName :: Named a => String -> a -> M Name
withName :: Tag -> M a -> M a
getName :: M Tag
skolem :: Variable -> Set Variable -> M Term
literal :: String -> Set Variable -> M Atomic
instance GHC.Show.Show Jukebox.Tools.Clausify.ClausifyFlags

module Jukebox.Tools.EncodeTypes
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.TPTP.Print

-- | Pretty print a value with the <a>prettyNormal</a> level.
prettyShow :: Pretty a => a -> String
prettyNames :: Symbolic a => a -> a
showClauses :: Problem Clause -> String
pPrintClauses :: Problem Clause -> Doc
showProblem :: Problem Form -> String
pPrintProblem :: String -> Problem Form -> Doc
pPrintProof :: Problem Form -> Doc
instance Text.PrettyPrint.HughesPJClass.Pretty a => Text.PrettyPrint.HughesPJClass.Pretty (Jukebox.Form.Input a)
instance Text.PrettyPrint.HughesPJClass.Pretty a => GHC.Show.Show (Jukebox.Form.Input a)
instance Text.PrettyPrint.HughesPJClass.Pretty Jukebox.Form.Clause
instance GHC.Show.Show Jukebox.Form.Clause
instance Text.PrettyPrint.HughesPJClass.Pretty Jukebox.Form.Type
instance GHC.Show.Show Jukebox.Form.Type
instance Text.PrettyPrint.HughesPJClass.Pretty Jukebox.Form.FunType
instance GHC.Show.Show Jukebox.Form.FunType
instance Text.PrettyPrint.HughesPJClass.Pretty Jukebox.Name.Name
instance GHC.Show.Show Jukebox.TPTP.Lexer.Token
instance Text.PrettyPrint.HughesPJClass.Pretty Jukebox.Form.Term
instance GHC.Show.Show Jukebox.Form.Term
instance Text.PrettyPrint.HughesPJClass.Pretty Jukebox.Form.Atomic
instance GHC.Show.Show Jukebox.Form.Atomic
instance Text.PrettyPrint.HughesPJClass.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
instance GHC.Show.Show Jukebox.Form.AxKind
instance GHC.Show.Show Jukebox.Form.ConjKind

module Jukebox.TPTP.Parse.Core
data ParseState
MkState :: Maybe String -> ![Input Form] -> !Map Symbol Type -> !Map Symbol [Function] -> !Map Symbol Variable -> !Int64 -> ParseState
type Parser = Parsec ParsecState
type ParsecState = UserState ParseState TokenStream
data IncludeStatement
Include :: String -> Maybe [Tag] -> IncludeStatement
initialState :: Maybe String -> ParseState
initialStateFrom :: Maybe String -> [Name] -> Map Symbol Type -> Map Symbol [Function] -> ParseState
data ParseResult a
ParseFailed :: Location -> [String] -> ParseResult a
ParseSucceeded :: a -> ParseResult a
ParseStalled :: Location -> FilePath -> (String -> ParseResult a) -> ParseResult a
data Location
Location :: FilePath -> Integer -> Integer -> Location
makeLocation :: FilePath -> Pos -> Location
parseProblem :: FilePath -> String -> ParseResult [Input Form]
parseProblemFrom :: ParseState -> FilePath -> String -> ParseResult [Input Form]
testParser :: Parser a -> String -> Either [String] a
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
operator :: Parsec ParsecState Token
defined' :: Stream a Token => (Defined -> Bool) -> Parsec a Defined
defined :: Stream a Token => Defined -> Parsec a Defined
variable :: Parsec ParsecState Symbol
number :: Parsec ParsecState Integer
ratNumber :: Parsec ParsecState Rational
realNumber :: Parsec ParsecState Rational
atom :: Parsec ParsecState Symbol
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 ()
newFunction :: Symbol -> FunType -> Parser Function
showTypes :: [FunType] -> String
applyFunction :: Symbol -> [Term] -> Type -> Parser Term
typeError :: Stream a c => [Name ::: FunType] -> [Term] -> Parsec a b
lookupType :: Symbol -> Parser Type
lookupFunction :: FunType -> Symbol -> Parser [Name ::: FunType]
cnf :: Parser Form
tff :: Parser Form
fof :: Parser Form
data Thing
Apply :: !Symbol -> ![Term] -> Thing
Term :: !Term -> Thing
Formula :: !Form -> Thing
class TermLike a
fromThing :: TermLike a => Thing -> Parser a
var :: TermLike a => Mode -> Map Symbol Variable -> Parser a
parseFormula :: TermLike a => Parser Form -> Parser a
parser :: TermLike a => Mode -> Map Symbol Variable -> Parser a
data Mode
Typed :: Mode
Untyped :: Mode
NoQuantification :: Mode
atomic :: TermLike a => Mode -> Map Symbol Variable -> Parser a
unary :: TermLike a => Mode -> Map Symbol Variable -> Parser a
term :: TermLike a => Mode -> Map Symbol Variable -> Parser a
literal :: TermLike a => Mode -> Map Symbol Variable -> Parser a
unitary :: TermLike a => Mode -> Map Symbol Variable -> Parser a
quantified :: TermLike a => Mode -> Map Symbol Variable -> Parser a
formula :: TermLike a => Mode -> Map Symbol Variable -> Parser a
binder :: Mode -> 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.Base.Functor Jukebox.TPTP.Parse.Core.ParseResult
instance GHC.Show.Show Jukebox.TPTP.Parse.Core.IncludeStatement
instance Jukebox.TPTP.Parse.Core.TermLike Jukebox.Form.Form
instance Jukebox.TPTP.Parse.Core.TermLike Jukebox.Form.Term
instance Jukebox.TPTP.Parse.Core.TermLike Jukebox.TPTP.Parse.Core.Thing
instance GHC.Show.Show Jukebox.TPTP.Parse.Core.Thing
instance GHC.Base.Applicative Jukebox.TPTP.Parse.Core.ParseResult
instance GHC.Base.Monad Jukebox.TPTP.Parse.Core.ParseResult
instance GHC.Show.Show Jukebox.TPTP.Parse.Core.Location
instance Jukebox.TPTP.Parsec.Stream Jukebox.TPTP.Lexer.TokenStream Jukebox.TPTP.Lexer.Token

module Jukebox.TPTP.ParseSnippet
tff :: [(String, Type)] -> [(String, Function)] -> String -> Form
cnf :: [(String, Type)] -> [(String, Function)] -> String -> Form
form :: Symbolic a => Parser a -> [(String, Type)] -> [(String, Function)] -> String -> a

module Jukebox.Tools.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.TPTP.Parse
parseString :: String -> IO (Problem Form)
parseProblem :: [FilePath] -> FilePath -> IO (Either String (Problem Form))
parseProblemWith :: (FilePath -> IO (Maybe FilePath)) -> FilePath -> IO (Either String (Problem Form))

module Jukebox.Sat.Easy
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 :: [Form a] -> Form a
Or :: [Form a] -> Form a
nt :: Form a -> Form a
true :: Form a
false :: Form a
unique :: [Form a] -> Form a
runSat :: Ord b => Watch a -> [b] -> Sat a b c -> IO c
runSat1 :: Ord a => Watch a -> Sat1 a b -> IO b
atIndex :: (Ord a, Ord b) => b -> Sat1 a c -> Sat a b c
solve :: Ord a => [Signed a] -> Sat1 a Bool
model :: Ord a => Sat1 a (a -> Bool)
modelValue :: Ord a => a -> Sat1 a Bool
addForm :: Ord a => Form a -> Sat1 a ()
flatten :: Ord a => Form a -> Sat1 a [[Lit]]
lit :: Ord a => Signed a -> Sat1 a Lit
var :: Ord a => a -> Sat1 a Lit
instance Control.Monad.IO.Class.MonadIO (Jukebox.Sat.Easy.Sat a b)
instance GHC.Base.Monad (Jukebox.Sat.Easy.Sat a b)
instance GHC.Base.Applicative (Jukebox.Sat.Easy.Sat a b)
instance GHC.Base.Functor (Jukebox.Sat.Easy.Sat a b)
instance Control.Monad.IO.Class.MonadIO (Jukebox.Sat.Easy.Sat1 a)
instance GHC.Base.Monad (Jukebox.Sat.Easy.Sat1 a)
instance GHC.Base.Applicative (Jukebox.Sat.Easy.Sat1 a)
instance GHC.Base.Functor (Jukebox.Sat.Easy.Sat1 a)

module Jukebox.Tools.AnalyseMonotonicity
data Extension
TrueExtend :: Extension
FalseExtend :: Extension
CopyExtend :: Extension
data Var
FalseExtended :: Function -> Var
TrueExtended :: Function -> Var
analyseMonotonicity :: Problem Clause -> IO (Set Type)
monotone :: [Clause] -> IO (Map Type (Maybe (Map Function Extension)))
fromModel :: [Function] -> Type -> (Var -> Bool) -> Map 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.Tools.AnalyseMonotonicity.Var
instance GHC.Classes.Eq Jukebox.Tools.AnalyseMonotonicity.Var
instance GHC.Show.Show Jukebox.Tools.AnalyseMonotonicity.Extension

module Jukebox.SMTLIB
keywords :: [String]
renamings :: [(String, String)]
renameAvoidingKeywords :: Symbolic a => a -> NameM a
renameTPTP :: Symbolic a => a -> a
showProblem :: Problem Form -> String
pPrintProblem :: Problem Form -> Doc
pPrintDecls :: Problem Form -> [Doc]
sexp :: [Doc] -> Doc
pPrintName :: Name -> Doc
pPrintType :: Type -> Doc
pPrintInput :: Input Form -> Doc
pPrintForm :: Form -> Doc
pPrintQuant :: Doc -> Set Variable -> Form -> Doc
pPrintAtomic :: Atomic -> Doc
pPrintTerm :: Term -> Doc

module Jukebox.Toolbox
data GlobalFlags
GlobalFlags :: Bool -> GlobalFlags
[quiet] :: GlobalFlags -> Bool
globalFlags :: OptionParser GlobalFlags
data TSTPFlags
TSTPFlags :: Bool -> TSTPFlags
[tstp] :: TSTPFlags -> Bool
tstpFlags :: OptionParser TSTPFlags
comment :: String -> IO ()
quietly :: GlobalFlags -> IO () -> IO ()
indent :: String -> String
(=>>=) :: OptionParser (a -> IO b) -> OptionParser (b -> IO c) -> OptionParser (a -> IO c)
infixl 1 =>>=
(=>>) :: OptionParser (IO a) -> OptionParser (IO b) -> OptionParser (IO b)
infixl 1 =>>
forAllFilesBox :: OptionParser ((FilePath -> IO ()) -> IO ())
forAllFiles :: [FilePath] -> (FilePath -> IO ()) -> IO ()
readTPTPFileBox :: OptionParser (FilePath -> IO String)
readTPTPFile :: [FilePath] -> FilePath -> IO String
readProblemBox :: OptionParser (FilePath -> IO (Problem Form))
readProblem :: [FilePath] -> FilePath -> IO (Problem Form)
printProblemBox :: OptionParser (Problem Form -> IO ())
printProblemSMTBox :: OptionParser (Problem Form -> IO ())
printClausesBox :: OptionParser (Problem Clause -> IO ())
prettyPrintIO :: (a -> String) -> (String -> IO ()) -> a -> IO ()
writeFileBox :: OptionParser (String -> IO ())
clausifyBox :: OptionParser (Problem Form -> IO CNF)
oneConjectureBox :: OptionParser (CNF -> IO (Problem Clause))
oneConjecture :: Maybe Int -> CNF -> IO (Problem Clause)
toFormulasBox :: OptionParser (Problem Clause -> IO (Problem Form))
type Solver = (IO () -> IO ()) -> Problem Clause -> IO Answer
forAllConjecturesBox :: OptionParser (Solver -> CNF -> IO ())
forAllConjectures :: TSTPFlags -> Solver -> CNF -> IO ()
toFofBox :: OptionParser (Problem Form -> IO (Problem Form))
toFof :: (Problem Form -> IO CNF) -> Scheme -> Problem Form -> IO (Problem Form)
schemeBox :: OptionParser Scheme
analyseMonotonicityBox :: OptionParser (Problem Clause -> IO (Set Type))
showMonotonicityBox :: OptionParser (Problem Clause -> IO String)
guessModelBox :: OptionParser (Problem Form -> IO (Problem Form))
inferBox :: OptionParser (Problem Clause -> IO (Problem Clause, Type -> Type))
printInferredBox :: OptionParser ((Problem Clause, Type -> Type) -> IO (Problem Clause))
hornToUnitBox :: OptionParser (Problem Clause -> IO (Either Answer (Problem Clause)))
hornToUnitIO :: HornFlags -> Problem Clause -> IO (Either Answer (Problem Clause))
instance GHC.Show.Show Jukebox.Toolbox.TSTPFlags
instance GHC.Show.Show Jukebox.Toolbox.GlobalFlags

module Jukebox.ExternalProvers.SPASS
data SPASSFlags
SPASSFlags :: String -> Maybe Int -> Bool -> SPASSFlags
[spass] :: SPASSFlags -> String
[timeout] :: SPASSFlags -> Maybe Int
[sos] :: SPASSFlags -> Bool
spassFlags :: OptionParser SPASSFlags
runSPASS :: SPASSFlags -> Problem Form -> IO Answer
extractAnswer :: String -> Answer

module Jukebox.ExternalProvers.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 :: EFlags -> Problem Form -> IO (Either Answer [Term])
extractAnswer :: Symbolic a => a -> String -> Either Answer [Term]