never executed always true always false
1 {-# LANGUAGE DeriveDataTypeable #-}
2 {-# LANGUAGE DeriveGeneric #-}
3 {-# LANGUAGE RecordWildCards #-}
4
5 module Conjure.UI.SolveStats (mkSolveStats, SolveStats (..), SolveStatus (..)) where
6
7 import Conjure.Bug
8 import Conjure.Prelude
9 import Conjure.UI (UI (..), versionLine)
10 import Data.HashMap.Strict qualified as M -- unordered-containers
11 import Data.Text qualified as T (isInfixOf, null, unlines) -- text
12 import Data.Time (UTCTime, getCurrentTime) -- time
13 import Network.HostName (getHostName) -- hostname
14 import Shelly (run) -- shelly
15
16 data SolveStats = SolveStats
17 { status :: SolveStatus,
18 totalTime :: Maybe Double,
19 savilerowInfo :: M.HashMap String String,
20 runsolverInfo :: M.HashMap String String,
21 essence :: FilePath,
22 essenceParams :: [FilePath],
23 useExistingModels :: [FilePath],
24 savilerowOptions :: [String],
25 solverOptions :: [String],
26 solver :: String,
27 computer :: String,
28 timestamp :: UTCTime,
29 conjureVersion :: String,
30 savilerowVersion :: String,
31 savilerowLogs :: SavileRowLogs
32 }
33 deriving (Eq, Ord, Show, Data, Typeable, Generic)
34
35 instance Hashable SolveStats
36
37 instance ToJSON SolveStats where toJSON = genericToJSON jsonOptions
38
39 instance FromJSON SolveStats where parseJSON = genericParseJSON jsonOptions
40
41 -- OK: solved, can be sat or unsat.
42 -- Invalid: instance is not valid.
43 -- TimeOut/MemOut: what they sound like.
44 -- Error: could be a bug, but could also be to do with a very large encoding.
45 data SolveStatus = OK | Invalid | TimeOut | MemOut | Error
46 deriving (Eq, Ord, Show, Data, Typeable, Generic)
47
48 instance Hashable SolveStatus
49
50 instance ToJSON SolveStatus where toJSON = genericToJSON jsonOptions
51
52 instance FromJSON SolveStatus where parseJSON = genericParseJSON jsonOptions
53
54 data SavileRowLogs = SavileRowLogs
55 { exitCode :: Int,
56 stderr :: Maybe [String],
57 stdout :: Maybe [String]
58 }
59 deriving (Eq, Ord, Show, Data, Typeable, Generic)
60
61 instance Hashable SavileRowLogs
62
63 instance ToJSON SavileRowLogs where toJSON = genericToJSON jsonOptions
64
65 instance FromJSON SavileRowLogs where parseJSON = genericParseJSON jsonOptions
66
67 mkSolveStats :: UI -> (Int, Text, Text) -> String -> String -> IO SolveStats
68 mkSolveStats Solve {..} (exitCodeSR, stdoutSR, stderrSR) savilerowInfoText runsolverInfoText = do
69 let combinedSR = T.unlines [stdoutSR, stderrSR]
70
71 savilerowInfo = M.fromList [(k, v) | [k, v] <- map (splitOn ":") (lines savilerowInfoText)]
72
73 runsolverInfo = M.fromList [(k, v) | [k, v] <- map (splitOn "=") (lines runsolverInfoText)]
74
75 status
76 | or
77 [ T.isInfixOf msg combinedSR
78 | msg <-
79 [ "type error: undefined identifier",
80 "MiniZinc error: Memory violation detected", -- minizinc
81 "Check failed: ParseFlatzincFile",
82 "parse error: unexpected end-of-file after parsing number of clauses", -- kissat
83 "error: Cannot open file",
84 "kissat: error: can not read", -- kissat
85 "kissat: fatal error: maximum arena capacity", -- kissat
86 "Error: syntax error, unexpected ]]", -- cplex
87 "*** Check failure stack trace: ***", -- or-tools
88 "Error: evaluation error: Index set mismatch.",
89 "Savile Row killed by: java.lang.AssertionError",
90 "java.lang.ClassCastException",
91 "ERROR: File not found", -- savilerow
92 "ERROR: Failed when writing SAT encoding to file." -- savilerow
93 ]
94 ] =
95 Error
96 | or
97 [ T.isInfixOf msg combinedSR
98 | msg <-
99 [ "java.lang.OutOfMemoryError",
100 "ERROR: Out of Memory",
101 "Maximum memory exceeded" -- for when runsolver prints this message but won't set MEMOUT=true for some reason
102 ]
103 ] =
104 MemOut
105 | or
106 [ T.isInfixOf msg combinedSR
107 | msg <-
108 [ "Savile Row timed out.",
109 "time out: time limit reached",
110 "Received SIGTERM or SIGINT, killing child" -- for when runsolver prints this message but won't set MEMOUT=true or TIMEOUT=true for some reason
111 ]
112 ] =
113 TimeOut
114 | T.isInfixOf "ERROR: In statement: where false" combinedSR = Invalid
115 | M.lookup "MEMOUT" runsolverInfo == Just "true" = MemOut
116 | M.lookup "TIMEOUT" runsolverInfo == Just "true" = TimeOut
117 | M.lookup "SavileRowTimeOut" savilerowInfo == Just "1" = TimeOut
118 | M.lookup "SavileRowClauseOut" savilerowInfo == Just "1" = TimeOut
119 | M.lookup "SolverTimeOut" savilerowInfo == Just "1" = TimeOut
120 | exitCodeSR /= 0 = Error
121 | otherwise = OK
122
123 totalTime
124 | Just srTotalTime <- M.lookup "SavileRowTotalTime" savilerowInfo >>= readMay,
125 Just solverTotalTime <- M.lookup "SolverTotalTime" savilerowInfo >>= readMay =
126 Just (srTotalTime + solverTotalTime)
127 | otherwise = Nothing
128
129 computer <- getHostName
130 timestamp <- getCurrentTime
131 let conjureVersion = versionLine
132 savilerowVersion <- head . lines . textToString <$> sh (run "savilerow" ["-help"])
133 let savilerowLogs =
134 SavileRowLogs
135 { exitCode = exitCodeSR,
136 stdout = if T.null stdoutSR then Nothing else Just (lines (textToString stdoutSR)),
137 stderr = if T.null stderrSR then Nothing else Just (lines (textToString stderrSR))
138 }
139 return SolveStats {..}
140 mkSolveStats _ _ _ _ = bug "mkSolveStats"