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
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"
consCheck
:: Darwin.ProverBinary
-> String
-> TacticScript
-> TheoryMorphism Sign Sentence Morphism ProofTree
-> [FreeDefMorphism Sentence Morphism]
-> 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 }