    ------------------------------------------------------------------------
    -- |
    -- Module           : What4.Solver.Boolector
    -- Description      : Interface for running Boolector
    -- Copyright        : (c) Galois, Inc 2014-2020
    -- License          : BSD3
    -- Maintainer       : Rob Dockins <rdockins@galois.com>
    -- Stability        : provisional
    --
    -- This module provides an interface for running Boolector and parsing
    -- the results back.
    ------------------------------------------------------------------------
    {-# LANGUAGE CPP #-}
    {-# LANGUAGE FlexibleInstances #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE OverloadedStrings #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    module What4.Solver.Boolector
      ( Boolector(..)
      , boolectorPath
      , boolectorTimeout
      , boolectorOptions
      , boolectorAdapter
      , runBoolectorInOverride
      , withBoolector
      , boolectorFeatures
      ) 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 Boolector = Boolector deriving Int -> Boolector -> ShowS
    [Boolector] -> ShowS
    Boolector -> String
    (Int -> Boolector -> ShowS)
    -> (Boolector -> String)
    -> ([Boolector] -> ShowS)
    -> Show Boolector
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> Boolector -> ShowS
    showsPrec :: Int -> Boolector -> ShowS
    $cshow :: Boolector -> String
    show :: Boolector -> String
    $cshowList :: [Boolector] -> ShowS
    showList :: [Boolector] -> ShowS
    Show

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

    boolectorPathOLD :: ConfigOption (BaseStringType Unicode)
    boolectorPathOLD :: ConfigOption (BaseStringType Unicode)
    boolectorPathOLD = 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
    "boolector_path"

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

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

    boolectorOptions :: [ConfigDesc]
    boolectorOptions :: [ConfigDesc]
    boolectorOptions =
      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 boolector 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
    "boolector"))
          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)
    boolectorPath
          bp2 :: ConfigDesc
    bp2 = [ConfigDesc] -> ConfigDesc -> ConfigDesc
    deprecatedOpt [ConfigDesc
    bp] (ConfigDesc -> ConfigDesc) -> ConfigDesc -> ConfigDesc
    forall a b. (a -> b) -> a -> b
    $ ConfigOption (BaseStringType Unicode) -> ConfigDesc
    bpOpt ConfigOption (BaseStringType Unicode)
    boolectorPathOLD
      in [ ConfigDesc
    bp, ConfigDesc
    bp2
         , ConfigOption BaseIntegerType -> ConfigDesc
    mkTmo ConfigOption BaseIntegerType
    boolectorTimeout
         , (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
    boolectorStrictParsing) ConfigDesc
    strictSMTParseOpt
         ] [ConfigDesc] -> [ConfigDesc] -> [ConfigDesc]
    forall a. Semigroup a => a -> a -> a
    <> [ConfigDesc]
    SMT2.smtlib2Options

    boolectorAdapter :: SolverAdapter st
    boolectorAdapter :: forall (st :: Type -> Type). SolverAdapter st
    boolectorAdapter =
      SolverAdapter
      { solver_adapter_name :: String
    solver_adapter_name = String
    "boolector"
      , solver_adapter_config_options :: [ConfigDesc]
    solver_adapter_config_options = [ConfigDesc]
    boolectorOptions
      , 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
    runBoolectorInOverride
      , 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
    "Boolector" ProblemFeatures
    defaultWriteSMTLIB2Features
          (ConfigOption BaseBoolType -> Maybe (ConfigOption BaseBoolType)
    forall a. a -> Maybe a
    Just ConfigOption BaseBoolType
    boolectorStrictParsing)
      }

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

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

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

    boolectorFeatures :: ProblemFeatures
    boolectorFeatures :: ProblemFeatures
    boolectorFeatures = ProblemFeatures
    useSymbolicArrays
                    ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    forall a. Bits a => a -> a -> a
    .|. ProblemFeatures
    useBitvectors

    instance SMT2.SMTLib2GenericSolver Boolector where
      defaultSolverPath :: forall t (st :: Type -> Type) fs.
    Boolector -> ExprBuilder t st fs -> IO String
    defaultSolverPath Boolector
    _ = ConfigOption (BaseStringType Unicode) -> Config -> IO String
    findSolverPath ConfigOption (BaseStringType Unicode)
    boolectorPath (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.
    Boolector -> ExprBuilder t st fs -> IO [String]
    defaultSolverArgs Boolector
    _ ExprBuilder t st fs
    _ = [String] -> IO [String]
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return [String
    "--smt2", String
    "--incremental", String
    "--output-format=smt2", String
    "-e=0"]
      defaultFeatures :: Boolector -> ProblemFeatures
    defaultFeatures Boolector
    _ = ProblemFeatures
    boolectorFeatures
      setDefaultLogicAndOptions :: forall t. WriterConn t (Writer Boolector) -> IO ()
    setDefaultLogicAndOptions WriterConn t (Writer Boolector)
    writer = do
        WriterConn t (Writer Boolector) -> Logic -> IO ()
    forall a t.
    SMTLib2Tweaks a =>
    WriterConn t (Writer a) -> Logic -> IO ()
    SMT2.setLogic WriterConn t (Writer Boolector)
    writer Logic
    Syntax.allLogic
        WriterConn t (Writer Boolector) -> Bool -> IO ()
    forall a t.
    SMTLib2Tweaks a =>
    WriterConn t (Writer a) -> Bool -> IO ()
    SMT2.setProduceModels WriterConn t (Writer Boolector)
    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 Boolector) where
      startSolverProcess :: forall scope (st :: Type -> Type) fs.
    ProblemFeatures
    -> Maybe Handle
    -> ExprBuilder scope st fs
    -> IO (SolverProcess scope (Writer Boolector))
    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
    boolectorTimeout (ExprBuilder scope st fs -> Config
    forall sym. IsExprBuilder sym => sym -> Config
    getConfiguration ExprBuilder scope st fs
    sym))
        SMT2.startSolver Boolector SMT2.smtAckResult
                                setInteractiveLogicAndOptions
                                timeout
                                feat
                                (Just boolectorStrictParsing) mbIOh sym
      shutdownSolverProcess :: forall scope.
    SolverProcess scope (Writer Boolector) -> IO (ExitCode, Text)
    shutdownSolverProcess = Boolector
    -> SolverProcess scope (Writer Boolector) -> IO (ExitCode, Text)
    forall a t.
    SMTLib2GenericSolver a =>
    a -> SolverProcess t (Writer a) -> IO (ExitCode, Text)
    SMT2.shutdownSolver Boolector
    Boolector