Sketch parser for Vampire's status lines

3 files changed, 111 insertions, 14 deletions

diff --git a/source/Provers.hs b/source/Provers.hs
index 25a6430..c5489d7 100644
--- a/source/Provers.hs
+++ b/source/Provers.hs
@@ -20,6 +20,8 @@ import System.Exit (ExitCode)
 import System.IO (hClose, hSetEncoding, utf8)
 import System.Process (CreateProcess(..), StdStream(CreatePipe), createProcess, proc, waitForProcess)
 import TextBuilder
+import Text.Megaparsec
+import Text.Megaparsec.Char qualified as Char
 import UnliftIO.Async (concurrently)
 
 type Prover = Verbosity -> TimeLimit -> MemoryLimit -> ProverInstance
@@ -112,10 +114,10 @@ iprover _verbosity timeLimit _memoryLimit = Prover
 -- contains the error message of the prover verbatim.
 data ProverAnswer
     = Yes
-    | No Text
-    | ContradictoryAxioms Text
-    | Uncertain Text
-    | Error Text Text Text
+    | No
+    | ContradictoryAxioms
+    | Uncertain
+    | Error Text Text
     deriving (Show, Eq)
 
 nominalDiffTimeToText :: NominalDiffTime -> Text
@@ -170,16 +172,63 @@ runProverProcess path args task = do
 
 -- | Parse the answer of a prover based on the configured prefixes of responses.
 recognizeAnswer :: ProverInstance -> Task -> Text -> Text -> ProverAnswer
-recognizeAnswer Prover{..} task answer answerErr =
+recognizeAnswer prover@Prover{..} task answer answerErr =
+    if
+        | proverName == "vampire" -> recognizeVampireAnswer prover task answer answerErr
+        | otherwise ->
+            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
+                | doesNotKnow -> Uncertain
+                | warned -> ContradictoryAxioms
+                | otherwise -> Error (Text.pack(show (taskConjectureLabel task))) (answer <> answerErr)
+
+
+
+
+recognizeVampireAnswer :: ProverInstance -> Task -> Text -> Text -> ProverAnswer
+recognizeVampireAnswer Prover{..} task 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
+        statuses = [status | Just status <- parseMaybe vampireStatusParser <$> Text.lines (answer <> "\n" <> answerErr)]
+        statusLines = ("% SZS status " <>) <$> statuses
+        matches prefixes = any (\l -> any (`Text.isPrefixOf` l) prefixes) statusLines
+        saidYes = matches proverSaysYes
+        saidNo = matches proverSaysNo
+        doesNotKnow = matches proverDoesNotKnow
+        warned = matches proverWarnsContradiction
     in if
         | saidYes || (warned && isIndirect task) -> Yes
-        | saidNo -> No (encodeTaskText task)
-        | doesNotKnow -> Uncertain (encodeTaskText task)
-        | warned -> ContradictoryAxioms (encodeTaskText task)
-        | otherwise -> Error (answer <> answerErr) (encodeTaskText task) (Text.pack(show (taskConjectureLabel task)))
+        | saidNo -> No
+        | doesNotKnow -> Uncertain
+        | warned -> ContradictoryAxioms
+        | otherwise -> Error (Text.pack(show (taskConjectureLabel task))) (answer <> answerErr)
+
+
+-- | Parse a Vampire SZS status line.
+--
+-- Recognizes both standard lines like:
+--   % SZS status Timeout for 123
+-- and lines prefixed by worker ids (seen with portfolio output), e.g.:
+--   % (2581105)SZS status Timeout for
+vampireStatusParser :: Parsec Void Text Text
+vampireStatusParser = do
+    _ <- Char.char '%'
+    Char.hspace
+    optional do
+        _ <- Char.char '('
+        _ <- some Char.digitChar
+        _ <- Char.char ')'
+        Char.hspace
+    _ <- chunk "SZS"
+    Char.hspace1
+    _ <- chunk "status"
+    Char.hspace1
+    status <- takeWhile1P (Just "SZS status") (\c -> c /= ' ' && c /= '\t')
+    _ <- takeRest
+    pure status
diff --git a/source/Test/Unit.hs b/source/Test/Unit.hs
index de2012a..f3fcfec 100644
--- a/source/Test/Unit.hs
+++ b/source/Test/Unit.hs
@@ -3,12 +3,14 @@ module Test.Unit where
 
 import Test.Tasty
 import Test.Tasty.HUnit
+import Test.Unit.Provers qualified as Provers
 import Test.Unit.Symdiff qualified as Symdiff
 import Test.Unit.Syntax qualified as Syntax
 
 unitTests :: TestTree
 unitTests = testGroup "unit tests"
     [testCase "filter" filtersWell
+    , Provers.unitTests
     , Syntax.unitTests  -- include the Syntax.DeBruijn tests
     ]
 
diff --git a/source/Test/Unit/Provers.hs b/source/Test/Unit/Provers.hs
new file mode 100644
index 0000000..557a08d
--- /dev/null
+++ b/source/Test/Unit/Provers.hs
@@ -0,0 +1,46 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module Test.Unit.Provers (unitTests) where
+
+import Base
+import Provers
+import Report.Location (pattern Nowhere)
+import Syntax.Internal (Directness(..), Marker(..), Task(..), pattern Top)
+
+import Test.Tasty
+import Test.Tasty.HUnit
+import Text.Megaparsec (parseMaybe)
+
+shouldBe :: (Eq a, Show a, HasCallStack) => a -> a -> Assertion
+shouldBe = flip (assertEqual "")
+
+unitTests :: TestTree
+unitTests = testGroup "Provers"
+    [ testCase "vampireStatusParser parses canonical SZS status line" do
+        parseMaybe vampireStatusParser "% SZS status ContradictoryAxioms for 2260"
+            `shouldBe` Just "ContradictoryAxioms"
+    , testCase "vampireStatusParser parses worker-prefixed SZS status line" do
+        parseMaybe vampireStatusParser "% (2581105)SZS status Timeout for "
+            `shouldBe` Just "Timeout"
+    , testCase "Vampire recognizer reads status from stderr too" do
+        recognizeAnswer vampireProver directTask "" "% (2581105)SZS status Timeout for "
+            `shouldBe` Uncertain
+    , testCase "ContradictoryAxioms counts as Yes for indirect goals" do
+        recognizeAnswer vampireProver indirectTask "" "% (2581105)SZS status ContradictoryAxioms for "
+            `shouldBe` Yes
+    ]
+
+directTask :: Task
+directTask = Task
+    { taskDirectness = Direct
+    , taskHypotheses = []
+    , taskConjectureLabel = Marker "dummy"
+    , taskLocation = Nowhere
+    , taskConjecture = Top
+    }
+
+indirectTask :: Task
+indirectTask = directTask{taskDirectness = Indirect Top}
+
+vampireProver :: ProverInstance
+vampireProver = vampire "vampire" Silent defaultTimeLimit defaultMemoryLimit