    {-# LANGUAGE CPP #-}
    {- |
    Module      : What4.Protocol.Online
    Description : Online solver interactions
    Copyright   : (c) Galois, Inc 2018-2020
    License     : BSD3
    Maintainer  : Rob Dockins <rdockins@galois.com>

    This module defines an API for interacting with
    solvers that support online interaction modes.

    -}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE LambdaCase #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE TypeApplications #-}
    module What4.Protocol.Online
      ( OnlineSolver(..)
      , AnOnlineSolver(..)
      , SolverProcess(..)
      , solverStdin
      , solverResponse
      , SolverGoalTimeout(..)
      , getGoalTimeoutInSeconds
      , withLocalGoalTimeout
      , ErrorBehavior(..)
      , killSolver
      , push
      , pop
      , tryPop
      , reset
      , inNewFrame
      , inNewFrameWithVars
      , inNewFrame2Open
      , inNewFrame2Close
      , check
      , checkAndGetModel
      , checkWithAssumptions
      , checkWithAssumptionsAndModel
      , getModel
      , getUnsatCore
      , getAbducts
      , getUnsatAssumptions
      , getSatResult
      , checkSatisfiable
      , checkSatisfiableWithModel
      ) where

    import           Control.Concurrent ( threadDelay )
    import           Control.Concurrent.Async ( race )
    import           Control.Exception ( SomeException(..), catchJust, tryJust, displayException )
    import           Control.Monad ( unless )
    import           Control.Monad (void, forM, forM_)
    import           Control.Monad.Catch ( Exception, MonadMask, bracket_, catchIf
                                         , onException, throwM, fromException  )
    import           Control.Monad.IO.Class ( MonadIO, liftIO )
    import           Data.IORef
    #if MIN_VERSION_base(4,14,0)
    #else
    import qualified Data.List as L
    #endif
    import           Data.Parameterized.Some
    import           Data.Proxy
    import           Data.Text (Text)
    import qualified Data.Text.Lazy as LazyText
    import           Prettyprinter
    import           System.Exit
    import           System.IO
    import qualified System.IO.Error as IOE
    import qualified System.IO.Streams as Streams
    import           System.Process (ProcessHandle, terminateProcess, waitForProcess)

    import           What4.Expr
    import           What4.Interface (SolverEvent(..)
                                     , SolverStartSATQuery(..)
                                     , SolverEndSATQuery(..) )
    import           What4.ProblemFeatures
    import           What4.Protocol.SMTWriter
    import           What4.SatResult
    import           What4.Utils.HandleReader
    import           What4.Utils.Process (filterAsync)

    -- | Simple data-type encapsulating some implementation
    --   of an online solver.
    data AnOnlineSolver = forall s. OnlineSolver s => AnOnlineSolver (Proxy s)

    -- | This class provides an API for starting and shutting down
    --   connections to various different solvers that support
    --   online interaction modes.
    class SMTReadWriter solver => OnlineSolver solver where
      -- | Start a new solver process attached to the given `ExprBuilder`.
      startSolverProcess :: forall scope st fs.
        ProblemFeatures ->
        Maybe Handle ->
        ExprBuilder scope st fs ->
        IO (SolverProcess scope solver)

      -- | Shut down a solver process.  The process will be asked to shut down in
      --   a "polite" way, e.g., by sending an `(exit)` message, or by closing
      --   the process's `stdin`.  Use `killProcess` instead to shutdown a process
      --   via a signal.
      shutdownSolverProcess :: forall scope.
        SolverProcess scope solver ->
        IO (ExitCode, LazyText.Text)

    -- | This datatype describes how a solver will behave following an error.
    data ErrorBehavior
      = ImmediateExit -- ^ This indicates the solver will immediately exit following an error
      | ContinueOnError
         -- ^ This indicates the solver will remain live and respond to further
         --   commmands following an error

    -- | The amount of time that a solver is allowed to attempt to satisfy
    -- any particular goal.
    --
    -- The timeout value may be retrieved with
    -- 'getGoalTimeoutInMilliSeconds' or 'getGoalTimeoutInSeconds'.
    newtype SolverGoalTimeout = SolverGoalTimeout { SolverGoalTimeout -> Integer
    getGoalTimeoutInMilliSeconds :: Integer }

    -- | Get the SolverGoalTimeout raw numeric value in units of seconds.
    getGoalTimeoutInSeconds :: SolverGoalTimeout -> Integer
    getGoalTimeoutInSeconds :: SolverGoalTimeout -> Integer
    getGoalTimeoutInSeconds SolverGoalTimeout
    sgt =
      let msecs :: Integer
    msecs = SolverGoalTimeout -> Integer
    getGoalTimeoutInMilliSeconds SolverGoalTimeout
    sgt
          secs :: Integer
    secs = Integer
    msecs Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `div` Integer
    1000
          -- 0 is a special "no-timeout" value, so if the supplied goal
          -- timeout in milliseconds is less than one second, round up to
          -- a full second.
      in if Integer
    msecs Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > Integer
    0 Bool -> Bool -> Bool
    && Integer
    secs Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    0 then Integer
    1 else Integer
    secs

    instance Pretty SolverGoalTimeout where
      pretty :: forall ann. SolverGoalTimeout -> Doc ann
    pretty (SolverGoalTimeout Integer
    ms) = Integer -> Doc ann
    forall ann. Integer -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty Integer
    ms Doc ann -> Doc ann -> Doc ann
    forall a. Semigroup a => a -> a -> a
    <> String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "msec"

    instance Show SolverGoalTimeout where
      show :: SolverGoalTimeout -> String
    show = Doc Any -> String
    forall a. Show a => a -> String
    show (Doc Any -> String)
    -> (SolverGoalTimeout -> Doc Any) -> SolverGoalTimeout -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SolverGoalTimeout -> Doc Any
    forall a ann. Pretty a => a -> Doc ann
    forall ann. SolverGoalTimeout -> Doc ann
    pretty

    -- | A live connection to a running solver process.
    --
    --   This data structure should be used in a single-threaded
    --   manner or with external synchronization to ensure that
    --   only a single thread has access at a time. Unsynchronized
    --   multithreaded use will lead to race conditions and very
    --   strange results.
    data SolverProcess scope solver = SolverProcess
      { forall scope solver.
    SolverProcess scope solver -> WriterConn scope solver
    solverConn  :: !(WriterConn scope solver)
        -- ^ Writer for sending commands to the solver

      , forall scope solver. SolverProcess scope solver -> IO ExitCode
    solverCleanupCallback :: IO ExitCode
        -- ^ Callback for regular code paths to gracefully close associated pipes
        --   and wait for the process to shutdown

      , forall scope solver. SolverProcess scope solver -> ProcessHandle
    solverHandle :: !ProcessHandle
        -- ^ Handle to the solver process

      , forall scope solver. SolverProcess scope solver -> ErrorBehavior
    solverErrorBehavior :: !ErrorBehavior
        -- ^ Indicate this solver's behavior following an error response

      , forall scope solver. SolverProcess scope solver -> HandleReader
    solverStderr :: !HandleReader
        -- ^ Standard error for the solver process

      , forall scope solver.
    SolverProcess scope solver -> SMTEvalFunctions solver
    solverEvalFuns :: !(SMTEvalFunctions solver)
        -- ^ The functions used to parse values out of models.

      , forall scope solver.
    SolverProcess scope solver -> SolverEvent -> IO ()
    solverLogFn :: SolverEvent -> IO ()

      , forall scope solver. SolverProcess scope solver -> String
    solverName :: String

      , forall scope solver.
    SolverProcess scope solver -> IORef (Maybe Int)
    solverEarlyUnsat :: IORef (Maybe Int)
        -- ^ Some solvers will enter an 'UNSAT' state early, if they can easily
        --   determine that context is unsatisfiable.  If this IORef contains
        --   an integer value, it indicates how many \"pop\" operations need to
        --   be performed to return to a potentially satisfiable state.
        --   A @Just 0@ state indicates the special case that the top-level context
        --   is unsatisfiable, and must be \"reset\".

      , forall scope solver. SolverProcess scope solver -> Bool
    solverSupportsResetAssertions :: Bool
        -- ^ Some solvers do not have support for the SMTLib2.6 operation
        --   (reset-assertions), or an equivalent.
        --   For these solvers, we instead make sure to
        --   always have at least one assertion frame pushed, and pop all
        --   outstanding frames (and push a new top-level one) as a way
        --   to mimic the reset behavior.

      , forall scope solver.
    SolverProcess scope solver -> SolverGoalTimeout
    solverGoalTimeout :: SolverGoalTimeout
        -- ^ The amount of time (in seconds) that a solver should spend
        -- trying to satisfy any particular goal before giving up.  A
        -- value of zero indicates no time limit.
        --
        -- Note that it is not sufficient to set just this value to
        -- control timeouts; this value is used as a reference for common
        -- code (e.g. SMTLIB2) to determine the timeout for the associated
        -- timer.  When initialized, this field of the SolverProcess is
        -- initialized from a solver-specific timeout configuration
        -- (e.g. z3Timeout); the latter is the definitive reference for
        -- the timeout, and solver-specific code will likely use the the
        -- latter rather than this common field.
      }

    -- | Standard input stream for the solver process.
    solverStdin :: (SolverProcess t solver) -> (Streams.OutputStream Text)
    solverStdin :: forall t solver. SolverProcess t solver -> OutputStream Text
    solverStdin = WriterConn t solver -> OutputStream Text
    forall t h. WriterConn t h -> OutputStream Text
    connHandle (WriterConn t solver -> OutputStream Text)
    -> (SolverProcess t solver -> WriterConn t solver)
    -> SolverProcess t solver
    -> OutputStream Text
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SolverProcess t solver -> WriterConn t solver
    forall scope solver.
    SolverProcess scope solver -> WriterConn scope solver
    solverConn

    -- | The solver's stdout, for easier parsing of responses.
    solverResponse :: (SolverProcess t solver) -> (Streams.InputStream Text)
    solverResponse :: forall t solver. SolverProcess t solver -> InputStream Text
    solverResponse = WriterConn t solver -> InputStream Text
    forall t h. WriterConn t h -> InputStream Text
    connInputHandle (WriterConn t solver -> InputStream Text)
    -> (SolverProcess t solver -> WriterConn t solver)
    -> SolverProcess t solver
    -> InputStream Text
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SolverProcess t solver -> WriterConn t solver
    forall scope solver.
    SolverProcess scope solver -> WriterConn scope solver
    solverConn

    -- | An impolite way to shut down a solver.  Prefer to use
    --   `shutdownSolverProcess`, unless the solver is unresponsive
    --   or in some unrecoverable error state.
    killSolver :: SolverProcess t solver -> IO ()
    killSolver :: forall t solver. SolverProcess t solver -> IO ()
    killSolver SolverProcess t solver
    p =
      do (SomeException -> Maybe SomeException)
    -> IO () -> (SomeException -> IO ()) -> IO ()
    forall e b a.
    Exception e =>
    (e -> Maybe b) -> IO a -> (b -> IO a) -> IO a
    catchJust SomeException -> Maybe SomeException
    filterAsync
               (ProcessHandle -> IO ()
    terminateProcess (SolverProcess t solver -> ProcessHandle
    forall scope solver. SolverProcess scope solver -> ProcessHandle
    solverHandle SolverProcess t solver
    p)
                -- some solvers emit stderr messages on SIGTERM
                IO () -> IO Text -> IO Text
    forall a b. IO a -> IO b -> IO b
    forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
    >> HandleReader -> IO Text
    readAllLines (SolverProcess t solver -> HandleReader
    forall scope solver. SolverProcess scope solver -> HandleReader
    solverStderr SolverProcess t solver
    p)
                IO Text -> IO () -> IO ()
    forall a b. IO a -> IO b -> IO b
    forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
    >> () -> IO ()
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return ()
               )
               (\(SomeException
    ex :: SomeException) -> Handle -> String -> IO ()
    hPutStrLn Handle
    stderr (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ SomeException -> String
    forall e. Exception e => e -> String
    displayException SomeException
    ex)
         IO ExitCode -> IO ()
    forall (f :: Type -> Type) a. Functor f => f a -> f ()
    void (IO ExitCode -> IO ()) -> IO ExitCode -> IO ()
    forall a b. (a -> b) -> a -> b
    $ ProcessHandle -> IO ExitCode
    waitForProcess (SolverProcess t solver -> ProcessHandle
    forall scope solver. SolverProcess scope solver -> ProcessHandle
    solverHandle SolverProcess t solver
    p)

    -- | Check if the given formula is satisfiable in the current
    --   solver state, without requesting a model.  This is done in a
    --   fresh frame, which is exited after the check call.
    checkSatisfiable ::
      SMTReadWriter solver =>
      SolverProcess scope solver ->
      String ->
      BoolExpr scope ->
      IO (SatResult () ())
    checkSatisfiable :: forall solver scope.
    SMTReadWriter solver =>
    SolverProcess scope solver
    -> String -> BoolExpr scope -> IO (SatResult () ())
    checkSatisfiable SolverProcess scope solver
    proc String
    rsn BoolExpr scope
    p =
      IORef (Maybe Int) -> IO (Maybe Int)
    forall a. IORef a -> IO a
    readIORef (SolverProcess scope solver -> IORef (Maybe Int)
    forall scope solver.
    SolverProcess scope solver -> IORef (Maybe Int)
    solverEarlyUnsat SolverProcess scope solver
    proc) IO (Maybe Int)
    -> (Maybe Int -> IO (SatResult () ())) -> IO (SatResult () ())
    forall a b. IO a -> (a -> IO b) -> IO b
    forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        Just Int
    _  -> SatResult () () -> IO (SatResult () ())
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (() -> SatResult () ()
    forall mdl core. core -> SatResult mdl core
    Unsat ())
        Maybe Int
    Nothing ->
          let conn :: WriterConn scope solver
    conn = SolverProcess scope solver -> WriterConn scope solver
    forall scope solver.
    SolverProcess scope solver -> WriterConn scope solver
    solverConn SolverProcess scope solver
    proc in
          SolverProcess scope solver
    -> IO (SatResult () ()) -> IO (SatResult () ())
    forall (m :: Type -> Type) solver scope a.
    (MonadIO m, MonadMask m, SMTReadWriter solver) =>
    SolverProcess scope solver -> m a -> m a
    inNewFrame SolverProcess scope solver
    proc (IO (SatResult () ()) -> IO (SatResult () ()))
    -> IO (SatResult () ()) -> IO (SatResult () ())
    forall a b. (a -> b) -> a -> b
    $
            do WriterConn scope solver -> BoolExpr scope -> IO ()
    forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
    assume WriterConn scope solver
    conn BoolExpr scope
    p
               SolverProcess scope solver -> String -> IO (SatResult () ())
    forall solver scope.
    SMTReadWriter solver =>
    SolverProcess scope solver -> String -> IO (SatResult () ())
    check SolverProcess scope solver
    proc String
    rsn

    -- | @get-abuct nm t@ queries the solver for the first abduct, which is returned
    --   as an SMT function definition named @nm@. The remaining abducts are obtained
    --   from the solver by successive invocations of the @get-abduct-next@ command,
    --   which return SMT functions bound to the same @nm@ as the first. The name @nm@
    --   is bound within the current assertion frame.
    --   Note that this is an unstable API; we expect that the return type will change
    --   to a parsed expression in the future
    getAbducts ::
      SMTReadWriter solver =>
      SolverProcess scope solver ->
      Int ->
      Text ->
      BoolExpr scope ->
      IO [String]
    getAbducts :: forall solver scope.
    SMTReadWriter solver =>
    SolverProcess scope solver
    -> Int -> Text -> BoolExpr scope -> IO [String]
    getAbducts SolverProcess scope solver
    proc Int
    n Text
    nm BoolExpr scope
    t =
      if (Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    0) then do
        let conn :: WriterConn scope solver
    conn = SolverProcess scope solver -> WriterConn scope solver
    forall scope solver.
    SolverProcess scope solver -> WriterConn scope solver
    solverConn SolverProcess scope solver
    proc
        Bool -> IO () -> IO ()
    forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
    unless (WriterConn scope solver -> ProblemFeatures
    forall t h. WriterConn t h -> ProblemFeatures
    supportedFeatures WriterConn scope solver
    conn ProblemFeatures -> ProblemFeatures -> Bool
    `hasProblemFeature` ProblemFeatures
    useProduceAbducts) (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $
          String -> IO ()
    forall a. String -> IO a
    forall (m :: Type -> Type) a. MonadFail m => String -> m a
    fail (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ Doc Any -> String
    forall a. Show a => a -> String
    show (Doc Any -> String) -> Doc Any -> String
    forall a b. (a -> b) -> a -> b
    $ String -> Doc Any
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty (WriterConn scope solver -> String
    forall t h. WriterConn t h -> String
    smtWriterName WriterConn scope solver
    conn) Doc Any -> Doc Any -> Doc Any
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> String -> Doc Any
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "is not configured to produce abducts"
        Term solver
    f <- WriterConn scope solver -> BoolExpr scope -> IO (Term solver)
    forall h t.
    SMTWriter h =>
    WriterConn t h -> BoolExpr t -> IO (Term h)
    mkFormula WriterConn scope solver
    conn BoolExpr scope
    t
        -- get the first abduct using the get-abduct command
        WriterConn scope solver -> Command solver -> IO ()
    forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
    addCommandNoAck WriterConn scope solver
    conn (WriterConn scope solver -> Text -> Term solver -> Command solver
    forall h (f :: Type -> Type).
    SMTWriter h =>
    f h -> Text -> Term h -> Command h
    forall (f :: Type -> Type).
    f solver -> Text -> Term solver -> Command solver
    getAbductCommand WriterConn scope solver
    conn Text
    nm Term solver
    f)
        String
    abd1 <- WriterConn scope solver
    -> WriterConn scope solver -> Text -> Term solver -> IO String
    forall h (f :: Type -> Type) t.
    SMTReadWriter h =>
    f h -> WriterConn t h -> Text -> Term h -> IO String
    forall (f :: Type -> Type) t.
    f solver -> WriterConn t solver -> Text -> Term solver -> IO String
    smtAbductResult WriterConn scope solver
    conn WriterConn scope solver
    conn Text
    nm Term solver
    f
        -- get the remaining abducts using get-abduct-next commands
        if (Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    1) then do
          let rest :: Int
    rest = Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1
          [String]
    abdRest <- [Int] -> (Int -> IO String) -> IO [String]
    forall (t :: Type -> Type) (m :: Type -> Type) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [Int
    1..Int
    rest] ((Int -> IO String) -> IO [String])
    -> (Int -> IO String) -> IO [String]
    forall a b. (a -> b) -> a -> b
    $ \Int
    _ -> do
            WriterConn scope solver -> Command solver -> IO ()
    forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
    addCommandNoAck WriterConn scope solver
    conn (WriterConn scope solver -> Command solver
    forall h (f :: Type -> Type). SMTWriter h => f h -> Command h
    forall (f :: Type -> Type). f solver -> Command solver
    getAbductNextCommand WriterConn scope solver
    conn)
            WriterConn scope solver -> WriterConn scope solver -> IO String
    forall h (f :: Type -> Type) t.
    SMTReadWriter h =>
    f h -> WriterConn t h -> IO String
    forall (f :: Type -> Type) t.
    f solver -> WriterConn t solver -> IO String
    smtAbductNextResult WriterConn scope solver
    conn WriterConn scope solver
    conn
          [String] -> IO [String]
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (String
    abd1String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    :[String]
    abdRest)
        else [String] -> IO [String]
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return [String
    abd1]
      else [String] -> IO [String]
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return []

    -- | Check if the formula is satisifiable in the current
    --   solver state.  This is done in a
    --   fresh frame, which is exited after the continuation
    --   complets. The evaluation function can be used to query the model.
    --   The model is valid only in the given continuation.
    checkSatisfiableWithModel ::
      SMTReadWriter solver =>
      SolverProcess scope solver ->
      String ->
      BoolExpr scope ->
      (SatResult (GroundEvalFn scope) () -> IO a) ->
      IO a
    checkSatisfiableWithModel :: forall solver scope a.
    SMTReadWriter solver =>
    SolverProcess scope solver
    -> String
    -> BoolExpr scope
    -> (SatResult (GroundEvalFn scope) () -> IO a)
    -> IO a
    checkSatisfiableWithModel SolverProcess scope solver
    proc String
    rsn BoolExpr scope
    p SatResult (GroundEvalFn scope) () -> IO a
    k =
      IORef (Maybe Int) -> IO (Maybe Int)
    forall a. IORef a -> IO a
    readIORef (SolverProcess scope solver -> IORef (Maybe Int)
    forall scope solver.
    SolverProcess scope solver -> IORef (Maybe Int)
    solverEarlyUnsat SolverProcess scope solver
    proc) IO (Maybe Int) -> (Maybe Int -> IO a) -> IO a
    forall a b. IO a -> (a -> IO b) -> IO b
    forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        Just Int
    _  -> SatResult (GroundEvalFn scope) () -> IO a
    k (() -> SatResult (GroundEvalFn scope) ()
    forall mdl core. core -> SatResult mdl core
    Unsat ())
        Maybe Int
    Nothing ->
          let conn :: WriterConn scope solver
    conn = SolverProcess scope solver -> WriterConn scope solver
    forall scope solver.
    SolverProcess scope solver -> WriterConn scope solver
    solverConn SolverProcess scope solver
    proc in
          SolverProcess scope solver -> IO a -> IO a
    forall (m :: Type -> Type) solver scope a.
    (MonadIO m, MonadMask m, SMTReadWriter solver) =>
    SolverProcess scope solver -> m a -> m a
    inNewFrame SolverProcess scope solver
    proc (IO a -> IO a) -> IO a -> IO a
    forall a b. (a -> b) -> a -> b
    $
            do WriterConn scope solver -> BoolExpr scope -> IO ()
    forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
    assume WriterConn scope solver
    conn BoolExpr scope
    p
               SolverProcess scope solver
    -> String -> IO (SatResult (GroundEvalFn scope) ())
    forall solver scope.
    SMTReadWriter solver =>
    SolverProcess scope solver
    -> String -> IO (SatResult (GroundEvalFn scope) ())
    checkAndGetModel SolverProcess scope solver
    proc String
    rsn IO (SatResult (GroundEvalFn scope) ())
    -> (SatResult (GroundEvalFn scope) () -> IO a) -> IO a
    forall a b. IO a -> (a -> IO b) -> IO b
    forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
    >>= SatResult (GroundEvalFn scope) () -> IO a
    k

    --------------------------------------------------------------------------------
    -- Basic solver interaction.

    -- | Pop all assumption frames and remove all top-level
    --   asserts from the global scope.  Forget all declarations
    --   except those in scope at the top level.
    reset :: SMTReadWriter solver => SolverProcess scope solver -> IO ()
    reset :: forall solver scope.
    SMTReadWriter solver =>
    SolverProcess scope solver -> IO ()
    reset SolverProcess scope solver
    p =
      do let c :: WriterConn scope solver
    c = SolverProcess scope solver -> WriterConn scope solver
    forall scope solver.
    SolverProcess scope solver -> WriterConn scope solver
    solverConn SolverProcess scope solver
    p
         Int
    n <- WriterConn scope solver -> IO Int
    forall t h. WriterConn t h -> IO Int
    popEntryStackToTop WriterConn scope solver
    c
         IORef (Maybe Int) -> Maybe Int -> IO ()
    forall a. IORef a -> a -> IO ()
    writeIORef (SolverProcess scope solver -> IORef (Maybe Int)
    forall scope solver.
    SolverProcess scope solver -> IORef (Maybe Int)
    solverEarlyUnsat SolverProcess scope solver
    p) Maybe Int
    forall a. Maybe a
    Nothing
         if SolverProcess scope solver -> Bool
    forall scope solver. SolverProcess scope solver -> Bool
    solverSupportsResetAssertions SolverProcess scope solver
    p then
           WriterConn scope solver -> Command solver -> IO ()
    forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
    addCommand WriterConn scope solver
    c (WriterConn scope solver -> Command solver
    forall h (f :: Type -> Type). SMTWriter h => f h -> Command h
    forall (f :: Type -> Type). f solver -> Command solver
    resetCommand WriterConn scope solver
    c)
         else
           do (Command solver -> IO ()) -> [Command solver] -> IO ()
    forall (t :: Type -> Type) (m :: Type -> Type) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (WriterConn scope solver -> Command solver -> IO ()
    forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
    addCommand WriterConn scope solver
    c) (WriterConn scope solver -> Int -> [Command solver]
    forall h (f :: Type -> Type).
    SMTWriter h =>
    f h -> Int -> [Command h]
    forall (f :: Type -> Type). f solver -> Int -> [Command solver]
    popManyCommands WriterConn scope solver
    c Int
    n)
              WriterConn scope solver -> Command solver -> IO ()
    forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
    addCommand WriterConn scope solver
    c (WriterConn scope solver -> Command solver
    forall h (f :: Type -> Type). SMTWriter h => f h -> Command h
    forall (f :: Type -> Type). f solver -> Command solver
    pushCommand WriterConn scope solver
    c)

    -- | Push a new solver assumption frame.
    push :: SMTReadWriter solver => SolverProcess scope solver -> IO ()
    push :: forall solver scope.
    SMTReadWriter solver =>
    SolverProcess scope solver -> IO ()
    push SolverProcess scope solver
    p =
      IORef (Maybe Int) -> IO (Maybe Int)
    forall a. IORef a -> IO a
    readIORef (SolverProcess scope solver -> IORef (Maybe Int)
    forall scope solver.
    SolverProcess scope solver -> IORef (Maybe Int)
    solverEarlyUnsat SolverProcess scope solver
    p) IO (Maybe Int) -> (Maybe Int -> IO ()) -> IO ()
    forall a b. IO a -> (a -> IO b) -> IO b
    forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        Maybe Int
    Nothing -> do let c :: WriterConn scope solver
    c = SolverProcess scope solver -> WriterConn scope solver
    forall scope solver.
    SolverProcess scope solver -> WriterConn scope solver
    solverConn SolverProcess scope solver
    p
                      WriterConn scope solver -> IO ()
    forall t h. WriterConn t h -> IO ()
    pushEntryStack WriterConn scope solver
    c
                      WriterConn scope solver -> Command solver -> IO ()
    forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
    addCommand WriterConn scope solver
    c (WriterConn scope solver -> Command solver
    forall h (f :: Type -> Type). SMTWriter h => f h -> Command h
    forall (f :: Type -> Type). f solver -> Command solver
    pushCommand WriterConn scope solver
    c)
        Just Int
    i  -> IORef (Maybe Int) -> Maybe Int -> IO ()
    forall a. IORef a -> a -> IO ()
    writeIORef (SolverProcess scope solver -> IORef (Maybe Int)
    forall scope solver.
    SolverProcess scope solver -> IORef (Maybe Int)
    solverEarlyUnsat SolverProcess scope solver
    p) (Maybe Int -> IO ()) -> Maybe Int -> IO ()
    forall a b. (a -> b) -> a -> b
    $! (Int -> Maybe Int
    forall a. a -> Maybe a
    Just (Int -> Maybe Int) -> Int -> Maybe Int
    forall a b. (a -> b) -> a -> b
    $! Int
    iInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1)

    -- | Pop a previous solver assumption frame.
    pop :: SMTReadWriter solver => SolverProcess scope solver -> IO ()
    pop :: forall solver scope.
    SMTReadWriter solver =>
    SolverProcess scope solver -> IO ()
    pop SolverProcess scope solver
    p =
      IORef (Maybe Int) -> IO (Maybe Int)
    forall a. IORef a -> IO a
    readIORef (SolverProcess scope solver -> IORef (Maybe Int)
    forall scope solver.
    SolverProcess scope solver -> IORef (Maybe Int)
    solverEarlyUnsat SolverProcess scope solver
    p) IO (Maybe Int) -> (Maybe Int -> IO ()) -> IO ()
    forall a b. IO a -> (a -> IO b) -> IO b
    forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        Maybe Int
    Nothing -> do let c :: WriterConn scope solver
    c = SolverProcess scope solver -> WriterConn scope solver
    forall scope solver.
    SolverProcess scope solver -> WriterConn scope solver
    solverConn SolverProcess scope solver
    p
                      WriterConn scope solver -> IO ()
    forall t h. WriterConn t h -> IO ()
    popEntryStack WriterConn scope solver
    c
                      WriterConn scope solver -> Command solver -> IO ()
    forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
    addCommand WriterConn scope solver
    c (WriterConn scope solver -> Command solver
    forall h (f :: Type -> Type). SMTWriter h => f h -> Command h
    forall (f :: Type -> Type). f solver -> Command solver
    popCommand WriterConn scope solver
    c)
        Just Int
    i
          | Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int
    1 -> do let c :: WriterConn scope solver
    c = SolverProcess scope solver -> WriterConn scope solver
    forall scope solver.
    SolverProcess scope solver -> WriterConn scope solver
    solverConn SolverProcess scope solver
    p
                         WriterConn scope solver -> IO ()
    forall t h. WriterConn t h -> IO ()
    popEntryStack WriterConn scope solver
    c
                         IORef (Maybe Int) -> Maybe Int -> IO ()
    forall a. IORef a -> a -> IO ()
    writeIORef (SolverProcess scope solver -> IORef (Maybe Int)
    forall scope solver.
    SolverProcess scope solver -> IORef (Maybe Int)
    solverEarlyUnsat SolverProcess scope solver
    p) Maybe Int
    forall a. Maybe a
    Nothing
                         WriterConn scope solver -> Command solver -> IO ()
    forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
    addCommand WriterConn scope solver
    c (WriterConn scope solver -> Command solver
    forall h (f :: Type -> Type). SMTWriter h => f h -> Command h
    forall (f :: Type -> Type). f solver -> Command solver
    popCommand WriterConn scope solver
    c)
          | Bool
    otherwise -> IORef (Maybe Int) -> Maybe Int -> IO ()
    forall a. IORef a -> a -> IO ()
    writeIORef (SolverProcess scope solver -> IORef (Maybe Int)
    forall scope solver.
    SolverProcess scope solver -> IORef (Maybe Int)
    solverEarlyUnsat SolverProcess scope solver
    p) (Maybe Int -> IO ()) -> Maybe Int -> IO ()
    forall a b. (a -> b) -> a -> b
    $! (Int -> Maybe Int
    forall a. a -> Maybe a
    Just (Int -> Maybe Int) -> Int -> Maybe Int
    forall a b. (a -> b) -> a -> b
    $! Int
    iInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1)

    -- | Pop a previous solver assumption frame, but allow this to fail if
    -- the solver has exited.
    tryPop :: SMTReadWriter solver => SolverProcess scope solver -> IO ()
    tryPop :: forall solver scope.
    SMTReadWriter solver =>
    SolverProcess scope solver -> IO ()
    tryPop SolverProcess scope solver
    p =
      let trycmd :: WriterConn t h -> IO ()
    trycmd WriterConn t h
    conn = (IOError -> Bool) -> IO () -> (IOError -> IO ()) -> IO ()
    forall (m :: Type -> Type) e a.
    (HasCallStack, MonadCatch m, Exception e) =>
    (e -> Bool) -> m a -> (e -> m a) -> m a
    catchIf IOError -> Bool
    solverGone
                        (WriterConn t h -> Command h -> IO ()
    forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
    addCommand WriterConn t h
    conn (WriterConn t h -> Command h
    forall h (f :: Type -> Type). SMTWriter h => f h -> Command h
    forall (f :: Type -> Type). f h -> Command h
    popCommand WriterConn t h
    conn))
                        (IO () -> IOError -> IO ()
    forall a b. a -> b -> a
    const (IO () -> IOError -> IO ()) -> IO () -> IOError -> IO ()
    forall a b. (a -> b) -> a -> b
    $ RunawaySolverTimeout -> IO ()
    forall e a. (HasCallStack, Exception e) => e -> IO a
    forall (m :: Type -> Type) e a.
    (MonadThrow m, HasCallStack, Exception e) =>
    e -> m a
    throwM RunawaySolverTimeout
    RunawaySolverTimeout)
    #if MIN_VERSION_base(4,14,0)
          solverGone :: IOError -> Bool
    solverGone = IOError -> Bool
    IOE.isResourceVanishedError
    #else
          solverGone = L.isInfixOf "resource vanished" . IOE.ioeGetErrorString
    #endif
      in IORef (Maybe Int) -> IO (Maybe Int)
    forall a. IORef a -> IO a
    readIORef (SolverProcess scope solver -> IORef (Maybe Int)
    forall scope solver.
    SolverProcess scope solver -> IORef (Maybe Int)
    solverEarlyUnsat SolverProcess scope solver
    p) IO (Maybe Int) -> (Maybe Int -> IO ()) -> IO ()
    forall a b. IO a -> (a -> IO b) -> IO b
    forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        Maybe Int
    Nothing -> do let c :: WriterConn scope solver
    c = SolverProcess scope solver -> WriterConn scope solver
    forall scope solver.
    SolverProcess scope solver -> WriterConn scope solver
    solverConn SolverProcess scope solver
    p
                      WriterConn scope solver -> IO ()
    forall t h. WriterConn t h -> IO ()
    popEntryStack WriterConn scope solver
    c
                      WriterConn scope solver -> IO ()
    forall {h} {t}. SMTWriter h => WriterConn t h -> IO ()
    trycmd WriterConn scope solver
    c
        Just Int
    i
          | Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int
    1 -> do let c :: WriterConn scope solver
    c = SolverProcess scope solver -> WriterConn scope solver
    forall scope solver.
    SolverProcess scope solver -> WriterConn scope solver
    solverConn SolverProcess scope solver
    p
                         WriterConn scope solver -> IO ()
    forall t h. WriterConn t h -> IO ()
    popEntryStack WriterConn scope solver
    c
                         IORef (Maybe Int) -> Maybe Int -> IO ()
    forall a. IORef a -> a -> IO ()
    writeIORef (SolverProcess scope solver -> IORef (Maybe Int)
    forall scope solver.
    SolverProcess scope solver -> IORef (Maybe Int)
    solverEarlyUnsat SolverProcess scope solver
    p) Maybe Int
    forall a. Maybe a
    Nothing
                         WriterConn scope solver -> IO ()
    forall {h} {t}. SMTWriter h => WriterConn t h -> IO ()
    trycmd WriterConn scope solver
    c
          | Bool
    otherwise -> IORef (Maybe Int) -> Maybe Int -> IO ()
    forall a. IORef a -> a -> IO ()
    writeIORef (SolverProcess scope solver -> IORef (Maybe Int)
    forall scope solver.
    SolverProcess scope solver -> IORef (Maybe Int)
    solverEarlyUnsat SolverProcess scope solver
    p) (Maybe Int -> IO ()) -> Maybe Int -> IO ()
    forall a b. (a -> b) -> a -> b
    $! (Int -> Maybe Int
    forall a. a -> Maybe a
    Just (Int -> Maybe Int) -> Int -> Maybe Int
    forall a b. (a -> b) -> a -> b
    $! Int
    iInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1)

    -- | Perform an action in the scope of a solver assumption frame.
    inNewFrame :: (MonadIO m, MonadMask m, SMTReadWriter solver) => SolverProcess scope solver -> m a -> m a
    inNewFrame :: forall (m :: Type -> Type) solver scope a.
    (MonadIO m, MonadMask m, SMTReadWriter solver) =>
    SolverProcess scope solver -> m a -> m a
    inNewFrame SolverProcess scope solver
    p m a
    action = SolverProcess scope solver
    -> [Some (ExprBoundVar scope)] -> m a -> m a
    forall (m :: Type -> Type) solver scope a.
    (MonadIO m, MonadMask m, SMTReadWriter solver) =>
    SolverProcess scope solver
    -> [Some (ExprBoundVar scope)] -> m a -> m a
    inNewFrameWithVars SolverProcess scope solver
    p [] m a
    action

    -- | Open a second solver assumption frame.
    -- For abduction, we want the final assertion to be a in a new frame, so that it
    -- can be closed before asking for abducts. The following two commands allow frame 2
    -- to be pushed and popped independently of other commands
    inNewFrame2Open :: SMTReadWriter solver => SolverProcess scope solver -> IO ()
    inNewFrame2Open :: forall solver scope.
    SMTReadWriter solver =>
    SolverProcess scope solver -> IO ()
    inNewFrame2Open SolverProcess scope solver
    sp = let c :: WriterConn scope solver
    c = SolverProcess scope solver -> WriterConn scope solver
    forall scope solver.
    SolverProcess scope solver -> WriterConn scope solver
    solverConn SolverProcess scope solver
    sp in WriterConn scope solver -> Command solver -> IO ()
    forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
    addCommand WriterConn scope solver
    c (WriterConn scope solver -> Command solver
    forall h (f :: Type -> Type). SMTWriter h => f h -> Command h
    forall (f :: Type -> Type). f solver -> Command solver
    push2Command WriterConn scope solver
    c)

    -- | Close a second solver assumption frame.
    inNewFrame2Close :: SMTReadWriter solver => SolverProcess scope solver -> IO ()
    inNewFrame2Close :: forall solver scope.
    SMTReadWriter solver =>
    SolverProcess scope solver -> IO ()
    inNewFrame2Close SolverProcess scope solver
    sp = let c :: WriterConn scope solver
    c = SolverProcess scope solver -> WriterConn scope solver
    forall scope solver.
    SolverProcess scope solver -> WriterConn scope solver
    solverConn SolverProcess scope solver
    sp in WriterConn scope solver -> Command solver -> IO ()
    forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
    addCommand WriterConn scope solver
    c (WriterConn scope solver -> Command solver
    forall h (f :: Type -> Type). SMTWriter h => f h -> Command h
    forall (f :: Type -> Type). f solver -> Command solver
    pop2Command WriterConn scope solver
    c)

    -- | Perform an action in the scope of a solver assumption frame, where the given
    -- bound variables are considered free within that frame.
    inNewFrameWithVars :: (MonadIO m, MonadMask m, SMTReadWriter solver)
                       => SolverProcess scope solver
                       -> [Some (ExprBoundVar scope)]
                       -> m a
                       -> m a
    inNewFrameWithVars :: forall (m :: Type -> Type) solver scope a.
    (MonadIO m, MonadMask m, SMTReadWriter solver) =>
    SolverProcess scope solver
    -> [Some (ExprBoundVar scope)] -> m a -> m a
    inNewFrameWithVars SolverProcess scope solver
    p [Some (ExprBoundVar scope)]
    vars m a
    action =
      case SolverProcess scope solver -> ErrorBehavior
    forall scope solver. SolverProcess scope solver -> ErrorBehavior
    solverErrorBehavior SolverProcess scope solver
    p of
        ErrorBehavior
    ContinueOnError ->
          m () -> m () -> m a -> m a
    forall (m :: Type -> Type) a c b.
    (HasCallStack, MonadMask m) =>
    m a -> m c -> m b -> m b
    bracket_ (IO () -> m ()
    forall a. IO a -> m a
    forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
    liftIO (IO () -> m ()) -> IO () -> m ()
    forall a b. (a -> b) -> a -> b
    $ IO ()
    pushWithVars)
                   (IO () -> m ()
    forall a. IO a -> m a
    forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
    liftIO (IO () -> m ()) -> IO () -> m ()
    forall a b. (a -> b) -> a -> b
    $ SolverProcess scope solver -> IO ()
    forall solver scope.
    SMTReadWriter solver =>
    SolverProcess scope solver -> IO ()
    tryPop SolverProcess scope solver
    p)
                   m a
    action
        ErrorBehavior
    ImmediateExit ->
          do IO () -> m ()
    forall a. IO a -> m a
    forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
    liftIO (IO () -> m ()) -> IO () -> m ()
    forall a b. (a -> b) -> a -> b
    $ IO ()
    pushWithVars
             m a -> m () -> m a
    forall (m :: Type -> Type) a b.
    (HasCallStack, MonadCatch m) =>
    m a -> m b -> m a
    onException (do a
    x <- m a
    action
                             IO () -> m ()
    forall a. IO a -> m a
    forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
    liftIO (IO () -> m ()) -> IO () -> m ()
    forall a b. (a -> b) -> a -> b
    $ SolverProcess scope solver -> IO ()
    forall solver scope.
    SMTReadWriter solver =>
    SolverProcess scope solver -> IO ()
    pop SolverProcess scope solver
    p
                             a -> m a
    forall a. a -> m a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return a
    x
                         )
               (IO () -> m ()
    forall a. IO a -> m a
    forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
    liftIO (IO () -> m ()) -> IO () -> m ()
    forall a b. (a -> b) -> a -> b
    $ SolverProcess scope solver -> IO ()
    forall solver scope.
    SMTReadWriter solver =>
    SolverProcess scope solver -> IO ()
    tryPop SolverProcess scope solver
    p)
      where
        conn :: WriterConn scope solver
    conn = SolverProcess scope solver -> WriterConn scope solver
    forall scope solver.
    SolverProcess scope solver -> WriterConn scope solver
    solverConn SolverProcess scope solver
    p
        pushWithVars :: IO ()
    pushWithVars = do
          SolverProcess scope solver -> IO ()
    forall solver scope.
    SMTReadWriter solver =>
    SolverProcess scope solver -> IO ()
    push SolverProcess scope solver
    p
          [Some (ExprBoundVar scope)]
    -> (Some (ExprBoundVar scope) -> IO ()) -> IO ()
    forall (t :: Type -> Type) (m :: Type -> Type) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [Some (ExprBoundVar scope)]
    vars (\(Some ExprBoundVar scope x
    bv) -> WriterConn scope solver -> ExprBoundVar scope x -> IO ()
    forall h t (tp :: BaseType).
    SMTWriter h =>
    WriterConn t h -> ExprBoundVar t tp -> IO ()
    bindVarAsFree WriterConn scope solver
    conn ExprBoundVar scope x
    bv)

    checkWithAssumptions ::
      SMTReadWriter solver =>
      SolverProcess scope solver ->
      String ->
      [BoolExpr scope] ->
      IO ([Text], SatResult () ())
    checkWithAssumptions :: forall solver scope.
    SMTReadWriter solver =>
    SolverProcess scope solver
    -> String -> [BoolExpr scope] -> IO ([Text], SatResult () ())
    checkWithAssumptions SolverProcess scope solver
    proc String
    rsn [BoolExpr scope]
    ps =
      do let conn :: WriterConn scope solver
    conn = SolverProcess scope solver -> WriterConn scope solver
    forall scope solver.
    SolverProcess scope solver -> WriterConn scope solver
    solverConn SolverProcess scope solver
    proc
         IORef (Maybe Int) -> IO (Maybe Int)
    forall a. IORef a -> IO a
    readIORef (SolverProcess scope solver -> IORef (Maybe Int)
    forall scope solver.
    SolverProcess scope solver -> IORef (Maybe Int)
    solverEarlyUnsat SolverProcess scope solver
    proc) IO (Maybe Int)
    -> (Maybe Int -> IO ([Text], SatResult () ()))
    -> IO ([Text], SatResult () ())
    forall a b. IO a -> (a -> IO b) -> IO b
    forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
           Just Int
    _  -> ([Text], SatResult () ()) -> IO ([Text], SatResult () ())
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return ([], () -> SatResult () ()
    forall mdl core. core -> SatResult mdl core
    Unsat ())
           Maybe Int
    Nothing ->
             do [Term solver]
    tms <- [BoolExpr scope]
    -> (BoolExpr scope -> IO (Term solver)) -> IO [Term solver]
    forall (t :: Type -> Type) (m :: Type -> Type) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [BoolExpr scope]
    ps (WriterConn scope solver -> BoolExpr scope -> IO (Term solver)
    forall h t.
    SMTWriter h =>
    WriterConn t h -> BoolExpr t -> IO (Term h)
    mkFormula WriterConn scope solver
    conn)
                [Text]
    nms <- [Term solver] -> (Term solver -> IO Text) -> IO [Text]
    forall (t :: Type -> Type) (m :: Type -> Type) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [Term solver]
    tms (WriterConn scope solver
    -> DefineStyle
    -> [(Text, Some TypeMap)]
    -> TypeMap 'BaseBoolType
    -> Term solver
    -> IO Text
    forall h t (rtp :: BaseType).
    SMTWriter h =>
    WriterConn t h
    -> DefineStyle
    -> [(Text, Some TypeMap)]
    -> TypeMap rtp
    -> Term h
    -> IO Text
    freshBoundVarName WriterConn scope solver
    conn DefineStyle
    EqualityDefinition [] TypeMap 'BaseBoolType
    BoolTypeMap)
                SolverProcess scope solver -> SolverEvent -> IO ()
    forall scope solver.
    SolverProcess scope solver -> SolverEvent -> IO ()
    solverLogFn SolverProcess scope solver
    proc
                  (SolverStartSATQuery -> SolverEvent
    SolverStartSATQuery (SolverStartSATQuery -> SolverEvent)
    -> SolverStartSATQuery -> SolverEvent
    forall a b. (a -> b) -> a -> b
    $ SolverStartSATQueryRec
                  { satQuerySolverName :: String
    satQuerySolverName = SolverProcess scope solver -> String
    forall scope solver. SolverProcess scope solver -> String
    solverName SolverProcess scope solver
    proc
                  , satQueryReason :: String
    satQueryReason = String
    rsn
                  })
                WriterConn scope solver -> [Command solver] -> IO ()
    forall h t. SMTWriter h => WriterConn t h -> [Command h] -> IO ()
    addCommands WriterConn scope solver
    conn (WriterConn scope solver -> [Text] -> [Command solver]
    forall h (f :: Type -> Type).
    SMTWriter h =>
    f h -> [Text] -> [Command h]
    forall (f :: Type -> Type). f solver -> [Text] -> [Command solver]
    checkWithAssumptionsCommands WriterConn scope solver
    conn [Text]
    nms)
                SatResult () ()
    sat_result <- SolverProcess scope solver -> IO (SatResult () ())
    forall s t.
    SMTReadWriter s =>
    SolverProcess t s -> IO (SatResult () ())
    getSatResult SolverProcess scope solver
    proc
                SolverProcess scope solver -> SolverEvent -> IO ()
    forall scope solver.
    SolverProcess scope solver -> SolverEvent -> IO ()
    solverLogFn SolverProcess scope solver
    proc
                  (SolverEndSATQuery -> SolverEvent
    SolverEndSATQuery (SolverEndSATQuery -> SolverEvent)
    -> SolverEndSATQuery -> SolverEvent
    forall a b. (a -> b) -> a -> b
    $ SolverEndSATQueryRec
                  { satQueryResult :: SatResult () ()
    satQueryResult = SatResult () ()
    sat_result
                  , satQueryError :: Maybe String
    satQueryError = Maybe String
    forall a. Maybe a
    Nothing
                  })
                ([Text], SatResult () ()) -> IO ([Text], SatResult () ())
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return ([Text]
    nms, SatResult () ()
    sat_result)

    checkWithAssumptionsAndModel ::
      SMTReadWriter solver =>
      SolverProcess scope solver ->
      String ->
      [BoolExpr scope] ->
      IO (SatResult (GroundEvalFn scope) ())
    checkWithAssumptionsAndModel :: forall solver scope.
    SMTReadWriter solver =>
    SolverProcess scope solver
    -> String
    -> [BoolExpr scope]
    -> IO (SatResult (GroundEvalFn scope) ())
    checkWithAssumptionsAndModel SolverProcess scope solver
    proc String
    rsn [BoolExpr scope]
    ps =
      do ([Text]
    _nms, SatResult () ()
    sat_result) <- SolverProcess scope solver
    -> String -> [BoolExpr scope] -> IO ([Text], SatResult () ())
    forall solver scope.
    SMTReadWriter solver =>
    SolverProcess scope solver
    -> String -> [BoolExpr scope] -> IO ([Text], SatResult () ())
    checkWithAssumptions SolverProcess scope solver
    proc String
    rsn [BoolExpr scope]
    ps
         case SatResult () ()
    sat_result of
           SatResult () ()
    Unknown -> SatResult (GroundEvalFn scope) ()
    -> IO (SatResult (GroundEvalFn scope) ())
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return SatResult (GroundEvalFn scope) ()
    forall mdl core. SatResult mdl core
    Unknown
           Unsat ()
    x -> SatResult (GroundEvalFn scope) ()
    -> IO (SatResult (GroundEvalFn scope) ())
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (() -> SatResult (GroundEvalFn scope) ()
    forall mdl core. core -> SatResult mdl core
    Unsat ()
    x)
           Sat{} -> GroundEvalFn scope -> SatResult (GroundEvalFn scope) ()
    forall mdl core. mdl -> SatResult mdl core
    Sat (GroundEvalFn scope -> SatResult (GroundEvalFn scope) ())
    -> IO (GroundEvalFn scope)
    -> IO (SatResult (GroundEvalFn scope) ())
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> SolverProcess scope solver -> IO (GroundEvalFn scope)
    forall solver scope.
    SMTReadWriter solver =>
    SolverProcess scope solver -> IO (GroundEvalFn scope)
    getModel SolverProcess scope solver
    proc

    -- | Send a check command to the solver, and get the SatResult without asking
    --   a model.
    check :: SMTReadWriter solver => SolverProcess scope solver -> String -> IO (SatResult () ())
    check :: forall solver scope.
    SMTReadWriter solver =>
    SolverProcess scope solver -> String -> IO (SatResult () ())
    check SolverProcess scope solver
    p String
    rsn =
      IORef (Maybe Int) -> IO (Maybe Int)
    forall a. IORef a -> IO a
    readIORef (SolverProcess scope solver -> IORef (Maybe Int)
    forall scope solver.
    SolverProcess scope solver -> IORef (Maybe Int)
    solverEarlyUnsat SolverProcess scope solver
    p) IO (Maybe Int)
    -> (Maybe Int -> IO (SatResult () ())) -> IO (SatResult () ())
    forall a b. IO a -> (a -> IO b) -> IO b
    forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        Just Int
    _  -> SatResult () () -> IO (SatResult () ())
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (() -> SatResult () ()
    forall mdl core. core -> SatResult mdl core
    Unsat ())
        Maybe Int
    Nothing ->
          do let c :: WriterConn scope solver
    c = SolverProcess scope solver -> WriterConn scope solver
    forall scope solver.
    SolverProcess scope solver -> WriterConn scope solver
    solverConn SolverProcess scope solver
    p
             SolverProcess scope solver -> SolverEvent -> IO ()
    forall scope solver.
    SolverProcess scope solver -> SolverEvent -> IO ()
    solverLogFn SolverProcess scope solver
    p
               (SolverStartSATQuery -> SolverEvent
    SolverStartSATQuery (SolverStartSATQuery -> SolverEvent)
    -> SolverStartSATQuery -> SolverEvent
    forall a b. (a -> b) -> a -> b
    $ SolverStartSATQueryRec
               { satQuerySolverName :: String
    satQuerySolverName = SolverProcess scope solver -> String
    forall scope solver. SolverProcess scope solver -> String
    solverName SolverProcess scope solver
    p
               , satQueryReason :: String
    satQueryReason = String
    rsn
               })
             WriterConn scope solver -> [Command solver] -> IO ()
    forall h t. SMTWriter h => WriterConn t h -> [Command h] -> IO ()
    addCommands WriterConn scope solver
    c (WriterConn scope solver -> [Command solver]
    forall h (f :: Type -> Type). SMTWriter h => f h -> [Command h]
    forall (f :: Type -> Type). f solver -> [Command solver]
    checkCommands WriterConn scope solver
    c)
             SatResult () ()
    sat_result <- SolverProcess scope solver -> IO (SatResult () ())
    forall s t.
    SMTReadWriter s =>
    SolverProcess t s -> IO (SatResult () ())
    getSatResult SolverProcess scope solver
    p
             SolverProcess scope solver -> SolverEvent -> IO ()
    forall scope solver.
    SolverProcess scope solver -> SolverEvent -> IO ()
    solverLogFn SolverProcess scope solver
    p
               (SolverEndSATQuery -> SolverEvent
    SolverEndSATQuery (SolverEndSATQuery -> SolverEvent)
    -> SolverEndSATQuery -> SolverEvent
    forall a b. (a -> b) -> a -> b
    $ SolverEndSATQueryRec
               { satQueryResult :: SatResult () ()
    satQueryResult = SatResult () ()
    sat_result
               , satQueryError :: Maybe String
    satQueryError = Maybe String
    forall a. Maybe a
    Nothing
               })
             SatResult () () -> IO (SatResult () ())
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return SatResult () ()
    sat_result

    -- | Send a check command to the solver and get the model in the case of a SAT result.
    checkAndGetModel :: SMTReadWriter solver => SolverProcess scope solver -> String -> IO (SatResult (GroundEvalFn scope) ())
    checkAndGetModel :: forall solver scope.
    SMTReadWriter solver =>
    SolverProcess scope solver
    -> String -> IO (SatResult (GroundEvalFn scope) ())
    checkAndGetModel SolverProcess scope solver
    yp String
    rsn = do
      SatResult () ()
    sat_result <- SolverProcess scope solver -> String -> IO (SatResult () ())
    forall solver scope.
    SMTReadWriter solver =>
    SolverProcess scope solver -> String -> IO (SatResult () ())
    check SolverProcess scope solver
    yp String
    rsn
      case SatResult () ()
    sat_result of
        Unsat ()
    x -> SatResult (GroundEvalFn scope) ()
    -> IO (SatResult (GroundEvalFn scope) ())
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (SatResult (GroundEvalFn scope) ()
     -> IO (SatResult (GroundEvalFn scope) ()))
    -> SatResult (GroundEvalFn scope) ()
    -> IO (SatResult (GroundEvalFn scope) ())
    forall a b. (a -> b) -> a -> b
    $! () -> SatResult (GroundEvalFn scope) ()
    forall mdl core. core -> SatResult mdl core
    Unsat ()
    x
        SatResult () ()
    Unknown -> SatResult (GroundEvalFn scope) ()
    -> IO (SatResult (GroundEvalFn scope) ())
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return SatResult (GroundEvalFn scope) ()
    forall mdl core. SatResult mdl core
    Unknown
        Sat () -> GroundEvalFn scope -> SatResult (GroundEvalFn scope) ()
    forall mdl core. mdl -> SatResult mdl core
    Sat (GroundEvalFn scope -> SatResult (GroundEvalFn scope) ())
    -> IO (GroundEvalFn scope)
    -> IO (SatResult (GroundEvalFn scope) ())
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> SolverProcess scope solver -> IO (GroundEvalFn scope)
    forall solver scope.
    SMTReadWriter solver =>
    SolverProcess scope solver -> IO (GroundEvalFn scope)
    getModel SolverProcess scope solver
    yp

    -- | Following a successful check-sat command, build a ground evaluation function
    --   that will evaluate terms in the context of the current model.
    getModel :: SMTReadWriter solver => SolverProcess scope solver -> IO (GroundEvalFn scope)
    getModel :: forall solver scope.
    SMTReadWriter solver =>
    SolverProcess scope solver -> IO (GroundEvalFn scope)
    getModel SolverProcess scope solver
    p = WriterConn scope solver
    -> SMTEvalFunctions solver -> IO (GroundEvalFn scope)
    forall t h.
    SMTWriter h =>
    WriterConn t h -> SMTEvalFunctions h -> IO (GroundEvalFn t)
    smtExprGroundEvalFn (SolverProcess scope solver -> WriterConn scope solver
    forall scope solver.
    SolverProcess scope solver -> WriterConn scope solver
    solverConn SolverProcess scope solver
    p)
                 (SMTEvalFunctions solver -> IO (GroundEvalFn scope))
    -> SMTEvalFunctions solver -> IO (GroundEvalFn scope)
    forall a b. (a -> b) -> a -> b
    $ WriterConn scope solver
    -> InputStream Text -> SMTEvalFunctions solver
    forall h t.
    SMTReadWriter h =>
    WriterConn t h -> InputStream Text -> SMTEvalFunctions h
    forall t.
    WriterConn t solver -> InputStream Text -> SMTEvalFunctions solver
    smtEvalFuns (SolverProcess scope solver -> WriterConn scope solver
    forall scope solver.
    SolverProcess scope solver -> WriterConn scope solver
    solverConn SolverProcess scope solver
    p) (SolverProcess scope solver -> InputStream Text
    forall t solver. SolverProcess t solver -> InputStream Text
    solverResponse SolverProcess scope solver
    p)

    -- | After an unsatisfiable check-with-assumptions command, compute a set of the supplied
    --   assumptions that (together with previous assertions) form an unsatisfiable core.
    --   Note: the returned unsatisfiable set might not be minimal.  The boolean value
    --   returned along with the name indicates if the assumption was negated or not:
    --   @True@ indidcates a positive atom, and @False@ represents a negated atom.
    getUnsatAssumptions :: SMTReadWriter solver => SolverProcess scope solver -> IO [(Bool,Text)]
    getUnsatAssumptions :: forall solver scope.
    SMTReadWriter solver =>
    SolverProcess scope solver -> IO [(Bool, Text)]
    getUnsatAssumptions SolverProcess scope solver
    proc =
      do let conn :: WriterConn scope solver
    conn = SolverProcess scope solver -> WriterConn scope solver
    forall scope solver.
    SolverProcess scope solver -> WriterConn scope solver
    solverConn SolverProcess scope solver
    proc
         Bool -> IO () -> IO ()
    forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
    unless (WriterConn scope solver -> ProblemFeatures
    forall t h. WriterConn t h -> ProblemFeatures
    supportedFeatures WriterConn scope solver
    conn ProblemFeatures -> ProblemFeatures -> Bool
    `hasProblemFeature` ProblemFeatures
    useUnsatAssumptions) (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $
           String -> IO ()
    forall a. String -> IO a
    forall (m :: Type -> Type) a. MonadFail m => String -> m a
    fail (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ Doc Any -> String
    forall a. Show a => a -> String
    show (Doc Any -> String) -> Doc Any -> String
    forall a b. (a -> b) -> a -> b
    $ String -> Doc Any
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty (WriterConn scope solver -> String
    forall t h. WriterConn t h -> String
    smtWriterName WriterConn scope solver
    conn) Doc Any -> Doc Any -> Doc Any
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> String -> Doc Any
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "is not configured to produce UNSAT assumption lists"
         WriterConn scope solver -> Command solver -> IO ()
    forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
    addCommandNoAck WriterConn scope solver
    conn (WriterConn scope solver -> Command solver
    forall h (f :: Type -> Type). SMTWriter h => f h -> Command h
    forall (f :: Type -> Type). f solver -> Command solver
    getUnsatAssumptionsCommand WriterConn scope solver
    conn)
         WriterConn scope solver
    -> WriterConn scope solver -> IO [(Bool, Text)]
    forall h (f :: Type -> Type) t.
    SMTReadWriter h =>
    f h -> WriterConn t h -> IO [(Bool, Text)]
    forall (f :: Type -> Type) t.
    f solver -> WriterConn t solver -> IO [(Bool, Text)]
    smtUnsatAssumptionsResult WriterConn scope solver
    conn WriterConn scope solver
    conn

    -- | After an unsatisfiable check-sat command, compute a set of the named assertions
    --   that (together with all the unnamed assertions) form an unsatisfiable core.
    --   Note: the returned unsatisfiable core might not be minimal.
    getUnsatCore :: SMTReadWriter solver => SolverProcess scope solver -> IO [Text]
    getUnsatCore :: forall solver scope.
    SMTReadWriter solver =>
    SolverProcess scope solver -> IO [Text]
    getUnsatCore SolverProcess scope solver
    proc =
      do let conn :: WriterConn scope solver
    conn = SolverProcess scope solver -> WriterConn scope solver
    forall scope solver.
    SolverProcess scope solver -> WriterConn scope solver
    solverConn SolverProcess scope solver
    proc
         Bool -> IO () -> IO ()
    forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
    unless (WriterConn scope solver -> ProblemFeatures
    forall t h. WriterConn t h -> ProblemFeatures
    supportedFeatures WriterConn scope solver
    conn ProblemFeatures -> ProblemFeatures -> Bool
    `hasProblemFeature` ProblemFeatures
    useUnsatCores) (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $
           String -> IO ()
    forall a. String -> IO a
    forall (m :: Type -> Type) a. MonadFail m => String -> m a
    fail (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ Doc Any -> String
    forall a. Show a => a -> String
    show (Doc Any -> String) -> Doc Any -> String
    forall a b. (a -> b) -> a -> b
    $ String -> Doc Any
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty (WriterConn scope solver -> String
    forall t h. WriterConn t h -> String
    smtWriterName WriterConn scope solver
    conn) Doc Any -> Doc Any -> Doc Any
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> String -> Doc Any
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "is not configured to produce UNSAT cores"
         WriterConn scope solver -> Command solver -> IO ()
    forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
    addCommandNoAck WriterConn scope solver
    conn (WriterConn scope solver -> Command solver
    forall h (f :: Type -> Type). SMTWriter h => f h -> Command h
    forall (f :: Type -> Type). f solver -> Command solver
    getUnsatCoreCommand WriterConn scope solver
    conn)
         WriterConn scope solver -> WriterConn scope solver -> IO [Text]
    forall h (f :: Type -> Type) t.
    SMTReadWriter h =>
    f h -> WriterConn t h -> IO [Text]
    forall (f :: Type -> Type) t.
    f solver -> WriterConn t solver -> IO [Text]
    smtUnsatCoreResult WriterConn scope solver
    conn WriterConn scope solver
    conn

    -- | Get the sat result from a previous SAT command.
    getSatResult :: SMTReadWriter s => SolverProcess t s -> IO (SatResult () ())
    getSatResult :: forall s t.
    SMTReadWriter s =>
    SolverProcess t s -> IO (SatResult () ())
    getSatResult SolverProcess t s
    yp = do
      let ph :: ProcessHandle
    ph = SolverProcess t s -> ProcessHandle
    forall scope solver. SolverProcess scope solver -> ProcessHandle
    solverHandle SolverProcess t s
    yp
      let action :: WriterConn t s -> IO (SatResult () ())
    action = SolverProcess t s -> WriterConn t s -> IO (SatResult () ())
    forall h (f :: Type -> Type) t.
    SMTReadWriter h =>
    f h -> WriterConn t h -> IO (SatResult () ())
    forall (f :: Type -> Type) t.
    f s -> WriterConn t s -> IO (SatResult () ())
    smtSatResult SolverProcess t s
    yp
      Either SomeException (SatResult () ())
    sat_result <- SolverProcess t s
    -> (WriterConn t s -> IO (SatResult () ()))
    -> IO (Either SomeException (SatResult () ()))
    forall t s.
    SolverProcess t s
    -> (WriterConn t s -> IO (SatResult () ()))
    -> IO (Either SomeException (SatResult () ()))
    withLocalGoalTimeout SolverProcess t s
    yp WriterConn t s -> IO (SatResult () ())
    action

      case Either SomeException (SatResult () ())
    sat_result of
        Right SatResult () ()
    ok -> SatResult () () -> IO (SatResult () ())
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return SatResult () ()
    ok

        Left e :: SomeException
    e@(SomeException e
    _)
          | Just RunawaySolverTimeout
    RunawaySolverTimeout <- SomeException -> Maybe RunawaySolverTimeout
    forall e. Exception e => SomeException -> Maybe e
    fromException SomeException
    e -> do
              -- Deadman timeout fired, so this is effectively Incomplete
              SatResult () () -> IO (SatResult () ())
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return SatResult () ()
    forall mdl core. SatResult mdl core
    Unknown

        Left (SomeException e
    e) ->
           do -- Interrupt process
              ProcessHandle -> IO ()
    terminateProcess ProcessHandle
    ph

              Text
    txt <- HandleReader -> IO Text
    readAllLines (HandleReader -> IO Text) -> HandleReader -> IO Text
    forall a b. (a -> b) -> a -> b
    $ SolverProcess t s -> HandleReader
    forall scope solver. SolverProcess scope solver -> HandleReader
    solverStderr SolverProcess t s
    yp

              -- Wait for process to end
              ExitCode
    ec <- ProcessHandle -> IO ExitCode
    waitForProcess ProcessHandle
    ph
              let ec_code :: Int
    ec_code = case ExitCode
    ec of
                              ExitCode
    ExitSuccess -> Int
    0
                              ExitFailure Int
    code -> Int
    code
              String -> IO (SatResult () ())
    forall a. String -> IO a
    forall (m :: Type -> Type) a. MonadFail m => String -> m a
    fail (String -> IO (SatResult () ())) -> String -> IO (SatResult () ())
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines
                      [ String
    "The solver terminated with exit code "String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++
                                                  Int -> String
    forall a. Show a => a -> String
    show Int
    ec_code String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ".\n"
                      , String
    "*** exception: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ e -> String
    forall e. Exception e => e -> String
    displayException e
    e
                      , String
    "*** standard error:"
                      , Text -> String
    LazyText.unpack Text
    txt
                      ]

    -- | If the solver cannot voluntarily limit itself to the requested
    -- timeout period, this runs a local async process with a slightly
    -- longer time period that will forcibly terminate the solver process
    -- if it expires while the solver process is still running.
    --
    -- Note that this will require re-establishment of the solver process
    -- and any associated context for any subsequent solver goal
    -- evaluation.

    withLocalGoalTimeout ::
      SolverProcess t s
      -> (WriterConn t s -> IO (SatResult () ()))
      -> IO (Either SomeException (SatResult () ()))
    withLocalGoalTimeout :: forall t s.
    SolverProcess t s
    -> (WriterConn t s -> IO (SatResult () ()))
    -> IO (Either SomeException (SatResult () ()))
    withLocalGoalTimeout SolverProcess t s
    solverProc WriterConn t s -> IO (SatResult () ())
    action =
      if SolverGoalTimeout -> Integer
    getGoalTimeoutInSeconds (SolverProcess t s -> SolverGoalTimeout
    forall scope solver.
    SolverProcess scope solver -> SolverGoalTimeout
    solverGoalTimeout SolverProcess t s
    solverProc) Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    0
      then do (SomeException -> Maybe SomeException)
    -> IO (SatResult () ())
    -> IO (Either SomeException (SatResult () ()))
    forall e b a.
    Exception e =>
    (e -> Maybe b) -> IO a -> IO (Either b a)
    tryJust SomeException -> Maybe SomeException
    filterAsync (WriterConn t s -> IO (SatResult () ())
    action (WriterConn t s -> IO (SatResult () ()))
    -> WriterConn t s -> IO (SatResult () ())
    forall a b. (a -> b) -> a -> b
    $ SolverProcess t s -> WriterConn t s
    forall scope solver.
    SolverProcess scope solver -> WriterConn scope solver
    solverConn SolverProcess t s
    solverProc)
      else let deadmanTimeoutPeriodMicroSeconds :: Int
    deadmanTimeoutPeriodMicroSeconds =
                 (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger (Integer -> Int) -> Integer -> Int
    forall a b. (a -> b) -> a -> b
    $
                  SolverGoalTimeout -> Integer
    getGoalTimeoutInMilliSeconds (SolverProcess t s -> SolverGoalTimeout
    forall scope solver.
    SolverProcess scope solver -> SolverGoalTimeout
    solverGoalTimeout SolverProcess t s
    solverProc)
                  Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    500  -- allow solver to honor timeout first
                 ) Int -> Int -> Int
    forall a. Num a => a -> a -> a
    * Int
    1000  -- convert msec to usec
               deadmanTimer :: IO ()
    deadmanTimer = Int -> IO ()
    threadDelay Int
    deadmanTimeoutPeriodMicroSeconds
           in
              do IO () -> IO (SatResult () ()) -> IO (Either () (SatResult () ()))
    forall a b. IO a -> IO b -> IO (Either a b)
    race IO ()
    deadmanTimer (WriterConn t s -> IO (SatResult () ())
    action (WriterConn t s -> IO (SatResult () ()))
    -> WriterConn t s -> IO (SatResult () ())
    forall a b. (a -> b) -> a -> b
    $ SolverProcess t s -> WriterConn t s
    forall scope solver.
    SolverProcess scope solver -> WriterConn scope solver
    solverConn SolverProcess t s
    solverProc) IO (Either () (SatResult () ()))
    -> (Either () (SatResult () ())
        -> IO (Either SomeException (SatResult () ())))
    -> IO (Either SomeException (SatResult () ()))
    forall a b. IO a -> (a -> IO b) -> IO b
    forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
                   Left () -> do SolverProcess t s -> IO ()
    forall t solver. SolverProcess t solver -> IO ()
    killSolver SolverProcess t s
    solverProc
                                 Either SomeException (SatResult () ())
    -> IO (Either SomeException (SatResult () ()))
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (Either SomeException (SatResult () ())
     -> IO (Either SomeException (SatResult () ())))
    -> Either SomeException (SatResult () ())
    -> IO (Either SomeException (SatResult () ()))
    forall a b. (a -> b) -> a -> b
    $ SomeException -> Either SomeException (SatResult () ())
    forall a b. a -> Either a b
    Left (SomeException -> Either SomeException (SatResult () ()))
    -> SomeException -> Either SomeException (SatResult () ())
    forall a b. (a -> b) -> a -> b
    $ RunawaySolverTimeout -> SomeException
    forall e. Exception e => e -> SomeException
    SomeException RunawaySolverTimeout
    RunawaySolverTimeout
                   Right SatResult () ()
    x -> Either SomeException (SatResult () ())
    -> IO (Either SomeException (SatResult () ()))
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (Either SomeException (SatResult () ())
     -> IO (Either SomeException (SatResult () ())))
    -> Either SomeException (SatResult () ())
    -> IO (Either SomeException (SatResult () ()))
    forall a b. (a -> b) -> a -> b
    $ SatResult () () -> Either SomeException (SatResult () ())
    forall a b. b -> Either a b
    Right SatResult () ()
    x

    -- | The RunawaySolverTimeout is thrown when the solver cannot
    -- voluntarily limit itself to the requested solver-timeout period and
    -- has subsequently been forcibly stopped.
    data RunawaySolverTimeout = RunawaySolverTimeout deriving Int -> RunawaySolverTimeout -> ShowS
    [RunawaySolverTimeout] -> ShowS
    RunawaySolverTimeout -> String
    (Int -> RunawaySolverTimeout -> ShowS)
    -> (RunawaySolverTimeout -> String)
    -> ([RunawaySolverTimeout] -> ShowS)
    -> Show RunawaySolverTimeout
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> RunawaySolverTimeout -> ShowS
    showsPrec :: Int -> RunawaySolverTimeout -> ShowS
    $cshow :: RunawaySolverTimeout -> String
    show :: RunawaySolverTimeout -> String
    $cshowList :: [RunawaySolverTimeout] -> ShowS
    showList :: [RunawaySolverTimeout] -> ShowS
    Show
    instance Exception RunawaySolverTimeout