SolverCache.hs

{- |
Module      : SAWScript.SolverCache
Description : Caching SMT solver results for SAWScript
License     : BSD3
Maintainer  : m-yac
Stability   : provisional

This file defines an interface for caching SMT/SAT solver results using an LMDB
database. The interface, as used in 'applyProverToGoal', works as follows:

1. An 'SMTQuery' is converted into a string using 'scWriteExternal', and
   along with any relevant 'SolverBackendVersion's (obtained using
   'getSolverBackendVersions' from @SAWScript.SolverVersions@), is then hashed
   using SHA256 ('mkSolverCacheKey').
2. The core of the 'SolverCache' is an LMDB database mapping these hashes to
   previously obtained results ('solverCacheEnv', 'solverCacheDB'). If this is
   the first time solver caching is being used and the `SAW_SOLVER_CACHE_PATH`
   environment variable was set at startup, then open an LMDB database at the
   specified path and use this database for all subsequent uses of the solver
   cache. Note that this only occurs if there have been no prior calls to the
   `set_solver_cache_path` command, which immediately opens an LMDB database at
   specified path when called.
3. If the hash corresponding to the 'SATQuery' and 'SolverBackendVersion's
   can be found in the database ('lookupInSolverCache'), then the corresponding
   result is used.
4. Otherwise, the 'SATQuery' is dispatched to the requested backend and a
   result is obtained. This result is then added to the database using the
   aforementioned hash as the key ('insertInSolverCache').

A interesting detail is how results are represented. For all of the backends
which use 'applyProverToGoal', the type of a result is:
@Maybe [(ExtCns Term, FirstOrderValue)]@, where 'Nothing' represents a result
of "unsat," and 'Just' represents a result of "sat" along with a list of
counterexamples. Since 'ExtCns' contains execution-specific 'VarIndex'es, we
don't want to save these results directly. Instead, we represent each 'ExtCns'
as its index in the 'satVariables' field of 'SATQuery' (which is where they
were obtained by the backends in the first place).
-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE GeneralisedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE ViewPatterns #-}

module SAWScript.SolverCache
  ( SolverBackend(..)
  , allBackends
  , sbvBackends
  , SolverBackendOption(..)
  , optionBackends
  , SolverBackendVersions
  , SolverCacheKey(..)
  , mkSolverCacheKey
  , SolverCacheValue(..)
  , toSolverCacheValue
  , fromSolverCacheValue
  , SolverCache(..)
  , lazyOpenSolverCache
  , openSolverCache
  , SolverCacheOp
  , solverCacheOp
  , solverCacheOpDefault
  , lookupInSolverCache
  , insertInSolverCache
  , setSolverCachePath
  , printSolverCacheByHex
  , cleanSolverCache
  , printSolverCacheStats
  , testSolverCacheStats
  ) where

import System.Directory (createDirectoryIfMissing)
import Control.Exception (try, SomeException)
import Control.Monad (when, forM_)
import System.Timeout (timeout)

import GHC.Generics (Generic)
import Data.IORef (IORef, newIORef, modifyIORef, readIORef)
import Data.Time.Clock (UTCTime, getCurrentTime)
import Data.Tuple.Extra (first, firstM)
import Data.List (elemIndex, intercalate, isPrefixOf)
import Data.Maybe (fromMaybe, isJust)
import Data.Functor ((<&>))
import Numeric (readHex)

import Data.Map.Strict (Map)
import qualified Data.Map.Strict as M

import qualified Data.Text as T
import Data.Text.Encoding (encodeUtf8)
import Text.Printf (printf)

import Data.ByteString (ByteString)
import qualified Data.ByteString as BS

import qualified Crypto.Hash.SHA256 as SHA256

import Data.Aeson ( FromJSON(..), ToJSON(..), FromJSONKey(..), ToJSONKey(..)
                  , (.:), (.:?), (.=), fromJSON )
import qualified Data.Aeson as JSON
import Codec.CBOR.JSON (encodeValue, decodeValue)
import Codec.Serialise (Serialise(..))

import qualified Database.LMDB.Simple as LMDB
import qualified Database.LMDB.Simple.Extra as LMDB

import qualified Data.SBV.Dynamic as SBV

import Verifier.SAW.FiniteValue
import Verifier.SAW.SATQuery
import Verifier.SAW.ExternalFormat
import Verifier.SAW.SharedTerm

import SAWScript.Options
import SAWScript.Proof


-- Helper Functions ------------------------------------------------------------

-- | Run the given IO action, but if the given 'timeout' (in microseconds) is
-- reached or the action encounters any 'SomeException', 'Left' is returned
tryWithTimeout :: Int -> IO a -> IO (Either String a)
tryWithTimeout t_us m = try (timeout t_us m) <&> \case
  Right (Just a) -> Right a
  Right Nothing -> let t_str | t_us `mod` 1000000 == 0 = show (t_us `div` 1000000) ++ "s"
                             | t_us `mod` 1000    == 0 = show (t_us `div` 1000) ++ "ms"
                             | otherwise               = show t_us ++ "us"
                    in Left $ "Operation timed out (" ++ t_str ++ ")"
  Left (exn :: SomeException) -> Left $ show exn

-- | Encode a 'ByteString' as a hex string
encodeHex :: ByteString -> String
encodeHex = concatMap (printf "%02x") . BS.unpack

-- | Decode a hex string as a 'ByteString'
decodeHex :: String -> Either String ByteString
decodeHex s = BS.pack <$> go s
  where go (c0:c1:cs) | [(b,[])] <- readHex [c0,c1] = (b:) <$> go cs
        go [] = return []
        go _ = Left $ "Hex decoding failure on: " ++ s


-- Solver Backends -------------------------------------------------------------

-- | A datatype including all solver backends currently supported by SAW. This
-- 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 -- NOTE: Not currently supported by SAW
                   | CVC4
                   | CVC5
                   | DReal -- NOTE: Not currently supported by SAW
                   | MathSAT
                   | Yices
                   | Z3
                   deriving (Eq, Ord, Enum, Bounded, Show, Generic)

instance FromJSON SolverBackend where
  parseJSON = JSON.genericParseJSON JSON.defaultOptions
instance ToJSON SolverBackend where
  toJSON = JSON.genericToJSON JSON.defaultOptions
  toEncoding = JSON.genericToEncoding JSON.defaultOptions
instance FromJSONKey SolverBackend where
  fromJSONKey = JSON.genericFromJSONKey JSON.defaultJSONKeyOptions
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]
  where cvtSolver SBV.ABC       = ABC
        cvtSolver SBV.Boolector = Boolector
        cvtSolver SBV.Bitwuzla  = Bitwuzla
        cvtSolver SBV.CVC4      = CVC4
        cvtSolver SBV.CVC5      = CVC5
        cvtSolver SBV.DReal     = DReal
        cvtSolver SBV.MathSAT   = MathSAT
        cvtSolver SBV.Yices     = Yices
        cvtSolver SBV.Z3        = Z3

-- | A datatype representing an option to one of the 'SolverBackend's.
-- Currently, there are only the following options for using 'What4': with a
-- tactic ('W4_Tactic'), by converting to SMTLib2 then calling ABC
-- ('W4_SMTLib2'), by converting to Verilog then calling ABC ('W4_Verilog'),
-- or by converting to AIGER then calling ABC ('W4_AIGER'). Note that certain
-- options may imply that additional 'SolverBackend's were used - see
-- 'optionBackends'.
data SolverBackendOption = W4_Tactic String
                         | W4_SMTLib2
                         | W4_Verilog
                         | W4_AIGER
                         deriving (Eq, Ord, Show, Generic)

instance FromJSON SolverBackendOption where
  parseJSON = JSON.genericParseJSON JSON.defaultOptions
                { JSON.sumEncoding = JSON.TwoElemArray }
instance ToJSON SolverBackendOption where
  toJSON = JSON.genericToJSON JSON.defaultOptions
             { JSON.sumEncoding = JSON.TwoElemArray }
  toEncoding = JSON.genericToEncoding JSON.defaultOptions
                { JSON.sumEncoding = JSON.TwoElemArray }

-- | Given a 'SolverBackendOption', return the list of additional
-- 'SolverBackend's that are used
optionBackends :: SolverBackendOption -> [SolverBackend]
optionBackends W4_AIGER = [AIG]
optionBackends _ = []

-- | A map from 'SolverBackend's to their version 'String's, if one could be
-- obtained
type SolverBackendVersions = Map SolverBackend (Maybe String)

-- | Pretty-print a 'SolverBackend' with its version 'String'
showSolverBackendVersion :: SolverBackend -> Maybe String -> [String] -> String
showSolverBackendVersion backend (Just v_str) opt_words =
  unwords $ show backend : v_str : opt_words
showSolverBackendVersion backend Nothing opt_words =
  showSolverBackendVersion backend (Just "[unknown version]") opt_words

-- | Pretty-print a set of 'SolverBackendVersions' and 'SolverBackendOption's
-- with the given 'String' separator
showBackendVersionsWithOptions :: String -> SolverBackendVersions ->
                                  [SolverBackendOption] -> String
showBackendVersionsWithOptions sep vs opts =
  let entries = M.unionWith (<>) (M.map (\v -> (v, [])) vs)
                                 (M.fromList $ optEntry <$> opts)
   in intercalate sep $ showEntry <$> M.toList entries
  where optEntry (W4_Tactic t) = (What4, (Nothing, ["using", t]))
        optEntry W4_SMTLib2    = (What4, (Nothing, ["to", "SMTLib2"]))
        optEntry W4_Verilog    = (What4, (Nothing, ["to", "Verilog"]))
        optEntry W4_AIGER      = (What4, (Nothing, ["to", "AIGER"]))
        showEntry (backend, (mb_v_str, opt_words)) =
          showSolverBackendVersion backend mb_v_str opt_words


-- Solver Cache Keys -----------------------------------------------------------

-- | The key type for 'SolverCache'. Each is a SHA256 hash of a 'SATQuery' (see
-- 'mkSolverCacheKey') along with optional solver version information used only
-- for pretty-printing.
data SolverCacheKey =
  SolverCacheKey 
  { solverCacheKeyVersions :: SolverBackendVersions
  , solverCacheKeyOptions  :: [SolverBackendOption]
  , solverCacheKeyHash     :: ByteString
  }

instance Eq SolverCacheKey where
  (SolverCacheKey _ _ bs1) == (SolverCacheKey _ _ bs2) = bs1 == bs2

instance Show SolverCacheKey where
  show (SolverCacheKey vs opts bs) = encodeHex (BS.take 8 bs) ++
    if M.null vs && null opts then ""
    else " (" ++ showBackendVersionsWithOptions ", " vs opts ++ ")"

-- | Make a 'SolverCacheKey' with no version information 
solverCacheKeyFromHash :: ByteString -> SolverCacheKey
solverCacheKeyFromHash = SolverCacheKey M.empty []

instance Serialise SolverCacheKey where
  encode = encode . solverCacheKeyHash
  decode = solverCacheKeyFromHash <$> decode

-- | Hash using SHA256 a 'String' representation of a 'SATQuery' and a 'Set' of
-- 'SolverBackendVersion's to get a 'SolverCacheKey'. In particular, this
-- 'String' representation contains all the 'SolverBackendVersion's, the
-- number of 'satVariables' in the 'SATQuery', the number of 'satUninterp's in
-- the 'SATQuery, and finally the 'scWriteExternal' representation of the
-- 'satQueryAsPropTerm' of the 'SATQuery' - with two additional things:
-- 1. Before calling 'scWriteExternal', we generalize ('scGeneralizeExts') over
--    all 'satVariables' and 'satUninterp's. This ensures the hash does not
--    depend on any execution-specific 'VarIndex'es.
-- 2. After calling 'scWriteExternal', all 'LocalName's in 'Pi' and 'Lam'
--    constructors are removed. This ensures that two terms which are alpha
--    equivalent are given the same hash.
mkSolverCacheKey :: SharedContext -> SolverBackendVersions ->
                    [SolverBackendOption] -> SATQuery -> IO SolverCacheKey
mkSolverCacheKey sc vs opts satq = do
  body <- satQueryAsPropTerm sc satq
  let ecs = M.keys (satVariables satq) ++
            filter (\ec -> ecVarIndex ec `elem` satUninterp satq)
                   (getAllExts body)
  tm <- scGeneralizeExts sc ecs body
  let str_prefix = [ showBackendVersionsWithOptions "\n" vs opts
                   , "satVariables " ++ show (M.size (satVariables satq))
                   , "satUninterp "  ++ show (length (satUninterp  satq)) ]
      str_to_hash = unlines str_prefix ++ anonLocalNames (scWriteExternal tm)
  return $ SolverCacheKey vs opts $ SHA256.hash $ encodeUtf8 $ T.pack $ str_to_hash
  where anonLocalNames = unlines . map (unwords . go . words) . lines
        go (x:y:_:xs) | y `elem` ["Pi", "Lam"] = x:y:"_":xs
        go xs = xs


-- Solver Cache Values ---------------------------------------------------------

-- | The value type for 'SolverCache': solver version information, the timestamp
-- of when the entry was last used, a 'String' representing the solver used, and
-- an optional list of counterexamples, represented as pairs of indexes into the
-- list of 'satVariables' of an associated 'SATQuery'
data SolverCacheValue =
  SolverCacheValue
  { solverCacheValueVersions   :: SolverBackendVersions
  , solverCacheValueOptions    :: [SolverBackendOption]
  , solverCacheValueSolverName :: String
  , solverCacheValueCEXs       :: Maybe [(Int, FirstOrderValue)]
  , solverCacheValueLastUsed   :: UTCTime
  } deriving Eq

instance FromJSON SolverCacheValue where
  parseJSON = JSON.withObject "SolverCacheValue" $ \v -> do
    vs      <- v .:  "vs"
    opts    <- v .:? "opts"
    nm      <- v .:  "nm"
    mb_cexs <- v .:? "cexs"
    t       <- v .:  "t"
    return $ SolverCacheValue vs (fromMaybe [] opts) nm mb_cexs t

instance ToJSON SolverCacheValue where
  toJSON (SolverCacheValue vs opts nm mb_cexs t) = JSON.object $
    ["vs" .= vs] ++ (if null opts then [] else ["opts" .= opts]) ++
    ["nm" .= nm] ++ maybe [] (\cexs -> ["cexs" .= cexs]) mb_cexs ++ ["t" .= t]
  toEncoding (SolverCacheValue vs opts nm mb_cexs t) = JSON.pairs $
    "vs" .= vs <> (if null opts then mempty else "opts" .= opts) <>
    "nm" .= nm <> maybe mempty (\cexs -> "cexs" .= cexs) mb_cexs <> "t" .= t

-- NOTE: We go through JSON because the `aeson` library gives us much nicer and
-- more customizable encodings than the `serialise` library, and because there
-- is a bijection between JSON and CBOR so we can freely pass between the two
instance Serialise SolverCacheValue where
  encode = encodeValue . toJSON
  decode = do
    v <- decodeValue False
    case fromJSON v of
      JSON.Success x -> return x
      JSON.Error e -> fail e

-- | Convert the result of a solver call on the given 'SATQuery' to a
-- 'SolverCacheValue'
toSolverCacheValue :: SolverBackendVersions -> [SolverBackendOption] ->
                      SATQuery -> (Maybe CEX, String) ->
                      IO (Maybe SolverCacheValue)
toSolverCacheValue vs opts satq (cexs, solver_name) = do
  getCurrentTime <&> \t -> case firstsMaybeM (`elemIndex` ecs) cexs of
    Just cexs' -> Just $ SolverCacheValue vs opts solver_name cexs' t
    Nothing -> Nothing
  where ecs = M.keys $ satVariables satq
        firstsMaybeM :: Monad m => (a -> m b) ->
                        Maybe [(a, c)] -> m (Maybe [(b, c)])
        firstsMaybeM = mapM . mapM . firstM

-- | Convert a 'SolverCacheValue' to something which has the same form as the
-- result of a solver call on the given 'SATQuery'
fromSolverCacheValue :: SATQuery -> SolverCacheValue -> (Maybe CEX, String)
fromSolverCacheValue satq (SolverCacheValue _ _ solver_name cexs _) =
  (firstsMaybe (ecs !!) cexs, solver_name)
  where ecs = M.keys $ satVariables satq
        firstsMaybe :: (a -> b) -> Maybe [(a, c)] -> Maybe [(b, c)]
        firstsMaybe = fmap . fmap . first


-- The Solver Cache ------------------------------------------------------------

-- | A 'SolverCache' consists of a 'FilePath' to an LMDB database (which may or
-- may not exist yet), an optional LMDB database at that path (represented as an
-- 'LMDB.Environment' and 'LMDB.Database' once it is created), counters for how
-- many lookups, failed lookups, insertions, and failed insertions have been made
-- (see 'SolverCacheStat'), a map size for the LMDB database, and a timeout to
-- use for database lookups and inserts. Note that the counters are stored in an
-- 'IORef' to make sure failures are counted correctly.
data SolverCache =
  SolverCache
  { solverCachePath    :: FilePath
  , solverCacheEnv     :: Maybe (LMDB.Environment LMDB.ReadWrite)
  , solverCacheDB      :: Maybe (LMDB.Database SolverCacheKey SolverCacheValue)
  , solverCacheStats   :: IORef (Map SolverCacheStat Integer)
  , solverCacheMapSize :: Int
  , solverCacheTimeout :: Int
  }

-- | A statistic to track in 'solverCacheStats'
data SolverCacheStat = Lookups | FailedLookups | Inserts | FailedInserts
                     deriving (Eq, Ord, Bounded, Enum)

-- | Create a 'SolverCache' with the given 'FilePath', but do not yet open an
-- LMDB database at that path (i.e. `solverCacheEnv` and `solverCacheDB` are
-- both set to 'Nothing')
lazyOpenSolverCache :: FilePath -> IO SolverCache
lazyOpenSolverCache path = do
  stats <- newIORef $ M.fromList ((,0) <$> [minBound..])
  return SolverCache { solverCachePath    = path,
                       solverCacheEnv     = Nothing,
                       solverCacheDB      = Nothing,
                       solverCacheStats   = stats,
                       solverCacheMapSize = 4 {- GiB -} * 1073741824,
                       solverCacheTimeout = 1 {- sec -} * 1000000 }

-- | Create a 'SolverCache' with the given 'FilePath' and open an LMDB database
-- at that path (i.e. `solverCacheEnv` and `solverCacheDB` are both 'Just')
openSolverCache :: FilePath -> IO SolverCache
openSolverCache path = do
  (_, _, cache') <- forceSolverCacheOpened =<< lazyOpenSolverCache path
  return cache'

-- | Ensure that the given 'SolverCache' has opened an LMDB database at its set
-- 'FilePath' - returning either the newly created or previously created
-- 'LMDB.Environment' and 'LMDB.Database', as well as an 'SolverCache'
-- containing both of them
forceSolverCacheOpened :: SolverCache ->
                          IO (LMDB.Environment LMDB.ReadWrite,
                              LMDB.Database SolverCacheKey SolverCacheValue,
                              SolverCache)
forceSolverCacheOpened cache@SolverCache{ solverCacheEnv = Just env
                                        , solverCacheDB  = Just db } =
  return (env, db, cache)
forceSolverCacheOpened cache@SolverCache{..} = do
  createDirectoryIfMissing True solverCachePath
  let limits = LMDB.defaultLimits { LMDB.mapSize = solverCacheMapSize }
  env <- LMDB.openEnvironment solverCachePath limits
  db <- LMDB.readOnlyTransaction env (LMDB.getDatabase Nothing)
  let cache' = cache { solverCacheEnv = Just env, solverCacheDB = Just db }
  return (env, db, cache')

-- | Try to call 'forceSolverCacheOpened' then try to perform the given
-- 'LMDB.Transaction' on the LMDB database associated to the given
-- 'SolverCache', returning 'Left' if an error or timeout occurred at any point
-- and 'Right' otherwise, as well as the updated 'SolverCache' returned by
-- 'forceSolverCacheOpened'
tryTransaction :: (LMDB.Mode tmode, LMDB.SubMode LMDB.ReadWrite tmode) =>
                  SolverCache ->
                  (LMDB.Database SolverCacheKey SolverCacheValue ->
                   LMDB.Transaction tmode a) ->
                  IO (Either String a, SolverCache)
tryTransaction cache@SolverCache{..} t =
  tryWithTimeout solverCacheTimeout (forceSolverCacheOpened cache) >>= \case
    Right (env, db, cache') -> 
      (,cache') <$> tryWithTimeout solverCacheTimeout
                                   (LMDB.transaction env (t db))
    Left err ->
      return (Left $ "Failed to open LMDB database: " ++ err, cache)

-- | An operation on a 'SolverCache', returning a value of the given type as
-- well as an updated 'SolverCache' ('solverCacheOp'). Additionally, in the case
-- of no enabled solver cache, the operation could either fail or return a
-- default value ('solverCacheOpDefault').
data SolverCacheOp a = SCOpOrFail (Options -> SolverCache -> IO (a, SolverCache))
                     | SCOpOrDefault a (Options -> SolverCache -> IO (a, SolverCache))

-- | Get the operation associated to a 'SolverCacheOp'
solverCacheOp :: SolverCacheOp a -> Options -> SolverCache -> IO (a, SolverCache)
solverCacheOp (SCOpOrFail f) = f
solverCacheOp (SCOpOrDefault _ f) = f

-- | Get the default value associated to a 'SolverCacheOp', if any
solverCacheOpDefault :: SolverCacheOp a -> Maybe a
solverCacheOpDefault (SCOpOrFail _) = Nothing
solverCacheOpDefault (SCOpOrDefault a _) = Just a

-- | Lookup a 'SolverCacheKey' in the solver result cache
lookupInSolverCache :: SolverCacheKey -> SolverCacheOp (Maybe SolverCacheValue)
lookupInSolverCache k = SCOpOrDefault Nothing $ \opts cache@SolverCache{..} ->
  getCurrentTime >>= \now ->
  let upd _ v = Just v { solverCacheValueLastUsed = now } in
  tryTransaction cache (LMDB.updateLookupWithKey upd k) >>= \case
    (Right (Just v), cache') -> do
      printOutLn opts Debug ("Using cached result: " ++ show k)
      modifyIORef solverCacheStats $ M.adjust (+1) Lookups
      return (Just v, cache')
    (Left err, cache') -> do
      printOutLn opts Warn ("Solver cache lookup failed:\n" ++ err)
      modifyIORef solverCacheStats $ M.adjust (+1) FailedLookups
      return (Nothing, cache')
    (Right Nothing, cache') -> do
      return (Nothing, cache')

-- | Add a 'SolverCacheValue' to the solver result cache
insertInSolverCache :: SolverCacheKey -> SolverCacheValue -> SolverCacheOp ()
insertInSolverCache k v = SCOpOrDefault () $ \opts cache@SolverCache{..} ->
  printOutLn opts Debug ("Caching result: " ++ show k) >>
  tryTransaction cache (LMDB.insert k v) >>= \case
    (Right (), cache') -> do
      modifyIORef solverCacheStats $ M.adjust (+1) Inserts
      return ((), cache')
    (Left err, cache') -> do
      printOutLn opts Warn ("Solver cache insert failed:\n" ++ err)
      modifyIORef solverCacheStats $ M.adjust (+1) FailedInserts
      return ((), cache')

-- | Set the 'FilePath' of the solver result cache and save all results cached
-- so far
setSolverCachePath :: FilePath -> SolverCacheOp ()
setSolverCachePath path = SCOpOrFail $ \opts cache@SolverCache{..} ->
  if path == solverCachePath
  then do
    (_, _, cache') <- forceSolverCacheOpened cache
    return ((), cache')
  else do
    (new_env, new_db, cache') <-
        forceSolverCacheOpened cache { solverCachePath = path
                                     , solverCacheEnv  = Nothing
                                     , solverCacheDB   = Nothing }
    case (solverCacheEnv, solverCacheDB) of
      (Just old_env, Just old_db) -> do
        kvs <- LMDB.readOnlyTransaction old_env $ LMDB.toList old_db
        forM_ kvs $ \(k,v) -> LMDB.transaction new_env $ LMDB.insert k v new_db
        printOutLn opts Info ("Saved " ++ show (length kvs) ++ " cached result" ++
                              (if length kvs == 1 then "" else "s") ++ " to disk")
        return ((), cache')
      _ -> return ((), cache')

-- | Print all entries in the solver result cache whose SHA256 hash keys start
-- with the given string
printSolverCacheByHex :: String -> SolverCacheOp ()
printSolverCacheByHex hex_pref = SCOpOrFail $ \opts cache -> do
  (env, db, cache') <- forceSolverCacheOpened cache
  let flt k v kvs = if hex_pref `isPrefixOf` encodeHex (solverCacheKeyHash k)
                    then (k,v):kvs else kvs
  kvs <- case decodeHex hex_pref of
    Right (solverCacheKeyFromHash -> k) -> do
      LMDB.readOnlyTransaction env (LMDB.lookup k db) >>= \case
        Just v -> return [(k,v)]
        Nothing -> LMDB.readOnlyTransaction env $ LMDB.foldrWithKey flt [] db
    Left _ -> LMDB.readOnlyTransaction env $ LMDB.foldrWithKey flt [] db
  when (length kvs == 0) $ printOutLn opts Info "No keys found"
  forM_ kvs $ \(k, SolverCacheValue vs bk_opts nm mb_cexs t) -> do
    let vs_str = showBackendVersionsWithOptions ", " vs bk_opts
        res_str = maybe "unsat" (("sat " ++) . show) mb_cexs
    printOutLn opts Info $ "SHA: " ++ encodeHex (solverCacheKeyHash k)
    printOutLn opts Info $ "- Result: " ++ res_str
    printOutLn opts Info $ "- Solver: " ++ show nm
    printOutLn opts Info $ "- Versions: " ++ vs_str
    printOutLn opts Info $ "- Last used: " ++ show t ++ "\n"
  return ((), cache')

-- | Remove all entries in the solver result cache which have version(s) that
-- do not match the current version(s) or are marked as stale
cleanSolverCache :: SolverBackendVersions -> SolverCacheOp ()
cleanSolverCache curr_base_vs = SCOpOrFail $ \opts cache -> do
  let known_curr_base_vs = M.filter isJust curr_base_vs
      mismatched_vs vs = M.mapMaybe id $ M.intersectionWith
        (\base_ver v_ver -> if base_ver /= v_ver
                            then Just (base_ver, v_ver) else Nothing)
        known_curr_base_vs vs
      flt k v (ks, mvs) = let mvs' = mismatched_vs (solverCacheValueVersions v)
                           in if M.null mvs' then (ks, mvs)
                                             else (k:ks, M.union mvs mvs')
  (env, db, cache') <- forceSolverCacheOpened cache
  (ks, mvs) <- LMDB.readOnlyTransaction env $ LMDB.foldrWithKey flt ([], M.empty) db
  forM_ ks $ \k -> LMDB.transaction env $ LMDB.delete k db
  let s0 = if length ks == 1 then "" else "s"
      s1 = if M.size mvs == 0 then "" else ":"
  printOutLn opts Info $
    "Removed " ++ show (length ks) ++
    " cached result" ++ s0 ++ " with mismatched version" ++ s0 ++ s1
  forM_ (M.toList mvs) $ \(backend, (v1, v2)) ->
    printOutLn opts Info $
      "- " ++ showSolverBackendVersion backend v1 [] ++
      " (Current: " ++ showSolverBackendVersion backend v2 [] ++ ")"
  return ((), cache')

-- | Print out statistics about how the solver cache was used
printSolverCacheStats :: SolverCacheOp ()
printSolverCacheStats = SCOpOrFail $ \opts cache@SolverCache{..} -> do
  (env, db, cache') <- forceSolverCacheOpened cache
  printOutLn opts Info ("== Solver result cache statistics ==")
  sz <- LMDB.readOnlyTransaction env $ LMDB.size db
  printOutLn opts Info ("- " ++ show sz ++ " result" ++ pl sz
                             ++ " cached in " ++ solverCachePath)
  stats <- readIORef solverCacheStats
  let (ls, ls_f) = (stats M.! Lookups, stats M.! FailedLookups)
      (is, is_f) = (stats M.! Inserts, stats M.! FailedInserts)
  printOutLn opts Info $ "- " ++ show is ++ " insertion" ++ pl is
                              ++ " into the cache so far this run ("
                              ++ show is_f ++ " failed attempt" ++ pl is_f ++ ")"
  printOutLn opts Info $ "- " ++ show ls ++ " usage" ++ pl ls
                              ++ " of cached results so far this run ("
                              ++ show ls_f ++ " failed attempt" ++ pl ls_f ++ ")"
  return ((), cache')
  where pl i = if i == 1 then "" else "s"

-- | Check whether the values of the statistics printed out by
-- 'printSolverCacheStats' are equal to those given, failing if this does not
-- hold
testSolverCacheStats :: Integer -> Integer -> Integer -> Integer -> Integer ->
                        SolverCacheOp ()
testSolverCacheStats sz ls ls_f is is_f = SCOpOrFail $ \opts cache@SolverCache{..} -> do
  (env, db, cache') <- forceSolverCacheOpened cache
  sz_actual <- fromIntegral <$> LMDB.readOnlyTransaction env (LMDB.size db)
  test sz sz_actual "Size of solver cache"
  stats <- readIORef solverCacheStats
  test ls (stats M.! Lookups) "Number of usages of solver cache"
  test ls_f (stats M.! FailedLookups) "Number of failed usages of solver cache"
  test is (stats M.! Inserts) "Number of insertions into solver cache"
  test is_f (stats M.! FailedInserts) "Number of failed insertions into solver cache"
  printOutLn opts Info $ "Solver cache stats matched expected (" ++ show sz ++ " " ++
    show ls ++ " " ++ show ls_f ++ " " ++ show is ++ " " ++ show is_f ++ ")"
  return ((), cache')
  where test v v_actual str = when (v /= v_actual) $ fail $
          str ++ " (" ++ show v_actual ++ ")"
              ++ " did not match expected (" ++ show v ++ ")"