module OWL2.ProveHermit
( runTimedHermit
, hermitJar
, hermitEnv
, hermitProver
, hermitConsChecker
) where
import Logic.Prover
import OWL2.Morphism
import OWL2.Sign
import OWL2.ProfilesAndSublogics
import OWL2.ProverState
import OWL2.AS
import GUI.GenericATP
import Interfaces.GenericATPState
import Proofs.BatchProcessing
import Common.AS_Annotation
import Common.ProofTree
import Common.Result as Result
import Common.ProverTools
import Common.Utils
import Data.Char (isDigit)
import Data.List (isPrefixOf)
import Data.Maybe
import Data.Time (timeToTimeOfDay)
import Data.Time.Clock (secondsToDiffTime)
import System.Directory
import Control.Monad (when)
import Control.Concurrent
import Debug.Trace
hermitS :: String
hermitS = "Hermit"
hermitJar :: String
hermitJar = "HermiT.jar"
hermitEnv :: String
hermitEnv = "HERMIT_PATH"
hermitCheck :: IO (Maybe String)
hermitCheck = fmap
(\ l ->
if null l
then Just $ hermitJar ++ " not found in $" ++ hermitEnv
else Nothing)
$ check4FileAux hermitJar hermitEnv
hermitProver :: Prover Sign Axiom OWLMorphism ProfSub ProofTree
hermitProver =
(mkAutomaticProver "java" hermitS dlS hermitGUI hermitCMDLautomaticBatch)
{ proverUsable = hermitCheck }
hermitConsChecker :: ConsChecker Sign Axiom ProfSub OWLMorphism ProofTree
hermitConsChecker = (mkConsChecker hermitS topS consCheck)
{ ccNeedsTimer = False
, ccUsable = hermitCheck }
atpFun :: String
-> ATPFunctions Sign Axiom OWLMorphism ProofTree ProverState
atpFun _ = ATPFunctions
{ initialProverState = owlProverState
, atpTransSenName = id
, atpInsertSentence = insertOWLAxiom
, goalOutput = \ a b _ -> showOWLProblem a b
, proverHelpText = "http://www.hermit-reasoner.com/using.html\n"
, batchTimeEnv = "HETS_HermiT_BATCH_TIME_LIMIT"
, fileExtensions = FileExtensions { problemOutput = ".owl"
, proverOutput = ".pellet"
, theoryConfiguration = ".pconf" }
, runProver = runHermit
, createProverOptions = extraOpts }
hermitGUI :: String
-> Theory Sign Axiom ProofTree
-> [FreeDefMorphism Axiom OWLMorphism]
-> IO [ProofStatus ProofTree]
hermitGUI thName th freedefs =
genericATPgui (atpFun thName) True hermitS thName th
freedefs emptyProofTree
hermitCMDLautomaticBatch ::
Bool
-> Bool
-> MVar (Result.Result [ProofStatus ProofTree])
-> String
-> TacticScript
-> Theory Sign Axiom ProofTree
-> [FreeDefMorphism Axiom OWLMorphism]
-> IO (ThreadId, MVar ())
hermitCMDLautomaticBatch inclProvedThs saveProblem_batch resultMVar
thName defTS th freedefs =
genericCMDLautomaticBatch (atpFun thName) inclProvedThs saveProblem_batch
resultMVar hermitS thName
(parseTacticScript batchTimeLimit [] defTS) th freedefs emptyProofTree
consCheck :: String
-> TacticScript
-> TheoryMorphism Sign Axiom OWLMorphism ProofTree
-> [FreeDefMorphism Axiom OWLMorphism]
-> IO (CCStatus ProofTree)
consCheck thName (TacticScript tl) tm freedefs = case tTarget tm of
Theory sig nSens -> do
let proverStateI = owlProverState sig (toNamedList nSens) freedefs
prob = showOWLProblemS proverStateI
pStatus out tUsed = CCStatus
{ ccResult = Nothing
, ccProofTree = ProofTree $ unlines out ++ "\n\n" ++ prob
, ccUsedTime = timeToTimeOfDay $ secondsToDiffTime $ toInteger tUsed }
tLim = readMaybe tl
res <- runTimedHermit "consistency" (basename thName ++ ".owl") prob Nothing
$ fromMaybe maxBound $ readMaybe tl
return $ case res of
Nothing -> pStatus ["Timeout after " ++ tl ++ " seconds"]
(fromMaybe (0 :: Int) tLim)
Just (progTh, outp, eOut) -> if progTh then
let (_, exCode, out, tUsed) = analyseOutput outp eOut
in (pStatus out tUsed) { ccResult = exCode }
else pStatus ["Hermit not found"] (0 :: Int)
runTimedHermit :: String
-> FilePath
-> String
-> Maybe String
-> Int
-> IO (Maybe (Bool, String, String))
runTimedHermit opts tmpFileName prob entail secs = do
(progTh, pPath) <- check4jarFile hermitEnv hermitJar
if progTh then withinDirectory pPath $ do
timeTmpFile <- getTempFile prob tmpFileName
timeTmpEnt <- getTempFile (fromMaybe "" entail) tmpFileName
let entFile = timeTmpFile ++ ".entail.owl"
doEntail = trace (show opts) (isJust entail)
args = "-Xmx1024M" : "-jar" : hermitJar
: (if doEntail then ["--premise=file://"++timeTmpFile, "--conclusion=file://"++entFile, "-E"]
else ["-k", timeTmpFile]) ++ words opts
case entail of
Just c -> writeFile entFile c
Nothing -> return ()
mex <- timeoutCommand secs "java" args
removeFile timeTmpEnt
when doEntail $ removeFile entFile
return $ fmap (\ (_, outS, errS) -> (True, outS, errS)) mex
else return $ Just (False, "", "")
runHermit :: ProverState
-> GenericConfig ProofTree
-> Bool
-> String
-> Named Axiom
-> IO (ATPRetval, GenericConfig ProofTree)
runHermit sps cfg saveHermit thName nGoal = do
let simpleOptions = extraOpts cfg
tLimit = fromMaybe 800 $ timeLimit cfg
goalSuffix = '_' : senAttr nGoal
tmpFileName = basename thName ++ goalSuffix ++ ".owl"
tScript = TacticScript $ show ATPTacticScript
{ tsTimeLimit = configTimeLimit cfg
, tsExtraOpts = simpleOptions }
defaultProofStatus out =
(openProofStatus (senAttr nGoal) hermitS $ ProofTree out)
{ tacticScript = tScript }
prob = showOWLProblemS sps
entail = showOWLProblemS
sps { initialState = [ nGoal {isAxiom = True } ] }
when saveHermit $ do
writeFile tmpFileName prob
writeFile (tmpFileName ++ ".entail.owl") entail
res <- runTimedHermit "" tmpFileName prob (Just entail) tLimit
((err, retval), output, tUsed) <- return $ case res of
Nothing ->
((ATPTLimitExceeded, defaultProofStatus "Timeout"), [], tLimit)
Just (progTh, output, eOut) ->
if progTh then
let (atpr, exCode, outp, tUsed) = analyseOutput output eOut
openStat = defaultProofStatus $ unlines outp
disProvedStatus = openStat
{ goalStatus = Disproved
, usedTime =
timeToTimeOfDay $ secondsToDiffTime $ toInteger tUsed }
provedStatus = disProvedStatus
{ goalStatus = Proved True
, usedAxioms = map senAttr $ initialState sps }
proofStat = case exCode of
Just True -> provedStatus
Just False -> disProvedStatus
_ -> openStat
in ((atpr, proofStat), outp, tUsed)
else
((ATPError "Could not find hermit reasoner. Is $HERMIT_PATH set?"
, defaultProofStatus ""), [], 0)
return (err, cfg
{ proofStatus = retval
, resultOutput = output
, timeUsed = timeToTimeOfDay $ secondsToDiffTime $ toInteger tUsed
})
analyseOutput :: String -> String -> (ATPRetval, Maybe Bool, [String], Int)
analyseOutput err outp =
let ls = lines outp ++ lines err
anaHelp (atp, exCode, to) line =
case words line of
"Consistent:" : v : _ -> case v of
"Yes" -> (ATPSuccess, Just True, to)
"No" -> (ATPSuccess, Just False, to)
_ -> (atp, exCode, to)
["true"] ->
(ATPSuccess, Just True, to)
["false"] ->
(ATPSuccess, Just False, to)
ne : _ | isPrefixOf "Non-entailments" ne ->
(ATPSuccess, Just False, to)
"Usage:" : "java" : "Hermit" : _ -> (ATPError line, Nothing, to)
"ERROR:" : _ -> (ATPError line, Nothing, to)
tm : num : _ | isPrefixOf "Time" tm && all isDigit num ->
(atp, exCode, read num)
_ -> (atp, exCode, to)
(atpr, st, tmo) = foldl anaHelp (ATPError "", Nothing, -1) ls
in case atpr of
ATPError s | null s -> (ATPError "unexpected hermit output", st, ls, tmo)
_ -> (atpr, st, ls, tmo)