    -- |
    -- Module      :  Cryptol.Symbolic.What4
    -- Copyright   :  (c) 2013-2020 Galois, Inc.
    -- License     :  BSD3
    -- Maintainer  :  cryptol@galois.com
    -- Stability   :  provisional
    -- Portability :  portable

    {-# LANGUAGE BlockArguments #-}
    {-# LANGUAGE FlexibleContexts #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE ImplicitParams #-}
    {-# LANGUAGE LambdaCase #-}
    {-# LANGUAGE ParallelListComp #-}
    {-# LANGUAGE PatternGuards #-}
    {-# LANGUAGE RankNTypes #-}
    {-# LANGUAGE RecordWildCards #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE TupleSections #-}
    {-# LANGUAGE TypeFamilies #-}
    {-# LANGUAGE TypeOperators #-}
    {-# LANGUAGE FlexibleContexts #-}
    {-# LANGUAGE ViewPatterns #-}

    module Cryptol.Symbolic.What4
     ( W4ProverConfig
     , defaultProver
     , proverNames
     , setupProver
     , satProve
     , satProveOffline
     , W4Exception(..)
     ) where

    import Control.Applicative
    import Control.Concurrent.Async
    import Control.Concurrent.MVar
    import Control.Monad.IO.Class
    import Control.Monad (when, foldM, forM_, void)
    import qualified Control.Exception as X
    import System.IO (Handle, IOMode(..), withFile)
    import Data.Time
    import Data.IORef
    import Data.List (intercalate, tails, inits)
    import Data.List.NonEmpty (NonEmpty(..))
    import Data.Proxy
    import qualified Data.Map as Map
    import           Data.Set (Set)
    import qualified Data.Set as Set
    import           Data.Text (Text)
    import qualified Data.Text as Text
    import qualified Data.List.NonEmpty as NE
    import System.Exit

    import qualified Cryptol.ModuleSystem as M hiding (getPrimMap)
    import qualified Cryptol.ModuleSystem.Env as M
    import qualified Cryptol.ModuleSystem.Base as M
    import qualified Cryptol.ModuleSystem.Monad as M
    import qualified Cryptol.ModuleSystem.Name as M

    import qualified Cryptol.Backend.FloatHelpers as FH
    import           Cryptol.Backend.What4

    import qualified Cryptol.Eval as Eval
    import qualified Cryptol.Eval.Concrete as Concrete
    import qualified Cryptol.Eval.Value as Eval
    import           Cryptol.Eval.Type (TValue)
    import           Cryptol.Eval.What4

    import           Cryptol.Parser.Position (emptyRange)
    import           Cryptol.Symbolic
    import           Cryptol.TypeCheck.AST
    import           Cryptol.Utils.Logger(logPutStrLn,logPutStr,Logger)
    import           Cryptol.Utils.Ident (preludeReferenceName, prelPrim, identText)

    import qualified What4.Config as W4
    import qualified What4.Interface as W4
    import qualified What4.Expr.Builder as W4
    import qualified What4.Expr.GroundEval as W4
    import qualified What4.SatResult as W4
    import qualified What4.SFloat as W4
    import qualified What4.SWord as SW
    import           What4.Solver
    import qualified What4.Solver.Boolector as W4
    import qualified What4.Solver.CVC4 as W4
    import qualified What4.Solver.CVC5 as W4
    import qualified What4.Solver.ExternalABC as W4
    import qualified What4.Solver.Yices as W4
    import qualified What4.Solver.Z3 as W4
    import qualified What4.Solver.Adapter as W4
    import qualified What4.Protocol.Online as W4
    import qualified What4.Protocol.SMTLib2 as W4
    import qualified What4.ProblemFeatures as W4

    import qualified Data.BitVector.Sized as BV
    import           Data.Parameterized.Nonce

    import Prelude ()
    import Prelude.Compat

    data W4Exception
      = W4Ex X.SomeException
      | W4PortfolioFailure [ (Either X.SomeException (Maybe String, String)) ]

    instance Show W4Exception where
      show :: W4Exception -> String
    show (W4Ex SomeException
    e) = SomeException -> String
    forall e. Exception e => e -> String
    X.displayException SomeException
    e
      show (W4PortfolioFailure [Either SomeException (Maybe String, String)]
    exs) =
           [String] -> String
    unlines (String
    "All solveres in the portfolio failed!"String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    :(Either SomeException (Maybe String, String) -> String)
    -> [Either SomeException (Maybe String, String)] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map Either SomeException (Maybe String, String) -> String
    forall {e}.
    Exception e =>
    Either e (Maybe String, String) -> String
    f [Either SomeException (Maybe String, String)]
    exs)
        where
        f :: Either e (Maybe String, String) -> String
    f (Left e
    e) = e -> String
    forall e. Exception e => e -> String
    X.displayException e
    e
        f (Right (Maybe String
    Nothing, String
    msg)) = String
    msg
        f (Right (Just String
    nm, String
    msg)) = String
    nm String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ": " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    msg

    instance X.Exception W4Exception

    rethrowW4Exception :: IO a -> IO a
    rethrowW4Exception :: forall a. IO a -> IO a
    rethrowW4Exception IO a
    m = (SomeException -> Maybe SomeException)
    -> IO a -> (SomeException -> IO a) -> IO a
    forall e b a.
    Exception e =>
    (e -> Maybe b) -> IO a -> (b -> IO a) -> IO a
    X.catchJust SomeException -> Maybe SomeException
    f IO a
    m (W4Exception -> IO a
    forall e a. Exception e => e -> IO a
    X.throwIO (W4Exception -> IO a)
    -> (SomeException -> W4Exception) -> SomeException -> IO a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SomeException -> W4Exception
    W4Ex)
      where
      f :: SomeException -> Maybe SomeException
    f SomeException
    e
        | Just ( AsyncException
    _ :: X.AsyncException) <- SomeException -> Maybe AsyncException
    forall e. Exception e => SomeException -> Maybe e
    X.fromException SomeException
    e = Maybe SomeException
    forall a. Maybe a
    Nothing
        | Just ( Unsupported
    _ :: Eval.Unsupported) <- SomeException -> Maybe Unsupported
    forall e. Exception e => SomeException -> Maybe e
    X.fromException SomeException
    e = Maybe SomeException
    forall a. Maybe a
    Nothing
        | Bool
    otherwise = SomeException -> Maybe SomeException
    forall a. a -> Maybe a
    Just SomeException
    e

    protectStack :: (String -> M.ModuleCmd a)
                 -> M.ModuleCmd a
                 -> M.ModuleCmd a
    protectStack :: forall a. (String -> ModuleCmd a) -> ModuleCmd a -> ModuleCmd a
    protectStack String -> ModuleCmd a
    mkErr ModuleCmd a
    cmd ModuleInput IO
    modEnv =
      IO (ModuleRes a) -> IO (ModuleRes a)
    forall a. IO a -> IO a
    rethrowW4Exception (IO (ModuleRes a) -> IO (ModuleRes a))
    -> IO (ModuleRes a) -> IO (ModuleRes a)
    forall a b. (a -> b) -> a -> b
    $
      (AsyncException -> Maybe ())
    -> IO (ModuleRes a) -> (() -> IO (ModuleRes a)) -> IO (ModuleRes a)
    forall e b a.
    Exception e =>
    (e -> Maybe b) -> IO a -> (b -> IO a) -> IO a
    X.catchJust AsyncException -> Maybe ()
    isOverflow (ModuleCmd a
    cmd ModuleInput IO
    modEnv) () -> IO (ModuleRes a)
    handler
      where isOverflow :: AsyncException -> Maybe ()
    isOverflow AsyncException
    X.StackOverflow = () -> Maybe ()
    forall a. a -> Maybe a
    Just ()
            isOverflow AsyncException
    _               = Maybe ()
    forall a. Maybe a
    Nothing
            msg :: String
    msg = String
    "Symbolic evaluation failed to terminate."
            handler :: () -> IO (ModuleRes a)
    handler () = String -> ModuleCmd a
    mkErr String
    msg ModuleInput IO
    modEnv

    -- | Returns definitions, together with the value and it safety predicate.
    doW4Eval ::
      (W4.IsExprBuilder sym, MonadIO m) =>
      sym -> W4Eval sym a -> m (W4.Pred sym, a)
    doW4Eval :: forall sym (m :: * -> *) a.
    (IsExprBuilder sym, MonadIO m) =>
    sym -> W4Eval sym a -> m (Pred sym, a)
    doW4Eval sym
    sym W4Eval sym a
    m =
      do W4Result sym a
    res <- IO (W4Result sym a) -> m (W4Result sym a)
    forall a. IO a -> m a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (W4Result sym a) -> m (W4Result sym a))
    -> IO (W4Result sym a) -> m (W4Result sym a)
    forall a b. (a -> b) -> a -> b
    $ CallStack -> Eval (W4Result sym a) -> IO (W4Result sym a)
    forall a. CallStack -> Eval a -> IO a
    Eval.runEval CallStack
    forall a. Monoid a => a
    mempty (W4Eval sym a -> sym -> Eval (W4Result sym a)
    forall sym a. W4Eval sym a -> sym -> Eval (W4Result sym a)
    w4Eval W4Eval sym a
    m sym
    sym)
         case W4Result sym a
    res of
           W4Error EvalErrorEx
    err  -> IO (Pred sym, a) -> m (Pred sym, a)
    forall a. IO a -> m a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (EvalErrorEx -> IO (Pred sym, a)
    forall e a. Exception e => e -> IO a
    X.throwIO EvalErrorEx
    err)
           W4Result Pred sym
    p a
    x -> (Pred sym, a) -> m (Pred sym, a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Pred sym
    p,a
    x)

    data AnAdapter
      = AnAdapter (forall st. SolverAdapter st)
      | forall s. W4.OnlineSolver s =>
         AnOnlineAdapter
           String
           W4.ProblemFeatures
           [W4.ConfigDesc]
           (Proxy s)

    data W4ProverConfig
      = W4ProverConfig AnAdapter
      | W4OfflineConfig
      | W4Portfolio (NonEmpty AnAdapter)

    proverConfigs :: [(String, W4ProverConfig)]
    proverConfigs :: [(String, W4ProverConfig)]
    proverConfigs =
      [ (String
    "w4-cvc4"      , AnAdapter -> W4ProverConfig
    W4ProverConfig AnAdapter
    cvc4OnlineAdapter)
      , (String
    "w4-cvc5"      , AnAdapter -> W4ProverConfig
    W4ProverConfig AnAdapter
    cvc5OnlineAdapter)
      , (String
    "w4-yices"     , AnAdapter -> W4ProverConfig
    W4ProverConfig AnAdapter
    yicesOnlineAdapter)
      , (String
    "w4-z3"        , AnAdapter -> W4ProverConfig
    W4ProverConfig AnAdapter
    z3OnlineAdapter)
      , (String
    "w4-boolector" , AnAdapter -> W4ProverConfig
    W4ProverConfig AnAdapter
    boolectorOnlineAdapter)

      , (String
    "w4-abc"       , AnAdapter -> W4ProverConfig
    W4ProverConfig ((forall (st :: * -> *). SolverAdapter st) -> AnAdapter
    AnAdapter SolverAdapter st
    forall (st :: * -> *). SolverAdapter st
    W4.externalABCAdapter))

      , (String
    "w4-offline"   , W4ProverConfig
    W4OfflineConfig )
      , (String
    "w4-any"       , W4ProverConfig
    allSolvers)
      ]

    z3OnlineAdapter :: AnAdapter
    z3OnlineAdapter :: AnAdapter
    z3OnlineAdapter =
      String
    -> ProblemFeatures
    -> [ConfigDesc]
    -> Proxy (Writer Z3)
    -> AnAdapter
    forall s.
    OnlineSolver s =>
    String -> ProblemFeatures -> [ConfigDesc] -> Proxy s -> AnAdapter
    AnOnlineAdapter String
    "Z3" ProblemFeatures
    W4.z3Features [ConfigDesc]
    W4.z3Options
             (Proxy (Writer Z3)
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy (W4.Writer W4.Z3))

    yicesOnlineAdapter :: AnAdapter
    yicesOnlineAdapter :: AnAdapter
    yicesOnlineAdapter =
      String
    -> ProblemFeatures -> [ConfigDesc] -> Proxy Connection -> AnAdapter
    forall s.
    OnlineSolver s =>
    String -> ProblemFeatures -> [ConfigDesc] -> Proxy s -> AnAdapter
    AnOnlineAdapter String
    "Yices" ProblemFeatures
    W4.yicesDefaultFeatures [ConfigDesc]
    W4.yicesOptions
             (Proxy Connection
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy W4.Connection)

    cvc4OnlineAdapter :: AnAdapter
    cvc4OnlineAdapter :: AnAdapter
    cvc4OnlineAdapter =
      String
    -> ProblemFeatures
    -> [ConfigDesc]
    -> Proxy (Writer CVC4)
    -> AnAdapter
    forall s.
    OnlineSolver s =>
    String -> ProblemFeatures -> [ConfigDesc] -> Proxy s -> AnAdapter
    AnOnlineAdapter String
    "CVC4" ProblemFeatures
    W4.cvc4Features [ConfigDesc]
    W4.cvc4Options
             (Proxy (Writer CVC4)
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy (W4.Writer W4.CVC4))

    cvc5OnlineAdapter :: AnAdapter
    cvc5OnlineAdapter :: AnAdapter
    cvc5OnlineAdapter =
      String
    -> ProblemFeatures
    -> [ConfigDesc]
    -> Proxy (Writer CVC5)
    -> AnAdapter
    forall s.
    OnlineSolver s =>
    String -> ProblemFeatures -> [ConfigDesc] -> Proxy s -> AnAdapter
    AnOnlineAdapter String
    "CVC5" ProblemFeatures
    W4.cvc5Features [ConfigDesc]
    W4.cvc5Options
             (Proxy (Writer CVC5)
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy (W4.Writer W4.CVC5))

    boolectorOnlineAdapter :: AnAdapter
    boolectorOnlineAdapter :: AnAdapter
    boolectorOnlineAdapter =
      String
    -> ProblemFeatures
    -> [ConfigDesc]
    -> Proxy (Writer Boolector)
    -> AnAdapter
    forall s.
    OnlineSolver s =>
    String -> ProblemFeatures -> [ConfigDesc] -> Proxy s -> AnAdapter
    AnOnlineAdapter String
    "Boolector" ProblemFeatures
    W4.boolectorFeatures [ConfigDesc]
    W4.boolectorOptions
             (Proxy (Writer Boolector)
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy (W4.Writer W4.Boolector))

    allSolvers :: W4ProverConfig
    allSolvers :: W4ProverConfig
    allSolvers = NonEmpty AnAdapter -> W4ProverConfig
    W4Portfolio
      (NonEmpty AnAdapter -> W4ProverConfig)
    -> NonEmpty AnAdapter -> W4ProverConfig
    forall a b. (a -> b) -> a -> b
    $ AnAdapter
    z3OnlineAdapter AnAdapter -> [AnAdapter] -> NonEmpty AnAdapter
    forall a. a -> [a] -> NonEmpty a
    :|
      [ AnAdapter
    cvc4OnlineAdapter
      , AnAdapter
    cvc5OnlineAdapter
      , AnAdapter
    boolectorOnlineAdapter
      , AnAdapter
    yicesOnlineAdapter
      , (forall (st :: * -> *). SolverAdapter st) -> AnAdapter
    AnAdapter SolverAdapter st
    forall (st :: * -> *). SolverAdapter st
    W4.externalABCAdapter
      ]

    defaultProver :: W4ProverConfig
    defaultProver :: W4ProverConfig
    defaultProver = AnAdapter -> W4ProverConfig
    W4ProverConfig AnAdapter
    z3OnlineAdapter

    proverNames :: [String]
    proverNames :: [String]
    proverNames = ((String, W4ProverConfig) -> String)
    -> [(String, W4ProverConfig)] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (String, W4ProverConfig) -> String
    forall a b. (a, b) -> a
    fst [(String, W4ProverConfig)]
    proverConfigs

    setupProver :: String -> IO (Either String ([String], W4ProverConfig))
    setupProver :: String -> IO (Either String ([String], W4ProverConfig))
    setupProver String
    nm =
      IO (Either String ([String], W4ProverConfig))
    -> IO (Either String ([String], W4ProverConfig))
    forall a. IO a -> IO a
    rethrowW4Exception (IO (Either String ([String], W4ProverConfig))
     -> IO (Either String ([String], W4ProverConfig)))
    -> IO (Either String ([String], W4ProverConfig))
    -> IO (Either String ([String], W4ProverConfig))
    forall a b. (a -> b) -> a -> b
    $
      case String -> [(String, W4ProverConfig)] -> Maybe W4ProverConfig
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup String
    nm [(String, W4ProverConfig)]
    proverConfigs of
        Just cfg :: W4ProverConfig
    cfg@(W4ProverConfig AnAdapter
    p) ->
          do Maybe SomeException
    st <- AnAdapter -> IO (Maybe SomeException)
    tryAdapter AnAdapter
    p
             let ws :: [String]
    ws = case Maybe SomeException
    st of
                        Maybe SomeException
    Nothing -> []
                        Just SomeException
    ex -> [ String
    "Warning: solver interaction failed with " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    nm, String
    "    " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SomeException -> String
    forall a. Show a => a -> String
    show SomeException
    ex ]
             Either String ([String], W4ProverConfig)
    -> IO (Either String ([String], W4ProverConfig))
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (([String], W4ProverConfig)
    -> Either String ([String], W4ProverConfig)
    forall a b. b -> Either a b
    Right ([String]
    ws, W4ProverConfig
    cfg))

        Just (W4Portfolio NonEmpty AnAdapter
    ps) ->
          [AnAdapter] -> IO [AnAdapter]
    filterAdapters (NonEmpty AnAdapter -> [AnAdapter]
    forall a. NonEmpty a -> [a]
    NE.toList NonEmpty AnAdapter
    ps) IO [AnAdapter]
    -> ([AnAdapter] -> IO (Either String ([String], W4ProverConfig)))
    -> IO (Either String ([String], W4ProverConfig))
    forall a b. IO a -> (a -> IO b) -> IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
             [] -> Either String ([String], W4ProverConfig)
    -> IO (Either String ([String], W4ProverConfig))
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (String -> Either String ([String], W4ProverConfig)
    forall a b. a -> Either a b
    Left String
    "What4 could not communicate with any provers!")
             (AnAdapter
    p:[AnAdapter]
    ps') ->
               let msg :: String
    msg = String
    "What4 found the following solvers: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    forall a. Show a => a -> String
    show ([AnAdapter] -> [String]
    adapterNames (AnAdapter
    pAnAdapter -> [AnAdapter] -> [AnAdapter]
    forall a. a -> [a] -> [a]
    :[AnAdapter]
    ps')) in
               Either String ([String], W4ProverConfig)
    -> IO (Either String ([String], W4ProverConfig))
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (([String], W4ProverConfig)
    -> Either String ([String], W4ProverConfig)
    forall a b. b -> Either a b
    Right ([String
    msg], NonEmpty AnAdapter -> W4ProverConfig
    W4Portfolio (AnAdapter
    pAnAdapter -> [AnAdapter] -> NonEmpty AnAdapter
    forall a. a -> [a] -> NonEmpty a
    :|[AnAdapter]
    ps')))

        Just W4ProverConfig
    W4OfflineConfig -> Either String ([String], W4ProverConfig)
    -> IO (Either String ([String], W4ProverConfig))
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (([String], W4ProverConfig)
    -> Either String ([String], W4ProverConfig)
    forall a b. b -> Either a b
    Right ([], W4ProverConfig
    W4OfflineConfig))

        Maybe W4ProverConfig
    Nothing -> Either String ([String], W4ProverConfig)
    -> IO (Either String ([String], W4ProverConfig))
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (String -> Either String ([String], W4ProverConfig)
    forall a b. a -> Either a b
    Left (String
    "unknown solver name: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    nm))

      where
      adapterNames :: [AnAdapter] -> [String]
    adapterNames [] = []
      adapterNames (AnAdapter forall (st :: * -> *). SolverAdapter st
    adpt : [AnAdapter]
    ps) =
        SolverAdapter Any -> String
    forall (st :: * -> *). SolverAdapter st -> String
    solver_adapter_name SolverAdapter Any
    forall (st :: * -> *). SolverAdapter st
    adpt String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : [AnAdapter] -> [String]
    adapterNames [AnAdapter]
    ps
      adapterNames (AnOnlineAdapter String
    n ProblemFeatures
    _ [ConfigDesc]
    _ Proxy s
    _ : [AnAdapter]
    ps) =
        String
    n String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : [AnAdapter] -> [String]
    adapterNames [AnAdapter]
    ps

      filterAdapters :: [AnAdapter] -> IO [AnAdapter]
    filterAdapters [] = [AnAdapter] -> IO [AnAdapter]
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure []
      filterAdapters (AnAdapter
    p:[AnAdapter]
    ps) =
        AnAdapter -> IO (Maybe SomeException)
    tryAdapter AnAdapter
    p IO (Maybe SomeException)
    -> (Maybe SomeException -> IO [AnAdapter]) -> IO [AnAdapter]
    forall a b. IO a -> (a -> IO b) -> IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
          Just SomeException
    _err -> [AnAdapter] -> IO [AnAdapter]
    filterAdapters [AnAdapter]
    ps
          Maybe SomeException
    Nothing   -> (AnAdapter
    pAnAdapter -> [AnAdapter] -> [AnAdapter]
    forall a. a -> [a] -> [a]
    :) ([AnAdapter] -> [AnAdapter]) -> IO [AnAdapter] -> IO [AnAdapter]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [AnAdapter] -> IO [AnAdapter]
    filterAdapters [AnAdapter]
    ps

      tryAdapter :: AnAdapter -> IO (Maybe X.SomeException)

      tryAdapter :: AnAdapter -> IO (Maybe SomeException)
    tryAdapter (AnAdapter forall (st :: * -> *). SolverAdapter st
    adpt) =
         do ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
    sym <- FloatModeRepr 'FloatIEEE
    -> CryptolState GlobalNonceGenerator
    -> NonceGenerator IO GlobalNonceGenerator
    -> IO
         (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
    forall (fm :: FloatMode) (st :: * -> *) t.
    FloatModeRepr fm
    -> st t -> NonceGenerator IO t -> IO (ExprBuilder t st (Flags fm))
    W4.newExprBuilder FloatModeRepr 'FloatIEEE
    W4.FloatIEEERepr CryptolState GlobalNonceGenerator
    forall t. CryptolState t
    CryptolState NonceGenerator IO GlobalNonceGenerator
    globalNonceGenerator
            [ConfigDesc] -> Config -> IO ()
    W4.extendConfig (SolverAdapter Any -> [ConfigDesc]
    forall (st :: * -> *). SolverAdapter st -> [ConfigDesc]
    W4.solver_adapter_config_options SolverAdapter Any
    forall (st :: * -> *). SolverAdapter st
    adpt) (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
    -> Config
    forall sym. IsExprBuilder sym => sym -> Config
    W4.getConfiguration ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
    sym)
            ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
    -> SolverAdapter CryptolState -> IO (Maybe SomeException)
    forall t (st :: * -> *) fs.
    ExprBuilder t st fs -> SolverAdapter st -> IO (Maybe SomeException)
    W4.smokeTest ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
    sym SolverAdapter CryptolState
    forall (st :: * -> *). SolverAdapter st
    adpt

      tryAdapter (AnOnlineAdapter String
    _ ProblemFeatures
    fs [ConfigDesc]
    opts (Proxy s
    _ :: Proxy s)) = IO (Maybe SomeException)
    test IO (Maybe SomeException)
    -> (SomeException -> IO (Maybe SomeException))
    -> IO (Maybe SomeException)
    forall e a. Exception e => IO a -> (e -> IO a) -> IO a
    `X.catch` (Maybe SomeException -> IO (Maybe SomeException)
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Maybe SomeException -> IO (Maybe SomeException))
    -> (SomeException -> Maybe SomeException)
    -> SomeException
    -> IO (Maybe SomeException)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SomeException -> Maybe SomeException
    forall a. a -> Maybe a
    Just)
       where
        test :: IO (Maybe SomeException)
    test =
          do ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
    sym <- FloatModeRepr 'FloatIEEE
    -> CryptolState GlobalNonceGenerator
    -> NonceGenerator IO GlobalNonceGenerator
    -> IO
         (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
    forall (fm :: FloatMode) (st :: * -> *) t.
    FloatModeRepr fm
    -> st t -> NonceGenerator IO t -> IO (ExprBuilder t st (Flags fm))
    W4.newExprBuilder FloatModeRepr 'FloatIEEE
    W4.FloatIEEERepr CryptolState GlobalNonceGenerator
    forall t. CryptolState t
    CryptolState NonceGenerator IO GlobalNonceGenerator
    globalNonceGenerator
             [ConfigDesc] -> Config -> IO ()
    W4.extendConfig [ConfigDesc]
    opts (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
    -> Config
    forall sym. IsExprBuilder sym => sym -> Config
    W4.getConfiguration ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
    sym)
             (SolverProcess GlobalNonceGenerator s
    proc :: W4.SolverProcess GlobalNonceGenerator s) <- ProblemFeatures
    -> Maybe Handle
    -> ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
    -> IO (SolverProcess GlobalNonceGenerator s)
    forall solver scope (st :: * -> *) fs.
    OnlineSolver solver =>
    ProblemFeatures
    -> Maybe Handle
    -> ExprBuilder scope st fs
    -> IO (SolverProcess scope solver)
    forall scope (st :: * -> *) fs.
    ProblemFeatures
    -> Maybe Handle
    -> ExprBuilder scope st fs
    -> IO (SolverProcess scope s)
    W4.startSolverProcess ProblemFeatures
    fs Maybe Handle
    forall a. Maybe a
    Nothing ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
    sym
             SatResult () ()
    res <- SolverProcess GlobalNonceGenerator s
    -> String -> BoolExpr GlobalNonceGenerator -> IO (SatResult () ())
    forall solver scope.
    SMTReadWriter solver =>
    SolverProcess scope solver
    -> String -> BoolExpr scope -> IO (SatResult () ())
    W4.checkSatisfiable SolverProcess GlobalNonceGenerator s
    proc String
    "smoke test" (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
    -> Pred
         (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
    forall sym. IsExprBuilder sym => sym -> Pred sym
    W4.falsePred ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
    sym)
             case SatResult () ()
    res of
               W4.Unsat () -> () -> IO ()
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
               SatResult () ()
    _ -> String -> IO ()
    forall a. String -> IO a
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail String
    "smoke test failed, expected UNSAT!"
             IO (ExitCode, Text) -> IO ()
    forall (f :: * -> *) a. Functor f => f a -> f ()
    void (SolverProcess GlobalNonceGenerator s -> IO (ExitCode, Text)
    forall scope. SolverProcess scope s -> IO (ExitCode, Text)
    forall solver scope.
    OnlineSolver solver =>
    SolverProcess scope solver -> IO (ExitCode, Text)
    W4.shutdownSolverProcess SolverProcess GlobalNonceGenerator s
    proc)
             Maybe SomeException -> IO (Maybe SomeException)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe SomeException
    forall a. Maybe a
    Nothing

    proverError :: String -> M.ModuleCmd (Maybe String, ProverResult)
    proverError :: String -> ModuleCmd (Maybe String, ProverResult)
    proverError String
    msg ModuleInput IO
    minp =
      ModuleRes (Maybe String, ProverResult)
    -> IO (ModuleRes (Maybe String, ProverResult))
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (((Maybe String, ProverResult), ModuleEnv)
    -> Either ModuleError ((Maybe String, ProverResult), ModuleEnv)
    forall a b. b -> Either a b
    Right ((Maybe String
    forall a. Maybe a
    Nothing, String -> ProverResult
    ProverError String
    msg), ModuleInput IO -> ModuleEnv
    forall (m :: * -> *). ModuleInput m -> ModuleEnv
    M.minpModuleEnv ModuleInput IO
    minp), [])

    data CryptolState t = CryptolState

    setupAdapterOptions :: W4ProverConfig -> W4.ExprBuilder t CryptolState fs -> IO ()
    setupAdapterOptions :: forall t fs.
    W4ProverConfig -> ExprBuilder t CryptolState fs -> IO ()
    setupAdapterOptions W4ProverConfig
    cfg ExprBuilder t CryptolState fs
    sym =
       case W4ProverConfig
    cfg of
         W4ProverConfig AnAdapter
    p -> AnAdapter -> IO ()
    setupAnAdapter AnAdapter
    p
         W4Portfolio NonEmpty AnAdapter
    ps -> (AnAdapter -> IO ()) -> NonEmpty AnAdapter -> IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ AnAdapter -> IO ()
    setupAnAdapter NonEmpty AnAdapter
    ps
         W4ProverConfig
    W4OfflineConfig -> () -> IO ()
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

      where
      setupAnAdapter :: AnAdapter -> IO ()
    setupAnAdapter (AnAdapter forall (st :: * -> *). SolverAdapter st
    adpt) =
        [ConfigDesc] -> Config -> IO ()
    W4.extendConfig (SolverAdapter Any -> [ConfigDesc]
    forall (st :: * -> *). SolverAdapter st -> [ConfigDesc]
    W4.solver_adapter_config_options SolverAdapter Any
    forall (st :: * -> *). SolverAdapter st
    adpt) (ExprBuilder t CryptolState fs -> Config
    forall sym. IsExprBuilder sym => sym -> Config
    W4.getConfiguration ExprBuilder t CryptolState fs
    sym)
      setupAnAdapter (AnOnlineAdapter String
    _n ProblemFeatures
    _fs [ConfigDesc]
    opts Proxy s
    _p) =
        [ConfigDesc] -> Config -> IO ()
    W4.extendConfig [ConfigDesc]
    opts (ExprBuilder t CryptolState fs -> Config
    forall sym. IsExprBuilder sym => sym -> Config
    W4.getConfiguration ExprBuilder t CryptolState fs
    sym)

    what4FreshFns :: W4.IsSymExprBuilder sym => sym -> FreshVarFns (What4 sym)
    what4FreshFns :: forall sym. IsSymExprBuilder sym => sym -> FreshVarFns (What4 sym)
    what4FreshFns sym
    sym =
      FreshVarFns
      { freshBitVar :: IO (SBit (What4 sym))
    freshBitVar     = sym
    -> SolverSymbol
    -> BaseTypeRepr 'BaseBoolType
    -> IO (SymExpr sym 'BaseBoolType)
    forall sym (tp :: BaseType).
    IsSymExprBuilder sym =>
    sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
    forall (tp :: BaseType).
    sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
    W4.freshConstant sym
    sym SolverSymbol
    W4.emptySymbol BaseTypeRepr 'BaseBoolType
    W4.BaseBoolRepr
      , freshWordVar :: Integer -> IO (SWord (What4 sym))
    freshWordVar    = sym -> SolverSymbol -> Integer -> IO (SWord sym)
    forall sym.
    IsSymExprBuilder sym =>
    sym -> SolverSymbol -> Integer -> IO (SWord sym)
    SW.freshBV sym
    sym SolverSymbol
    W4.emptySymbol
      , freshIntegerVar :: Maybe Integer -> Maybe Integer -> IO (SInteger (What4 sym))
    freshIntegerVar = sym
    -> SolverSymbol
    -> Maybe Integer
    -> Maybe Integer
    -> IO (SymInteger sym)
    forall sym.
    IsSymExprBuilder sym =>
    sym
    -> SolverSymbol
    -> Maybe Integer
    -> Maybe Integer
    -> IO (SymInteger sym)
    W4.freshBoundedInt sym
    sym SolverSymbol
    W4.emptySymbol
      , freshFloatVar :: Integer -> Integer -> IO (SFloat (What4 sym))
    freshFloatVar   = sym -> Integer -> Integer -> IO (SFloat sym)
    forall sym.
    IsSymExprBuilder sym =>
    sym -> Integer -> Integer -> IO (SFloat sym)
    W4.fpFresh sym
    sym
      }

    -- | Simulate and manipulate query into a form suitable to be sent
    -- to a solver.
    prepareQuery ::
      W4.IsSymExprBuilder sym =>
      What4 sym ->
      ProverCommand ->
      M.ModuleT IO (Either String
                           ([FinType],[VarShape (What4 sym)],W4.Pred sym, W4.Pred sym)
                   )
    prepareQuery :: forall sym.
    IsSymExprBuilder sym =>
    What4 sym
    -> ProverCommand
    -> ModuleT
         IO
         (Either
            String ([FinType], [VarShape (What4 sym)], Pred sym, Pred sym))
    prepareQuery What4 sym
    sym ProverCommand { Bool
    String
    [DeclGroup]
    Maybe String
    IORef ProverStats
    Schema
    Expr
    QueryType
    pcQueryType :: QueryType
    pcProverName :: String
    pcVerbose :: Bool
    pcValidate :: Bool
    pcProverStats :: IORef ProverStats
    pcExtraDecls :: [DeclGroup]
    pcSmtFile :: Maybe String
    pcExpr :: Expr
    pcSchema :: Schema
    pcIgnoreSafety :: Bool
    pcQueryType :: ProverCommand -> QueryType
    pcProverName :: ProverCommand -> String
    pcVerbose :: ProverCommand -> Bool
    pcValidate :: ProverCommand -> Bool
    pcProverStats :: ProverCommand -> IORef ProverStats
    pcExtraDecls :: ProverCommand -> [DeclGroup]
    pcSmtFile :: ProverCommand -> Maybe String
    pcExpr :: ProverCommand -> Expr
    pcSchema :: ProverCommand -> Schema
    pcIgnoreSafety :: ProverCommand -> Bool
    .. } = do
      Map Name Newtype
    ntEnv <- ModuleM (Map Name Newtype)
    M.getNewtypes
      case QueryType -> Schema -> Either String [FinType]
    predArgTypes QueryType
    pcQueryType Schema
    pcSchema of
        Left String
    msg -> Either
      String ([FinType], [VarShape (What4 sym)], Pred sym, Pred sym)
    -> ModuleT
         IO
         (Either
            String ([FinType], [VarShape (What4 sym)], Pred sym, Pred sym))
    forall a. a -> ModuleT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (String
    -> Either
         String ([FinType], [VarShape (What4 sym)], Pred sym, Pred sym)
    forall a b. a -> Either a b
    Left String
    msg)
        Right [FinType]
    ts ->
          do [VarShape (What4 sym)]
    args <- IO [VarShape (What4 sym)] -> ModuleT IO [VarShape (What4 sym)]
    forall a. IO a -> ModuleT IO a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO ((FinType -> IO (VarShape (What4 sym)))
    -> [FinType] -> IO [VarShape (What4 sym)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (FreshVarFns (What4 sym) -> FinType -> IO (VarShape (What4 sym))
    forall sym.
    Backend sym =>
    FreshVarFns sym -> FinType -> IO (VarShape sym)
    freshVar (sym -> FreshVarFns (What4 sym)
    forall sym. IsSymExprBuilder sym => sym -> FreshVarFns (What4 sym)
    what4FreshFns (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym))) [FinType]
    ts)
             (Pred sym
    safety,Pred sym
    b) <- Map Name Newtype
    -> [VarShape (What4 sym)] -> ModuleT IO (Pred sym, Pred sym)
    simulate Map Name Newtype
    ntEnv [VarShape (What4 sym)]
    args
             IO
      (Either
         String ([FinType], [VarShape (What4 sym)], Pred sym, Pred sym))
    -> ModuleT
         IO
         (Either
            String ([FinType], [VarShape (What4 sym)], Pred sym, Pred sym))
    forall a. IO a -> ModuleT IO a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO
               do -- Ignore the safety condition if the flag is set
                  let safety' :: Pred sym
    safety' = if Bool
    pcIgnoreSafety then sym -> Pred sym
    forall sym. IsExprBuilder sym => sym -> Pred sym
    W4.truePred (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) else Pred sym
    safety

                  Pred sym
    defs <- MVar (Pred sym) -> IO (Pred sym)
    forall a. MVar a -> IO a
    readMVar (What4 sym -> MVar (Pred sym)
    forall sym. What4 sym -> MVar (Pred sym)
    w4defs What4 sym
    sym)

                  ([FinType], [VarShape (What4 sym)], Pred sym, Pred sym)
    -> Either
         String ([FinType], [VarShape (What4 sym)], Pred sym, Pred sym)
    forall a b. b -> Either a b
    Right (([FinType], [VarShape (What4 sym)], Pred sym, Pred sym)
     -> Either
          String ([FinType], [VarShape (What4 sym)], Pred sym, Pred sym))
    -> IO ([FinType], [VarShape (What4 sym)], Pred sym, Pred sym)
    -> IO
         (Either
            String ([FinType], [VarShape (What4 sym)], Pred sym, Pred sym))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
                    case QueryType
    pcQueryType of
                      QueryType
    ProveQuery ->
                        do Pred sym
    q <- sym -> Pred sym -> IO (Pred sym)
    forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
    W4.notPred (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) (Pred sym -> IO (Pred sym)) -> IO (Pred sym) -> IO (Pred sym)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> Pred sym -> Pred sym -> IO (Pred sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Pred sym -> Pred sym -> IO (Pred sym)
    W4.andPred (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) Pred sym
    safety' Pred sym
    b
                           Pred sym
    q' <- sym -> Pred sym -> Pred sym -> IO (Pred sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Pred sym -> Pred sym -> IO (Pred sym)
    W4.andPred (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) Pred sym
    defs Pred sym
    q
                           ([FinType], [VarShape (What4 sym)], Pred sym, Pred sym)
    -> IO ([FinType], [VarShape (What4 sym)], Pred sym, Pred sym)
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ([FinType]
    ts,[VarShape (What4 sym)]
    args,Pred sym
    safety',Pred sym
    q')

                      QueryType
    SafetyQuery ->
                        do Pred sym
    q <- sym -> Pred sym -> IO (Pred sym)
    forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
    W4.notPred (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) Pred sym
    safety
                           Pred sym
    q' <- sym -> Pred sym -> Pred sym -> IO (Pred sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Pred sym -> Pred sym -> IO (Pred sym)
    W4.andPred (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) Pred sym
    defs Pred sym
    q
                           ([FinType], [VarShape (What4 sym)], Pred sym, Pred sym)
    -> IO ([FinType], [VarShape (What4 sym)], Pred sym, Pred sym)
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ([FinType]
    ts,[VarShape (What4 sym)]
    args,Pred sym
    safety,Pred sym
    q')

                      SatQuery SatNum
    _ ->
                        do Pred sym
    q <- sym -> Pred sym -> Pred sym -> IO (Pred sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Pred sym -> Pred sym -> IO (Pred sym)
    W4.andPred (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) Pred sym
    safety' Pred sym
    b
                           Pred sym
    q' <- sym -> Pred sym -> Pred sym -> IO (Pred sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Pred sym -> Pred sym -> IO (Pred sym)
    W4.andPred (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) Pred sym
    defs Pred sym
    q
                           ([FinType], [VarShape (What4 sym)], Pred sym, Pred sym)
    -> IO ([FinType], [VarShape (What4 sym)], Pred sym, Pred sym)
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ([FinType]
    ts,[VarShape (What4 sym)]
    args,Pred sym
    safety',Pred sym
    q')
      where
      simulate :: Map Name Newtype
    -> [VarShape (What4 sym)] -> ModuleT IO (Pred sym, Pred sym)
    simulate Map Name Newtype
    ntEnv [VarShape (What4 sym)]
    args =
        do let lPutStrLn :: String -> ModuleM ()
    lPutStrLn = (Logger -> String -> IO ()) -> String -> ModuleM ()
    forall a b. (Logger -> a -> IO b) -> a -> ModuleM b
    M.withLogger Logger -> String -> IO ()
    logPutStrLn
           Bool -> ModuleM () -> ModuleM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when Bool
    pcVerbose (String -> ModuleM ()
    lPutStrLn String
    "Simulating...")

           Map PrimIdent Expr
    ds <- do (ModulePath
    _mp, TCTopEntity
    ent) <- Bool -> ImportSource -> ModuleM (ModulePath, TCTopEntity)
    M.loadModuleFrom Bool
    True (ModName -> ImportSource
    M.FromModule ModName
    preludeReferenceName)
                    let m :: Module
    m = TCTopEntity -> Module
    tcTopEntityToModule TCTopEntity
    ent
                    let decls :: [DeclGroup]
    decls = Module -> [DeclGroup]
    forall mname. ModuleG mname -> [DeclGroup]
    mDecls Module
    m
                    let nms :: [Name]
    nms = (Name, IfaceDecl) -> Name
    forall a b. (a, b) -> a
    fst ((Name, IfaceDecl) -> Name) -> [(Name, IfaceDecl)] -> [Name]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Map Name IfaceDecl -> [(Name, IfaceDecl)]
    forall k a. Map k a -> [(k, a)]
    Map.toList (IfaceDecls -> Map Name IfaceDecl
    M.ifDecls (IfaceG ModName -> IfaceDecls
    forall name. IfaceG name -> IfaceDecls
    M.ifDefines (Module -> IfaceG ModName
    forall name. ModuleG name -> IfaceG name
    M.genIface Module
    m)))
                    let ds :: Map PrimIdent Expr
    ds = [(PrimIdent, Expr)] -> Map PrimIdent Expr
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList [ (Text -> PrimIdent
    prelPrim (Ident -> Text
    identText (Name -> Ident
    M.nameIdent Name
    nm)), Expr -> [DeclGroup] -> Expr
    EWhere (Name -> Expr
    EVar Name
    nm) [DeclGroup]
    decls) | Name
    nm <- [Name]
    nms ]
                    Map PrimIdent Expr -> ModuleT IO (Map PrimIdent Expr)
    forall a. a -> ModuleT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Map PrimIdent Expr
    ds

           IO EvalOpts
    getEOpts <- ModuleM (IO EvalOpts)
    M.getEvalOptsAction
           let tbl :: Map PrimIdent (Prim (What4 sym))
    tbl = What4 sym -> IO EvalOpts -> Map PrimIdent (Prim (What4 sym))
    forall sym.
    IsSymExprBuilder sym =>
    What4 sym -> IO EvalOpts -> Map PrimIdent (Prim (What4 sym))
    primTable What4 sym
    sym IO EvalOpts
    getEOpts
           let ?evalPrim = \PrimIdent
    i -> (Prim (What4 sym) -> Either Expr (Prim (What4 sym))
    forall a b. b -> Either a b
    Right (Prim (What4 sym) -> Either Expr (Prim (What4 sym)))
    -> Maybe (Prim (What4 sym))
    -> Maybe (Either Expr (Prim (What4 sym)))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> PrimIdent
    -> Map PrimIdent (Prim (What4 sym)) -> Maybe (Prim (What4 sym))
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup PrimIdent
    i Map PrimIdent (Prim (What4 sym))
    tbl) Maybe (Either Expr (Prim (What4 sym)))
    -> Maybe (Either Expr (Prim (What4 sym)))
    -> Maybe (Either Expr (Prim (What4 sym)))
    forall a. Maybe a -> Maybe a -> Maybe a
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|>
                                 (Expr -> Either Expr (Prim (What4 sym))
    forall a b. a -> Either a b
    Left (Expr -> Either Expr (Prim (What4 sym)))
    -> Maybe Expr -> Maybe (Either Expr (Prim (What4 sym)))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> PrimIdent -> Map PrimIdent Expr -> Maybe Expr
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup PrimIdent
    i Map PrimIdent Expr
    ds)
           let ?range = ?range::Range
    Range
    emptyRange
           Bool
    callStacks <- ModuleT IO Bool
    forall (m :: * -> *). Monad m => ModuleT m Bool
    M.getCallStacks
           let ?callStacks = ?callStacks::Bool
    Bool
    callStacks

           ModuleEnv
    modEnv <- ModuleT IO ModuleEnv
    forall (m :: * -> *). Monad m => ModuleT m ModuleEnv
    M.getModuleEnv
           let extDgs :: [DeclGroup]
    extDgs = ModuleEnv -> [DeclGroup]
    M.allDeclGroups ModuleEnv
    modEnv [DeclGroup] -> [DeclGroup] -> [DeclGroup]
    forall a. [a] -> [a] -> [a]
    ++ [DeclGroup]
    pcExtraDecls

           sym -> W4Eval sym (Pred sym) -> ModuleT IO (Pred sym, Pred sym)
    forall sym (m :: * -> *) a.
    (IsExprBuilder sym, MonadIO m) =>
    sym -> W4Eval sym a -> m (Pred sym, a)
    doW4Eval (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym)
             do GenEvalEnv (What4 sym)
    env <- What4 sym
    -> [DeclGroup]
    -> GenEvalEnv (What4 sym)
    -> SEval (What4 sym) (GenEvalEnv (What4 sym))
    forall sym.
    EvalPrims sym =>
    sym -> [DeclGroup] -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
    Eval.evalDecls What4 sym
    sym [DeclGroup]
    extDgs (GenEvalEnv (What4 sym) -> W4Eval sym (GenEvalEnv (What4 sym)))
    -> W4Eval sym (GenEvalEnv (What4 sym))
    -> W4Eval sym (GenEvalEnv (What4 sym))
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<<
                         What4 sym
    -> Map Name Newtype
    -> GenEvalEnv (What4 sym)
    -> SEval (What4 sym) (GenEvalEnv (What4 sym))
    forall sym.
    EvalPrims sym =>
    sym
    -> Map Name Newtype -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
    Eval.evalNewtypeDecls What4 sym
    sym Map Name Newtype
    ntEnv GenEvalEnv (What4 sym)
    forall a. Monoid a => a
    mempty

                GenValue (What4 sym)
    v   <- What4 sym
    -> GenEvalEnv (What4 sym)
    -> Expr
    -> SEval (What4 sym) (GenValue (What4 sym))
    forall sym.
    (?range::Range, EvalPrims sym) =>
    sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
    Eval.evalExpr  What4 sym
    sym GenEvalEnv (What4 sym)
    env    Expr
    pcExpr
                GenValue (What4 sym)
    appliedVal <-
                  (GenValue (What4 sym)
     -> W4Eval sym (GenValue (What4 sym))
     -> W4Eval sym (GenValue (What4 sym)))
    -> GenValue (What4 sym)
    -> [W4Eval sym (GenValue (What4 sym))]
    -> W4Eval sym (GenValue (What4 sym))
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Monad m) =>
    (b -> a -> m b) -> b -> t a -> m b
    foldM (What4 sym
    -> GenValue (What4 sym)
    -> SEval (What4 sym) (GenValue (What4 sym))
    -> SEval (What4 sym) (GenValue (What4 sym))
    forall sym.
    Backend sym =>
    sym
    -> GenValue sym
    -> SEval sym (GenValue sym)
    -> SEval sym (GenValue sym)
    Eval.fromVFun What4 sym
    sym) GenValue (What4 sym)
    v ((VarShape (What4 sym) -> W4Eval sym (GenValue (What4 sym)))
    -> [VarShape (What4 sym)] -> [W4Eval sym (GenValue (What4 sym))]
    forall a b. (a -> b) -> [a] -> [b]
    map (GenValue (What4 sym) -> W4Eval sym (GenValue (What4 sym))
    forall a. a -> W4Eval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (GenValue (What4 sym) -> W4Eval sym (GenValue (What4 sym)))
    -> (VarShape (What4 sym) -> GenValue (What4 sym))
    -> VarShape (What4 sym)
    -> W4Eval sym (GenValue (What4 sym))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . What4 sym -> VarShape (What4 sym) -> GenValue (What4 sym)
    forall sym. Backend sym => sym -> VarShape sym -> GenValue sym
    varShapeToValue What4 sym
    sym) [VarShape (What4 sym)]
    args)

                case QueryType
    pcQueryType of
                  QueryType
    SafetyQuery ->
                    do GenValue (What4 sym) -> SEval (What4 sym) ()
    forall sym. Backend sym => GenValue sym -> SEval sym ()
    Eval.forceValue GenValue (What4 sym)
    appliedVal
                       Pred sym -> W4Eval sym (Pred sym)
    forall a. a -> W4Eval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (sym -> Pred sym
    forall sym. IsExprBuilder sym => sym -> Pred sym
    W4.truePred (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym))

                  QueryType
    _ -> Pred sym -> W4Eval sym (Pred sym)
    forall a. a -> W4Eval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (GenValue (What4 sym) -> SBit (What4 sym)
    forall sym. GenValue sym -> SBit sym
    Eval.fromVBit GenValue (What4 sym)
    appliedVal)

    satProve ::
      W4ProverConfig ->
      Bool {- ^ hash consing -} ->
      Bool {- ^ warn on uninterpreted functions -} ->
      ProverCommand ->
      M.ModuleCmd (Maybe String, ProverResult)

    satProve :: W4ProverConfig
    -> Bool
    -> Bool
    -> ProverCommand
    -> ModuleCmd (Maybe String, ProverResult)
    satProve W4ProverConfig
    solverCfg Bool
    hashConsing Bool
    warnUninterp pc :: ProverCommand
    pc@ProverCommand {Bool
    String
    [DeclGroup]
    Maybe String
    IORef ProverStats
    Schema
    Expr
    QueryType
    pcQueryType :: ProverCommand -> QueryType
    pcProverName :: ProverCommand -> String
    pcVerbose :: ProverCommand -> Bool
    pcValidate :: ProverCommand -> Bool
    pcProverStats :: ProverCommand -> IORef ProverStats
    pcExtraDecls :: ProverCommand -> [DeclGroup]
    pcSmtFile :: ProverCommand -> Maybe String
    pcExpr :: ProverCommand -> Expr
    pcSchema :: ProverCommand -> Schema
    pcIgnoreSafety :: ProverCommand -> Bool
    pcQueryType :: QueryType
    pcProverName :: String
    pcVerbose :: Bool
    pcValidate :: Bool
    pcProverStats :: IORef ProverStats
    pcExtraDecls :: [DeclGroup]
    pcSmtFile :: Maybe String
    pcExpr :: Expr
    pcSchema :: Schema
    pcIgnoreSafety :: Bool
    ..} =
      (String -> ModuleCmd (Maybe String, ProverResult))
    -> ModuleCmd (Maybe String, ProverResult)
    -> ModuleCmd (Maybe String, ProverResult)
    forall a. (String -> ModuleCmd a) -> ModuleCmd a -> ModuleCmd a
    protectStack String -> ModuleCmd (Maybe String, ProverResult)
    proverError \ModuleInput IO
    modIn ->
      ModuleInput IO
    -> ModuleM (Maybe String, ProverResult)
    -> IO (ModuleRes (Maybe String, ProverResult))
    forall a.
    ModuleInput IO
    -> ModuleM a
    -> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
    M.runModuleM ModuleInput IO
    modIn
      do ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
    w4sym   <- IO
      (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
    -> ModuleT
         IO
         (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
    forall a. IO a -> ModuleT IO a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO IO
      (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
    makeSym
         MVar (BoolExpr GlobalNonceGenerator)
    defVar  <- IO (MVar (BoolExpr GlobalNonceGenerator))
    -> ModuleT IO (MVar (BoolExpr GlobalNonceGenerator))
    forall a. IO a -> ModuleT IO a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (BoolExpr GlobalNonceGenerator
    -> IO (MVar (BoolExpr GlobalNonceGenerator))
    forall a. a -> IO (MVar a)
    newMVar (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
    -> Pred
         (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
    forall sym. IsExprBuilder sym => sym -> Pred sym
    W4.truePred ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
    w4sym))
         MVar
      (What4FunCache
         (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))
    funVar  <- IO
      (MVar
         (What4FunCache
            (ExprBuilder
               GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))))
    -> ModuleT
         IO
         (MVar
            (What4FunCache
               (ExprBuilder
                  GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))))
    forall a. IO a -> ModuleT IO a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (What4FunCache
      (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
    -> IO
         (MVar
            (What4FunCache
               (ExprBuilder
                  GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))))
    forall a. a -> IO (MVar a)
    newMVar What4FunCache
      (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
    forall a. Monoid a => a
    mempty)
         MVar (Set Text)
    uninterpWarnVar <- IO (MVar (Set Text)) -> ModuleT IO (MVar (Set Text))
    forall a. IO a -> ModuleT IO a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (Set Text -> IO (MVar (Set Text))
    forall a. a -> IO (MVar a)
    newMVar Set Text
    forall a. Monoid a => a
    mempty)
         let sym :: What4
      (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
    sym = ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
    -> MVar
         (Pred
            (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))
    -> MVar
         (What4FunCache
            (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))
    -> MVar (Set Text)
    -> What4
         (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
    forall sym.
    sym
    -> MVar (Pred sym)
    -> MVar (What4FunCache sym)
    -> MVar (Set Text)
    -> What4 sym
    What4 ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
    w4sym MVar
      (Pred
         (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))
    MVar (BoolExpr GlobalNonceGenerator)
    defVar MVar
      (What4FunCache
         (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))
    funVar MVar (Set Text)
    uninterpWarnVar
         LogData
    logData <- (Logger -> () -> IO LogData) -> () -> ModuleM LogData
    forall a b. (Logger -> a -> IO b) -> a -> ModuleM b
    M.withLogger Logger -> () -> IO LogData
    forall {f :: * -> *}. Applicative f => Logger -> () -> f LogData
    doLog ()
         UTCTime
    start   <- IO UTCTime -> ModuleT IO UTCTime
    forall a. IO a -> ModuleT IO a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO IO UTCTime
    getCurrentTime
         Either
      String
      ([FinType],
       [VarShape
          (What4
             (ExprBuilder
                GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))],
       BoolExpr GlobalNonceGenerator, BoolExpr GlobalNonceGenerator)
    query   <- What4
      (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
    -> ProverCommand
    -> ModuleT
         IO
         (Either
            String
            ([FinType],
             [VarShape
                (What4
                   (ExprBuilder
                      GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))],
             Pred
               (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)),
             Pred
               (ExprBuilder
                  GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))))
    forall sym.
    IsSymExprBuilder sym =>
    What4 sym
    -> ProverCommand
    -> ModuleT
         IO
         (Either
            String ([FinType], [VarShape (What4 sym)], Pred sym, Pred sym))
    prepareQuery What4
      (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
    sym ProverCommand { Bool
    String
    [DeclGroup]
    Maybe String
    IORef ProverStats
    Schema
    Expr
    QueryType
    pcQueryType :: QueryType
    pcProverName :: String
    pcVerbose :: Bool
    pcValidate :: Bool
    pcProverStats :: IORef ProverStats
    pcExtraDecls :: [DeclGroup]
    pcSmtFile :: Maybe String
    pcExpr :: Expr
    pcSchema :: Schema
    pcIgnoreSafety :: Bool
    pcQueryType :: QueryType
    pcProverName :: String
    pcVerbose :: Bool
    pcValidate :: Bool
    pcProverStats :: IORef ProverStats
    pcExtraDecls :: [DeclGroup]
    pcSmtFile :: Maybe String
    pcExpr :: Expr
    pcSchema :: Schema
    pcIgnoreSafety :: Bool
    .. }
         PrimMap
    primMap <- ModuleM PrimMap
    M.getPrimMap
         Bool -> ModuleM () -> ModuleM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when Bool
    warnUninterp
           ((Logger -> Set Text -> IO ()) -> Set Text -> ModuleM ()
    forall a b. (Logger -> a -> IO b) -> a -> ModuleM b
    M.withLogger Logger -> Set Text -> IO ()
    printUninterpWarn (Set Text -> ModuleM ()) -> ModuleT IO (Set Text) -> ModuleM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< IO (Set Text) -> ModuleT IO (Set Text)
    forall a. IO a -> ModuleT IO a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (MVar (Set Text) -> IO (Set Text)
    forall a. MVar a -> IO a
    readMVar MVar (Set Text)
    uninterpWarnVar))
         IO (Maybe String, ProverResult)
    -> ModuleM (Maybe String, ProverResult)
    forall a. IO a -> ModuleT IO a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO
           do (Maybe String, ProverResult)
    result <- What4
      (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
    -> LogData
    -> PrimMap
    -> Either
         String
         ([FinType],
          [VarShape
             (What4
                (ExprBuilder
                   GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))],
          BoolExpr GlobalNonceGenerator, BoolExpr GlobalNonceGenerator)
    -> IO (Maybe String, ProverResult)
    runProver What4
      (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
    sym LogData
    logData PrimMap
    primMap Either
      String
      ([FinType],
       [VarShape
          (What4
             (ExprBuilder
                GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))],
       BoolExpr GlobalNonceGenerator, BoolExpr GlobalNonceGenerator)
    query
              UTCTime
    end <- IO UTCTime
    getCurrentTime
              IORef ProverStats -> ProverStats -> IO ()
    forall a. IORef a -> a -> IO ()
    writeIORef IORef ProverStats
    pcProverStats (UTCTime -> UTCTime -> ProverStats
    diffUTCTime UTCTime
    end UTCTime
    start)
              (Maybe String, ProverResult) -> IO (Maybe String, ProverResult)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe String, ProverResult)
    result
      where
      makeSym :: IO
      (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
    makeSym =
        do ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
    w4sym <- FloatModeRepr 'FloatIEEE
    -> CryptolState GlobalNonceGenerator
    -> NonceGenerator IO GlobalNonceGenerator
    -> IO
         (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
    forall (fm :: FloatMode) (st :: * -> *) t.
    FloatModeRepr fm
    -> st t -> NonceGenerator IO t -> IO (ExprBuilder t st (Flags fm))
    W4.newExprBuilder FloatModeRepr 'FloatIEEE
    W4.FloatIEEERepr
                                      CryptolState GlobalNonceGenerator
    forall t. CryptolState t
    CryptolState
                                      NonceGenerator IO GlobalNonceGenerator
    globalNonceGenerator
           W4ProverConfig
    -> ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
    -> IO ()
    forall t fs.
    W4ProverConfig -> ExprBuilder t CryptolState fs -> IO ()
    setupAdapterOptions W4ProverConfig
    solverCfg ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
    w4sym
           Bool -> IO () -> IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when Bool
    hashConsing (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
    -> IO ()
    forall t (st :: * -> *) fs. ExprBuilder t st fs -> IO ()
    W4.startCaching ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
    w4sym)
           ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
    -> IO
         (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
    w4sym

      doLog :: Logger -> () -> f LogData
    doLog Logger
    lg () =
        LogData -> f LogData
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure
        LogData
    defaultLogData
          { logCallbackVerbose :: Int -> String -> IO ()
    logCallbackVerbose = \Int
    i String
    msg -> Bool -> IO () -> IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    2) (Logger -> String -> IO ()
    logPutStrLn Logger
    lg String
    msg)
          , logReason :: String
    logReason = String
    "solver query"
          }

      runProver :: What4
      (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
    -> LogData
    -> PrimMap
    -> Either
         String
         ([FinType],
          [VarShape
             (What4
                (ExprBuilder
                   GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))],
          BoolExpr GlobalNonceGenerator, BoolExpr GlobalNonceGenerator)
    -> IO (Maybe String, ProverResult)
    runProver What4
      (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
    sym LogData
    logData PrimMap
    primMap Either
      String
      ([FinType],
       [VarShape
          (What4
             (ExprBuilder
                GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))],
       BoolExpr GlobalNonceGenerator, BoolExpr GlobalNonceGenerator)
    q =
        case Either
      String
      ([FinType],
       [VarShape
          (What4
             (ExprBuilder
                GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))],
       BoolExpr GlobalNonceGenerator, BoolExpr GlobalNonceGenerator)
    q of
          Left String
    msg -> (Maybe String, ProverResult) -> IO (Maybe String, ProverResult)
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Maybe String
    forall a. Maybe a
    Nothing, String -> ProverResult
    ProverError String
    msg)
          Right ([FinType]
    ts,[VarShape
       (What4
          (ExprBuilder
             GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))]
    args,BoolExpr GlobalNonceGenerator
    safety,BoolExpr GlobalNonceGenerator
    query) ->
            case QueryType
    pcQueryType of
              QueryType
    ProveQuery ->
                What4
      (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
    -> W4ProverConfig
    -> ProverCommand
    -> PrimMap
    -> LogData
    -> [FinType]
    -> [VarShape
          (What4
             (ExprBuilder
                GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))]
    -> Maybe
         (Pred
            (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))
    -> Pred
         (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
    -> IO (Maybe String, ProverResult)
    forall sym t fm.
    (sym ~ ExprBuilder t CryptolState fm) =>
    What4 sym
    -> W4ProverConfig
    -> ProverCommand
    -> PrimMap
    -> LogData
    -> [FinType]
    -> [VarShape (What4 sym)]
    -> Maybe (Pred sym)
    -> Pred sym
    -> IO (Maybe String, ProverResult)
    singleQuery What4
      (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
    sym W4ProverConfig
    solverCfg ProverCommand
    pc PrimMap
    primMap LogData
    logData [FinType]
    ts [VarShape
       (What4
          (ExprBuilder
             GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))]
    args (BoolExpr GlobalNonceGenerator
    -> Maybe (BoolExpr GlobalNonceGenerator)
    forall a. a -> Maybe a
    Just BoolExpr GlobalNonceGenerator
    safety) Pred
      (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
    BoolExpr GlobalNonceGenerator
    query

              QueryType
    SafetyQuery ->
                What4
      (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
    -> W4ProverConfig
    -> ProverCommand
    -> PrimMap
    -> LogData
    -> [FinType]
    -> [VarShape
          (What4
             (ExprBuilder
                GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))]
    -> Maybe
         (Pred
            (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))
    -> Pred
         (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
    -> IO (Maybe String, ProverResult)
    forall sym t fm.
    (sym ~ ExprBuilder t CryptolState fm) =>
    What4 sym
    -> W4ProverConfig
    -> ProverCommand
    -> PrimMap
    -> LogData
    -> [FinType]
    -> [VarShape (What4 sym)]
    -> Maybe (Pred sym)
    -> Pred sym
    -> IO (Maybe String, ProverResult)
    singleQuery What4
      (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
    sym W4ProverConfig
    solverCfg ProverCommand
    pc PrimMap
    primMap LogData
    logData [FinType]
    ts [VarShape
       (What4
          (ExprBuilder
             GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))]
    args (BoolExpr GlobalNonceGenerator
    -> Maybe (BoolExpr GlobalNonceGenerator)
    forall a. a -> Maybe a
    Just BoolExpr GlobalNonceGenerator
    safety) Pred
      (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
    BoolExpr GlobalNonceGenerator
    query

              SatQuery SatNum
    num ->
                What4
      (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
    -> W4ProverConfig
    -> ProverCommand
    -> PrimMap
    -> LogData
    -> [FinType]
    -> [VarShape
          (What4
             (ExprBuilder
                GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))]
    -> Pred
         (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
    -> SatNum
    -> IO (Maybe String, ProverResult)
    forall sym t fm.
    (sym ~ ExprBuilder t CryptolState fm) =>
    What4 sym
    -> W4ProverConfig
    -> ProverCommand
    -> PrimMap
    -> LogData
    -> [FinType]
    -> [VarShape (What4 sym)]
    -> Pred sym
    -> SatNum
    -> IO (Maybe String, ProverResult)
    multiSATQuery What4
      (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
    sym W4ProverConfig
    solverCfg ProverCommand
    pc PrimMap
    primMap LogData
    logData [FinType]
    ts [VarShape
       (What4
          (ExprBuilder
             GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))]
    args Pred
      (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
    BoolExpr GlobalNonceGenerator
    query SatNum
    num

    printUninterpWarn :: Logger -> Set Text -> IO ()
    printUninterpWarn :: Logger -> Set Text -> IO ()
    printUninterpWarn Logger
    lg Set Text
    uninterpWarns =
      case Set Text -> [Text]
    forall a. Set a -> [a]
    Set.toList Set Text
    uninterpWarns of
        []  -> () -> IO ()
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()
        [Text
    x] -> Logger -> String -> IO ()
    logPutStrLn Logger
    lg (String
    "[Warning] Uninterpreted functions used to represent " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Text -> String
    Text.unpack Text
    x String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " operations.")
        [Text]
    xs  -> Logger -> String -> IO ()
    logPutStr Logger
    lg (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines
                 [ String
    "[Warning] Uninterpreted functions used to represent the following operations:"
                 , String
    "  " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    ", " ((Text -> String) -> [Text] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map Text -> String
    Text.unpack [Text]
    xs) ]

    satProveOffline ::
      Bool {- ^ hash consing -} ->
      Bool {- ^ warn on uninterpreted functions -} ->
      ProverCommand ->
      ((Handle -> IO ()) -> IO ()) ->
      M.ModuleCmd (Maybe String)

    satProveOffline :: Bool
    -> Bool
    -> ProverCommand
    -> ((Handle -> IO ()) -> IO ())
    -> ModuleCmd (Maybe String)
    satProveOffline Bool
    hashConsing Bool
    warnUninterp ProverCommand{ Bool
    String
    [DeclGroup]
    Maybe String
    IORef ProverStats
    Schema
    Expr
    QueryType
    pcQueryType :: ProverCommand -> QueryType
    pcProverName :: ProverCommand -> String
    pcVerbose :: ProverCommand -> Bool
    pcValidate :: ProverCommand -> Bool
    pcProverStats :: ProverCommand -> IORef ProverStats
    pcExtraDecls :: ProverCommand -> [DeclGroup]
    pcSmtFile :: ProverCommand -> Maybe String
    pcExpr :: ProverCommand -> Expr
    pcSchema :: ProverCommand -> Schema
    pcIgnoreSafety :: ProverCommand -> Bool
    pcQueryType :: QueryType
    pcProverName :: String
    pcVerbose :: Bool
    pcValidate :: Bool
    pcProverStats :: IORef ProverStats
    pcExtraDecls :: [DeclGroup]
    pcSmtFile :: Maybe String
    pcExpr :: Expr
    pcSchema :: Schema
    pcIgnoreSafety :: Bool
    .. } (Handle -> IO ()) -> IO ()
    outputContinuation =

      (String -> ModuleCmd (Maybe String))
    -> ModuleCmd (Maybe String) -> ModuleCmd (Maybe String)
    forall a. (String -> ModuleCmd a) -> ModuleCmd a -> ModuleCmd a
    protectStack String -> ModuleCmd (Maybe String)
    forall {f :: * -> *} {a} {m :: * -> *} {a} {a}.
    Applicative f =>
    a -> ModuleInput m -> f (Either a (Maybe a, ModuleEnv), [a])
    onError \ModuleInput IO
    modIn ->
      ModuleInput IO
    -> ModuleM (Maybe String)
    -> IO
         (Either ModuleError (Maybe String, ModuleEnv), [ModuleWarning])
    forall a.
    ModuleInput IO
    -> ModuleM a
    -> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
    M.runModuleM ModuleInput IO
    modIn
       do ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
    w4sym <- IO
      (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
    -> ModuleT
         IO
         (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
    forall a. IO a -> ModuleT IO a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO IO
      (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
    makeSym
          MVar (BoolExpr GlobalNonceGenerator)
    defVar  <- IO (MVar (BoolExpr GlobalNonceGenerator))
    -> ModuleT IO (MVar (BoolExpr GlobalNonceGenerator))
    forall a. IO a -> ModuleT IO a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (BoolExpr GlobalNonceGenerator
    -> IO (MVar (BoolExpr GlobalNonceGenerator))
    forall a. a -> IO (MVar a)
    newMVar (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
    -> Pred
         (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
    forall sym. IsExprBuilder sym => sym -> Pred sym
    W4.truePred ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
    w4sym))
          MVar
      (What4FunCache
         (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))
    funVar  <- IO
      (MVar
         (What4FunCache
            (ExprBuilder
               GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))))
    -> ModuleT
         IO
         (MVar
            (What4FunCache
               (ExprBuilder
                  GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))))
    forall a. IO a -> ModuleT IO a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (What4FunCache
      (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
    -> IO
         (MVar
            (What4FunCache
               (ExprBuilder
                  GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))))
    forall a. a -> IO (MVar a)
    newMVar What4FunCache
      (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
    forall a. Monoid a => a
    mempty)
          MVar (Set Text)
    uninterpWarnVar <- IO (MVar (Set Text)) -> ModuleT IO (MVar (Set Text))
    forall a. IO a -> ModuleT IO a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (Set Text -> IO (MVar (Set Text))
    forall a. a -> IO (MVar a)
    newMVar Set Text
    forall a. Monoid a => a
    mempty)
          let sym :: What4
      (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
    sym = ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
    -> MVar
         (Pred
            (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))
    -> MVar
         (What4FunCache
            (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))
    -> MVar (Set Text)
    -> What4
         (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
    forall sym.
    sym
    -> MVar (Pred sym)
    -> MVar (What4FunCache sym)
    -> MVar (Set Text)
    -> What4 sym
    What4 ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
    w4sym MVar
      (Pred
         (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))
    MVar (BoolExpr GlobalNonceGenerator)
    defVar MVar
      (What4FunCache
         (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))
    funVar MVar (Set Text)
    uninterpWarnVar
          Either
      String
      ([FinType],
       [VarShape
          (What4
             (ExprBuilder
                GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))],
       BoolExpr GlobalNonceGenerator, BoolExpr GlobalNonceGenerator)
    ok  <- What4
      (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
    -> ProverCommand
    -> ModuleT
         IO
         (Either
            String
            ([FinType],
             [VarShape
                (What4
                   (ExprBuilder
                      GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))],
             Pred
               (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)),
             Pred
               (ExprBuilder
                  GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))))
    forall sym.
    IsSymExprBuilder sym =>
    What4 sym
    -> ProverCommand
    -> ModuleT
         IO
         (Either
            String ([FinType], [VarShape (What4 sym)], Pred sym, Pred sym))
    prepareQuery What4
      (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
    sym ProverCommand { Bool
    String
    [DeclGroup]
    Maybe String
    IORef ProverStats
    Schema
    Expr
    QueryType
    pcQueryType :: QueryType
    pcProverName :: String
    pcVerbose :: Bool
    pcValidate :: Bool
    pcProverStats :: IORef ProverStats
    pcExtraDecls :: [DeclGroup]
    pcSmtFile :: Maybe String
    pcExpr :: Expr
    pcSchema :: Schema
    pcIgnoreSafety :: Bool
    pcQueryType :: QueryType
    pcProverName :: String
    pcVerbose :: Bool
    pcValidate :: Bool
    pcProverStats :: IORef ProverStats
    pcExtraDecls :: [DeclGroup]
    pcSmtFile :: Maybe String
    pcExpr :: Expr
    pcSchema :: Schema
    pcIgnoreSafety :: Bool
    .. }
          Bool -> ModuleM () -> ModuleM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when Bool
    warnUninterp
            ((Logger -> Set Text -> IO ()) -> Set Text -> ModuleM ()
    forall a b. (Logger -> a -> IO b) -> a -> ModuleM b
    M.withLogger Logger -> Set Text -> IO ()
    printUninterpWarn (Set Text -> ModuleM ()) -> ModuleT IO (Set Text) -> ModuleM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< IO (Set Text) -> ModuleT IO (Set Text)
    forall a. IO a -> ModuleT IO a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (MVar (Set Text) -> IO (Set Text)
    forall a. MVar a -> IO a
    readMVar MVar (Set Text)
    uninterpWarnVar))
          IO (Maybe String) -> ModuleM (Maybe String)
    forall a. IO a -> ModuleT IO a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO
            case Either
      String
      ([FinType],
       [VarShape
          (What4
             (ExprBuilder
                GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))],
       BoolExpr GlobalNonceGenerator, BoolExpr GlobalNonceGenerator)
    ok of
              Left String
    msg -> Maybe String -> IO (Maybe String)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (String -> Maybe String
    forall a. a -> Maybe a
    Just String
    msg)
              Right ([FinType]
    _ts,[VarShape
       (What4
          (ExprBuilder
             GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))]
    _args,BoolExpr GlobalNonceGenerator
    _safety,BoolExpr GlobalNonceGenerator
    query) ->
                do (Handle -> IO ()) -> IO ()
    outputContinuation (\Handle
    hdl -> ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
    -> Handle -> [BoolExpr GlobalNonceGenerator] -> IO ()
    forall t (st :: * -> *) fs.
    ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
    W4.writeZ3SMT2File ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
    w4sym Handle
    hdl [BoolExpr GlobalNonceGenerator
    query])
                   Maybe String -> IO (Maybe String)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe String
    forall a. Maybe a
    Nothing
      where
      makeSym :: IO
      (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
    makeSym =
        do ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
    sym <- FloatModeRepr 'FloatIEEE
    -> CryptolState GlobalNonceGenerator
    -> NonceGenerator IO GlobalNonceGenerator
    -> IO
         (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
    forall (fm :: FloatMode) (st :: * -> *) t.
    FloatModeRepr fm
    -> st t -> NonceGenerator IO t -> IO (ExprBuilder t st (Flags fm))
    W4.newExprBuilder FloatModeRepr 'FloatIEEE
    W4.FloatIEEERepr CryptolState GlobalNonceGenerator
    forall t. CryptolState t
    CryptolState NonceGenerator IO GlobalNonceGenerator
    globalNonceGenerator
           [ConfigDesc] -> Config -> IO ()
    W4.extendConfig [ConfigDesc]
    W4.z3Options (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
    -> Config
    forall sym. IsExprBuilder sym => sym -> Config
    W4.getConfiguration ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
    sym)
           Bool -> IO () -> IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when Bool
    hashConsing  (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
    -> IO ()
    forall t (st :: * -> *) fs. ExprBuilder t st fs -> IO ()
    W4.startCaching ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
    sym)
           ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
    -> IO
         (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
    sym

      onError :: a -> ModuleInput m -> f (Either a (Maybe a, ModuleEnv), [a])
    onError a
    msg ModuleInput m
    minp = (Either a (Maybe a, ModuleEnv), [a])
    -> f (Either a (Maybe a, ModuleEnv), [a])
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ((Maybe a, ModuleEnv) -> Either a (Maybe a, ModuleEnv)
    forall a b. b -> Either a b
    Right (a -> Maybe a
    forall a. a -> Maybe a
    Just a
    msg, ModuleInput m -> ModuleEnv
    forall (m :: * -> *). ModuleInput m -> ModuleEnv
    M.minpModuleEnv ModuleInput m
    minp), [])

    {-
    decSatNum :: SatNum -> SatNum
    decSatNum (SomeSat n) | n > 0 = SomeSat (n-1)
    decSatNum n = n
    -}

    multiSATQuery :: forall sym t fm.
      sym ~ W4.ExprBuilder t CryptolState fm =>
      What4 sym ->
      W4ProverConfig ->
      ProverCommand ->
      PrimMap ->
      W4.LogData ->
      [FinType] ->
      [VarShape (What4 sym)] ->
      W4.Pred sym ->
      SatNum ->
      IO (Maybe String, ProverResult)

    multiSATQuery :: forall sym t fm.
    (sym ~ ExprBuilder t CryptolState fm) =>
    What4 sym
    -> W4ProverConfig
    -> ProverCommand
    -> PrimMap
    -> LogData
    -> [FinType]
    -> [VarShape (What4 sym)]
    -> Pred sym
    -> SatNum
    -> IO (Maybe String, ProverResult)
    multiSATQuery What4 sym
    sym W4ProverConfig
    solverCfg ProverCommand
    pc PrimMap
    primMap LogData
    logData [FinType]
    ts [VarShape (What4 sym)]
    args Pred sym
    query (SomeSat Int
    n) | Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int
    1 =
      What4 sym
    -> W4ProverConfig
    -> ProverCommand
    -> PrimMap
    -> LogData
    -> [FinType]
    -> [VarShape (What4 sym)]
    -> Maybe (Pred sym)
    -> Pred sym
    -> IO (Maybe String, ProverResult)
    forall sym t fm.
    (sym ~ ExprBuilder t CryptolState fm) =>
    What4 sym
    -> W4ProverConfig
    -> ProverCommand
    -> PrimMap
    -> LogData
    -> [FinType]
    -> [VarShape (What4 sym)]
    -> Maybe (Pred sym)
    -> Pred sym
    -> IO (Maybe String, ProverResult)
    singleQuery What4 sym
    sym W4ProverConfig
    solverCfg ProverCommand
    pc PrimMap
    primMap LogData
    logData [FinType]
    ts [VarShape (What4 sym)]
    args Maybe (Pred sym)
    Maybe (Expr t 'BaseBoolType)
    forall a. Maybe a
    Nothing Pred sym
    query

    multiSATQuery What4 sym
    _sym W4ProverConfig
    W4OfflineConfig ProverCommand
    _pc PrimMap
    _primMap LogData
    _logData [FinType]
    _ts [VarShape (What4 sym)]
    _args Pred sym
    _query SatNum
    _satNum =
      String -> IO (Maybe String, ProverResult)
    forall a. String -> IO a
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail String
    "What4 offline solver cannot be used for multi-SAT queries"

    multiSATQuery What4 sym
    _sym (W4Portfolio NonEmpty AnAdapter
    _) ProverCommand
    _pc PrimMap
    _primMap LogData
    _logData [FinType]
    _ts [VarShape (What4 sym)]
    _args Pred sym
    _query SatNum
    _satNum =
      String -> IO (Maybe String, ProverResult)
    forall a. String -> IO a
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail String
    "What4 portfolio solver cannot be used for multi-SAT queries"

    multiSATQuery What4 sym
    _sym (W4ProverConfig (AnAdapter forall (st :: * -> *). SolverAdapter st
    adpt)) ProverCommand
    _pc PrimMap
    _primMap LogData
    _logData [FinType]
    _ts [VarShape (What4 sym)]
    _args Pred sym
    _query SatNum
    _satNum =
      String -> IO (Maybe String, ProverResult)
    forall a. String -> IO a
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail (String
    "Solver " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SolverAdapter Any -> String
    forall (st :: * -> *). SolverAdapter st -> String
    solver_adapter_name SolverAdapter Any
    forall (st :: * -> *). SolverAdapter st
    adpt String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " does not support incremental solving and " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++
            String
    "cannot be used for multi-SAT queries.")

    multiSATQuery What4 sym
    sym (W4ProverConfig (AnOnlineAdapter String
    nm ProblemFeatures
    fs [ConfigDesc]
    _opts (Proxy s
    _ :: Proxy s)))
                   ProverCommand{Bool
    String
    [DeclGroup]
    Maybe String
    IORef ProverStats
    Schema
    Expr
    QueryType
    pcQueryType :: ProverCommand -> QueryType
    pcProverName :: ProverCommand -> String
    pcVerbose :: ProverCommand -> Bool
    pcValidate :: ProverCommand -> Bool
    pcProverStats :: ProverCommand -> IORef ProverStats
    pcExtraDecls :: ProverCommand -> [DeclGroup]
    pcSmtFile :: ProverCommand -> Maybe String
    pcExpr :: ProverCommand -> Expr
    pcSchema :: ProverCommand -> Schema
    pcIgnoreSafety :: ProverCommand -> Bool
    pcQueryType :: QueryType
    pcProverName :: String
    pcVerbose :: Bool
    pcValidate :: Bool
    pcProverStats :: IORef ProverStats
    pcExtraDecls :: [DeclGroup]
    pcSmtFile :: Maybe String
    pcExpr :: Expr
    pcSchema :: Schema
    pcIgnoreSafety :: Bool
    ..} PrimMap
    primMap LogData
    _logData [FinType]
    ts [VarShape (What4 sym)]
    args Pred sym
    query SatNum
    satNum0 =
        Maybe String
    -> IOMode
    -> (Maybe Handle -> IO (Maybe String, ProverResult))
    -> IO (Maybe String, ProverResult)
    forall r. Maybe String -> IOMode -> (Maybe Handle -> IO r) -> IO r
    withMaybeFile Maybe String
    pcSmtFile IOMode
    WriteMode ((Maybe Handle -> IO (Maybe String, ProverResult))
     -> IO (Maybe String, ProverResult))
    -> (Maybe Handle -> IO (Maybe String, ProverResult))
    -> IO (Maybe String, ProverResult)
    forall a b. (a -> b) -> a -> b
    $ \Maybe Handle
    smtFileHdl ->
        IO (SolverProcess t s)
    -> (SolverProcess t s -> IO ())
    -> (SolverProcess t s -> IO (Maybe String, ProverResult))
    -> IO (Maybe String, ProverResult)
    forall a b c. IO a -> (a -> IO b) -> (a -> IO c) -> IO c
    X.bracket
          (ProblemFeatures
    -> Maybe Handle
    -> ExprBuilder t CryptolState fm
    -> IO (SolverProcess t s)
    forall solver scope (st :: * -> *) fs.
    OnlineSolver solver =>
    ProblemFeatures
    -> Maybe Handle
    -> ExprBuilder scope st fs
    -> IO (SolverProcess scope solver)
    forall scope (st :: * -> *) fs.
    ProblemFeatures
    -> Maybe Handle
    -> ExprBuilder scope st fs
    -> IO (SolverProcess scope s)
    W4.startSolverProcess ProblemFeatures
    fs Maybe Handle
    smtFileHdl (What4 (ExprBuilder t CryptolState fm)
    -> ExprBuilder t CryptolState fm
    forall sym. What4 sym -> sym
    w4 What4 sym
    What4 (ExprBuilder t CryptolState fm)
    sym))
          (IO (ExitCode, Text) -> IO ()
    forall (f :: * -> *) a. Functor f => f a -> f ()
    void (IO (ExitCode, Text) -> IO ())
    -> (SolverProcess t s -> IO (ExitCode, Text))
    -> SolverProcess t s
    -> IO ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SolverProcess t s -> IO (ExitCode, Text)
    forall scope. SolverProcess scope s -> IO (ExitCode, Text)
    forall solver scope.
    OnlineSolver solver =>
    SolverProcess scope solver -> IO (ExitCode, Text)
    W4.shutdownSolverProcess)
          (\ (SolverProcess t s
    proc :: W4.SolverProcess t s) ->
            do WriterConn t s -> Expr t 'BaseBoolType -> IO ()
    forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
    W4.assume (SolverProcess t s -> WriterConn t s
    forall scope solver.
    SolverProcess scope solver -> WriterConn scope solver
    W4.solverConn SolverProcess t s
    proc) Pred sym
    Expr t 'BaseBoolType
    query
               SatResult (GroundEvalFn t) ()
    res <- SolverProcess t s -> String -> IO (SatResult (GroundEvalFn t) ())
    forall solver scope.
    SMTReadWriter solver =>
    SolverProcess scope solver
    -> String -> IO (SatResult (GroundEvalFn scope) ())
    W4.checkAndGetModel SolverProcess t s
    proc String
    "query"
               case SatResult (GroundEvalFn t) ()
    res of
                 SatResult (GroundEvalFn t) ()
    W4.Unknown -> (Maybe String, ProverResult) -> IO (Maybe String, ProverResult)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (String -> Maybe String
    forall a. a -> Maybe a
    Just String
    nm, String -> ProverResult
    ProverError String
    "Solver returned UNKNOWN")
                 W4.Unsat ()
    _ -> (Maybe String, ProverResult) -> IO (Maybe String, ProverResult)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (String -> Maybe String
    forall a. a -> Maybe a
    Just String
    nm, [TValue] -> ProverResult
    ThmResult ((FinType -> TValue) -> [FinType] -> [TValue]
    forall a b. (a -> b) -> [a] -> [b]
    map FinType -> TValue
    unFinType [FinType]
    ts))
                 W4.Sat GroundEvalFn t
    evalFn ->
                   do [VarShape Concrete]
    xs <- (VarShape (What4 (ExprBuilder t CryptolState fm))
     -> IO (VarShape Concrete))
    -> [VarShape (What4 (ExprBuilder t CryptolState fm))]
    -> IO [VarShape Concrete]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (GroundEvalFn t
    -> VarShape (What4 (ExprBuilder t CryptolState fm))
    -> IO (VarShape Concrete)
    forall t fm.
    GroundEvalFn t
    -> VarShape (What4 (ExprBuilder t CryptolState fm))
    -> IO (VarShape Concrete)
    varShapeToConcrete GroundEvalFn t
    evalFn) [VarShape (What4 sym)]
    [VarShape (What4 (ExprBuilder t CryptolState fm))]
    args
                      let mdl :: [(TValue, Expr, Value)]
    mdl = PrimMap
    -> [FinType] -> [VarShape Concrete] -> [(TValue, Expr, Value)]
    computeModel PrimMap
    primMap [FinType]
    ts [VarShape Concrete]
    xs
                      -- NB, we flatten these shapes to make sure that we can split
                      -- our search across all of the atomic variables
                      let vs :: [VarShape (What4 sym)]
    vs = [VarShape (What4 sym)]
    -> [VarShape (What4 sym)] -> [VarShape (What4 sym)]
    forall sym. [VarShape sym] -> [VarShape sym] -> [VarShape sym]
    flattenShapes [VarShape (What4 sym)]
    args []
                      let cs :: [VarShape Concrete]
    cs = [VarShape Concrete] -> [VarShape Concrete] -> [VarShape Concrete]
    forall sym. [VarShape sym] -> [VarShape sym] -> [VarShape sym]
    flattenShapes [VarShape Concrete]
    xs []
                      Models
    mdls <- SatNum -> MultiSat () -> IO Models
    forall a. SatNum -> MultiSat a -> IO Models
    runMultiSat SatNum
    satNum0 (MultiSat () -> IO Models) -> MultiSat () -> IO Models
    forall a b. (a -> b) -> a -> b
    $
                                do [(TValue, Expr, Value)] -> MultiSat ()
    yield [(TValue, Expr, Value)]
    mdl
                                   SolverProcess t s
    -> [VarShape (What4 sym)] -> [VarShape Concrete] -> MultiSat ()
    computeMoreModels SolverProcess t s
    proc [VarShape (What4 sym)]
    vs [VarShape Concrete]
    cs
                      (Maybe String, ProverResult) -> IO (Maybe String, ProverResult)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (String -> Maybe String
    forall a. a -> Maybe a
    Just String
    nm, Models -> ProverResult
    AllSatResult Models
    mdls))

      where
      -- This search procedure uses incremental solving and push/pop to split on the concrete
      -- values of variables, while also helping to prevent the accumulation of unhelpful
      -- lemmas in the solver state.  This algorithm is basically taken from:
      --   http://theory.stanford.edu/%7Enikolaj/programmingz3.html#sec-blocking-evaluations
      computeMoreModels ::
        W4.SolverProcess t s ->
        [VarShape (What4 sym)] ->
        [VarShape Concrete.Concrete] ->
        MultiSat ()
      computeMoreModels :: SolverProcess t s
    -> [VarShape (What4 sym)] -> [VarShape Concrete] -> MultiSat ()
    computeMoreModels SolverProcess t s
    proc [VarShape (What4 sym)]
    vs [VarShape Concrete]
    cs =
        -- Enumerate all the ways to split up the current model
        [([(VarShape (What4 sym), VarShape Concrete)],
      VarShape (What4 sym), VarShape Concrete, [VarShape (What4 sym)])]
    -> (([(VarShape (What4 sym), VarShape Concrete)],
         VarShape (What4 sym), VarShape Concrete, [VarShape (What4 sym)])
        -> MultiSat ())
    -> MultiSat ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ ([VarShape (What4 sym)]
    -> [VarShape Concrete]
    -> [([(VarShape (What4 sym), VarShape Concrete)],
         VarShape (What4 sym), VarShape Concrete, [VarShape (What4 sym)])]
    forall sym.
    [VarShape (What4 sym)]
    -> [VarShape Concrete]
    -> [([(VarShape (What4 sym), VarShape Concrete)],
         VarShape (What4 sym), VarShape Concrete, [VarShape (What4 sym)])]
    computeSplits [VarShape (What4 sym)]
    vs [VarShape Concrete]
    cs) ((([(VarShape (What4 sym), VarShape Concrete)],
       VarShape (What4 sym), VarShape Concrete, [VarShape (What4 sym)])
      -> MultiSat ())
     -> MultiSat ())
    -> (([(VarShape (What4 sym), VarShape Concrete)],
         VarShape (What4 sym), VarShape Concrete, [VarShape (What4 sym)])
        -> MultiSat ())
    -> MultiSat ()
    forall a b. (a -> b) -> a -> b
    $ \ ([(VarShape (What4 sym), VarShape Concrete)]
    prefix, VarShape (What4 sym)
    vi, VarShape Concrete
    ci, [VarShape (What4 sym)]
    suffix) ->
          do -- open a new solver frame
             IO () -> MultiSat ()
    forall a. IO a -> MultiSat a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> MultiSat ()) -> IO () -> MultiSat ()
    forall a b. (a -> b) -> a -> b
    $ SolverProcess t s -> IO ()
    forall solver scope.
    SMTReadWriter solver =>
    SolverProcess scope solver -> IO ()
    W4.push SolverProcess t s
    proc
             -- force the selected pair to be different
             IO () -> MultiSat ()
    forall a. IO a -> MultiSat a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> MultiSat ()) -> IO () -> MultiSat ()
    forall a b. (a -> b) -> a -> b
    $ WriterConn t s -> Expr t 'BaseBoolType -> IO ()
    forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
    W4.assume (SolverProcess t s -> WriterConn t s
    forall scope solver.
    SolverProcess scope solver -> WriterConn scope solver
    W4.solverConn SolverProcess t s
    proc) (Expr t 'BaseBoolType -> IO ())
    -> IO (Expr t 'BaseBoolType) -> IO ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> Pred sym -> IO (Pred sym)
    forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
    W4.notPred (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) (Expr t 'BaseBoolType -> IO (Expr t 'BaseBoolType))
    -> IO (Expr t 'BaseBoolType) -> IO (Expr t 'BaseBoolType)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< What4 sym
    -> VarShape (What4 sym) -> VarShape Concrete -> IO (Pred sym)
    forall sym t fm.
    (sym ~ ExprBuilder t CryptolState fm) =>
    What4 sym
    -> VarShape (What4 sym) -> VarShape Concrete -> IO (Pred sym)
    computeModelPred What4 sym
    sym VarShape (What4 sym)
    vi VarShape Concrete
    ci
             -- force the prefix values to be the same
             IO () -> MultiSat ()
    forall a. IO a -> MultiSat a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> MultiSat ()) -> IO () -> MultiSat ()
    forall a b. (a -> b) -> a -> b
    $ [(VarShape (What4 sym), VarShape Concrete)]
    -> ((VarShape (What4 sym), VarShape Concrete) -> IO ()) -> IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [(VarShape (What4 sym), VarShape Concrete)]
    prefix (((VarShape (What4 sym), VarShape Concrete) -> IO ()) -> IO ())
    -> ((VarShape (What4 sym), VarShape Concrete) -> IO ()) -> IO ()
    forall a b. (a -> b) -> a -> b
    $ \(VarShape (What4 sym)
    v,VarShape Concrete
    c) ->
               WriterConn t s -> Expr t 'BaseBoolType -> IO ()
    forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
    W4.assume (SolverProcess t s -> WriterConn t s
    forall scope solver.
    SolverProcess scope solver -> WriterConn scope solver
    W4.solverConn SolverProcess t s
    proc) (Expr t 'BaseBoolType -> IO ())
    -> IO (Expr t 'BaseBoolType) -> IO ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< What4 sym
    -> VarShape (What4 sym) -> VarShape Concrete -> IO (Pred sym)
    forall sym t fm.
    (sym ~ ExprBuilder t CryptolState fm) =>
    What4 sym
    -> VarShape (What4 sym) -> VarShape Concrete -> IO (Pred sym)
    computeModelPred What4 sym
    sym VarShape (What4 sym)
    v VarShape Concrete
    c
             -- under these assumptions, find all the remaining models
             SolverProcess t s -> [VarShape (What4 sym)] -> MultiSat ()
    findMoreModels SolverProcess t s
    proc (VarShape (What4 sym)
    viVarShape (What4 sym)
    -> [VarShape (What4 sym)] -> [VarShape (What4 sym)]
    forall a. a -> [a] -> [a]
    :[VarShape (What4 sym)]
    suffix)
             -- pop the current assumption frame
             IO () -> MultiSat ()
    forall a. IO a -> MultiSat a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> MultiSat ()) -> IO () -> MultiSat ()
    forall a b. (a -> b) -> a -> b
    $ SolverProcess t s -> IO ()
    forall solver scope.
    SMTReadWriter solver =>
    SolverProcess scope solver -> IO ()
    W4.pop SolverProcess t s
    proc

      findMoreModels ::
        W4.SolverProcess t s ->
        [VarShape (What4 sym)] ->
        MultiSat ()
      findMoreModels :: SolverProcess t s -> [VarShape (What4 sym)] -> MultiSat ()
    findMoreModels SolverProcess t s
    proc [VarShape (What4 sym)]
    vs =
        -- see if our current assumptions are consistent
        do SatResult (GroundEvalFn t) ()
    res <- IO (SatResult (GroundEvalFn t) ())
    -> MultiSat (SatResult (GroundEvalFn t) ())
    forall a. IO a -> MultiSat a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (SolverProcess t s -> String -> IO (SatResult (GroundEvalFn t) ())
    forall solver scope.
    SMTReadWriter solver =>
    SolverProcess scope solver
    -> String -> IO (SatResult (GroundEvalFn scope) ())
    W4.checkAndGetModel SolverProcess t s
    proc String
    "find model")
           case SatResult (GroundEvalFn t) ()
    res of
             -- if the solver gets stuck, drop all the way out and stop search
             SatResult (GroundEvalFn t) ()
    W4.Unknown -> MultiSat ()
    forall a. MultiSat a
    done
             -- if our assumptions are already unsatisfiable, stop search and return
             W4.Unsat ()
    _ -> () -> MultiSat ()
    forall a. a -> MultiSat a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
             W4.Sat GroundEvalFn t
    evalFn ->
               -- We found a model.  Record it and then use it to split the remaining
               -- search variables some more.
               do [VarShape Concrete]
    xs <- IO [VarShape Concrete] -> MultiSat [VarShape Concrete]
    forall a. IO a -> MultiSat a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO ((VarShape (What4 (ExprBuilder t CryptolState fm))
     -> IO (VarShape Concrete))
    -> [VarShape (What4 (ExprBuilder t CryptolState fm))]
    -> IO [VarShape Concrete]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (GroundEvalFn t
    -> VarShape (What4 (ExprBuilder t CryptolState fm))
    -> IO (VarShape Concrete)
    forall t fm.
    GroundEvalFn t
    -> VarShape (What4 (ExprBuilder t CryptolState fm))
    -> IO (VarShape Concrete)
    varShapeToConcrete GroundEvalFn t
    evalFn) [VarShape (What4 sym)]
    [VarShape (What4 (ExprBuilder t CryptolState fm))]
    args)
                  [(TValue, Expr, Value)] -> MultiSat ()
    yield (PrimMap
    -> [FinType] -> [VarShape Concrete] -> [(TValue, Expr, Value)]
    computeModel PrimMap
    primMap [FinType]
    ts [VarShape Concrete]
    xs)
                  [VarShape Concrete]
    cs <- IO [VarShape Concrete] -> MultiSat [VarShape Concrete]
    forall a. IO a -> MultiSat a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO ((VarShape (What4 (ExprBuilder t CryptolState fm))
     -> IO (VarShape Concrete))
    -> [VarShape (What4 (ExprBuilder t CryptolState fm))]
    -> IO [VarShape Concrete]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (GroundEvalFn t
    -> VarShape (What4 (ExprBuilder t CryptolState fm))
    -> IO (VarShape Concrete)
    forall t fm.
    GroundEvalFn t
    -> VarShape (What4 (ExprBuilder t CryptolState fm))
    -> IO (VarShape Concrete)
    varShapeToConcrete GroundEvalFn t
    evalFn) [VarShape (What4 sym)]
    [VarShape (What4 (ExprBuilder t CryptolState fm))]
    vs)
                  SolverProcess t s
    -> [VarShape (What4 sym)] -> [VarShape Concrete] -> MultiSat ()
    computeMoreModels SolverProcess t s
    proc [VarShape (What4 sym)]
    vs [VarShape Concrete]
    cs

    -- == Support operations for multi-SAT ==
    type Models = [[(TValue, Expr, Concrete.Value)]]

    newtype MultiSat a =
      MultiSat { forall a.
    MultiSat a
    -> Models
    -> SatNum
    -> (a -> Models -> SatNum -> IO Models)
    -> IO Models
    unMultiSat ::  Models -> SatNum -> (a -> Models -> SatNum -> IO Models) -> IO Models }

    instance Functor MultiSat where
      fmap :: forall a b. (a -> b) -> MultiSat a -> MultiSat b
    fmap a -> b
    f MultiSat a
    m = (Models
     -> SatNum -> (b -> Models -> SatNum -> IO Models) -> IO Models)
    -> MultiSat b
    forall a.
    (Models
     -> SatNum -> (a -> Models -> SatNum -> IO Models) -> IO Models)
    -> MultiSat a
    MultiSat (\Models
    ms SatNum
    satNum b -> Models -> SatNum -> IO Models
    k -> MultiSat a
    -> Models
    -> SatNum
    -> (a -> Models -> SatNum -> IO Models)
    -> IO Models
    forall a.
    MultiSat a
    -> Models
    -> SatNum
    -> (a -> Models -> SatNum -> IO Models)
    -> IO Models
    unMultiSat MultiSat a
    m Models
    ms SatNum
    satNum (b -> Models -> SatNum -> IO Models
    k (b -> Models -> SatNum -> IO Models)
    -> (a -> b) -> a -> Models -> SatNum -> IO Models
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> b
    f))

    instance Applicative MultiSat where
      pure :: forall a. a -> MultiSat a
    pure a
    x = (Models
     -> SatNum -> (a -> Models -> SatNum -> IO Models) -> IO Models)
    -> MultiSat a
    forall a.
    (Models
     -> SatNum -> (a -> Models -> SatNum -> IO Models) -> IO Models)
    -> MultiSat a
    MultiSat (\Models
    ms SatNum
    satNum a -> Models -> SatNum -> IO Models
    k -> a -> Models -> SatNum -> IO Models
    k a
    x Models
    ms SatNum
    satNum)
      MultiSat (a -> b)
    mf <*> :: forall a b. MultiSat (a -> b) -> MultiSat a -> MultiSat b
    <*> MultiSat a
    mx = MultiSat (a -> b)
    mf MultiSat (a -> b) -> ((a -> b) -> MultiSat b) -> MultiSat b
    forall a b. MultiSat a -> (a -> MultiSat b) -> MultiSat b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a -> b
    f -> (a -> b) -> MultiSat a -> MultiSat b
    forall a b. (a -> b) -> MultiSat a -> MultiSat b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap a -> b
    f MultiSat a
    mx

    instance Monad MultiSat where
      MultiSat a
    m >>= :: forall a b. MultiSat a -> (a -> MultiSat b) -> MultiSat b
    >>= a -> MultiSat b
    f = (Models
     -> SatNum -> (b -> Models -> SatNum -> IO Models) -> IO Models)
    -> MultiSat b
    forall a.
    (Models
     -> SatNum -> (a -> Models -> SatNum -> IO Models) -> IO Models)
    -> MultiSat a
    MultiSat (\Models
    ms SatNum
    satNum b -> Models -> SatNum -> IO Models
    k -> MultiSat a
    -> Models
    -> SatNum
    -> (a -> Models -> SatNum -> IO Models)
    -> IO Models
    forall a.
    MultiSat a
    -> Models
    -> SatNum
    -> (a -> Models -> SatNum -> IO Models)
    -> IO Models
    unMultiSat MultiSat a
    m Models
    ms SatNum
    satNum (\a
    x Models
    ms' SatNum
    satNum' -> MultiSat b
    -> Models
    -> SatNum
    -> (b -> Models -> SatNum -> IO Models)
    -> IO Models
    forall a.
    MultiSat a
    -> Models
    -> SatNum
    -> (a -> Models -> SatNum -> IO Models)
    -> IO Models
    unMultiSat (a -> MultiSat b
    f a
    x) Models
    ms' SatNum
    satNum' b -> Models -> SatNum -> IO Models
    k))

    instance MonadIO MultiSat where
      liftIO :: forall a. IO a -> MultiSat a
    liftIO IO a
    m = (Models
     -> SatNum -> (a -> Models -> SatNum -> IO Models) -> IO Models)
    -> MultiSat a
    forall a.
    (Models
     -> SatNum -> (a -> Models -> SatNum -> IO Models) -> IO Models)
    -> MultiSat a
    MultiSat (\Models
    ms SatNum
    satNum a -> Models -> SatNum -> IO Models
    k -> do a
    x <- IO a
    m; a -> Models -> SatNum -> IO Models
    k a
    x Models
    ms SatNum
    satNum)

    runMultiSat :: SatNum -> MultiSat a -> IO Models
    runMultiSat :: forall a. SatNum -> MultiSat a -> IO Models
    runMultiSat SatNum
    satNum MultiSat a
    m = Models -> Models
    forall a. [a] -> [a]
    reverse (Models -> Models) -> IO Models -> IO Models
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MultiSat a
    -> Models
    -> SatNum
    -> (a -> Models -> SatNum -> IO Models)
    -> IO Models
    forall a.
    MultiSat a
    -> Models
    -> SatNum
    -> (a -> Models -> SatNum -> IO Models)
    -> IO Models
    unMultiSat MultiSat a
    m [] SatNum
    satNum (\a
    _ Models
    ms SatNum
    _ -> Models -> IO Models
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Models
    ms)

    done :: MultiSat a
    done :: forall a. MultiSat a
    done = (Models
     -> SatNum -> (a -> Models -> SatNum -> IO Models) -> IO Models)
    -> MultiSat a
    forall a.
    (Models
     -> SatNum -> (a -> Models -> SatNum -> IO Models) -> IO Models)
    -> MultiSat a
    MultiSat (\Models
    ms SatNum
    _satNum a -> Models -> SatNum -> IO Models
    _k -> Models -> IO Models
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Models
    ms)

    yield :: [(TValue, Expr, Concrete.Value)] -> MultiSat ()
    yield :: [(TValue, Expr, Value)] -> MultiSat ()
    yield [(TValue, Expr, Value)]
    mdl = (Models
     -> SatNum -> (() -> Models -> SatNum -> IO Models) -> IO Models)
    -> MultiSat ()
    forall a.
    (Models
     -> SatNum -> (a -> Models -> SatNum -> IO Models) -> IO Models)
    -> MultiSat a
    MultiSat (\Models
    ms SatNum
    satNum () -> Models -> SatNum -> IO Models
    k ->
      case SatNum
    satNum of
        SomeSat Int
    n
          | Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    1 -> () -> Models -> SatNum -> IO Models
    k () ([(TValue, Expr, Value)]
    mdl[(TValue, Expr, Value)] -> Models -> Models
    forall a. a -> [a] -> [a]
    :Models
    ms) (Int -> SatNum
    SomeSat (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1))
          | Bool
    otherwise -> Models -> IO Models
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([(TValue, Expr, Value)]
    mdl[(TValue, Expr, Value)] -> Models -> Models
    forall a. a -> [a] -> [a]
    :Models
    ms)
        SatNum
    _ -> () -> Models -> SatNum -> IO Models
    k () ([(TValue, Expr, Value)]
    mdl[(TValue, Expr, Value)] -> Models -> Models
    forall a. a -> [a] -> [a]
    :Models
    ms) SatNum
    satNum)

    -- Compute all the ways to split a sequences of variables
    -- and concrete values for those variables.  Each element
    -- of the list consists of a prefix of (varaible,value)
    -- pairs whose values we will fix, a single (varaible,value)
    -- pair that we will force to be different, and a list of
    -- additional unconstrained variables.
    computeSplits ::
      [VarShape (What4 sym)] ->
      [VarShape Concrete.Concrete] ->
      [ ( [(VarShape (What4 sym), VarShape Concrete.Concrete)]
        , VarShape (What4 sym)
        , VarShape Concrete.Concrete
        , [VarShape (What4 sym)]
        )
      ]
    computeSplits :: forall sym.
    [VarShape (What4 sym)]
    -> [VarShape Concrete]
    -> [([(VarShape (What4 sym), VarShape Concrete)],
         VarShape (What4 sym), VarShape Concrete, [VarShape (What4 sym)])]
    computeSplits [VarShape (What4 sym)]
    vs [VarShape Concrete]
    cs = [([(VarShape (What4 sym), VarShape Concrete)],
      VarShape (What4 sym), VarShape Concrete, [VarShape (What4 sym)])]
    -> [([(VarShape (What4 sym), VarShape Concrete)],
         VarShape (What4 sym), VarShape Concrete, [VarShape (What4 sym)])]
    forall a. [a] -> [a]
    reverse
      [ ([(VarShape (What4 sym), VarShape Concrete)]
    prefix, VarShape (What4 sym)
    v, VarShape Concrete
    c, [VarShape (What4 sym)]
    tl)
      | [(VarShape (What4 sym), VarShape Concrete)]
    prefix <- [(VarShape (What4 sym), VarShape Concrete)]
    -> [[(VarShape (What4 sym), VarShape Concrete)]]
    forall a. [a] -> [[a]]
    inits ([VarShape (What4 sym)]
    -> [VarShape Concrete]
    -> [(VarShape (What4 sym), VarShape Concrete)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [VarShape (What4 sym)]
    vs [VarShape Concrete]
    cs)
      | VarShape (What4 sym)
    v      <- [VarShape (What4 sym)]
    vs
      | VarShape Concrete
    c      <- [VarShape Concrete]
    cs
      | [VarShape (What4 sym)]
    tl     <- [[VarShape (What4 sym)]] -> [[VarShape (What4 sym)]]
    forall a. HasCallStack => [a] -> [a]
    tail ([VarShape (What4 sym)] -> [[VarShape (What4 sym)]]
    forall a. [a] -> [[a]]
    tails [VarShape (What4 sym)]
    vs)
      ]
    -- == END Support operations for multi-SAT ==

    singleQuery ::
      sym ~ W4.ExprBuilder t CryptolState fm =>
      What4 sym ->
      W4ProverConfig ->
      ProverCommand ->
      PrimMap ->
      W4.LogData ->
      [FinType] ->
      [VarShape (What4 sym)] ->
      Maybe (W4.Pred sym) {- ^ optional safety predicate.  Nothing = SAT query -} ->
      W4.Pred sym ->
      IO (Maybe String, ProverResult)

    singleQuery :: forall sym t fm.
    (sym ~ ExprBuilder t CryptolState fm) =>
    What4 sym
    -> W4ProverConfig
    -> ProverCommand
    -> PrimMap
    -> LogData
    -> [FinType]
    -> [VarShape (What4 sym)]
    -> Maybe (Pred sym)
    -> Pred sym
    -> IO (Maybe String, ProverResult)
    singleQuery What4 sym
    _ W4ProverConfig
    W4OfflineConfig ProverCommand
    _pc PrimMap
    _primMap LogData
    _logData [FinType]
    _ts [VarShape (What4 sym)]
    _args Maybe (Pred sym)
    _msafe Pred sym
    _query =
      -- this shouldn't happen...
      String -> IO (Maybe String, ProverResult)
    forall a. String -> IO a
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail String
    "What4 offline solver cannot be used for direct queries"

    singleQuery What4 sym
    sym (W4Portfolio NonEmpty AnAdapter
    ps) ProverCommand
    pc PrimMap
    primMap LogData
    logData [FinType]
    ts [VarShape (What4 sym)]
    args Maybe (Pred sym)
    msafe Pred sym
    query =
      do [Async (Maybe String, ProverResult)]
    as <- (IO (Maybe String, ProverResult)
     -> IO (Async (Maybe String, ProverResult)))
    -> [IO (Maybe String, ProverResult)]
    -> IO [Async (Maybe String, ProverResult)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM IO (Maybe String, ProverResult)
    -> IO (Async (Maybe String, ProverResult))
    forall a. IO a -> IO (Async a)
    async [ What4 sym
    -> W4ProverConfig
    -> ProverCommand
    -> PrimMap
    -> LogData
    -> [FinType]
    -> [VarShape (What4 sym)]
    -> Maybe (Pred sym)
    -> Pred sym
    -> IO (Maybe String, ProverResult)
    forall sym t fm.
    (sym ~ ExprBuilder t CryptolState fm) =>
    What4 sym
    -> W4ProverConfig
    -> ProverCommand
    -> PrimMap
    -> LogData
    -> [FinType]
    -> [VarShape (What4 sym)]
    -> Maybe (Pred sym)
    -> Pred sym
    -> IO (Maybe String, ProverResult)
    singleQuery What4 sym
    sym (AnAdapter -> W4ProverConfig
    W4ProverConfig AnAdapter
    p) ProverCommand
    pc PrimMap
    primMap LogData
    logData [FinType]
    ts [VarShape (What4 sym)]
    args Maybe (Pred sym)
    msafe Pred sym
    query
                          | AnAdapter
    p <- NonEmpty AnAdapter -> [AnAdapter]
    forall a. NonEmpty a -> [a]
    NE.toList NonEmpty AnAdapter
    ps
                          ]
         [Either SomeException (Maybe String, String)]
    -> [Async (Maybe String, ProverResult)]
    -> IO (Maybe String, ProverResult)
    waitForResults [] [Async (Maybe String, ProverResult)]
    as

     where
     waitForResults :: [Either SomeException (Maybe String, String)]
    -> [Async (Maybe String, ProverResult)]
    -> IO (Maybe String, ProverResult)
    waitForResults [Either SomeException (Maybe String, String)]
    exs [] = W4Exception -> IO (Maybe String, ProverResult)
    forall e a. Exception e => e -> IO a
    X.throwIO ([Either SomeException (Maybe String, String)] -> W4Exception
    W4PortfolioFailure [Either SomeException (Maybe String, String)]
    exs)
     waitForResults [Either SomeException (Maybe String, String)]
    exs [Async (Maybe String, ProverResult)]
    as =
       do (Async (Maybe String, ProverResult)
    winner, Either SomeException (Maybe String, ProverResult)
    result) <- [Async (Maybe String, ProverResult)]
    -> IO
         (Async (Maybe String, ProverResult),
          Either SomeException (Maybe String, ProverResult))
    forall a. [Async a] -> IO (Async a, Either SomeException a)
    waitAnyCatch [Async (Maybe String, ProverResult)]
    as
          let others :: [Async (Maybe String, ProverResult)]
    others = (Async (Maybe String, ProverResult) -> Bool)
    -> [Async (Maybe String, ProverResult)]
    -> [Async (Maybe String, ProverResult)]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Async (Maybe String, ProverResult)
    -> Async (Maybe String, ProverResult) -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Async (Maybe String, ProverResult)
    winner) [Async (Maybe String, ProverResult)]
    as
          case Either SomeException (Maybe String, ProverResult)
    result of
            Left SomeException
    ex ->
              [Either SomeException (Maybe String, String)]
    -> [Async (Maybe String, ProverResult)]
    -> IO (Maybe String, ProverResult)
    waitForResults (SomeException -> Either SomeException (Maybe String, String)
    forall a b. a -> Either a b
    Left SomeException
    exEither SomeException (Maybe String, String)
    -> [Either SomeException (Maybe String, String)]
    -> [Either SomeException (Maybe String, String)]
    forall a. a -> [a] -> [a]
    :[Either SomeException (Maybe String, String)]
    exs) [Async (Maybe String, ProverResult)]
    others
            Right (Maybe String
    nm, ProverError String
    err) ->
              [Either SomeException (Maybe String, String)]
    -> [Async (Maybe String, ProverResult)]
    -> IO (Maybe String, ProverResult)
    waitForResults ((Maybe String, String)
    -> Either SomeException (Maybe String, String)
    forall a b. b -> Either a b
    Right (Maybe String
    nm,String
    err) Either SomeException (Maybe String, String)
    -> [Either SomeException (Maybe String, String)]
    -> [Either SomeException (Maybe String, String)]
    forall a. a -> [a] -> [a]
    : [Either SomeException (Maybe String, String)]
    exs) [Async (Maybe String, ProverResult)]
    others
            Right (Maybe String, ProverResult)
    r ->
              do [Async (Maybe String, ProverResult)]
    -> (Async (Maybe String, ProverResult) -> IO ()) -> IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [Async (Maybe String, ProverResult)]
    others (\Async (Maybe String, ProverResult)
    a -> ThreadId -> ExitCode -> IO ()
    forall e. Exception e => ThreadId -> e -> IO ()
    X.throwTo (Async (Maybe String, ProverResult) -> ThreadId
    forall a. Async a -> ThreadId
    asyncThreadId Async (Maybe String, ProverResult)
    a) ExitCode
    ExitSuccess)
                 (Maybe String, ProverResult) -> IO (Maybe String, ProverResult)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe String, ProverResult)
    r

    singleQuery What4 sym
    sym (W4ProverConfig (AnAdapter forall (st :: * -> *). SolverAdapter st
    adpt)) ProverCommand
    _pc PrimMap
    primMap LogData
    logData [FinType]
    ts [VarShape (What4 sym)]
    args Maybe (Pred sym)
    msafe Pred sym
    query =
      do ProverResult
    pres <- SolverAdapter CryptolState
    -> forall t fs a.
       ExprBuilder t CryptolState fs
       -> LogData
       -> [BoolExpr t]
       -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
           -> IO a)
       -> IO a
    forall (st :: * -> *).
    SolverAdapter st
    -> forall t fs a.
       ExprBuilder t st fs
       -> LogData
       -> [BoolExpr t]
       -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
           -> IO a)
       -> IO a
    W4.solver_adapter_check_sat SolverAdapter CryptolState
    forall (st :: * -> *). SolverAdapter st
    adpt (What4 (ExprBuilder t CryptolState fm)
    -> ExprBuilder t CryptolState fm
    forall sym. What4 sym -> sym
    w4 What4 sym
    What4 (ExprBuilder t CryptolState fm)
    sym) LogData
    logData [Pred sym
    BoolExpr t
    query] ((SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
      -> IO ProverResult)
     -> IO ProverResult)
    -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
        -> IO ProverResult)
    -> IO ProverResult
    forall a b. (a -> b) -> a -> b
    $ \SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    res ->
             case SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    res of
               SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    W4.Unknown -> ProverResult -> IO ProverResult
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (String -> ProverResult
    ProverError String
    "Solver returned UNKNOWN")
               W4.Unsat ()
    _ -> ProverResult -> IO ProverResult
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([TValue] -> ProverResult
    ThmResult ((FinType -> TValue) -> [FinType] -> [TValue]
    forall a b. (a -> b) -> [a] -> [b]
    map FinType -> TValue
    unFinType [FinType]
    ts))
               W4.Sat (GroundEvalFn t
    evalFn,Maybe (ExprRangeBindings t)
    _) ->
                 do [VarShape Concrete]
    xs <- (VarShape (What4 (ExprBuilder t CryptolState fm))
     -> IO (VarShape Concrete))
    -> [VarShape (What4 (ExprBuilder t CryptolState fm))]
    -> IO [VarShape Concrete]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (GroundEvalFn t
    -> VarShape (What4 (ExprBuilder t CryptolState fm))
    -> IO (VarShape Concrete)
    forall t fm.
    GroundEvalFn t
    -> VarShape (What4 (ExprBuilder t CryptolState fm))
    -> IO (VarShape Concrete)
    varShapeToConcrete GroundEvalFn t
    evalFn) [VarShape (What4 sym)]
    [VarShape (What4 (ExprBuilder t CryptolState fm))]
    args
                    let model :: [(TValue, Expr, Value)]
    model = PrimMap
    -> [FinType] -> [VarShape Concrete] -> [(TValue, Expr, Value)]
    computeModel PrimMap
    primMap [FinType]
    ts [VarShape Concrete]
    xs
                    case Maybe (Pred sym)
    msafe of
                      Just Pred sym
    s ->
                        do Bool
    s' <- GroundEvalFn t
    -> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
    forall t.
    GroundEvalFn t
    -> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
    W4.groundEval GroundEvalFn t
    evalFn Pred sym
    BoolExpr t
    s
                           let cexType :: CounterExampleType
    cexType = if Bool
    s' then CounterExampleType
    PredicateFalsified else CounterExampleType
    SafetyViolation
                           ProverResult -> IO ProverResult
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (CounterExampleType -> [(TValue, Expr, Value)] -> ProverResult
    CounterExample CounterExampleType
    cexType [(TValue, Expr, Value)]
    model)
                      Maybe (Pred sym)
    Nothing -> ProverResult -> IO ProverResult
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Models -> ProverResult
    AllSatResult [ [(TValue, Expr, Value)]
    model ])

         (Maybe String, ProverResult) -> IO (Maybe String, ProverResult)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (String -> Maybe String
    forall a. a -> Maybe a
    Just (SolverAdapter Any -> String
    forall (st :: * -> *). SolverAdapter st -> String
    W4.solver_adapter_name SolverAdapter Any
    forall (st :: * -> *). SolverAdapter st
    adpt), ProverResult
    pres)

    singleQuery What4 sym
    sym (W4ProverConfig (AnOnlineAdapter String
    nm ProblemFeatures
    fs [ConfigDesc]
    _opts (Proxy s
    _ :: Proxy s)))
                  ProverCommand{Bool
    String
    [DeclGroup]
    Maybe String
    IORef ProverStats
    Schema
    Expr
    QueryType
    pcQueryType :: ProverCommand -> QueryType
    pcProverName :: ProverCommand -> String
    pcVerbose :: ProverCommand -> Bool
    pcValidate :: ProverCommand -> Bool
    pcProverStats :: ProverCommand -> IORef ProverStats
    pcExtraDecls :: ProverCommand -> [DeclGroup]
    pcSmtFile :: ProverCommand -> Maybe String
    pcExpr :: ProverCommand -> Expr
    pcSchema :: ProverCommand -> Schema
    pcIgnoreSafety :: ProverCommand -> Bool
    pcQueryType :: QueryType
    pcProverName :: String
    pcVerbose :: Bool
    pcValidate :: Bool
    pcProverStats :: IORef ProverStats
    pcExtraDecls :: [DeclGroup]
    pcSmtFile :: Maybe String
    pcExpr :: Expr
    pcSchema :: Schema
    pcIgnoreSafety :: Bool
    ..} PrimMap
    primMap LogData
    _logData [FinType]
    ts [VarShape (What4 sym)]
    args Maybe (Pred sym)
    msafe Pred sym
    query =
      Maybe String
    -> IOMode
    -> (Maybe Handle -> IO (Maybe String, ProverResult))
    -> IO (Maybe String, ProverResult)
    forall r. Maybe String -> IOMode -> (Maybe Handle -> IO r) -> IO r
    withMaybeFile Maybe String
    pcSmtFile IOMode
    WriteMode ((Maybe Handle -> IO (Maybe String, ProverResult))
     -> IO (Maybe String, ProverResult))
    -> (Maybe Handle -> IO (Maybe String, ProverResult))
    -> IO (Maybe String, ProverResult)
    forall a b. (a -> b) -> a -> b
    $ \Maybe Handle
    smtFileHdl ->
      IO (SolverProcess t s)
    -> (SolverProcess t s -> IO ())
    -> (SolverProcess t s -> IO (Maybe String, ProverResult))
    -> IO (Maybe String, ProverResult)
    forall a b c. IO a -> (a -> IO b) -> (a -> IO c) -> IO c
    X.bracket
        (ProblemFeatures
    -> Maybe Handle
    -> ExprBuilder t CryptolState fm
    -> IO (SolverProcess t s)
    forall solver scope (st :: * -> *) fs.
    OnlineSolver solver =>
    ProblemFeatures
    -> Maybe Handle
    -> ExprBuilder scope st fs
    -> IO (SolverProcess scope solver)
    forall scope (st :: * -> *) fs.
    ProblemFeatures
    -> Maybe Handle
    -> ExprBuilder scope st fs
    -> IO (SolverProcess scope s)
    W4.startSolverProcess ProblemFeatures
    fs Maybe Handle
    smtFileHdl (What4 (ExprBuilder t CryptolState fm)
    -> ExprBuilder t CryptolState fm
    forall sym. What4 sym -> sym
    w4 What4 sym
    What4 (ExprBuilder t CryptolState fm)
    sym))
        (IO (ExitCode, Text) -> IO ()
    forall (f :: * -> *) a. Functor f => f a -> f ()
    void (IO (ExitCode, Text) -> IO ())
    -> (SolverProcess t s -> IO (ExitCode, Text))
    -> SolverProcess t s
    -> IO ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SolverProcess t s -> IO (ExitCode, Text)
    forall scope. SolverProcess scope s -> IO (ExitCode, Text)
    forall solver scope.
    OnlineSolver solver =>
    SolverProcess scope solver -> IO (ExitCode, Text)
    W4.shutdownSolverProcess)
        (\ (SolverProcess t s
    proc :: W4.SolverProcess t s) ->
            do WriterConn t s -> BoolExpr t -> IO ()
    forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
    W4.assume (SolverProcess t s -> WriterConn t s
    forall scope solver.
    SolverProcess scope solver -> WriterConn scope solver
    W4.solverConn SolverProcess t s
    proc) Pred sym
    BoolExpr t
    query
               SatResult (GroundEvalFn t) ()
    res <- SolverProcess t s -> String -> IO (SatResult (GroundEvalFn t) ())
    forall solver scope.
    SMTReadWriter solver =>
    SolverProcess scope solver
    -> String -> IO (SatResult (GroundEvalFn scope) ())
    W4.checkAndGetModel SolverProcess t s
    proc String
    "query"
               case SatResult (GroundEvalFn t) ()
    res of
                 SatResult (GroundEvalFn t) ()
    W4.Unknown -> (Maybe String, ProverResult) -> IO (Maybe String, ProverResult)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (String -> Maybe String
    forall a. a -> Maybe a
    Just String
    nm, String -> ProverResult
    ProverError String
    "Solver returned UNKNOWN")
                 W4.Unsat ()
    _ -> (Maybe String, ProverResult) -> IO (Maybe String, ProverResult)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (String -> Maybe String
    forall a. a -> Maybe a
    Just String
    nm, [TValue] -> ProverResult
    ThmResult ((FinType -> TValue) -> [FinType] -> [TValue]
    forall a b. (a -> b) -> [a] -> [b]
    map FinType -> TValue
    unFinType [FinType]
    ts))
                 W4.Sat GroundEvalFn t
    evalFn ->
                   do [VarShape Concrete]
    xs <- (VarShape (What4 (ExprBuilder t CryptolState fm))
     -> IO (VarShape Concrete))
    -> [VarShape (What4 (ExprBuilder t CryptolState fm))]
    -> IO [VarShape Concrete]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (GroundEvalFn t
    -> VarShape (What4 (ExprBuilder t CryptolState fm))
    -> IO (VarShape Concrete)
    forall t fm.
    GroundEvalFn t
    -> VarShape (What4 (ExprBuilder t CryptolState fm))
    -> IO (VarShape Concrete)
    varShapeToConcrete GroundEvalFn t
    evalFn) [VarShape (What4 sym)]
    [VarShape (What4 (ExprBuilder t CryptolState fm))]
    args
                      let model :: [(TValue, Expr, Value)]
    model = PrimMap
    -> [FinType] -> [VarShape Concrete] -> [(TValue, Expr, Value)]
    computeModel PrimMap
    primMap [FinType]
    ts [VarShape Concrete]
    xs
                      case Maybe (Pred sym)
    msafe of
                        Just Pred sym
    s ->
                          do Bool
    s' <- GroundEvalFn t
    -> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
    forall t.
    GroundEvalFn t
    -> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
    W4.groundEval GroundEvalFn t
    evalFn Pred sym
    BoolExpr t
    s
                             let cexType :: CounterExampleType
    cexType = if Bool
    s' then CounterExampleType
    PredicateFalsified else CounterExampleType
    SafetyViolation
                             (Maybe String, ProverResult) -> IO (Maybe String, ProverResult)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (String -> Maybe String
    forall a. a -> Maybe a
    Just String
    nm, CounterExampleType -> [(TValue, Expr, Value)] -> ProverResult
    CounterExample CounterExampleType
    cexType [(TValue, Expr, Value)]
    model)
                        Maybe (Pred sym)
    Nothing -> (Maybe String, ProverResult) -> IO (Maybe String, ProverResult)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (String -> Maybe String
    forall a. a -> Maybe a
    Just String
    nm, Models -> ProverResult
    AllSatResult [ [(TValue, Expr, Value)]
    model ])
        )

    -- | Like 'withFile', but lifted to work over 'Maybe'.
    withMaybeFile :: Maybe FilePath -> IOMode -> (Maybe Handle -> IO r) -> IO r
    withMaybeFile :: forall r. Maybe String -> IOMode -> (Maybe Handle -> IO r) -> IO r
    withMaybeFile Maybe String
    mbFP IOMode
    mode Maybe Handle -> IO r
    action =
      case Maybe String
    mbFP of
        Just String
    fp -> String -> IOMode -> (Handle -> IO r) -> IO r
    forall r. String -> IOMode -> (Handle -> IO r) -> IO r
    withFile String
    fp IOMode
    mode (Maybe Handle -> IO r
    action (Maybe Handle -> IO r)
    -> (Handle -> Maybe Handle) -> Handle -> IO r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Handle -> Maybe Handle
    forall a. a -> Maybe a
    Just)
        Maybe String
    Nothing -> Maybe Handle -> IO r
    action Maybe Handle
    forall a. Maybe a
    Nothing

    computeModelPred ::
      sym ~ W4.ExprBuilder t CryptolState fm =>
      What4 sym ->
      VarShape (What4 sym) ->
      VarShape Concrete.Concrete ->
      IO (W4.Pred sym)
    computeModelPred :: forall sym t fm.
    (sym ~ ExprBuilder t CryptolState fm) =>
    What4 sym
    -> VarShape (What4 sym) -> VarShape Concrete -> IO (Pred sym)
    computeModelPred What4 sym
    sym VarShape (What4 sym)
    v VarShape Concrete
    c =
      (Expr t 'BaseBoolType, Expr t 'BaseBoolType)
    -> Expr t 'BaseBoolType
    forall a b. (a, b) -> b
    snd ((Expr t 'BaseBoolType, Expr t 'BaseBoolType)
     -> Expr t 'BaseBoolType)
    -> IO (Expr t 'BaseBoolType, Expr t 'BaseBoolType)
    -> IO (Expr t 'BaseBoolType)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym
    -> W4Eval sym (Expr t 'BaseBoolType)
    -> IO (SymExpr sym 'BaseBoolType, Expr t 'BaseBoolType)
    forall sym (m :: * -> *) a.
    (IsExprBuilder sym, MonadIO m) =>
    sym -> W4Eval sym a -> m (Pred sym, a)
    doW4Eval (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) (What4 sym
    -> (VarShape (What4 sym), VarShape Concrete)
    -> SEval (What4 sym) (SBit (What4 sym))
    forall sym.
    Backend sym =>
    sym -> (VarShape sym, VarShape Concrete) -> SEval sym (SBit sym)
    varModelPred What4 sym
    sym (VarShape (What4 sym)
    v, VarShape Concrete
    c))

    varShapeToConcrete ::
      W4.GroundEvalFn t ->
      VarShape (What4 (W4.ExprBuilder t CryptolState fm)) ->
      IO (VarShape Concrete.Concrete)
    varShapeToConcrete :: forall t fm.
    GroundEvalFn t
    -> VarShape (What4 (ExprBuilder t CryptolState fm))
    -> IO (VarShape Concrete)
    varShapeToConcrete GroundEvalFn t
    evalFn VarShape (What4 (ExprBuilder t CryptolState fm))
    v =
      case VarShape (What4 (ExprBuilder t CryptolState fm))
    v of
        VarBit SBit (What4 (ExprBuilder t CryptolState fm))
    b -> Bool -> VarShape Concrete
    SBit Concrete -> VarShape Concrete
    forall sym. SBit sym -> VarShape sym
    VarBit (Bool -> VarShape Concrete) -> IO Bool -> IO (VarShape Concrete)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> GroundEvalFn t
    -> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
    forall t.
    GroundEvalFn t
    -> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
    W4.groundEval GroundEvalFn t
    evalFn Expr t 'BaseBoolType
    SBit (What4 (ExprBuilder t CryptolState fm))
    b
        VarInteger SInteger (What4 (ExprBuilder t CryptolState fm))
    i -> Integer -> VarShape Concrete
    SInteger Concrete -> VarShape Concrete
    forall sym. SInteger sym -> VarShape sym
    VarInteger (Integer -> VarShape Concrete)
    -> IO Integer -> IO (VarShape Concrete)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> GroundEvalFn t
    -> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
    forall t.
    GroundEvalFn t
    -> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
    W4.groundEval GroundEvalFn t
    evalFn Expr t BaseIntegerType
    SInteger (What4 (ExprBuilder t CryptolState fm))
    i
        VarRational SInteger (What4 (ExprBuilder t CryptolState fm))
    n SInteger (What4 (ExprBuilder t CryptolState fm))
    d -> Integer -> Integer -> VarShape Concrete
    SInteger Concrete -> SInteger Concrete -> VarShape Concrete
    forall sym. SInteger sym -> SInteger sym -> VarShape sym
    VarRational (Integer -> Integer -> VarShape Concrete)
    -> IO Integer -> IO (Integer -> VarShape Concrete)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> GroundEvalFn t
    -> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
    forall t.
    GroundEvalFn t
    -> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
    W4.groundEval GroundEvalFn t
    evalFn Expr t BaseIntegerType
    SInteger (What4 (ExprBuilder t CryptolState fm))
    n IO (Integer -> VarShape Concrete)
    -> IO Integer -> IO (VarShape Concrete)
    forall a b. IO (a -> b) -> IO a -> IO b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> GroundEvalFn t
    -> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
    forall t.
    GroundEvalFn t
    -> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
    W4.groundEval GroundEvalFn t
    evalFn Expr t BaseIntegerType
    SInteger (What4 (ExprBuilder t CryptolState fm))
    d
        VarWord SWord (ExprBuilder t CryptolState fm)
    SWord (What4 (ExprBuilder t CryptolState fm))
    SW.ZBV -> VarShape Concrete -> IO (VarShape Concrete)
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SWord Concrete -> VarShape Concrete
    forall sym. SWord sym -> VarShape sym
    VarWord (Integer -> Integer -> BV
    Concrete.mkBv Integer
    0 Integer
    0))
        VarWord (SW.DBV SymBV (ExprBuilder t CryptolState fm) w
    x) ->
          let w :: Integer
    w = NatRepr w -> Integer
    forall (n :: Natural). NatRepr n -> Integer
    W4.intValue (Expr t (BaseBVType w) -> NatRepr w
    forall (w :: Natural). Expr t (BaseBVType w) -> NatRepr w
    forall (e :: BaseType -> *) (w :: Natural).
    IsExpr e =>
    e (BaseBVType w) -> NatRepr w
    W4.bvWidth SymBV (ExprBuilder t CryptolState fm) w
    Expr t (BaseBVType w)
    x)
           in SWord Concrete -> VarShape Concrete
    BV -> VarShape Concrete
    forall sym. SWord sym -> VarShape sym
    VarWord (BV -> VarShape Concrete)
    -> (BV w -> BV) -> BV w -> VarShape Concrete
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Integer -> BV
    Concrete.mkBv Integer
    w (Integer -> BV) -> (BV w -> Integer) -> BV w -> BV
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BV w -> Integer
    forall (w :: Natural). BV w -> Integer
    BV.asUnsigned (BV w -> VarShape Concrete) -> IO (BV w) -> IO (VarShape Concrete)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> GroundEvalFn t
    -> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
    forall t.
    GroundEvalFn t
    -> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
    W4.groundEval GroundEvalFn t
    evalFn SymBV (ExprBuilder t CryptolState fm) w
    Expr t (BaseBVType w)
    x
        VarFloat fv :: SFloat (What4 (ExprBuilder t CryptolState fm))
    fv@(W4.SFloat SymFloat (ExprBuilder t CryptolState fm) fpp
    f) ->
          let (Integer
    e,Integer
    p) = SFloat (ExprBuilder t CryptolState fm) -> (Integer, Integer)
    forall sym. SFloat sym -> (Integer, Integer)
    W4.fpSize SFloat (ExprBuilder t CryptolState fm)
    SFloat (What4 (ExprBuilder t CryptolState fm))
    fv
           in BF -> VarShape Concrete
    SFloat Concrete -> VarShape Concrete
    forall sym. SFloat sym -> VarShape sym
    VarFloat (BF -> VarShape Concrete)
    -> (BigFloat -> BF) -> BigFloat -> VarShape Concrete
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Integer -> BigFloat -> BF
    FH.BF Integer
    e Integer
    p (BigFloat -> VarShape Concrete)
    -> IO BigFloat -> IO (VarShape Concrete)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> GroundEvalFn t
    -> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
    forall t.
    GroundEvalFn t
    -> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
    W4.groundEval GroundEvalFn t
    evalFn SymFloat (ExprBuilder t CryptolState fm) fpp
    Expr t (BaseFloatType fpp)
    f
        VarFinSeq Integer
    n [VarShape (What4 (ExprBuilder t CryptolState fm))]
    vs ->
          Integer -> [VarShape Concrete] -> VarShape Concrete
    forall sym. Integer -> [VarShape sym] -> VarShape sym
    VarFinSeq Integer
    n ([VarShape Concrete] -> VarShape Concrete)
    -> IO [VarShape Concrete] -> IO (VarShape Concrete)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (VarShape (What4 (ExprBuilder t CryptolState fm))
     -> IO (VarShape Concrete))
    -> [VarShape (What4 (ExprBuilder t CryptolState fm))]
    -> IO [VarShape Concrete]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (GroundEvalFn t
    -> VarShape (What4 (ExprBuilder t CryptolState fm))
    -> IO (VarShape Concrete)
    forall t fm.
    GroundEvalFn t
    -> VarShape (What4 (ExprBuilder t CryptolState fm))
    -> IO (VarShape Concrete)
    varShapeToConcrete GroundEvalFn t
    evalFn) [VarShape (What4 (ExprBuilder t CryptolState fm))]
    vs
        VarTuple [VarShape (What4 (ExprBuilder t CryptolState fm))]
    vs ->
          [VarShape Concrete] -> VarShape Concrete
    forall sym. [VarShape sym] -> VarShape sym
    VarTuple ([VarShape Concrete] -> VarShape Concrete)
    -> IO [VarShape Concrete] -> IO (VarShape Concrete)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (VarShape (What4 (ExprBuilder t CryptolState fm))
     -> IO (VarShape Concrete))
    -> [VarShape (What4 (ExprBuilder t CryptolState fm))]
    -> IO [VarShape Concrete]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (GroundEvalFn t
    -> VarShape (What4 (ExprBuilder t CryptolState fm))
    -> IO (VarShape Concrete)
    forall t fm.
    GroundEvalFn t
    -> VarShape (What4 (ExprBuilder t CryptolState fm))
    -> IO (VarShape Concrete)
    varShapeToConcrete GroundEvalFn t
    evalFn) [VarShape (What4 (ExprBuilder t CryptolState fm))]
    vs
        VarRecord RecordMap Ident (VarShape (What4 (ExprBuilder t CryptolState fm)))
    fs ->
          RecordMap Ident (VarShape Concrete) -> VarShape Concrete
    forall sym. RecordMap Ident (VarShape sym) -> VarShape sym
    VarRecord (RecordMap Ident (VarShape Concrete) -> VarShape Concrete)
    -> IO (RecordMap Ident (VarShape Concrete))
    -> IO (VarShape Concrete)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (VarShape (What4 (ExprBuilder t CryptolState fm))
     -> IO (VarShape Concrete))
    -> RecordMap
         Ident (VarShape (What4 (ExprBuilder t CryptolState fm)))
    -> IO (RecordMap Ident (VarShape Concrete))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> RecordMap Ident a -> f (RecordMap Ident b)
    traverse (GroundEvalFn t
    -> VarShape (What4 (ExprBuilder t CryptolState fm))
    -> IO (VarShape Concrete)
    forall t fm.
    GroundEvalFn t
    -> VarShape (What4 (ExprBuilder t CryptolState fm))
    -> IO (VarShape Concrete)
    varShapeToConcrete GroundEvalFn t
    evalFn) RecordMap Ident (VarShape (What4 (ExprBuilder t CryptolState fm)))
    fs