ProveSatallax.hs revision 4b9f1c9f95296f3292b2e53dbc3d196751b862db
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 {
4b9f1c9f95296f3292b2e53dbc3d196751b862dbJonathan von Schroeder cfgTimeout = \ cfg -> maybe 10 (+1) (timeLimit cfg),
4b9f1c9f95296f3292b2e53dbc3d196751b862dbJonathan von Schroeder proverCommand = \ tout tmpFile _ ->
4b9f1c9f95296f3292b2e53dbc3d196751b862dbJonathan von Schroeder return ("time",["satallax", "-t", show tout, tmpFile]),
4b9f1c9f95296f3292b2e53dbc3d196751b862dbJonathan von Schroeder getMessage = \ res' _ _ -> res',
4b9f1c9f95296f3292b2e53dbc3d196751b862dbJonathan 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''
4b9f1c9f95296f3292b2e53dbc3d196751b862dbJonathan von Schroeder where (w,s'') = break p s'
4b9f1c9f95296f3292b2e53dbc3d196751b862dbJonathan von Schroeder (m:secs:_) = sp (=='m') s
4b9f1c9f95296f3292b2e53dbc3d196751b862dbJonathan 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."
4b9f1c9f95296f3292b2e53dbc3d196751b862dbJonathan von Schroeder ++" The particular form of higher-order logic supported by Satallax"
4b9f1c9f95296f3292b2e53dbc3d196751b862dbJonathan von Schroeder ++" is Church's simple type theory with extensionality and choice operators.")