{- |
Module      :  ./TPTP/Prover/EProver.hs
Description :  Interface for the E Theorem Prover.
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.Common where

import TPTP.Prover.ProverState
import TPTP.Morphism
import TPTP.Sign
import TPTP.Sublogic

import Common.AS_Annotation
import Common.ProofTree
import Common.Result
import Common.SZSOntology
import Common.Timing
import Common.Utils
import GUI.GenericATP
import Interfaces.GenericATPState hiding (proverState, timeUsed)
import Logic.Prover
import Proofs.BatchProcessing

import qualified Control.Concurrent as Concurrent
import Control.Monad
import Data.Char (toUpper)
import Data.Maybe
import Data.Time.LocalTime
import System.Directory
import System.Exit

type AtpFunType =
  String -> ATPFunctions Sign Sentence Morphism ProofTree ProverState

type RunTheProverType =
     ProverState
     {- ^ logical part containing the input Sign and axioms and possibly
     goals that have been proved earlier as additional axioms -}
  -> GenericConfig ProofTree -- ^ configuration to use
  -> Bool -- ^ True means save TPTP file
  -> String -- ^ name of the theory in the DevGraph
  -> Named Sentence -- ^ goal to prove
  -> IO (ATPRetval, GenericConfig ProofTree)
     -- ^ (retval, configuration with proof status and complete output)

mkProver :: String
         -> String
         -> Sublogic
         -> RunTheProverType
         -> Prover Sign Sentence Morphism Sublogic ProofTree
mkProver :: String
-> String
-> Sublogic
-> RunTheProverType
-> Prover Sign Sentence Morphism Sublogic ProofTree
mkProver binary_name :: String
binary_name prover_name :: String
prover_name sublogics :: Sublogic
sublogics runTheProver :: RunTheProverType
runTheProver =
  String
-> String
-> Sublogic
-> (String
    -> Theory Sign Sentence ProofTree
    -> [FreeDefMorphism Sentence Morphism]
    -> IO [ProofStatus ProofTree])
-> (Bool
    -> Bool
    -> MVar (Result [ProofStatus ProofTree])
    -> String
    -> TacticScript
    -> Theory Sign Sentence ProofTree
    -> [FreeDefMorphism Sentence Morphism]
    -> IO (ThreadId, MVar ()))
-> Prover Sign Sentence Morphism Sublogic ProofTree
forall sublogics theory sentence morphism proof_tree.
String
-> String
-> sublogics
-> (String
    -> theory
    -> [FreeDefMorphism sentence morphism]
    -> IO [ProofStatus proof_tree])
-> (Bool
    -> Bool
    -> MVar (Result [ProofStatus proof_tree])
    -> String
    -> TacticScript
    -> theory
    -> [FreeDefMorphism sentence morphism]
    -> IO (ThreadId, MVar ()))
-> ProverTemplate theory sentence morphism sublogics proof_tree
mkAutomaticProver String
binary_name String
prover_name Sublogic
sublogics String
-> Theory Sign Sentence ProofTree
-> [FreeDefMorphism Sentence Morphism]
-> IO [ProofStatus ProofTree]
proverGUI Bool
-> Bool
-> MVar (Result [ProofStatus ProofTree])
-> String
-> TacticScript
-> Theory Sign Sentence ProofTree
-> [FreeDefMorphism Sentence Morphism]
-> IO (ThreadId, MVar ())
proverCLI
  where
    atpFun :: String
           -> ATPFunctions Sign Sentence Morphism ProofTree ProverState
    atpFun :: String -> ATPFunctions Sign Sentence Morphism ProofTree ProverState
atpFun theoryName :: String
theoryName = ATPFunctions :: forall sign sentence morphism proof_tree pst.
InitialProverState sign sentence morphism pst
-> TransSenName
-> (pst -> Named sentence -> pst)
-> (pst -> Named sentence -> [String] -> IO String)
-> String
-> String
-> FileExtensions
-> RunProver sentence proof_tree pst
-> (GenericConfig proof_tree -> [String])
-> ATPFunctions sign sentence morphism proof_tree pst
ATPFunctions
      { initialProverState :: InitialProverState Sign Sentence Morphism ProverState
initialProverState = InitialProverState Sign Sentence Morphism ProverState
tptpProverState,
        atpTransSenName :: TransSenName
atpTransSenName = TransSenName
forall a. a -> a
id,
        atpInsertSentence :: ProverState -> Named Sentence -> ProverState
atpInsertSentence = ProverState -> Named Sentence -> ProverState
insertSentenceIntoProverState,
        goalOutput :: ProverState -> Named Sentence -> [String] -> IO String
goalOutput = String -> ProverState -> Named Sentence -> [String] -> IO String
ioShowTPTPProblem String
theoryName,
        proverHelpText :: String
proverHelpText = String
helpText,
        batchTimeEnv :: String
batchTimeEnv = "HETS_" String -> TransSenName
forall a. [a] -> [a] -> [a]
++ (Char -> Char) -> TransSenName
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toUpper String
prover_name String -> TransSenName
forall a. [a] -> [a] -> [a]
++ "_BATCH_TIME_LIMIT",
        fileExtensions :: FileExtensions
fileExtensions =
          FileExtensions :: String -> String -> String -> FileExtensions
FileExtensions { problemOutput :: String
problemOutput = ".tptp"
                         , proverOutput :: String
proverOutput = "."String -> TransSenName
forall a. [a] -> [a] -> [a]
++ String
prover_name String -> TransSenName
forall a. [a] -> [a] -> [a]
++ ".out"
                         , theoryConfiguration :: String
theoryConfiguration = "." String -> TransSenName
forall a. [a] -> [a] -> [a]
++ String
prover_name String -> TransSenName
forall a. [a] -> [a] -> [a]
++ ".conf"
                         },
        runProver :: RunTheProverType
runProver = RunTheProverType
runTheProver,
        createProverOptions :: GenericConfig ProofTree -> [String]
createProverOptions = GenericConfig ProofTree -> [String]
forall proof_tree. GenericConfig proof_tree -> [String]
extraOpts}

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

    proverGUI :: String
              -> Theory Sign Sentence ProofTree
              -> [FreeDefMorphism Sentence Morphism]
              -> IO [ProofStatus ProofTree]
    proverGUI :: String
-> Theory Sign Sentence ProofTree
-> [FreeDefMorphism Sentence Morphism]
-> IO [ProofStatus ProofTree]
proverGUI theoryName :: String
theoryName theory :: Theory Sign Sentence ProofTree
theory freenessConstraints :: [FreeDefMorphism Sentence Morphism]
freenessConstraints =
      ATPFunctions Sign Sentence Morphism ProofTree ProverState
-> Bool
-> String
-> String
-> Theory Sign Sentence ProofTree
-> [FreeDefMorphism Sentence Morphism]
-> ProofTree
-> IO [ProofStatus ProofTree]
forall sentence proof_tree sign mor pst.
(Show sentence, Ord proof_tree, Ord sentence) =>
ATPFunctions sign sentence mor proof_tree pst
-> Bool
-> String
-> String
-> Theory sign sentence proof_tree
-> [FreeDefMorphism sentence mor]
-> proof_tree
-> IO [ProofStatus proof_tree]
genericATPgui
        (String -> ATPFunctions Sign Sentence Morphism ProofTree ProverState
atpFun String
theoryName)
        Bool
True
        String
prover_name
        String
theoryName
        Theory Sign Sentence ProofTree
theory
        [FreeDefMorphism Sentence Morphism]
freenessConstraints
        ProofTree
emptyProofTree

    proverCLI :: Bool
              -> Bool
              -> Concurrent.MVar (Result [ProofStatus ProofTree])
              -> String
              -> TacticScript
              -> Theory Sign Sentence ProofTree
              -> [FreeDefMorphism Sentence Morphism]
              -> IO (Concurrent.ThreadId, Concurrent.MVar ())
    proverCLI :: Bool
-> Bool
-> MVar (Result [ProofStatus ProofTree])
-> String
-> TacticScript
-> Theory Sign Sentence ProofTree
-> [FreeDefMorphism Sentence Morphism]
-> IO (ThreadId, MVar ())
proverCLI includeProvedTheorems :: Bool
includeProvedTheorems saveProblemFile :: Bool
saveProblemFile batchResultStore :: MVar (Result [ProofStatus ProofTree])
batchResultStore theoryName :: String
theoryName
                defaultTacticScript :: TacticScript
defaultTacticScript theory :: Theory Sign Sentence ProofTree
theory freenessConstraints :: [FreeDefMorphism Sentence Morphism]
freenessConstraints =
      ATPFunctions Sign Sentence Morphism ProofTree ProverState
-> Bool
-> Bool
-> MVar (Result [ProofStatus ProofTree])
-> String
-> String
-> ATPTacticScript
-> Theory Sign Sentence ProofTree
-> [FreeDefMorphism Sentence Morphism]
-> ProofTree
-> IO (ThreadId, MVar ())
forall sentence proof_tree sign mor pst.
(Show sentence, Ord proof_tree, Ord sentence) =>
ATPFunctions sign sentence mor proof_tree pst
-> Bool
-> Bool
-> MVar (Result [ProofStatus proof_tree])
-> String
-> String
-> ATPTacticScript
-> Theory sign sentence proof_tree
-> [FreeDefMorphism sentence mor]
-> proof_tree
-> IO (ThreadId, MVar ())
genericCMDLautomaticBatch
        (String -> ATPFunctions Sign Sentence Morphism ProofTree ProverState
atpFun String
theoryName)
        Bool
includeProvedTheorems
        Bool
saveProblemFile
        MVar (Result [ProofStatus ProofTree])
batchResultStore
        String
prover_name
        String
theoryName
        (TacticScript -> ATPTacticScript
parseProverTacticScript TacticScript
defaultTacticScript)
        Theory Sign Sentence ProofTree
theory
        [FreeDefMorphism Sentence Morphism]
freenessConstraints
        ProofTree
emptyProofTree

    parseProverTacticScript :: TacticScript -> ATPTacticScript
    parseProverTacticScript :: TacticScript -> ATPTacticScript
parseProverTacticScript = Int -> [String] -> TacticScript -> ATPTacticScript
parseTacticScript Int
batchTimeLimit []


mkTheoryFileName :: String -> Named Sentence -> String
mkTheoryFileName :: String -> Named Sentence -> String
mkTheoryFileName theoryName :: String
theoryName namedGoal :: Named Sentence
namedGoal =
  TransSenName
basename (String
theoryName String -> TransSenName
forall a. [a] -> [a] -> [a]
++ '_' Char -> TransSenName
forall a. a -> [a] -> [a]
: Named Sentence -> String
forall s a. SenAttr s a -> a
senAttr Named Sentence
namedGoal String -> TransSenName
forall a. [a] -> [a] -> [a]
++ ".tptp")

getTimeLimit :: GenericConfig ProofTree -> Int
getTimeLimit :: GenericConfig ProofTree -> Int
getTimeLimit cfg :: GenericConfig ProofTree
cfg = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe 100 (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ GenericConfig ProofTree -> Maybe Int
forall proof_tree. GenericConfig proof_tree -> Maybe Int
timeLimit GenericConfig ProofTree
cfg

hardTimeLimit :: GenericConfig ProofTree -> Int
hardTimeLimit :: GenericConfig ProofTree -> Int
hardTimeLimit cfg :: GenericConfig ProofTree
cfg =
  let configuredTimeLimit :: Int
configuredTimeLimit = GenericConfig ProofTree -> Int
getTimeLimit GenericConfig ProofTree
cfg
  in [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum [ Int
configuredTimeLimit Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 30
             , Double -> Int
forall a b. (RealFrac a, Integral b) => a -> b
round ((1.5 :: Double) Double -> Double -> Double
forall a. Num a => a -> a -> a
* Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
configuredTimeLimit)
             ]

gnuTimeout :: IO String
gnuTimeout :: IO String
gnuTimeout = do
  Maybe String
path <- String -> IO (Maybe String)
findExecutable "gtimeout"
  String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> IO String) -> String -> IO String
forall a b. (a -> b) -> a -> b
$ if Maybe String -> Bool
forall a. Maybe a -> Bool
isJust Maybe String
path then "gtimeout" else "timeout"


prepareProverInput :: ProverState
                   -> GenericConfig ProofTree
                   -> Bool
                   -> String
                   -> Named Sentence
                   -> String
                   -> IO String
prepareProverInput :: ProverState
-> GenericConfig ProofTree
-> Bool
-> String
-> Named Sentence
-> String
-> IO String
prepareProverInput proverState :: ProverState
proverState cfg :: GenericConfig ProofTree
cfg saveTPTPFile :: Bool
saveTPTPFile theoryName :: String
theoryName namedGoal :: Named Sentence
namedGoal prover_name :: String
prover_name =
  do
    let theoryFileName :: String
theoryFileName = String -> Named Sentence -> String
mkTheoryFileName String
theoryName Named Sentence
namedGoal
    String
tptpProblemString <- IO String
getProblemString
    String
problemFileName <- String -> String -> IO String
getTempFile String
tptpProblemString String
theoryFileName
    String -> String -> IO ()
saveProblemFileIfNeeded String
theoryFileName String
tptpProblemString
    String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return String
problemFileName
  where
    getProblemString :: IO String
    getProblemString :: IO String
getProblemString = String -> ProverState -> Named Sentence -> [String] -> IO String
ioShowTPTPProblem String
theoryName ProverState
proverState Named Sentence
namedGoal ([String] -> IO String) -> [String] -> IO String
forall a b. (a -> b) -> a -> b
$
        GenericConfig ProofTree -> [String]
forall proof_tree. GenericConfig proof_tree -> [String]
extraOpts GenericConfig ProofTree
cfg [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ["Requested prover: " String -> TransSenName
forall a. [a] -> [a] -> [a]
++ String
prover_name]

    saveProblemFileIfNeeded :: String -> String -> IO ()
    saveProblemFileIfNeeded :: String -> String -> IO ()
saveProblemFileIfNeeded theoryFileName :: String
theoryFileName tptpProblemString :: String
tptpProblemString =
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
saveTPTPFile (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> String -> IO ()
writeFile String
theoryFileName String
tptpProblemString

executeTheProver :: String -> [String] -> IO (ExitCode, [String], TimeOfDay)
executeTheProver :: String -> [String] -> IO (ExitCode, [String], TimeOfDay)
executeTheProver binary_name :: String
binary_name options :: [String]
options = do
  HetsTime
startTime <- IO HetsTime
getHetsTime
  (exitCode :: ExitCode
exitCode, pout :: String
pout, perr :: String
perr) <- String -> [String] -> String -> IO (ExitCode, String, String)
executeProcess String
binary_name [String]
options ""
  HetsTime
endTime <- ExitCode -> IO ExitCode
forall (m :: * -> *) a. Monad m => a -> m a
return ExitCode
exitCode IO ExitCode -> IO HetsTime -> IO HetsTime
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IO HetsTime
getHetsTime
  let wallTimeUsed :: TimeOfDay
wallTimeUsed = HetsTime -> HetsTime -> TimeOfDay
diffHetsTime HetsTime
endTime HetsTime
startTime
  let out :: [String]
out = String -> [String]
lines (String
perr String -> TransSenName
forall a. [a] -> [a] -> [a]
++ String
pout)
  (ExitCode, [String], TimeOfDay)
-> IO (ExitCode, [String], TimeOfDay)
forall (m :: * -> *) a. Monad m => a -> m a
return (ExitCode
exitCode, [String]
out, TimeOfDay
wallTimeUsed)

atpRetValAndProofStatus :: GenericConfig ProofTree
                        -> Named Sentence
                        -> TimeOfDay
                        -> [String]
                        -> String
                        -> String
                        -> (ATPRetval, ProofStatus ProofTree)
atpRetValAndProofStatus :: GenericConfig ProofTree
-> Named Sentence
-> TimeOfDay
-> [String]
-> String
-> String
-> (ATPRetval, ProofStatus ProofTree)
atpRetValAndProofStatus cfg :: GenericConfig ProofTree
cfg namedGoal :: Named Sentence
namedGoal = GenericConfig ProofTree
-> String
-> TimeOfDay
-> [String]
-> String
-> String
-> (ATPRetval, ProofStatus ProofTree)
atpRetValAndProofStatus' GenericConfig ProofTree
cfg (String
 -> TimeOfDay
 -> [String]
 -> String
 -> String
 -> (ATPRetval, ProofStatus ProofTree))
-> String
-> TimeOfDay
-> [String]
-> String
-> String
-> (ATPRetval, ProofStatus ProofTree)
forall a b. (a -> b) -> a -> b
$ Named Sentence -> String
forall s a. SenAttr s a -> a
senAttr Named Sentence
namedGoal

atpRetValAndProofStatus' :: GenericConfig ProofTree
                        -> String
                        -> TimeOfDay
                        -> [String]
                        -> String
                        -> String
                        -> (ATPRetval, ProofStatus ProofTree)
atpRetValAndProofStatus' :: GenericConfig ProofTree
-> String
-> TimeOfDay
-> [String]
-> String
-> String
-> (ATPRetval, ProofStatus ProofTree)
atpRetValAndProofStatus' cfg :: GenericConfig ProofTree
cfg nameOfGoal :: String
nameOfGoal timeUsed :: TimeOfDay
timeUsed axiomsUsed :: [String]
axiomsUsed szsStatusLine :: String
szsStatusLine prover_name :: String
prover_name =
  let statuses :: (ProofStatus ProofTree, ProofStatus ProofTree,
 ProofStatus ProofTree)
statuses = GenericConfig ProofTree
-> String
-> TimeOfDay
-> [String]
-> String
-> (ProofStatus ProofTree, ProofStatus ProofTree,
    ProofStatus ProofTree)
proofStatuses' GenericConfig ProofTree
cfg String
nameOfGoal TimeOfDay
timeUsed [String]
axiomsUsed String
prover_name
  in (ProofStatus ProofTree, ProofStatus ProofTree,
 ProofStatus ProofTree)
-> String -> (ATPRetval, ProofStatus ProofTree)
selectRetValAndProofStatus (ProofStatus ProofTree, ProofStatus ProofTree,
 ProofStatus ProofTree)
statuses String
szsStatusLine

selectRetValAndProofStatus :: (ProofStatus ProofTree,
                               ProofStatus ProofTree,
                               ProofStatus ProofTree)
                           -> String
                           -> (ATPRetval, ProofStatus ProofTree)
selectRetValAndProofStatus :: (ProofStatus ProofTree, ProofStatus ProofTree,
 ProofStatus ProofTree)
-> String -> (ATPRetval, ProofStatus ProofTree)
selectRetValAndProofStatus (defaultPS :: ProofStatus ProofTree
defaultPS, proved :: ProofStatus ProofTree
proved, disproved :: ProofStatus ProofTree
disproved) szsStatusLine :: String
szsStatusLine =
  case () of
    _ | String -> Bool
szsProved String
szsStatusLine    -> (ATPRetval
ATPSuccess, ProofStatus ProofTree
proved)
    _ | String -> Bool
szsDisproved String
szsStatusLine -> (ATPRetval
ATPSuccess, ProofStatus ProofTree
disproved)
    _ | String -> Bool
szsTimeout String
szsStatusLine   -> (ATPRetval
ATPTLimitExceeded, ProofStatus ProofTree
defaultPS)
    _ | String -> Bool
szsStopped String
szsStatusLine   -> (ATPRetval
ATPBatchStopped, ProofStatus ProofTree
defaultPS)
    _                              -> (String -> ATPRetval
ATPError String
szsStatusLine, ProofStatus ProofTree
defaultPS)

proofStatuses :: GenericConfig ProofTree
              -> Named Sentence
              -> TimeOfDay
              -> [String]
              -> String
              -> (ProofStatus ProofTree,
                  ProofStatus ProofTree,
                  ProofStatus ProofTree)
proofStatuses :: GenericConfig ProofTree
-> Named Sentence
-> TimeOfDay
-> [String]
-> String
-> (ProofStatus ProofTree, ProofStatus ProofTree,
    ProofStatus ProofTree)
proofStatuses cfg :: GenericConfig ProofTree
cfg namedGoal :: Named Sentence
namedGoal =
  GenericConfig ProofTree
-> String
-> TimeOfDay
-> [String]
-> String
-> (ProofStatus ProofTree, ProofStatus ProofTree,
    ProofStatus ProofTree)
proofStatuses' GenericConfig ProofTree
cfg (Named Sentence -> String
forall s a. SenAttr s a -> a
senAttr Named Sentence
namedGoal)

proofStatuses' :: GenericConfig ProofTree
              -> String
              -> TimeOfDay
              -> [String]
              -> String
              -> (ProofStatus ProofTree,
                  ProofStatus ProofTree,
                  ProofStatus ProofTree)
proofStatuses' :: GenericConfig ProofTree
-> String
-> TimeOfDay
-> [String]
-> String
-> (ProofStatus ProofTree, ProofStatus ProofTree,
    ProofStatus ProofTree)
proofStatuses' cfg :: GenericConfig ProofTree
cfg nameOfGoal :: String
nameOfGoal timeUsed :: TimeOfDay
timeUsed axiomsUsed :: [String]
axiomsUsed prover_name :: String
prover_name =
  let defaultPS :: ProofStatus ProofTree
defaultPS =
        (String -> String -> ProofTree -> ProofStatus ProofTree
forall pt. Ord pt => String -> String -> pt -> ProofStatus pt
openProofStatus String
nameOfGoal String
prover_name ProofTree
emptyProofTree)
          { usedTime :: TimeOfDay
usedTime = TimeOfDay
timeUsed
          , tacticScript :: TacticScript
tacticScript = String -> TacticScript
TacticScript (String -> TacticScript) -> String -> TacticScript
forall a b. (a -> b) -> a -> b
$ ATPTacticScript -> String
forall a. Show a => a -> String
show ATPTacticScript :: Int -> [String] -> ATPTacticScript
ATPTacticScript
             { tsTimeLimit :: Int
tsTimeLimit = GenericConfig ProofTree -> Int
forall proof_tree. GenericConfig proof_tree -> Int
configTimeLimit GenericConfig ProofTree
cfg
             , tsExtraOpts :: [String]
tsExtraOpts = GenericConfig ProofTree -> [String]
forall proof_tree. GenericConfig proof_tree -> [String]
extraOpts GenericConfig ProofTree
cfg } }
      disproved :: ProofStatus ProofTree
disproved = ProofStatus ProofTree
defaultPS { goalStatus :: GoalStatus
goalStatus = GoalStatus
Disproved }
      proved :: ProofStatus ProofTree
proved = ProofStatus ProofTree
defaultPS
        { goalStatus :: GoalStatus
goalStatus = Bool -> GoalStatus
Proved Bool
True
        , usedAxioms :: [String]
usedAxioms = [String]
axiomsUsed
        , usedProver :: String
usedProver = String
prover_name
        , usedTime :: TimeOfDay
usedTime = TimeOfDay
timeUsed
        }
  in  (ProofStatus ProofTree
defaultPS, ProofStatus ProofTree
proved, ProofStatus ProofTree
disproved)