    -----------------------------------------------------------------------
    -- |
    -- Module           : What4.Solver.Adapter
    -- Description      : Defines the low-level interface between a particular
    --                    solver and the SimpleBuilder family of backends.
    -- Copyright        : (c) Galois, Inc 2015-2020
    -- License          : BSD3
    -- Maintainer       : Rob Dockins <rdockins@galois.com>
    -- Stability        : provisional
    --
    ------------------------------------------------------------------------

    {-# LANGUAGE LambdaCase #-}
    {-# LANGUAGE RankNTypes #-}
    module What4.Solver.Adapter
      ( SolverAdapter(..)
      , defaultWriteSMTLIB2Features
      , defaultSolverAdapter
      , solverAdapterOptions
      , LogData(..)
      , logCallback
      , defaultLogData
      , smokeTest
      ) where

    import qualified Control.Exception as X
    import           Data.Bits
    import           Data.IORef
    import qualified Data.Map as Map
    import qualified Data.Text as T
    import           System.IO
    import qualified Prettyprinter as PP

    import           What4.BaseTypes
    import           What4.Config
    import           What4.Concrete
    import           What4.Interface
    import           What4.SatResult
    import           What4.ProblemFeatures
    import           What4.Expr.Builder
    import           What4.Expr.GroundEval

    -- | The main interface for interacting with a solver in an "offline" fashion,
    --   which means that a new solver process is started for each query.
    data SolverAdapter st =
      SolverAdapter
      { forall (st :: Type -> Type). SolverAdapter st -> String
    solver_adapter_name :: !String

        -- | Configuration options relevant to this solver adapter
      , forall (st :: Type -> Type). SolverAdapter st -> [ConfigDesc]
    solver_adapter_config_options
            :: ![ConfigDesc]

        -- | Operation to check the satisfiability of a formula.
        --   The final argument is a callback that calculates the ultimate result from
        --   a SatResult and operations for finding model values in the event of a SAT result.
        --   Note: the evaluation functions may cease to be avaliable after the
        --   callback completes, so any necessary information should be extracted from
        --   them before returning.
      , forall (st :: Type -> Type).
    SolverAdapter st
    -> 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
            :: !(forall t fs a.
               ExprBuilder t st fs
            -> LogData
            -> [BoolExpr t]
            -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a)
            -> IO a)

        -- | Write an SMTLib2 problem instance onto the given handle, incorporating
        --   any solver-specific tweaks appropriate to this solver
      , forall (st :: Type -> Type).
    SolverAdapter st
    -> forall t fs.
       ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
    solver_adapter_write_smt2 :: !(forall t fs . ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ())
      }

    -- | A collection of operations for producing output from solvers.
    --   Solvers can produce messages at varying verbosity levels that
    --   might be appropriate for user output by using the `logCallbackVerbose`
    --   operation.  If a `logHandle` is provided, the entire interaction
    --   sequence with the solver will be mirrored into that handle.
    data LogData = LogData { LogData -> Int -> String -> IO ()
    logCallbackVerbose :: Int -> String -> IO ()
                           -- ^ takes a verbosity and a message to log
                           , LogData -> Int
    logVerbosity :: Int
                           -- ^ the default verbosity; typical default is 2
                           , LogData -> String
    logReason :: String
                           -- ^ the reason for performing the operation
                           , LogData -> Maybe Handle
    logHandle :: Maybe Handle
                           -- ^ handle on which to mirror solver input/responses
                           }

    logCallback :: LogData -> (String -> IO ())
    logCallback :: LogData -> String -> IO ()
    logCallback LogData
    logData = LogData -> Int -> String -> IO ()
    logCallbackVerbose LogData
    logData (LogData -> Int
    logVerbosity LogData
    logData)

    defaultLogData :: LogData
    defaultLogData :: LogData
    defaultLogData = LogData { logCallbackVerbose :: Int -> String -> IO ()
    logCallbackVerbose = \Int
    _ String
    _ -> () -> IO ()
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return ()
                             , logVerbosity :: Int
    logVerbosity = Int
    2
                             , logReason :: String
    logReason = String
    "defaultReason"
                             , logHandle :: Maybe Handle
    logHandle = Maybe Handle
    forall a. Maybe a
    Nothing }

    instance Show (SolverAdapter st) where
      show :: SolverAdapter st -> String
    show = SolverAdapter st -> String
    forall (st :: Type -> Type). SolverAdapter st -> String
    solver_adapter_name
    instance Eq (SolverAdapter st) where
      SolverAdapter st
    x == :: SolverAdapter st -> SolverAdapter st -> Bool
    == SolverAdapter st
    y = SolverAdapter st -> String
    forall (st :: Type -> Type). SolverAdapter st -> String
    solver_adapter_name SolverAdapter st
    x String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == SolverAdapter st -> String
    forall (st :: Type -> Type). SolverAdapter st -> String
    solver_adapter_name SolverAdapter st
    y
    instance Ord (SolverAdapter st) where
      compare :: SolverAdapter st -> SolverAdapter st -> Ordering
    compare SolverAdapter st
    x SolverAdapter st
    y = String -> String -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (SolverAdapter st -> String
    forall (st :: Type -> Type). SolverAdapter st -> String
    solver_adapter_name SolverAdapter st
    x) (SolverAdapter st -> String
    forall (st :: Type -> Type). SolverAdapter st -> String
    solver_adapter_name SolverAdapter st
    y)

    -- | Default featues to use for writing SMTLIB2 files.
    defaultWriteSMTLIB2Features :: ProblemFeatures
    defaultWriteSMTLIB2Features :: ProblemFeatures
    defaultWriteSMTLIB2Features
      = ProblemFeatures
    useComputableReals
      ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    forall a. Bits a => a -> a -> a
    .|. ProblemFeatures
    useIntegerArithmetic
      ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    forall a. Bits a => a -> a -> a
    .|. ProblemFeatures
    useBitvectors
      ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    forall a. Bits a => a -> a -> a
    .|. ProblemFeatures
    useQuantifiers
      ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    forall a. Bits a => a -> a -> a
    .|. ProblemFeatures
    useSymbolicArrays

    defaultSolverAdapter :: ConfigOption (BaseStringType Unicode)
    defaultSolverAdapter :: ConfigOption (BaseStringType Unicode)
    defaultSolverAdapter = BaseTypeRepr (BaseStringType Unicode)
    -> String -> ConfigOption (BaseStringType Unicode)
    forall (tp :: BaseType).
    BaseTypeRepr tp -> String -> ConfigOption tp
    configOption (StringInfoRepr Unicode -> BaseTypeRepr (BaseStringType Unicode)
    forall (si :: StringInfo).
    StringInfoRepr si -> BaseTypeRepr ('BaseStringType si)
    BaseStringRepr StringInfoRepr Unicode
    UnicodeRepr) String
    "solver.default"

    deprecatedDefaultSolverAdapterConfig :: ConfigOption (BaseStringType Unicode)
    deprecatedDefaultSolverAdapterConfig :: ConfigOption (BaseStringType Unicode)
    deprecatedDefaultSolverAdapterConfig = BaseTypeRepr (BaseStringType Unicode)
    -> String -> ConfigOption (BaseStringType Unicode)
    forall (tp :: BaseType).
    BaseTypeRepr tp -> String -> ConfigOption tp
    configOption (StringInfoRepr Unicode -> BaseTypeRepr (BaseStringType Unicode)
    forall (si :: StringInfo).
    StringInfoRepr si -> BaseTypeRepr ('BaseStringType si)
    BaseStringRepr StringInfoRepr Unicode
    UnicodeRepr) String
    "default_solver"

    -- Given a list of solver adapters, returns a tuple of the full set of
    -- solver config options for all adapters (plus a configuration to
    -- specify the default adapter) and an IO operation that will return
    -- current default adapter when executed.

    solverAdapterOptions ::
      [SolverAdapter st] ->
      IO ([ConfigDesc], IO (SolverAdapter st))
    solverAdapterOptions :: forall (st :: Type -> Type).
    [SolverAdapter st] -> IO ([ConfigDesc], IO (SolverAdapter st))
    solverAdapterOptions [] = String -> IO ([ConfigDesc], IO (SolverAdapter st))
    forall a. String -> IO a
    forall (m :: Type -> Type) a. MonadFail m => String -> m a
    fail String
    "No solver adapters specified!"
    solverAdapterOptions xs :: [SolverAdapter st]
    xs@(SolverAdapter st
    def:[SolverAdapter st]
    _) =
      do IORef (SolverAdapter st)
    ref <- SolverAdapter st -> IO (IORef (SolverAdapter st))
    forall a. a -> IO (IORef a)
    newIORef SolverAdapter st
    def
         let opts :: [ConfigDesc]
    opts = IORef (SolverAdapter st) -> ConfigDesc
    sty IORef (SolverAdapter st)
    ref ConfigDesc -> [ConfigDesc] -> [ConfigDesc]
    forall a. a -> [a] -> [a]
    : IORef (SolverAdapter st) -> ConfigDesc
    sty' IORef (SolverAdapter st)
    ref ConfigDesc -> [ConfigDesc] -> [ConfigDesc]
    forall a. a -> [a] -> [a]
    : (SolverAdapter st -> [ConfigDesc])
    -> [SolverAdapter st] -> [ConfigDesc]
    forall (t :: Type -> Type) a b.
    Foldable t =>
    (a -> [b]) -> t a -> [b]
    concatMap SolverAdapter st -> [ConfigDesc]
    forall (st :: Type -> Type). SolverAdapter st -> [ConfigDesc]
    solver_adapter_config_options [SolverAdapter st]
    xs
         ([ConfigDesc], IO (SolverAdapter st))
    -> IO ([ConfigDesc], IO (SolverAdapter st))
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return ([ConfigDesc]
    opts, IORef (SolverAdapter st) -> IO (SolverAdapter st)
    forall a. IORef a -> IO a
    readIORef IORef (SolverAdapter st)
    ref)

     where
     f :: IORef (SolverAdapter st)
    -> SolverAdapter st -> (Text, IO OptionSetResult)
    f IORef (SolverAdapter st)
    ref SolverAdapter st
    x = (String -> Text
    T.pack (SolverAdapter st -> String
    forall (st :: Type -> Type). SolverAdapter st -> String
    solver_adapter_name SolverAdapter st
    x), IORef (SolverAdapter st) -> SolverAdapter st -> IO ()
    forall a. IORef a -> a -> IO ()
    atomicWriteIORef IORef (SolverAdapter st)
    ref SolverAdapter st
    x IO () -> IO OptionSetResult -> IO OptionSetResult
    forall a b. IO a -> IO b -> IO b
    forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
    >> OptionSetResult -> IO OptionSetResult
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return OptionSetResult
    optOK)
     vals :: IORef (SolverAdapter st) -> Map Text (IO OptionSetResult)
    vals IORef (SolverAdapter st)
    ref = [(Text, IO OptionSetResult)] -> Map Text (IO OptionSetResult)
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList ((SolverAdapter st -> (Text, IO OptionSetResult))
    -> [SolverAdapter st] -> [(Text, IO OptionSetResult)]
    forall a b. (a -> b) -> [a] -> [b]
    map (IORef (SolverAdapter st)
    -> SolverAdapter st -> (Text, IO OptionSetResult)
    forall {st :: Type -> Type}.
    IORef (SolverAdapter st)
    -> SolverAdapter st -> (Text, IO OptionSetResult)
    f IORef (SolverAdapter st)
    ref) [SolverAdapter st]
    xs)
     sty :: IORef (SolverAdapter st) -> ConfigDesc
    sty IORef (SolverAdapter st)
    ref = 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)
    defaultSolverAdapter
                     (Map Text (IO OptionSetResult)
    -> OptionStyle (BaseStringType Unicode)
    listOptSty (IORef (SolverAdapter st) -> Map Text (IO OptionSetResult)
    vals IORef (SolverAdapter st)
    ref))
                     (Doc Void -> Maybe (Doc Void)
    forall a. a -> Maybe a
    Just (String -> Doc Void
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    PP.pretty String
    "Indicates which solver to use for check-sat queries"))
                     (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 (Text -> StringLiteral Unicode
    UnicodeLiteral (String -> Text
    T.pack (SolverAdapter st -> String
    forall (st :: Type -> Type). SolverAdapter st -> String
    solver_adapter_name SolverAdapter st
    def)))))
     sty' :: IORef (SolverAdapter st) -> ConfigDesc
    sty' IORef (SolverAdapter st)
    ref = [ConfigDesc] -> ConfigDesc -> ConfigDesc
    deprecatedOpt [IORef (SolverAdapter st) -> ConfigDesc
    sty IORef (SolverAdapter st)
    ref] (ConfigDesc -> ConfigDesc) -> ConfigDesc -> ConfigDesc
    forall a b. (a -> b) -> a -> b
    $
                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)
    deprecatedDefaultSolverAdapterConfig
                      (Map Text (IO OptionSetResult)
    -> OptionStyle (BaseStringType Unicode)
    listOptSty (IORef (SolverAdapter st) -> Map Text (IO OptionSetResult)
    vals IORef (SolverAdapter st)
    ref))
                      (Doc Void -> Maybe (Doc Void)
    forall a. a -> Maybe a
    Just (String -> Doc Void
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    PP.pretty String
    "Indicates which solver to use for check-sat queries."))
                      (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 (Text -> StringLiteral Unicode
    UnicodeLiteral (String -> Text
    T.pack (SolverAdapter st -> String
    forall (st :: Type -> Type). SolverAdapter st -> String
    solver_adapter_name SolverAdapter st
    def)))))

    -- | Test the ability to interact with a solver by peforming a check-sat query
    --   on a trivially unsatisfiable problem.
    smokeTest :: ExprBuilder t st fs -> SolverAdapter st -> IO (Maybe X.SomeException)
    smokeTest :: forall t (st :: Type -> Type) fs.
    ExprBuilder t st fs -> SolverAdapter st -> IO (Maybe SomeException)
    smokeTest ExprBuilder t st fs
    sym SolverAdapter st
    adpt = IO (Maybe SomeException)
    test IO (Maybe SomeException)
    -> (SomeException -> IO (Maybe SomeException))
    -> IO (Maybe SomeException)
    forall e a. Exception e => IO a -> (e -> IO a) -> IO a
    `X.catch` (Maybe SomeException -> IO (Maybe SomeException)
    forall a. a -> IO a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (Maybe SomeException -> IO (Maybe SomeException))
    -> (SomeException -> Maybe SomeException)
    -> SomeException
    -> IO (Maybe SomeException)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SomeException -> Maybe SomeException
    forall a. a -> Maybe a
    Just)
      where
      test :: IO (Maybe X.SomeException)
      test :: IO (Maybe SomeException)
    test =
        SolverAdapter st
    -> forall t fs a.
       ExprBuilder t st fs
       -> LogData
       -> [BoolExpr t]
       -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
           -> IO a)
       -> IO a
    forall (st :: Type -> Type).
    SolverAdapter st
    -> 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 SolverAdapter st
    adpt ExprBuilder t st fs
    sym LogData
    defaultLogData [ExprBuilder t st fs -> Pred (ExprBuilder t st fs)
    forall sym. IsExprBuilder sym => sym -> Pred sym
    falsePred ExprBuilder t st fs
    sym] ((SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
      -> IO (Maybe SomeException))
     -> IO (Maybe SomeException))
    -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
        -> IO (Maybe SomeException))
    -> IO (Maybe SomeException)
    forall a b. (a -> b) -> a -> b
    $ \case
          Unsat{} -> Maybe SomeException -> IO (Maybe SomeException)
    forall a. a -> IO a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure Maybe SomeException
    forall a. Maybe a
    Nothing
          SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    _ -> String -> IO (Maybe SomeException)
    forall a. String -> IO a
    forall (m :: Type -> Type) a. MonadFail m => String -> m a
    fail String
    "Smoke test failed: expected UNSAT"