{- |

Module : ./TPTP/Prover/Vampire/ProofParser.hs

Description : Parses a Vampire proof.

Copyright : (c) Eugen Kuksa University of Magdeburg 2017

License : GPLv2 or higher, see LICENSE.txt

Maintainer : Eugen Kuksa <kuksa@iks.cs.ovgu.de>

Stability : provisional

Portability : non-portable (imports Logic)

-}

module TPTP.Prover.Vampire.ProofParser ( parseStatus

, parseTimeUsed

, filterProofLines

) where

import Common.Utils

import Data.Char

import Data.List hiding (lines)

import Data.Maybe

import Data.Time (TimeOfDay (..), midnight)

import Prelude hiding (lines)

parseStatus :: [String] -> String

parseStatus = fromMaybe "Unknown" . foldr parseStatusIfStatusline Nothing

where

parseStatusIfStatusline :: String -> Maybe String -> Maybe String

parseStatusIfStatusline line mStatus = case mStatus of

Nothing -> case () of

_ | isPrefixOf "Termination reason: Time limit" line -> Just "Timeout"

_ | isPrefixOf "Termination reason: Memory limit" line -> Just "MemoryOut"

_ | isPrefixOf "Termination reason: Refutation not found" line -> Just "GaveUp"

_ | isPrefixOf "Termination reason: Refutation" line -> Just "Theorem"

_ | isPrefixOf "Termination reason: Satisfiable" line -> Just "CounterSatisfiable" -- this is a model

_ | isPrefixOf "Termination reason: Unknown" line -> Just "Unknown"

_ -> mStatus

_ -> mStatus

parseTimeUsed :: [String] -> TimeOfDay

parseTimeUsed = fromMaybe midnight . foldr parseTimeUsedIfTimeLine Nothing

where

parseTimeUsedIfTimeLine :: String -> Maybe TimeOfDay -> Maybe TimeOfDay

parseTimeUsedIfTimeLine line mTime = case mTime of

Just _ -> mTime

Nothing -> case stripPrefix "Time elapsed: " line of

Just s -> Just $ parseTimeOfDay $

takeWhile (\ c -> isDigit c || c == '.') $ trimLeft s

Nothing -> mTime

parseTimeOfDay :: String -> TimeOfDay

parseTimeOfDay s = TimeOfDay

{ todHour = 0

, todMin = 0

, todSec = realToFrac (read s :: Double) }

data FilterState = Version | Separator | Proof deriving Show

-- filters the lines of the proof

-- The first line does not belong to the proof. The next lines before the

-- "------------------------------" belong to the proof.

-- Right after that separator, the version indicator appears.

filterProofLines :: [String] -> [String]

filterProofLines lines = fst $ foldr addIfInProof ([], Version) $ tail lines

where

addIfInProof :: String -> ([String], FilterState) -> ([String], FilterState)

addIfInProof line (addedLines, state) =

-- @state@ tells if the line is between "SZS output start/end".

-- Since the lines are in reverse order (by foldr), we need to parse after

-- the separator ("------------------------------").

case state of

Version ->

if isPrefixOf "Version: " line

then (addedLines, Separator)

else (addedLines, state)

Separator ->

if isPrefixOf "------------------------------" line

then (addedLines, Proof)

else (addedLines, state)

Proof -> (line : addedLines, state)