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

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 :: String -> TokenStream
data Pos
Pos :: {-# UNPACK #-} !Word -> {-# UNPACK #-} !Word -> Pos
data Token
Atom :: !Keyword -> !String -> Token
[keyword] :: Token -> !Keyword
[tokenName] :: Token -> !String
Defined :: !Defined -> Token
[defined] :: Token -> !Defined
Var :: !String -> Token
[tokenName] :: Token -> !String
DistinctObject :: !String -> Token
[tokenName] :: Token -> !String
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
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
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
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 Position a 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.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.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.Utils
usort :: Ord a => [a] -> [a]
merge :: Ord a => [a] -> [a] -> [a]
popen :: FilePath -> [String] -> String -> IO (ExitCode, String)

module Jukebox.Name
data Name
Fixed :: !FixedName -> Name
Unique :: {-# UNPACK #-} !Int64 -> String -> 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
renamer :: Named a => a -> Renamer
defaultRenamer :: Renamer
withRenamer :: Name -> Renamer -> Name
compareName :: Name -> Either FixedName Int64
class Named a
name :: Named a => a -> 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 GHC.Show.Show Jukebox.Name.FixedName
instance GHC.Classes.Eq Jukebox.Name.Name
instance GHC.Classes.Ord Jukebox.Name.Name
instance GHC.Show.Show Jukebox.Name.Name
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 => Jukebox.Name.Named (a Jukebox.Name.::: b)

module Jukebox.Form
debugging :: Bool
data DomainSize
Finite :: Int -> DomainSize
Infinite :: DomainSize
data Type
O :: Type
Type :: !Name -> DomainSize -> DomainSize -> Type
[tname] :: Type -> !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 :: [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]] -> String -> String -> CNF
[axioms] :: CNF -> [Input Clause]
[conjectures] :: CNF -> [[Input Clause]]
[satisfiable] :: CNF -> String
[unsatisfiable] :: CNF -> String
toCNF :: [Input Clause] -> [[Input Clause]] -> CNF
newtype Clause
Clause :: (Bind [Literal]) -> Clause
clause :: [Signed Atomic] -> Clause
toForm :: Clause -> Form
toLiterals :: Clause -> [Literal]
type Tag = String
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 = [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
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 :: Set Variable -> Subst -> Subst
mapName :: Symbolic a => (Name -> Name) -> 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 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 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 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.Form.Input a)
instance Jukebox.Form.Symbolic Jukebox.Form.CNF
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

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 :: 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

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 :: [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.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)], (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 ()

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 (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.Monotonox.Monotonicity.Var
instance GHC.Classes.Eq Jukebox.Monotonox.Monotonicity.Var
instance GHC.Show.Show Jukebox.Monotonox.Monotonicity.Extension

module Jukebox.TPTP.Parse.Core
data ParseState
MkState :: ![Input Form] -> !(Map String Type) -> !(Map String [Function]) -> !(Map String Variable) -> !Int64 -> ParseState
type Parser = Parsec ParsecState
type ParsecState = UserState ParseState TokenStream
data IncludeStatement
Include :: String -> (Maybe [Tag]) -> IncludeStatement
initialState :: ParseState
initialStateFrom :: [Name] -> Map String Type -> Map String [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
defined' :: Stream a Token => (Defined -> Bool) -> Parsec a Defined
defined :: Stream a Token => Defined -> Parsec a Defined
variable :: Parsec ParsecState String
number :: Parsec ParsecState Integer
ratNumber :: Parsec ParsecState Rational
realNumber :: Parsec ParsecState Rational
atom :: Parsec ParsecState String
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 :: String -> FunType -> Parser Function
showTypes :: [FunType] -> String
applyFunction :: String -> [Term] -> Type -> Parser Term
typeError :: Stream a c => [(:::) Name FunType] -> [Term] -> Parsec a b
lookupType :: String -> Parser Type
lookupFunction :: FunType -> String -> Parser [Name ::: FunType]
individual :: Type
cnf :: Parser Form
tff :: Parser Form
fof :: Parser Form
data Thing
Apply :: !String -> ![Term] -> Thing
Term :: !Term -> Thing
Formula :: !Form -> Thing
class TermLike a
fromThing :: TermLike a => Thing -> Parser a
var :: TermLike a => Mode -> Map String Variable -> Parser a
parser :: TermLike a => Mode -> Map String Variable -> Parser a
data Mode
Typed :: Mode
Untyped :: Mode
NoQuantification :: Mode
class TermLike a => FormulaLike a
fromFormula :: FormulaLike a => Form -> a
term :: TermLike a => Mode -> Map String Variable -> Parser a
intType :: Type
ratType :: Type
realType :: Type
literal :: FormulaLike a => Mode -> Map String Variable -> Parser a
unitary :: FormulaLike a => Mode -> Map String Variable -> Parser a
quantified :: FormulaLike a => Mode -> Map String Variable -> Parser a
formula :: FormulaLike a => Mode -> Map String 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.Parsec.Stream Jukebox.TPTP.Lexer.TokenStream Jukebox.TPTP.Lexer.Token
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 GHC.Show.Show Jukebox.TPTP.Parse.Core.Thing
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 Jukebox.TPTP.Parse.Core.FormulaLike Jukebox.Form.Form
instance Jukebox.TPTP.Parse.Core.FormulaLike Jukebox.TPTP.Parse.Core.Thing

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

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

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 :: SPASSFlags -> Problem Form -> IO Answer
extractAnswer :: String -> Answer

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.Clausify
newtype ClausifyFlags
ClausifyFlags :: Bool -> ClausifyFlags
[splitting] :: ClausifyFlags -> Bool
clausifyFlags :: OptionParser ClausifyFlags
clausify :: ClausifyFlags -> Problem Form -> CNF
split :: Form -> [Form]
clausForm :: String -> 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.Clausify.ClausifyFlags

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)
infixl 1 =>>=
(=>>) :: (Monad m, Applicative f) => f (m a) -> f (m b) -> f (m b)
infixl 1 =>>
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 :: GlobalFlags -> [FilePath] -> FilePath -> IO (Problem Form)
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))
prettyPrintProblemBox :: OptionParser (Problem Form -> IO ())
prettyPrintProblemSMTBox :: OptionParser (Problem Form -> IO ())
prettyPrintClausesBox :: OptionParser (Problem Clause -> IO ())
prettyPrintIO :: (a -> String) -> GlobalFlags -> (String -> IO ()) -> 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) -> CNF -> IO ())
allObligsIO :: ([Input Clause] -> IO Answer) -> CNF -> IO ()
inferBox :: OptionParser (Problem Clause -> IO (Problem Clause, Type -> Type))
printInferredBox :: OptionParser ((Problem Clause, Type -> Type) -> IO (Problem Clause))
instance GHC.Show.Show Jukebox.Toolbox.GlobalFlags