    ------------------------------------------------------------------------
    -- |
    -- Module           : What4.Solver.Bitwuzla
    -- Description      : Interface for running Bitwuzla
    -- Copyright        : (c) Galois, Inc 2014-2023
    -- License          : BSD3
    -- Maintainer       : Ryan Scott <rscott@galois.com>
    -- Stability        : provisional
    --
    -- This module provides an interface for running Bitwuzla and parsing
    -- the results back.
    ------------------------------------------------------------------------
    {-# LANGUAGE FlexibleInstances #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE OverloadedStrings #-}
    module What4.Solver.Bitwuzla
      ( Bitwuzla(..)
      , bitwuzlaPath
      , bitwuzlaTimeout
      , bitwuzlaOptions
      , bitwuzlaAdapter
      , runBitwuzlaInOverride
      , withBitwuzla
      , bitwuzlaFeatures
      ) where

    import           Control.Monad
    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 qualified What4.Protocol.SMTLib2.Syntax as Syntax
    import           What4.Protocol.SMTLib2.Response ( strictSMTParseOpt )
    import           What4.SatResult
    import           What4.Solver.Adapter
    import           What4.Utils.Process

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

    -- | Path to bitwuzla
    bitwuzlaPath :: ConfigOption (BaseStringType Unicode)
    bitwuzlaPath :: ConfigOption (BaseStringType Unicode)
    bitwuzlaPath = 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.bitwuzla.path"

    -- | Per-check timeout, in milliseconds (zero is none)
    bitwuzlaTimeout :: ConfigOption BaseIntegerType
    bitwuzlaTimeout :: ConfigOption BaseIntegerType
    bitwuzlaTimeout = 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.bitwuzla.timeout"

    -- | Control strict parsing for Bitwuzla solver responses (defaults
    -- to solver.strict-parsing option setting).
    bitwuzlaStrictParsing :: ConfigOption BaseBoolType
    bitwuzlaStrictParsing :: ConfigOption BaseBoolType
    bitwuzlaStrictParsing = 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.bitwuzla.strict_parsing"

    bitwuzlaOptions :: [ConfigDesc]
    bitwuzlaOptions :: [ConfigDesc]
    bitwuzlaOptions =
      let bpOpt :: ConfigOption (BaseStringType Unicode) -> ConfigDesc
    bpOpt 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 bitwuzla 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
    "bitwuzla"))
          mkTmo :: ConfigOption BaseIntegerType -> ConfigDesc
    mkTmo ConfigOption BaseIntegerType
    co = 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
    co
                     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))
          bp :: ConfigDesc
    bp = ConfigOption (BaseStringType Unicode) -> ConfigDesc
    bpOpt ConfigOption (BaseStringType Unicode)
    bitwuzlaPath
      in [ ConfigDesc
    bp
         , ConfigOption BaseIntegerType -> ConfigDesc
    mkTmo ConfigOption BaseIntegerType
    bitwuzlaTimeout
         , (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
    bitwuzlaStrictParsing) ConfigDesc
    strictSMTParseOpt
         ] [ConfigDesc] -> [ConfigDesc] -> [ConfigDesc]
    forall a. Semigroup a => a -> a -> a
    <> [ConfigDesc]
    SMT2.smtlib2Options

    bitwuzlaAdapter :: SolverAdapter st
    bitwuzlaAdapter :: forall (st :: Type -> Type). SolverAdapter st
    bitwuzlaAdapter =
      SolverAdapter
      { solver_adapter_name :: String
    solver_adapter_name = String
    "bitwuzla"
      , solver_adapter_config_options :: [ConfigDesc]
    solver_adapter_config_options = [ConfigDesc]
    bitwuzlaOptions
      , 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
    runBitwuzlaInOverride
      , solver_adapter_write_smt2 :: forall t fs. ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
    solver_adapter_write_smt2 =
          ()
    -> 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 () String
    "Bitwuzla" ProblemFeatures
    defaultWriteSMTLIB2Features
          (ConfigOption BaseBoolType -> Maybe (ConfigOption BaseBoolType)
    forall a. a -> Maybe a
    Just ConfigOption BaseBoolType
    bitwuzlaStrictParsing)
      }

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

    runBitwuzlaInOverride
      :: ExprBuilder t st fs
      -> LogData
      -> [BoolExpr t]
      -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a)
      -> IO a
    runBitwuzlaInOverride :: forall t (st :: Type -> Type) fs a.
    ExprBuilder t st fs
    -> LogData
    -> [BoolExpr t]
    -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
        -> IO a)
    -> IO a
    runBitwuzlaInOverride =
      Bitwuzla
    -> AcknowledgementAction t (Writer Bitwuzla)
    -> 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.
    Bitwuzla
    -> AcknowledgementAction t (Writer Bitwuzla)
    -> ProblemFeatures
    -> Maybe (ConfigOption BaseBoolType)
    -> ExprBuilder t st fs
    -> LogData
    -> [BoolExpr t]
    -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
        -> IO b)
    -> IO b
    SMT2.runSolverInOverride Bitwuzla
    Bitwuzla AcknowledgementAction t (Writer Bitwuzla)
    forall t h. AcknowledgementAction t h
    SMT2.nullAcknowledgementAction
      ProblemFeatures
    bitwuzlaFeatures (ConfigOption BaseBoolType -> Maybe (ConfigOption BaseBoolType)
    forall a. a -> Maybe a
    Just ConfigOption BaseBoolType
    bitwuzlaStrictParsing)

    -- | Run Bitwuzla in a session. Bitwuzla will be configured to produce models, but
    -- otherwise left with the default configuration.
    withBitwuzla
      :: ExprBuilder t st fs
      -> FilePath
        -- ^ Path to Bitwuzla executable
      -> LogData
      -> (SMT2.Session t Bitwuzla -> IO a)
        -- ^ Action to run
      -> IO a
    withBitwuzla :: forall t (st :: Type -> Type) fs a.
    ExprBuilder t st fs
    -> String -> LogData -> (Session t Bitwuzla -> IO a) -> IO a
    withBitwuzla = Bitwuzla
    -> AcknowledgementAction t (Writer Bitwuzla)
    -> ProblemFeatures
    -> Maybe (ConfigOption BaseBoolType)
    -> ExprBuilder t st fs
    -> String
    -> LogData
    -> (Session t Bitwuzla -> 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.
    Bitwuzla
    -> AcknowledgementAction t (Writer Bitwuzla)
    -> ProblemFeatures
    -> Maybe (ConfigOption BaseBoolType)
    -> ExprBuilder t st fs
    -> String
    -> LogData
    -> (Session t Bitwuzla -> IO b)
    -> IO b
    SMT2.withSolver Bitwuzla
    Bitwuzla AcknowledgementAction t (Writer Bitwuzla)
    forall t h. AcknowledgementAction t h
    SMT2.nullAcknowledgementAction
                   ProblemFeatures
    bitwuzlaFeatures (ConfigOption BaseBoolType -> Maybe (ConfigOption BaseBoolType)
    forall a. a -> Maybe a
    Just ConfigOption BaseBoolType
    bitwuzlaStrictParsing)

    bitwuzlaFeatures :: ProblemFeatures
    bitwuzlaFeatures :: ProblemFeatures
    bitwuzlaFeatures = ProblemFeatures
    useBitvectors
                   ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    forall a. Bits a => a -> a -> a
    .|. ProblemFeatures
    useFloatingPoint
                   ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    forall a. Bits a => a -> a -> a
    .|. ProblemFeatures
    useQuantifiers
                   ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    forall a. Bits a => a -> a -> a
    .|. ProblemFeatures
    useSymbolicArrays
                   ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    forall a. Bits a => a -> a -> a
    .|. ProblemFeatures
    useUninterpFunctions
                   ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    forall a. Bits a => a -> a -> a
    .|. ProblemFeatures
    useUnsatCores
                   ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    forall a. Bits a => a -> a -> a
    .|. ProblemFeatures
    useUnsatAssumptions

    instance SMT2.SMTLib2GenericSolver Bitwuzla where
      defaultSolverPath :: forall t (st :: Type -> Type) fs.
    Bitwuzla -> ExprBuilder t st fs -> IO String
    defaultSolverPath Bitwuzla
    _ = ConfigOption (BaseStringType Unicode) -> Config -> IO String
    findSolverPath ConfigOption (BaseStringType Unicode)
    bitwuzlaPath (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.
    Bitwuzla -> ExprBuilder t st fs -> IO [String]
    defaultSolverArgs Bitwuzla
    _ ExprBuilder t st fs
    sym = do
        let cfg :: Config
    cfg = ExprBuilder t st fs -> Config
    forall sym. IsExprBuilder sym => sym -> Config
    getConfiguration ExprBuilder t st fs
    sym
        timeout <- OptionSetting BaseIntegerType
    -> IO (Maybe (ConcreteVal BaseIntegerType))
    forall (tp :: BaseType).
    OptionSetting tp -> IO (Maybe (ConcreteVal tp))
    getOption (OptionSetting BaseIntegerType
     -> IO (Maybe (ConcreteVal BaseIntegerType)))
    -> IO (OptionSetting BaseIntegerType)
    -> IO (Maybe (ConcreteVal BaseIntegerType))
    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
    bitwuzlaTimeout Config
    cfg
        let extraOpts = case Maybe (ConcreteVal BaseIntegerType)
    timeout of
                          Just (ConcreteInteger Integer
    n) | Integer
    n Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > Integer
    0 -> [String
    "-t", Integer -> String
    forall a. Show a => a -> String
    show Integer
    n]
                          Maybe (ConcreteVal BaseIntegerType)
    _ -> []
        return $ ["--lang", "smt2"] ++ extraOpts
      defaultFeatures :: Bitwuzla -> ProblemFeatures
    defaultFeatures Bitwuzla
    _ = ProblemFeatures
    bitwuzlaFeatures
      setDefaultLogicAndOptions :: forall t. WriterConn t (Writer Bitwuzla) -> IO ()
    setDefaultLogicAndOptions WriterConn t (Writer Bitwuzla)
    writer = do
        WriterConn t (Writer Bitwuzla) -> Logic -> IO ()
    forall a t.
    SMTLib2Tweaks a =>
    WriterConn t (Writer a) -> Logic -> IO ()
    SMT2.setLogic WriterConn t (Writer Bitwuzla)
    writer Logic
    Syntax.allLogic
        WriterConn t (Writer Bitwuzla) -> Bool -> IO ()
    forall a t.
    SMTLib2Tweaks a =>
    WriterConn t (Writer a) -> Bool -> IO ()
    SMT2.setProduceModels WriterConn t (Writer Bitwuzla)
    writer Bool
    True

    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
        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"
        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"
        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
    "global-declarations" Text
    "true"
        Bool -> IO () -> IO ()
    forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
    when (WriterConn t (Writer a) -> ProblemFeatures
    forall t h. WriterConn t h -> ProblemFeatures
    SMT2.supportedFeatures WriterConn t (Writer a)
    writer ProblemFeatures -> ProblemFeatures -> Bool
    `hasProblemFeature` ProblemFeatures
    useUnsatCores) (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ do
          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-unsat-cores" Text
    "true"
        WriterConn t (Writer a) -> Logic -> IO ()
    forall a t.
    SMTLib2Tweaks a =>
    WriterConn t (Writer a) -> Logic -> IO ()
    SMT2.setLogic WriterConn t (Writer a)
    writer Logic
    Syntax.allLogic

    instance OnlineSolver (SMT2.Writer Bitwuzla) where
      startSolverProcess :: forall scope (st :: Type -> Type) fs.
    ProblemFeatures
    -> Maybe Handle
    -> ExprBuilder scope st fs
    -> IO (SolverProcess scope (Writer Bitwuzla))
    startSolverProcess ProblemFeatures
    feat Maybe Handle
    mbIOh ExprBuilder scope st fs
    sym = do
        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
    bitwuzlaTimeout (ExprBuilder scope st fs -> Config
    forall sym. IsExprBuilder sym => sym -> Config
    getConfiguration ExprBuilder scope st fs
    sym))
        SMT2.startSolver Bitwuzla SMT2.smtAckResult
                                setInteractiveLogicAndOptions
                                timeout
                                feat
                                (Just bitwuzlaStrictParsing) mbIOh sym
      shutdownSolverProcess :: forall scope.
    SolverProcess scope (Writer Bitwuzla) -> IO (ExitCode, Text)
    shutdownSolverProcess = Bitwuzla
    -> SolverProcess scope (Writer Bitwuzla) -> IO (ExitCode, Text)
    forall a t.
    SMTLib2GenericSolver a =>
    a -> SolverProcess t (Writer a) -> IO (ExitCode, Text)
    SMT2.shutdownSolver Bitwuzla
    Bitwuzla