Documentation

data GlobalFlags Source #

globalFlags :: OptionParser GlobalFlags Source #

data TSTPFlags Source #

tstpFlags :: OptionParser TSTPFlags Source #

comment :: String -> IO () Source #

quietly :: GlobalFlags -> IO () -> IO () Source #

indent :: String -> String Source #

(=>>=) :: OptionParser (a -> IO b) -> OptionParser (b -> IO c) -> OptionParser (a -> IO c) infixl 1 Source #

(=>>) :: OptionParser (IO a) -> OptionParser (IO b) -> OptionParser (IO b) infixl 1 Source #

forAllFilesBox :: OptionParser ((FilePath -> IO ()) -> IO ()) Source #

forAllFiles :: [FilePath] -> (FilePath -> IO ()) -> IO () Source #

readProblemBox :: OptionParser (FilePath -> IO (Problem Form)) Source #

readProblem :: [FilePath] -> FilePath -> IO (Problem Form) Source #

printProblemBox :: OptionParser (Problem Form -> IO ()) Source #

printProblemSMTBox :: OptionParser (Problem Form -> IO ()) Source #

printClausesBox :: OptionParser (Problem Clause -> IO ()) Source #

prettyPrintIO :: (a -> String) -> (String -> IO ()) -> a -> IO () Source #

writeFileBox :: OptionParser (String -> IO ()) Source #

clausifyBox :: OptionParser (Problem Form -> IO CNF) Source #

oneConjectureBox :: OptionParser (CNF -> IO (Problem Clause)) Source #

oneConjecture :: Maybe Int -> CNF -> IO (Problem Clause) Source #

toFormulasBox :: OptionParser (Problem Clause -> IO (Problem Form)) Source #

type Solver = (IO () -> IO ()) -> Problem Clause -> IO Answer Source #

forAllConjecturesBox :: OptionParser (Solver -> CNF -> IO ()) Source #

forAllConjectures :: TSTPFlags -> Solver -> CNF -> IO () Source #

toFofBox :: OptionParser (Problem Form -> IO (Problem Form)) Source #

toFof :: (Problem Form -> IO CNF) -> Scheme -> Problem Form -> IO (Problem Form) Source #

schemeBox :: OptionParser Scheme Source #

analyseMonotonicityBox :: OptionParser (Problem Clause -> IO (Set Type)) Source #

showMonotonicityBox :: OptionParser (Problem Clause -> IO String) Source #

guessModelBox :: OptionParser (Problem Form -> IO (Problem Form)) Source #

inferBox :: OptionParser (Problem Clause -> IO (Problem Clause, Type -> Type)) Source #

printInferredBox :: OptionParser ((Problem Clause, Type -> Type) -> IO (Problem Clause)) Source #

hornToUnitBox :: OptionParser (Problem Clause -> IO (Either Answer (Problem Clause))) Source #

hornToUnitIO :: HornFlags -> Problem Clause -> IO (Either Answer (Problem Clause)) Source #