{- |
Module      :  ./THF/ProveLeoII.hs
Description :  Interface to the Leo II 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

Leo II theorem prover for THF0
-}

module THF.ProveLeoII ( leoIIProver ) where

import THF.SZSProver
import Interfaces.GenericATPState
import Data.List (stripPrefix)
import Data.Maybe (fromMaybe)

pfun :: ProverFuncs
pfun :: ProverFuncs
pfun = ProverFuncs :: (GenericConfig ProofTree -> Int)
-> (Int
    -> String -> GenericConfig ProofTree -> IO (String, [String]))
-> (String -> String -> String -> String)
-> (String -> Maybe Int)
-> ProverFuncs
ProverFuncs {
 cfgTimeout :: GenericConfig ProofTree -> Int
cfgTimeout = Int -> (Int -> Int) -> Maybe Int -> Int
forall b a. b -> (a -> b) -> Maybe a -> b
maybe 601 (Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 20) (Maybe Int -> Int)
-> (GenericConfig ProofTree -> Maybe Int)
-> GenericConfig ProofTree
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenericConfig ProofTree -> Maybe Int
forall proof_tree. GenericConfig proof_tree -> Maybe Int
timeLimit,
 proverCommand :: Int -> String -> GenericConfig ProofTree -> IO (String, [String])
proverCommand = \ tout :: Int
tout tmpFile :: String
tmpFile _ ->
  let extraOptions :: String
extraOptions = ("-po 0 -t " String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String) -> (Int -> String) -> Int -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String
forall a. Show a => a -> String
show (Int -> String) -> Int -> String
forall a b. (a -> b) -> a -> b
$ Int
tout
  in (String, [String]) -> IO (String, [String])
forall (m :: * -> *) a. Monad m => a -> m a
return ("leo", String -> [String]
words String
extraOptions [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
tmpFile]),
 getMessage :: String -> String -> String -> String
getMessage = \ res' :: String
res' _ perr :: String
perr -> let msg :: String
msg = String
res' String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
perr
                               in if Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
msg then String
msg
                                  else [String] -> String
unlines
                                   ["Leo seem to have terminated early.",
                                    "Probably increasing the timelimit",
                                    "will help." ],
 getTimeUsed :: String -> Maybe Int
getTimeUsed = \ line :: String
line ->
  case String -> [String]
words (String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe "" (Maybe String -> String) -> Maybe String -> String
forall a b. (a -> b) -> a -> b
$ String -> String -> Maybe String
forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix "# Total time" String
line) of
   _ : (tim :: String
tim : _) -> Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ Float -> Int
forall a b. (RealFrac a, Integral b) => a -> b
round (Float -> Int) -> Float -> Int
forall a b. (a -> b) -> a -> b
$ (String -> Float
forall a. Read a => String -> a
read String
tim :: Float) Float -> Float -> Float
forall a. Num a => a -> a -> a
* 1000
   _ -> Maybe Int
forall a. Maybe a
Nothing }

leoIIHelpText :: String
leoIIHelpText :: String
leoIIHelpText =
  "No help available yet.\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
  "email hets-devel@informatik.uni-bremen.de " String -> String -> String
forall a. [a] -> [a] -> [a]
++
  "for more information.\n"

leoIIProver :: ProverType
leoIIProver :: ProverType
leoIIProver = String -> String -> String -> ProverFuncs -> ProverType
createSZSProver "leo" "Leo II"
 String
leoIIHelpText ProverFuncs
pfun