ProveSatallax.hs revision 87d946b3c13ffd7f6391aa796e786c2b31b122b1
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
4b9f1c9f95296f3292b2e53dbc3d196751b862dbJonathan von SchroederMaintainer : Jonathan von Schroeder <j.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
4b9f1c9f95296f3292b2e53dbc3d196751b862dbJonathan von SchroedersatallaxProver = createSZSProver "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.")