{- |
Module      :  ./TPTP/ConsChecker.hs
Description :  Interface to consistency checkers
Copyright   :  (c) (c) Otto-von-Guericke University of Magdeburg, 2020
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  mscodescu@gmail.com
Stability   :  provisional
Portability :  needs POSIX

-}

module TPTP.ConsChecker
    where

import Logic.Prover

import Common.ProofTree
import Common.SZSOntology

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

import Data.Time (timeToTimeOfDay)
import Data.Time.Clock (secondsToDiffTime)
import qualified SoftFOL.ProveDarwin as Darwin

extras :: Darwin.ProverBinary -> Bool -> String -> String
extras :: ProverBinary -> Bool -> String -> String
extras b :: ProverBinary
b cons :: Bool
cons tl :: String
tl = let
  tOut :: String
tOut = " -to " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tl
  darOpt :: String
darOpt = "-pc false"
  fdOpt :: String
fdOpt = String
darOpt String -> String -> String
forall a. [a] -> [a] -> [a]
++ (if Bool
cons then " -pmtptp true" else "") String -> String -> String
forall a. [a] -> [a] -> [a]
++ " -fd true"
  in case ProverBinary
b of
    Darwin.EProver -> String -> String
Darwin.eproverOpts (if Bool
cons then "-s" else "") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tl
    Darwin.Leo -> "-t " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tl
    Darwin.Darwin -> String
fdOpt String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tOut
    Darwin.DarwinFD -> String
fdOpt String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tOut
    Darwin.EDarwin -> String
fdOpt String -> String -> String
forall a. [a] -> [a] -> [a]
++ " -eq Axioms" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tOut
    Darwin.IProver -> "--time_out_real " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tl String -> String -> String
forall a. [a] -> [a] -> [a]
++ " --sat_mode true"

{- | Runs the Darwin service. The tactic script only contains a string for the
  time limit. -}
consCheck
  :: Darwin.ProverBinary
  -> String
  -> TacticScript
  -> TheoryMorphism Sign Sentence Morphism ProofTree
  -> [FreeDefMorphism Sentence Morphism] -- ^ freeness constraints
  -> IO (CCStatus ProofTree)
consCheck :: ProverBinary
-> String
-> TacticScript
-> TheoryMorphism Sign Sentence Morphism ProofTree
-> [FreeDefMorphism Sentence Morphism]
-> IO (CCStatus ProofTree)
consCheck b :: ProverBinary
b thName :: String
thName (TacticScript tl :: String
tl) tm :: TheoryMorphism Sign Sentence Morphism ProofTree
tm freedefs :: [FreeDefMorphism Sentence Morphism]
freedefs = case TheoryMorphism Sign Sentence Morphism ProofTree
-> Theory Sign Sentence ProofTree
forall sign sen mor proof_tree.
TheoryMorphism sign sen mor proof_tree
-> Theory sign sen proof_tree
tTarget TheoryMorphism Sign Sentence Morphism ProofTree
tm of
    Theory sig :: Sign
sig nSens :: ThSens Sentence (ProofStatus ProofTree)
nSens -> do
        let proverStateI :: ProverState
proverStateI = Sign
-> [Named Sentence]
-> [FreeDefMorphism Sentence Morphism]
-> ProverState
tptpProverState Sign
sig (ThSens Sentence (ProofStatus ProofTree) -> [Named Sentence]
forall a b. ThSens a b -> [Named a]
toNamedList ThSens Sentence (ProofStatus ProofTree)
nSens) [FreeDefMorphism Sentence Morphism]
freedefs
        String
prob <- String -> ProverState -> [String] -> IO String
showTPTPProblemM String
thName ProverState
proverStateI []
        (exitCode :: String
exitCode, out :: [String]
out, tUsed :: Int
tUsed) <-
          String
-> Bool -> String -> String -> String -> IO (String, [String], Int)
Darwin.runDarwinProcess (ProverBinary -> String
Darwin.darwinExe ProverBinary
b) Bool
False (ProverBinary -> Bool -> String -> String
extras ProverBinary
b Bool
True String
tl) String
thName String
prob
        let outState :: CCStatus ProofTree
outState = CCStatus :: forall proof_tree.
proof_tree -> TimeOfDay -> Maybe Bool -> CCStatus proof_tree
CCStatus
               { ccResult :: Maybe Bool
ccResult = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
               , ccProofTree :: ProofTree
ccProofTree = String -> ProofTree
ProofTree (String -> ProofTree) -> String -> ProofTree
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String
exitCode String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
out
               , ccUsedTime :: TimeOfDay
ccUsedTime = DiffTime -> TimeOfDay
timeToTimeOfDay (DiffTime -> TimeOfDay) -> DiffTime -> TimeOfDay
forall a b. (a -> b) -> a -> b
$ Integer -> DiffTime
secondsToDiffTime
                            (Integer -> DiffTime) -> Integer -> DiffTime
forall a b. (a -> b) -> a -> b
$ Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
tUsed }
        CCStatus ProofTree -> IO (CCStatus ProofTree)
forall (m :: * -> *) a. Monad m => a -> m a
return (CCStatus ProofTree -> IO (CCStatus ProofTree))
-> CCStatus ProofTree -> IO (CCStatus ProofTree)
forall a b. (a -> b) -> a -> b
$ if String -> Bool
szsProved String
exitCode then CCStatus ProofTree
outState else
                    CCStatus ProofTree
outState
                    { ccResult :: Maybe Bool
ccResult = if String -> Bool
szsDisproved String
exitCode then Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
                                 else Maybe Bool
forall a. Maybe a
Nothing }

darwinConsChecker
  :: Darwin.ProverBinary -> ConsChecker Sign Sentence Sublogic Morphism ProofTree
darwinConsChecker :: ProverBinary
-> ConsChecker Sign Sentence Sublogic Morphism ProofTree
darwinConsChecker b :: ProverBinary
b =
  (String
-> String
-> Sublogic
-> (String
    -> TacticScript
    -> TheoryMorphism Sign Sentence Morphism ProofTree
    -> [FreeDefMorphism Sentence Morphism]
    -> IO (CCStatus ProofTree))
-> ConsChecker Sign Sentence Sublogic Morphism ProofTree
forall sublogics sign sentence morphism proof_tree.
String
-> String
-> sublogics
-> (String
    -> TacticScript
    -> TheoryMorphism sign sentence morphism proof_tree
    -> [FreeDefMorphism sentence morphism]
    -> IO (CCStatus proof_tree))
-> ConsChecker sign sentence sublogics morphism proof_tree
mkUsableConsChecker (ProverBinary -> String
Darwin.darwinExe ProverBinary
b) (ProverBinary -> String
Darwin.proverBinary ProverBinary
b) Sublogic
FOF ((String
  -> TacticScript
  -> TheoryMorphism Sign Sentence Morphism ProofTree
  -> [FreeDefMorphism Sentence Morphism]
  -> IO (CCStatus ProofTree))
 -> ConsChecker Sign Sentence Sublogic Morphism ProofTree)
-> (String
    -> TacticScript
    -> TheoryMorphism Sign Sentence Morphism ProofTree
    -> [FreeDefMorphism Sentence Morphism]
    -> IO (CCStatus ProofTree))
-> ConsChecker Sign Sentence Sublogic Morphism ProofTree
forall a b. (a -> b) -> a -> b
$ ProverBinary
-> String
-> TacticScript
-> TheoryMorphism Sign Sentence Morphism ProofTree
-> [FreeDefMorphism Sentence Morphism]
-> IO (CCStatus ProofTree)
consCheck ProverBinary
b)
  { ccNeedsTimer :: Bool
ccNeedsTimer = Bool
False }