ProveSatallax.hs revision d2109cd698ad58a46bcd9df9bbb5856eb152dbd2
4b9f1c9f95296f3292b2e53dbc3d196751b862dbJonathan von SchroederModule : $Header$
4b9f1c9f95296f3292b2e53dbc3d196751b862dbJonathan von SchroederDescription : Interface to the Satallax theorem prover.
4b9f1c9f95296f3292b2e53dbc3d196751b862dbJonathan von SchroederCopyright : (c) Jonathan von Schroeder, DFKI Bremen 2012
4b9f1c9f95296f3292b2e53dbc3d196751b862dbJonathan von SchroederLicense : GPLv2 or higher, see LICENSE.txt
ad1df93673cf323534cdfe18981ad5daae4c90c0Jonathan von SchroederMaintainer : Jonathan von Schroeder <jonathan.von_schroeder@dfki.de>
4b9f1c9f95296f3292b2e53dbc3d196751b862dbJonathan von SchroederStability : provisional
4b9f1c9f95296f3292b2e53dbc3d196751b862dbJonathan von SchroederPortability : non-portable
4b9f1c9f95296f3292b2e53dbc3d196751b862dbJonathan von SchroederSatallax theorem prover for THF0
4b9f1c9f95296f3292b2e53dbc3d196751b862dbJonathan von Schroedermodule THF.ProveSatallax ( satallaxProver ) where
4b9f1c9f95296f3292b2e53dbc3d196751b862dbJonathan von Schroederimport Data.List (stripPrefix)
4b9f1c9f95296f3292b2e53dbc3d196751b862dbJonathan von Schroederimport Data.Maybe (fromMaybe)
4b9f1c9f95296f3292b2e53dbc3d196751b862dbJonathan von Schroederpfun :: ProverFuncs
4b9f1c9f95296f3292b2e53dbc3d196751b862dbJonathan von Schroederpfun = ProverFuncs {
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder cfgTimeout = maybe 10 (+ 1) . timeLimit,
4b9f1c9f95296f3292b2e53dbc3d196751b862dbJonathan von Schroeder proverCommand = \ tout tmpFile _ ->
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder return ("time", ["satallax", "-t", show tout, tmpFile]),
4b9f1c9f95296f3292b2e53dbc3d196751b862dbJonathan von Schroeder getMessage = \ res' _ _ -> res',
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder getTimeUsed = \ line -> case fromMaybe "" $ stripPrefix "real\t" line of
4b9f1c9f95296f3292b2e53dbc3d196751b862dbJonathan von Schroeder s -> let sp p str = case dropWhile p str of
4b9f1c9f95296f3292b2e53dbc3d196751b862dbJonathan von Schroeder s' -> w : sp p s''
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder where (w, s'') = break p s'
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder (m : secs : _) = sp (== 'm') s
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder in Just $ read m * 60 + read secs }
4b9f1c9f95296f3292b2e53dbc3d196751b862dbJonathan von SchroedersatallaxProver :: ProverType
d2109cd698ad58a46bcd9df9bbb5856eb152dbd2cmaedersatallaxProver = createSZSProver "satallax" "Satallax"
4b9f1c9f95296f3292b2e53dbc3d196751b862dbJonathan von Schroeder ("Satallax is an automated theorem prover for higher-order logic."
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder ++ " The particular form of higher-order logic supported by Satallax"
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder ++ " is Church's simple type theory with extensionality and choice operators.")