Jukebox.Toolbox

Documentation

data GlobalFlags

Constructors

GlobalFlags

Fields

• quiet :: Bool

Instances

Show GlobalFlags

Methods

showsPrec :: Int -> GlobalFlags -> ShowS

show :: GlobalFlags -> String

showList :: [GlobalFlags] -> ShowS

globalFlags :: OptionParser GlobalFlags

data TSTPFlags

Constructors

TSTPFlags

Fields

• tstp :: Bool

Instances

Show TSTPFlags

Methods

showsPrec :: Int -> TSTPFlags -> ShowS

show :: TSTPFlags -> String

showList :: [TSTPFlags] -> ShowS

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 ()

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