6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann{- |

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannModule : $Header$

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannDescription : Interface to the Isabelle theorem prover.

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannCopyright : (c) Jonathan von Schroeder, DFKI Bremen 2012

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannLicense : GPLv2 or higher, see LICENSE.txt

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannMaintainer : Jonathan von Schroeder <j.von_schroeder@dfki.de>

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannStability : provisional

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannPortability : non-portable

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannIsabelle theorem prover for THF0

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-}

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannmodule THF.ProveIsabelle ( isaProver, nitpickProver,

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann refuteProver, sledgehammerProver ) where

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport THF.SZSProver

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Interfaces.GenericATPState

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Data.List (isPrefixOf, stripPrefix)

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Data.Maybe (fromMaybe)

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannpfun :: String -> ProverFuncs

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannpfun tool = ProverFuncs {

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann cfgTimeout = maybe 20 (+ 10) . timeLimit,

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann proverCommand = \ tout tmpFile _ ->

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann return ("time", ["isabelle", tool, show (tout - 10), tmpFile]),

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann getMessage = \ res' pout _ ->

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann if null res' then concat $ filter (isPrefixOf "*** ") (lines pout)

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann else res',

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

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann [] -> Nothing

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann s -> let sp p str = case dropWhile p str of

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann "" -> []

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann s' -> w : sp p s''

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann where (w, s'') = break p s'

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann (m : secs : _) = sp (== 'm') s

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann in Just $ read m * 60 + read secs }

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannisaProver :: ProverType

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannisaProver = createSZSProver "Isabelle (automated)"

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann "Automated Isabelle calling all tools available"

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann $ pfun "tptp_isabelle_demo"

nitpickProver :: ProverType

nitpickProver = createSZSProver "Isabelle (nitpick)"

"Nitpick for TPTP problems"

$ pfun "tptp_nitpick"

refuteProver :: ProverType

refuteProver = createSZSProver "Isabelle (refute)"

"refute for TPTP problems"

$ pfun "tptp_refute"

sledgehammerProver :: ProverType

sledgehammerProver = createSZSProver "Isabelle (sledgehammer)"

"sledgehammer for TPTP problems"

$ pfun "tptp_sledgehammer"