1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
|
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE NamedFieldPuns #-}
module Provers where
import Base
import Encoding
import Syntax.Lexicon (Lexicon)
import Syntax.Internal (Formula, Task(..), isIndirect)
import Tptp.UnsortedFirstOrder qualified as Tptp
import Control.Monad.Logger
import Data.Text qualified as Text
import Data.Time
import System.Process.Text (readProcessWithExitCode)
import Text.Builder
type Prover = Verbosity -> TimeLimit -> MemoryLimit -> ProverInstance
-- | Prover responses are stored as a list of prefixes.
data ProverInstance = Prover
{ proverName :: String
, proverPath :: FilePath
, proverArgs :: [String]
, proverSaysYes :: [Text]
, proverSaysNo :: [Text]
, proverDoesNotKnow :: [Text]
, proverWarnsContradiction :: [Text]
} deriving (Show, Eq)
data Verbosity = Silent | Verbose deriving (Show, Eq)
newtype TimeLimit = Seconds Word64 deriving (Show, Eq, Num)
newtype MemoryLimit = Megabytes Word64 deriving (Show, Eq)
toSeconds :: TimeLimit -> String
toSeconds (Seconds secs) = show secs
toMegabytes :: MemoryLimit -> String
toMegabytes (Megabytes mbs) = show mbs
defaultTimeLimit :: TimeLimit
defaultTimeLimit = Seconds 10
defaultMemoryLimit :: MemoryLimit
defaultMemoryLimit = Megabytes 5000
eproverDev :: ProverInstance
eproverDev = eprover "eprover" Silent defaultTimeLimit defaultMemoryLimit
eprover :: FilePath -> Prover
eprover path verbosity timeLimit memoryLimit = Prover
{ proverName = "eprover"
, proverPath = path
, proverArgs =
[ "--tptp3-format"
, "--auto"
, case verbosity of
Silent -> "--silent"
Verbose -> "--verbose"
, "--soft-cpu-limit=" <> toSeconds timeLimit
, "--cpu-limit=" <> toSeconds (timeLimit + 5)
, "--memory-limit=" <> toMegabytes memoryLimit
]
, proverSaysYes = ["# SZS status Theorem"]
, proverSaysNo = ["# SZS status CounterSatisfiable"]
, proverDoesNotKnow = ["# SZS status ResourceOut", "# SZS status GaveUp"]
, proverWarnsContradiction = ["# SZS status ContradictoryAxioms"]
}
vampire :: FilePath -> Prover
vampire path _verbosity timeLimit memoryLimit = Prover
{ proverName = "vampire"
, proverPath = path
, proverArgs =
[ "--mode", "casc"
, "--time_limit", toSeconds timeLimit
, "--memory_limit", toMegabytes memoryLimit
]
, proverSaysYes = ["% SZS status Theorem"]
, proverSaysNo = ["% SZS status CounterSatisfiable"]
, proverDoesNotKnow = ["% SZS status Timeout"]
, proverWarnsContradiction = ["% SZS status ContradictoryAxioms"]
}
-- WIP: setting up a clausifier
iprover :: Prover
iprover _verbosity timeLimit _memoryLimit = Prover
{ proverName = "iProver"
, proverPath = "iproveropt"
, proverArgs =
[ "--time_out_real " <> toSeconds timeLimit
]
, proverSaysYes = ["% SZS status Theorem"]
, proverSaysNo = ["% SZS status CounterSatisfiable"]
, proverDoesNotKnow = ["% SZS status Unknown"]
, proverWarnsContradiction = []
}
-- | 'No', 'Uncertain', and 'ContradictoryAxioms' carry the 'Text'-encoded
-- TPTP problem that failed with them for debugging purposes. 'Error' simply
-- contains the error message of the prover verbatim.
data ProverAnswer
= Yes
| No Text
| ContradictoryAxioms Text
| Uncertain Text
| Error Text
deriving (Show, Eq)
nominalDiffTimeToText :: NominalDiffTime -> Text
nominalDiffTimeToText delta = run (nominalDiffTimeToBuilder delta)
nominalDiffTimeToBuilder :: NominalDiffTime -> Builder
nominalDiffTimeToBuilder delta = case hours of
0 -> padded minutes <> ":" <> padded restSeconds <> "." <> padded restCentis
_ -> padded hours <> ":" <> padded restMinutes <> ":" <> padded restSeconds
where
padded n = if n < 10 then char '0' <> decimal n else decimal n
centiseconds = truncate (100 * nominalDiffTimeToSeconds delta) :: Int
(seconds, restCentis) = divMod centiseconds 100
(minutes, restSeconds) = divMod seconds 60
(hours, restMinutes) = divMod minutes 60
timeDifferenceToText :: UTCTime -> UTCTime -> Text
timeDifferenceToText startTime endTime = nominalDiffTimeToText (diffUTCTime endTime startTime)
runProver :: (MonadIO io, MonadLogger io) => ProverInstance -> Lexicon -> Task -> io (Formula, ProverAnswer)
runProver prover@Prover{..} lexicon task = do
startTime <- liftIO getCurrentTime
let tptp = encodeTask lexicon task
let tptp' = Tptp.toText tptp
(_exitCode, answer, answerErr) <- liftIO (readProcessWithExitCode proverPath proverArgs tptp')
endTime <- liftIO getCurrentTime
let duration = timeDifferenceToText startTime endTime
logInfoN
let hypo = case tptp of
Tptp.Task (head : _) -> Tptp.Task [head]
_ -> Tptp.Task []
in duration <> " " <> Tptp.toText hypo
pure (taskConjecture task, recognizeAnswer prover task tptp' answer answerErr)
-- | Parse the answer of a prover based on the configured prefixes of responses.
recognizeAnswer :: ProverInstance -> Task -> Text -> Text -> Text -> ProverAnswer
recognizeAnswer Prover{..} task tptp answer answerErr =
let
matches prefixes = any (\l -> any (`Text.isPrefixOf` l) prefixes) (Text.lines answer)
saidYes = matches proverSaysYes
saidNo = matches proverSaysNo
doesNotKnow = matches proverDoesNotKnow
warned = matches proverWarnsContradiction
in if
| saidYes || (warned && isIndirect task) -> Yes
| saidNo -> No tptp
| doesNotKnow -> Uncertain tptp
| warned -> ContradictoryAxioms tptp
| otherwise -> Error (answer <> answerErr)
|
