Fix up the solver version probe logic

saw-central/src/SAWCentral/SolverCache.hs

@@ -163,26 +163,61 @@ decodeHex s = BS.pack <$> go s
 -- type is most often used in a list (@[SolverBackend]@), since at least one
 -- other backend is always used along with 'What4' or 'SBV' (e.g. 'SBV' with
 -- 'Z3' or 'W4' with 'AIG' and 'ABC').
--- NOTE: This definition includes all backends supported by SBV, even though not
--- all of them are currently supported by SAW (namely, 'Bitwuzla' and 'DReal').
--- This is to ensure the system for keeping track of solver backend versions
--- is not silently broken if support for these backends is ever added to SAW.
-data SolverBackend = What4
-                   | SBV
-                   | AIG
-                   | RME
-                   -- External solvers supported by SBV (copied from SBV.Solver)
-                   | ABC
-                   | Boolector
-                   | Bitwuzla
-                   | CVC4
-                   | CVC5
-                   | DReal -- NOTE: Not currently supported by SAW
-                   | MathSAT
-                   | OpenSMT -- NOTE: Not currently supported by SAW
-                   | Yices
-                   | Z3
-                   deriving (Eq, Ord, Enum, Bounded, Show, Generic)
+--
+-- NOTE: This definition includes all backends supported by SBV, even
+-- though not all of them are currently supported by SAW (namely,
+-- 'CVC4', 'Bitwuzla' and 'DReal'). It must also include all backends
+-- ever supported by SAW, even if (like 'CVC4') they are no longer
+-- supported.
+--
+-- This enumeration appears in the on-disk solver cache as part of the
+-- value side of the LMDB database and must therefore be stable. I
+-- think the database ends up storing the enumeration values as
+-- constructor name strings rather than numbers. However, to be safe:
+--    - Do not rename the constructors
+--    - Do not reorder the constructors
+--    - Add new constructors only at the end
+--
+-- XXX: it does not make sense to treat SBV and What4 as the same kind
+-- of thing as z3 and CVC5. Given the above considerations, however,
+-- reorganizing will take some work and needs to be done carefully.
+--
+data SolverBackend
+    = What4
+    | SBV
+    | AIG
+    | RME
+      -- External solvers supported by SBV (copied from SBV.Solver)
+    | ABC
+    | Boolector
+    | Bitwuzla
+    | CVC4
+    | CVC5
+    | DReal -- NOTE: Not currently supported by SAW
+    | MathSAT
+    | OpenSMT -- NOTE: Not currently supported by SAW
+    | Yices
+    | Z3
+    deriving (Eq, Ord, Enum, Show, Generic)
+
+-- | The list of all available 'SolverBackend's
+--
+--   This should not include solvers we don't support, because that
+--   will result in trying to query their version.
+allBackends :: [SolverBackend]
+allBackends = [
+    What4,
+    SBV,
+    AIG,
+    RME,
+    ABC,
+    Boolector,
+    Bitwuzla,
+    CVC5,
+    MathSAT,
+    Yices,
+    Z3
+ ]
 
 instance FromJSON SolverBackend where
   parseJSON = JSON.genericParseJSON JSON.defaultOptions
@@ -194,10 +229,6 @@ instance FromJSONKey SolverBackend where
 instance ToJSONKey SolverBackend where
   toJSONKey = JSON.genericToJSONKey JSON.defaultJSONKeyOptions
 
--- | The list of all available 'SolverBackend's
-allBackends :: [SolverBackend]
-allBackends = [minBound..]
-
 -- | Given an 'SBV.SMTConfig', return the list of corresponding 'SolverBackend's
 sbvBackends :: SBV.SMTConfig -> [SolverBackend]
 sbvBackends conf = [SBV, cvtSolver $ SBV.name $ SBV.solver conf]

saw-central/src/SAWCentral/SolverVersions.hs

@@ -7,10 +7,11 @@ Stability   : provisional
 -}
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TupleSections #-}
 
-module SAWCentral.SolverVersions where
+module SAWCentral.SolverVersions (getSolverBackendVersions) where
 
 import Control.Exception (SomeException, try)
 import System.Process (readProcessWithExitCode)
@@ -20,6 +21,7 @@ import qualified Data.Map as Map
 
 import qualified Data.SBV.Dynamic as SBV
 
+import SAWCentral.Panic (panic)
 import SAWCentral.SolverCache
 import SAWVersion.GitRev
 
@@ -29,6 +31,10 @@ import SAWVersion.GitRev
 getSolverVersion :: SBV.Solver -> IO (Maybe String)
 getSolverVersion s =
   let s' = SBV.solver $ SBV.defaultSolverConfig s
+      nope what = panic "getSolverVersion" [
+             "Version request for unsupported solver " <> what
+           ]
+
       (args, pref) = case SBV.name s' of
         -- n.b. abc will return a non-zero exit code if asked for command usage.
         SBV.ABC       -> (["s", "-q", "version;quit"], "UC Berkeley, ABC ")
@@ -38,10 +44,11 @@ getSolverVersion s =
         SBV.CVC5      -> (["--version"]              , "This is cvc5 version ")
         SBV.DReal     -> (["--version"]              , "dReal v")
         SBV.MathSAT   -> (["-version"]               , "MathSAT5 version ")
-        SBV.OpenSMT   -> error "opensmt not currently supported"
+        SBV.OpenSMT   -> nope "OpenSMT"
         SBV.Yices     -> (["--version"]              , "Yices ")
         SBV.Z3        -> (["--version"]              , "Z3 version ")
-  in try (readProcessWithExitCode (SBV.executable s') args "") >>= \case
+  in
+  try (readProcessWithExitCode (SBV.executable s') args "") >>= \case
     Right (ExitSuccess,o,_) | (l:_) <- lines o ->
       return $ Just $ dropPrefix pref l
     Right _                   -> return Nothing