01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederDescription : Interface to the Leo II theorem prover.
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerCopyright : (c) Jonathan von Schroeder, DFKI Bremen 2012
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiLicense : GPLv2 or higher, see LICENSE.txt
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuMaintainer : Jonathan von Schroeder <jonathan.von_schroeder@dfki.de>
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederStability : provisional
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederPortability : non-portable
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian MaederLeo II theorem prover for THF0
1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowskimodule THF.ProveLeoII ( leoIIProver ) where
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport Data.List (stripPrefix)
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport Data.Maybe (fromMaybe)
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederpfun :: ProverFuncs
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederpfun = ProverFuncs {
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder cfgTimeout = maybe 601 (+ 20) . timeLimit,
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder proverCommand = \ tout tmpFile _ ->
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder let extraOptions = ("-po 0 -t " ++) . show $ tout
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder in return ("leo", words extraOptions ++ [tmpFile]),
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder getMessage = \ res' _ perr -> let msg = res' ++ perr
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder in if not $ null msg then msg
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder ["Leo seem to have terminated early.",
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder "Probably increasing the timelimit",
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder "will help." ],
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder getTimeUsed = \ line ->
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder case words (fromMaybe "" $ stripPrefix "# Total time" line) of
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder _ : (tim : _) -> Just $ round $ (read tim :: Float) * 1000
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder _ -> Nothing }
351391e0e3226210e7ffb183b334da9f96de36eaChristian MaederleoIIHelpText :: String
351391e0e3226210e7ffb183b334da9f96de36eaChristian MaederleoIIHelpText =
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder "No help available yet.\n" ++
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder "email hets-devel@informatik.uni-bremen.de " ++
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder "for more information.\n"
351391e0e3226210e7ffb183b334da9f96de36eaChristian MaederleoIIProver :: ProverType
351391e0e3226210e7ffb183b334da9f96de36eaChristian MaederleoIIProver = createSZSProver "leo" "Leo II"
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder leoIIHelpText pfun