{- |

Module : $Header$

Description : Interface to the Satallax theorem prover.

Copyright : (c) Jonathan von Schroeder, DFKI Bremen 2012

License : GPLv2 or higher, see LICENSE.txt

Maintainer : Jonathan von Schroeder <jonathan.von_schroeder@dfki.de>

Stability : provisional

Portability : non-portable

Satallax theorem prover for THF0

-}

module THF.ProveSatallax ( satallaxProver ) where

import THF.SZSProver

import Interfaces.GenericATPState

import Data.List (stripPrefix)

import Data.Maybe (fromMaybe)

pfun :: ProverFuncs

pfun = ProverFuncs {

cfgTimeout = maybe 10 (+ 1) . timeLimit,

proverCommand = \ tout tmpFile _ ->

return ("time", ["satallax", "-t", show tout, tmpFile]),

getMessage = \ res' _ _ -> res',

getTimeUsed = \ line -> case fromMaybe "" $ stripPrefix "real\t" line of

[] -> Nothing

s -> let sp p str = case dropWhile p str of

"" -> []

s' -> w : sp p s''

where (w, s'') = break p s'

(m : secs : _) = sp (== 'm') s

in Just $ read m * 60 + read secs }

satallaxProver :: ProverType

satallaxProver = createSZSProver "Satallax"

("Satallax is an automated theorem prover for higher-order logic."

++ " The particular form of higher-order logic supported by Satallax"

++ " is Church's simple type theory with extensionality and choice operators.")

pfun