    ------------------------------------------------------------------------
    -- |
    -- Module      : What4.Solver.STP
    -- Description : Solver adapter code for STP
    -- Copyright   : (c) Galois, Inc 2015-2020
    -- License     : BSD3
    -- Maintainer  : Joe Hendrix <rdockins@galois.com>
    -- Stability   : provisional
    --
    -- STP-specific tweaks to the basic SMTLib2 solver interface.
    ------------------------------------------------------------------------
    {-# LANGUAGE FlexibleInstances #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE OverloadedStrings #-}
    module What4.Solver.STP
      ( STP(..)
      , stpAdapter
      , stpPath
      , stpTimeout
      , stpOptions
      , stpFeatures
      , runSTPInOverride
      , withSTP
      ) where

    import           Data.Bits

    import           What4.BaseTypes
    import           What4.Concrete
    import           What4.Config
    import           What4.Expr.Builder
    import           What4.Expr.GroundEval
    import           What4.Interface
    import           What4.ProblemFeatures
    import           What4.Protocol.Online
    import qualified What4.Protocol.SMTLib2 as SMT2
    import           What4.Protocol.SMTLib2.Response ( strictSMTParseOpt )
    import           What4.SatResult
    import           What4.Solver.Adapter
    import           What4.Utils.Process

    data STP = STP deriving Int -> STP -> ShowS
    [STP] -> ShowS
    STP -> String
    (Int -> STP -> ShowS)
    -> (STP -> String) -> ([STP] -> ShowS) -> Show STP
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> STP -> ShowS
    showsPrec :: Int -> STP -> ShowS
    $cshow :: STP -> String
    show :: STP -> String
    $cshowList :: [STP] -> ShowS
    showList :: [STP] -> ShowS
    Show

    -- | Path to stp
    stpPath :: ConfigOption (BaseStringType Unicode)
    stpPath :: ConfigOption (BaseStringType Unicode)
    stpPath = BaseTypeRepr (BaseStringType Unicode)
    -> String -> ConfigOption (BaseStringType Unicode)
    forall (tp :: BaseType).
    BaseTypeRepr tp -> String -> ConfigOption tp
    configOption BaseTypeRepr (BaseStringType Unicode)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr String
    "solver.stp.path"

    stpPathOLD :: ConfigOption (BaseStringType Unicode)
    stpPathOLD :: ConfigOption (BaseStringType Unicode)
    stpPathOLD = BaseTypeRepr (BaseStringType Unicode)
    -> String -> ConfigOption (BaseStringType Unicode)
    forall (tp :: BaseType).
    BaseTypeRepr tp -> String -> ConfigOption tp
    configOption BaseTypeRepr (BaseStringType Unicode)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr String
    "stp_path"

    -- | Per-check timeout, in milliseconds (zero is none)
    stpTimeout :: ConfigOption BaseIntegerType
    stpTimeout :: ConfigOption BaseIntegerType
    stpTimeout = BaseTypeRepr BaseIntegerType
    -> String -> ConfigOption BaseIntegerType
    forall (tp :: BaseType).
    BaseTypeRepr tp -> String -> ConfigOption tp
    configOption BaseTypeRepr BaseIntegerType
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr String
    "solver.stp.timeout"

    stpRandomSeed :: ConfigOption BaseIntegerType
    stpRandomSeed :: ConfigOption BaseIntegerType
    stpRandomSeed = BaseTypeRepr BaseIntegerType
    -> String -> ConfigOption BaseIntegerType
    forall (tp :: BaseType).
    BaseTypeRepr tp -> String -> ConfigOption tp
    configOption BaseTypeRepr BaseIntegerType
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr String
    "solver.stp.random-seed"

    stpRandomSeedOLD :: ConfigOption BaseIntegerType
    stpRandomSeedOLD :: ConfigOption BaseIntegerType
    stpRandomSeedOLD = BaseTypeRepr BaseIntegerType
    -> String -> ConfigOption BaseIntegerType
    forall (tp :: BaseType).
    BaseTypeRepr tp -> String -> ConfigOption tp
    configOption BaseTypeRepr BaseIntegerType
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr String
    "stp.random-seed"

    -- | Control strict parsing for Boolector solver responses (defaults
    -- to solver.strict-parsing option setting).
    stpStrictParsing :: ConfigOption BaseBoolType
    stpStrictParsing :: ConfigOption BaseBoolType
    stpStrictParsing = BaseTypeRepr BaseBoolType -> String -> ConfigOption BaseBoolType
    forall (tp :: BaseType).
    BaseTypeRepr tp -> String -> ConfigOption tp
    configOption BaseTypeRepr BaseBoolType
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr String
    "solver.stp.strict_parsing"

    intWithRangeOpt :: ConfigOption BaseIntegerType -> Integer -> Integer -> ConfigDesc
    intWithRangeOpt :: ConfigOption BaseIntegerType -> Integer -> Integer -> ConfigDesc
    intWithRangeOpt ConfigOption BaseIntegerType
    nm Integer
    lo Integer
    hi = ConfigOption BaseIntegerType
    -> OptionStyle BaseIntegerType
    -> Maybe (Doc Void)
    -> Maybe (ConcreteVal BaseIntegerType)
    -> ConfigDesc
    forall (tp :: BaseType).
    ConfigOption tp
    -> OptionStyle tp
    -> Maybe (Doc Void)
    -> Maybe (ConcreteVal tp)
    -> ConfigDesc
    mkOpt ConfigOption BaseIntegerType
    nm OptionStyle BaseIntegerType
    sty Maybe (Doc Void)
    forall a. Maybe a
    Nothing Maybe (ConcreteVal BaseIntegerType)
    forall a. Maybe a
    Nothing
      where sty :: OptionStyle BaseIntegerType
    sty = Bound Integer -> Bound Integer -> OptionStyle BaseIntegerType
    integerWithRangeOptSty (Integer -> Bound Integer
    forall r. r -> Bound r
    Inclusive Integer
    lo) (Integer -> Bound Integer
    forall r. r -> Bound r
    Inclusive Integer
    hi)

    stpOptions :: [ConfigDesc]
    stpOptions :: [ConfigDesc]
    stpOptions =
      let mkPath :: ConfigOption (BaseStringType Unicode) -> ConfigDesc
    mkPath ConfigOption (BaseStringType Unicode)
    co = ConfigOption (BaseStringType Unicode)
    -> OptionStyle (BaseStringType Unicode)
    -> Maybe (Doc Void)
    -> Maybe (ConcreteVal (BaseStringType Unicode))
    -> ConfigDesc
    forall (tp :: BaseType).
    ConfigOption tp
    -> OptionStyle tp
    -> Maybe (Doc Void)
    -> Maybe (ConcreteVal tp)
    -> ConfigDesc
    mkOpt ConfigOption (BaseStringType Unicode)
    co
                      OptionStyle (BaseStringType Unicode)
    executablePathOptSty
                      (Doc Void -> Maybe (Doc Void)
    forall a. a -> Maybe a
    Just Doc Void
    "Path to STP executable.")
                      (ConcreteVal (BaseStringType Unicode)
    -> Maybe (ConcreteVal (BaseStringType Unicode))
    forall a. a -> Maybe a
    Just (StringLiteral Unicode -> ConcreteVal (BaseStringType Unicode)
    forall (si :: StringInfo).
    StringLiteral si -> ConcreteVal ('BaseStringType si)
    ConcreteString StringLiteral Unicode
    "stp"))
          p1 :: ConfigDesc
    p1 = ConfigOption (BaseStringType Unicode) -> ConfigDesc
    mkPath ConfigOption (BaseStringType Unicode)
    stpPath
          randbitval :: Integer
    randbitval = Integer
    2Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^(Int
    30 :: Int)Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1
          r1 :: ConfigDesc
    r1 = ConfigOption BaseIntegerType -> Integer -> Integer -> ConfigDesc
    intWithRangeOpt ConfigOption BaseIntegerType
    stpRandomSeed (Integer -> Integer
    forall a. Num a => a -> a
    negate Integer
    randbitval) Integer
    randbitval
      in [ ConfigDesc
    p1, ConfigDesc
    r1
         , (Text -> Text) -> ConfigDesc -> ConfigDesc
    copyOpt (Text -> Text -> Text
    forall a b. a -> b -> a
    const (Text -> Text -> Text) -> Text -> Text -> Text
    forall a b. (a -> b) -> a -> b
    $ ConfigOption BaseBoolType -> Text
    forall (tp :: BaseType). ConfigOption tp -> Text
    configOptionText ConfigOption BaseBoolType
    stpStrictParsing) ConfigDesc
    strictSMTParseOpt
         , [ConfigDesc] -> ConfigDesc -> ConfigDesc
    deprecatedOpt [ConfigDesc
    p1] (ConfigDesc -> ConfigDesc) -> ConfigDesc -> ConfigDesc
    forall a b. (a -> b) -> a -> b
    $ ConfigOption (BaseStringType Unicode) -> ConfigDesc
    mkPath ConfigOption (BaseStringType Unicode)
    stpPathOLD
         , [ConfigDesc] -> ConfigDesc -> ConfigDesc
    deprecatedOpt [ConfigDesc
    r1] (ConfigDesc -> ConfigDesc) -> ConfigDesc -> ConfigDesc
    forall a b. (a -> b) -> a -> b
    $ ConfigOption BaseIntegerType -> Integer -> Integer -> ConfigDesc
    intWithRangeOpt ConfigOption BaseIntegerType
    stpRandomSeedOLD
           (Integer -> Integer
    forall a. Num a => a -> a
    negate Integer
    randbitval) Integer
    randbitval
         , ConfigOption BaseIntegerType
    -> OptionStyle BaseIntegerType
    -> Maybe (Doc Void)
    -> Maybe (ConcreteVal BaseIntegerType)
    -> ConfigDesc
    forall (tp :: BaseType).
    ConfigOption tp
    -> OptionStyle tp
    -> Maybe (Doc Void)
    -> Maybe (ConcreteVal tp)
    -> ConfigDesc
    mkOpt ConfigOption BaseIntegerType
    stpTimeout OptionStyle BaseIntegerType
    integerOptSty (Doc Void -> Maybe (Doc Void)
    forall a. a -> Maybe a
    Just Doc Void
    "Per-check timeout in milliseconds (zero is none)")
           (ConcreteVal BaseIntegerType -> Maybe (ConcreteVal BaseIntegerType)
    forall a. a -> Maybe a
    Just (Integer -> ConcreteVal BaseIntegerType
    ConcreteInteger Integer
    0))
         ] [ConfigDesc] -> [ConfigDesc] -> [ConfigDesc]
    forall a. Semigroup a => a -> a -> a
    <> [ConfigDesc]
    SMT2.smtlib2Options

    stpAdapter :: SolverAdapter st
    stpAdapter :: forall (st :: Type -> Type). SolverAdapter st
    stpAdapter =
      SolverAdapter
      { solver_adapter_name :: String
    solver_adapter_name = String
    "stp"
      , solver_adapter_config_options :: [ConfigDesc]
    solver_adapter_config_options = [ConfigDesc]
    stpOptions
      , solver_adapter_check_sat :: forall t fs a.
    ExprBuilder t st fs
    -> LogData
    -> [BoolExpr t]
    -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
        -> IO a)
    -> IO a
    solver_adapter_check_sat  = ExprBuilder t st fs
    -> LogData
    -> [BoolExpr t]
    -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
        -> IO a)
    -> IO a
    forall t fs a.
    ExprBuilder t st fs
    -> LogData
    -> [BoolExpr t]
    -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
        -> IO a)
    -> IO a
    forall t (st :: Type -> Type) fs a.
    ExprBuilder t st fs
    -> LogData
    -> [BoolExpr t]
    -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
        -> IO a)
    -> IO a
    runSTPInOverride
      , solver_adapter_write_smt2 :: forall t fs. ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
    solver_adapter_write_smt2 =
           STP
    -> String
    -> ProblemFeatures
    -> Maybe (ConfigOption BaseBoolType)
    -> ExprBuilder t st fs
    -> Handle
    -> [BoolExpr t]
    -> IO ()
    forall a t (st :: Type -> Type) fs.
    SMTLib2Tweaks a =>
    a
    -> String
    -> ProblemFeatures
    -> Maybe (ConfigOption BaseBoolType)
    -> ExprBuilder t st fs
    -> Handle
    -> [BoolExpr t]
    -> IO ()
    SMT2.writeDefaultSMT2 STP
    STP String
    "STP" ProblemFeatures
    defaultWriteSMTLIB2Features
           (ConfigOption BaseBoolType -> Maybe (ConfigOption BaseBoolType)
    forall a. a -> Maybe a
    Just ConfigOption BaseBoolType
    stpStrictParsing)
      }

    instance SMT2.SMTLib2Tweaks STP where
      smtlib2tweaks :: STP
    smtlib2tweaks = STP
    STP

    instance SMT2.SMTLib2GenericSolver STP where
      defaultSolverPath :: forall t (st :: Type -> Type) fs.
    STP -> ExprBuilder t st fs -> IO String
    defaultSolverPath STP
    _ = ConfigOption (BaseStringType Unicode) -> Config -> IO String
    findSolverPath ConfigOption (BaseStringType Unicode)
    stpPath (Config -> IO String)
    -> (ExprBuilder t st fs -> Config)
    -> ExprBuilder t st fs
    -> IO String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ExprBuilder t st fs -> Config
    forall sym. IsExprBuilder sym => sym -> Config
    getConfiguration

      defaultSolverArgs :: forall t (st :: Type -> Type) fs.
    STP -> ExprBuilder t st fs -> IO [String]
    defaultSolverArgs STP
    _ ExprBuilder t st fs
    _ = [String] -> IO [String]
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return [String
    "--SMTLIB2"]

      defaultFeatures :: STP -> ProblemFeatures
    defaultFeatures STP
    _ = ProblemFeatures
    stpFeatures

      setDefaultLogicAndOptions :: forall t. WriterConn t (Writer STP) -> IO ()
    setDefaultLogicAndOptions WriterConn t (Writer STP)
    writer = do
        WriterConn t (Writer STP) -> Bool -> IO ()
    forall a t.
    SMTLib2Tweaks a =>
    WriterConn t (Writer a) -> Bool -> IO ()
    SMT2.setProduceModels WriterConn t (Writer STP)
    writer Bool
    True
        WriterConn t (Writer STP) -> Logic -> IO ()
    forall a t.
    SMTLib2Tweaks a =>
    WriterConn t (Writer a) -> Logic -> IO ()
    SMT2.setLogic WriterConn t (Writer STP)
    writer Logic
    SMT2.qf_bv

    stpFeatures :: ProblemFeatures
    stpFeatures :: ProblemFeatures
    stpFeatures = ProblemFeatures
    useIntegerArithmetic ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    forall a. Bits a => a -> a -> a
    .|. ProblemFeatures
    useBitvectors

    runSTPInOverride
      :: ExprBuilder t st fs
      -> LogData
      -> [BoolExpr t]
      -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a)
      -> IO a
    runSTPInOverride :: forall t (st :: Type -> Type) fs a.
    ExprBuilder t st fs
    -> LogData
    -> [BoolExpr t]
    -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
        -> IO a)
    -> IO a
    runSTPInOverride = STP
    -> AcknowledgementAction t (Writer STP)
    -> ProblemFeatures
    -> Maybe (ConfigOption BaseBoolType)
    -> ExprBuilder t st fs
    -> LogData
    -> [BoolExpr t]
    -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
        -> IO a)
    -> IO a
    forall a t (st :: Type -> Type) fs b.
    SMTLib2GenericSolver a =>
    a
    -> AcknowledgementAction t (Writer a)
    -> ProblemFeatures
    -> Maybe (ConfigOption BaseBoolType)
    -> ExprBuilder t st fs
    -> LogData
    -> [BoolExpr t]
    -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
        -> IO b)
    -> IO b
    forall t (st :: Type -> Type) fs b.
    STP
    -> AcknowledgementAction t (Writer STP)
    -> ProblemFeatures
    -> Maybe (ConfigOption BaseBoolType)
    -> ExprBuilder t st fs
    -> LogData
    -> [BoolExpr t]
    -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
        -> IO b)
    -> IO b
    SMT2.runSolverInOverride STP
    STP AcknowledgementAction t (Writer STP)
    forall t h. AcknowledgementAction t h
    SMT2.nullAcknowledgementAction
                       (STP -> ProblemFeatures
    forall a. SMTLib2GenericSolver a => a -> ProblemFeatures
    SMT2.defaultFeatures STP
    STP) (ConfigOption BaseBoolType -> Maybe (ConfigOption BaseBoolType)
    forall a. a -> Maybe a
    Just ConfigOption BaseBoolType
    stpStrictParsing)

    -- | Run STP in a session. STP will be configured to produce models, buth
    -- otherwise left with the default configuration.
    withSTP
      :: ExprBuilder t st fs
      -> FilePath
        -- ^ Path to STP executable
      -> LogData
      -> (SMT2.Session t STP -> IO a)
        -- ^ Action to run
      -> IO a
    withSTP :: forall t (st :: Type -> Type) fs a.
    ExprBuilder t st fs
    -> String -> LogData -> (Session t STP -> IO a) -> IO a
    withSTP = STP
    -> AcknowledgementAction t (Writer STP)
    -> ProblemFeatures
    -> Maybe (ConfigOption BaseBoolType)
    -> ExprBuilder t st fs
    -> String
    -> LogData
    -> (Session t STP -> IO a)
    -> IO a
    forall a t (st :: Type -> Type) fs b.
    SMTLib2GenericSolver a =>
    a
    -> AcknowledgementAction t (Writer a)
    -> ProblemFeatures
    -> Maybe (ConfigOption BaseBoolType)
    -> ExprBuilder t st fs
    -> String
    -> LogData
    -> (Session t a -> IO b)
    -> IO b
    forall t (st :: Type -> Type) fs b.
    STP
    -> AcknowledgementAction t (Writer STP)
    -> ProblemFeatures
    -> Maybe (ConfigOption BaseBoolType)
    -> ExprBuilder t st fs
    -> String
    -> LogData
    -> (Session t STP -> IO b)
    -> IO b
    SMT2.withSolver STP
    STP AcknowledgementAction t (Writer STP)
    forall t h. AcknowledgementAction t h
    SMT2.nullAcknowledgementAction
              (STP -> ProblemFeatures
    forall a. SMTLib2GenericSolver a => a -> ProblemFeatures
    SMT2.defaultFeatures STP
    STP) (ConfigOption BaseBoolType -> Maybe (ConfigOption BaseBoolType)
    forall a. a -> Maybe a
    Just ConfigOption BaseBoolType
    stpStrictParsing)

    setInteractiveLogicAndOptions ::
      SMT2.SMTLib2Tweaks a =>
      SMT2.WriterConn t (SMT2.Writer a) ->
      IO ()
    setInteractiveLogicAndOptions :: forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
    setInteractiveLogicAndOptions WriterConn t (Writer a)
    writer = do
        -- Tell STP to acknowledge successful commands
        WriterConn t (Writer a) -> Text -> Text -> IO ()
    forall a t.
    SMTLib2Tweaks a =>
    WriterConn t (Writer a) -> Text -> Text -> IO ()
    SMT2.setOption WriterConn t (Writer a)
    writer Text
    "print-success"  Text
    "true"
        -- Tell STP to produce models
        WriterConn t (Writer a) -> Text -> Text -> IO ()
    forall a t.
    SMTLib2Tweaks a =>
    WriterConn t (Writer a) -> Text -> Text -> IO ()
    SMT2.setOption WriterConn t (Writer a)
    writer Text
    "produce-models" Text
    "true"

        -- Tell STP to make declarations global, so they are not removed by 'pop' commands
    -- TODO, add this command once https://github.com/stp/stp/issues/365 is closed
    --    SMT2.setOption writer "global-declarations" "true"

    instance OnlineSolver (SMT2.Writer STP) where

      startSolverProcess :: forall scope (st :: Type -> Type) fs.
    ProblemFeatures
    -> Maybe Handle
    -> ExprBuilder scope st fs
    -> IO (SolverProcess scope (Writer STP))
    startSolverProcess ProblemFeatures
    feat Maybe Handle
    mbIOh ExprBuilder scope st fs
    sym = do
        SolverGoalTimeout
    timeout <- Integer -> SolverGoalTimeout
    SolverGoalTimeout (Integer -> SolverGoalTimeout)
    -> IO Integer -> IO SolverGoalTimeout
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$>
                   (OptionSetting BaseIntegerType -> IO Integer
    forall (tp :: BaseType) a. Opt tp a => OptionSetting tp -> IO a
    getOpt (OptionSetting BaseIntegerType -> IO Integer)
    -> IO (OptionSetting BaseIntegerType) -> IO Integer
    forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ConfigOption BaseIntegerType
    -> Config -> IO (OptionSetting BaseIntegerType)
    forall (tp :: BaseType).
    ConfigOption tp -> Config -> IO (OptionSetting tp)
    getOptionSetting ConfigOption BaseIntegerType
    stpTimeout (ExprBuilder scope st fs -> Config
    forall sym. IsExprBuilder sym => sym -> Config
    getConfiguration ExprBuilder scope st fs
    sym))
        STP
    -> AcknowledgementAction scope (Writer STP)
    -> (WriterConn scope (Writer STP) -> IO ())
    -> SolverGoalTimeout
    -> ProblemFeatures
    -> Maybe (ConfigOption BaseBoolType)
    -> Maybe Handle
    -> ExprBuilder scope st fs
    -> IO (SolverProcess scope (Writer STP))
    forall a t (st :: Type -> Type) fs.
    SMTLib2GenericSolver a =>
    a
    -> AcknowledgementAction t (Writer a)
    -> (WriterConn t (Writer a) -> IO ())
    -> SolverGoalTimeout
    -> ProblemFeatures
    -> Maybe (ConfigOption BaseBoolType)
    -> Maybe Handle
    -> ExprBuilder t st fs
    -> IO (SolverProcess t (Writer a))
    SMT2.startSolver STP
    STP AcknowledgementAction scope (Writer STP)
    forall t a. AcknowledgementAction t (Writer a)
    SMT2.smtAckResult
          WriterConn scope (Writer STP) -> IO ()
    forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
    setInteractiveLogicAndOptions
          SolverGoalTimeout
    timeout
          ProblemFeatures
    feat
          (ConfigOption BaseBoolType -> Maybe (ConfigOption BaseBoolType)
    forall a. a -> Maybe a
    Just ConfigOption BaseBoolType
    stpStrictParsing) Maybe Handle
    mbIOh ExprBuilder scope st fs
    sym

      shutdownSolverProcess :: forall scope.
    SolverProcess scope (Writer STP) -> IO (ExitCode, Text)
    shutdownSolverProcess = STP -> SolverProcess scope (Writer STP) -> IO (ExitCode, Text)
    forall a t.
    SMTLib2GenericSolver a =>
    a -> SolverProcess t (Writer a) -> IO (ExitCode, Text)
    SMT2.shutdownSolver STP
    STP