    ------------------------------------------------------------------------
    -- |
    -- module           : What4.Solver.DReal
    -- Description      : Interface for running dReal
    -- Copyright        : (c) Galois, Inc 2014-2020
    -- License          : BSD3
    -- Maintainer       : Rob Dockins <rdockins@galois.com>
    -- Stability        : provisional
    --
    -- This module provides an interface for running dReal and parsing
    -- the results back.
    ------------------------------------------------------------------------
    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE OverloadedStrings #-}
    {-# LANGUAGE PatternGuards #-}
    module What4.Solver.DReal
      ( DReal(..)
      , DRealBindings
      , ExprRangeBindings
      , getAvgBindings
      , getBoundBindings
      , drealPath
      , drealOptions
      , drealAdapter
      , writeDRealSMT2File
      , runDRealInOverride
      ) where

    import           Control.Concurrent
    import           Control.Exception
    import           Control.Lens(folded)
    import           Control.Monad
    import           Data.Attoparsec.ByteString.Char8 hiding (try)
    import qualified Data.ByteString.UTF8 as UTF8
    import           Data.Map (Map)
    import qualified Data.Map as Map
    import           Data.Text.Encoding ( decodeUtf8 )
    import           Data.Text.Lazy (Text)
    import qualified Data.Text.Lazy as Text
    import qualified Data.Text.Lazy.Builder as Builder
    import           Numeric
    import           System.Exit
    import           System.IO
    import           System.IO.Error
    import qualified System.IO.Streams as Streams
    import qualified System.IO.Streams.Attoparsec as Streams
    import           System.Process

    import           What4.BaseTypes
    import           What4.Config
    import           What4.Solver.Adapter
    import           What4.Concrete
    import           What4.Interface
    import           What4.ProblemFeatures
    import           What4.SatResult
    import           What4.Expr.Builder
    import           What4.Expr.GroundEval
    import qualified What4.Protocol.SMTLib2 as SMT2
    import qualified What4.Protocol.SMTLib2.Response as RSP
    import qualified What4.Protocol.SMTWriter as SMTWriter
    import           What4.Utils.Process
    import           What4.Utils.Streams (logErrorStream)
    import           What4.Utils.HandleReader

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

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

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

    drealOptions :: [ConfigDesc]
    drealOptions :: [ConfigDesc]
    drealOptions =
      let dpOpt :: ConfigOption (BaseStringType Unicode) -> ConfigDesc
    dpOpt 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 dReal 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
    "dreal"))
          dp :: ConfigDesc
    dp = ConfigOption (BaseStringType Unicode) -> ConfigDesc
    dpOpt ConfigOption (BaseStringType Unicode)
    drealPath
      in [ ConfigDesc
    dp
         , [ConfigDesc] -> ConfigDesc -> ConfigDesc
    deprecatedOpt [ConfigDesc
    dp] (ConfigDesc -> ConfigDesc) -> ConfigDesc -> ConfigDesc
    forall a b. (a -> b) -> a -> b
    $ ConfigOption (BaseStringType Unicode) -> ConfigDesc
    dpOpt ConfigOption (BaseStringType Unicode)
    drealPathOLD
         ] [ConfigDesc] -> [ConfigDesc] -> [ConfigDesc]
    forall a. Semigroup a => a -> a -> a
    <> [ConfigDesc]
    SMT2.smtlib2Options

    drealAdapter :: SolverAdapter st
    drealAdapter :: forall (st :: Type -> Type). SolverAdapter st
    drealAdapter =
      SolverAdapter
      { solver_adapter_name :: String
    solver_adapter_name = String
    "dreal"
      , solver_adapter_config_options :: [ConfigDesc]
    solver_adapter_config_options = [ConfigDesc]
    drealOptions
      , 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
    sym LogData
    logData [BoolExpr t]
    ps SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a
    cont ->
          ExprBuilder t st fs
    -> LogData
    -> [BoolExpr t]
    -> (SatResult (WriterConn t (Writer DReal), DRealBindings) ()
        -> IO a)
    -> IO a
    forall t (st :: Type -> Type) fs a.
    ExprBuilder t st fs
    -> LogData
    -> [BoolExpr t]
    -> (SatResult (WriterConn t (Writer DReal), DRealBindings) ()
        -> IO a)
    -> IO a
    runDRealInOverride ExprBuilder t st fs
    sym LogData
    logData [BoolExpr t]
    ps ((SatResult (WriterConn t (Writer DReal), DRealBindings) ()
      -> IO a)
     -> IO a)
    -> (SatResult (WriterConn t (Writer DReal), DRealBindings) ()
        -> IO a)
    -> IO a
    forall a b. (a -> b) -> a -> b
    $ \SatResult (WriterConn t (Writer DReal), DRealBindings) ()
    res ->
             case SatResult (WriterConn t (Writer DReal), DRealBindings) ()
    res of
               Sat (WriterConn t (Writer DReal)
    c,DRealBindings
    m) -> do
                 evalFn <- WriterConn t (Writer DReal) -> DRealBindings -> IO (GroundEvalFn t)
    forall t.
    WriterConn t (Writer DReal) -> DRealBindings -> IO (GroundEvalFn t)
    getAvgBindings WriterConn t (Writer DReal)
    c DRealBindings
    m
                 rangeFn <- getBoundBindings c m
                 cont (Sat (evalFn, Just rangeFn))
               Unsat ()
    x -> SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a
    cont (() -> SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    forall mdl core. core -> SatResult mdl core
    Unsat ()
    x)
               SatResult (WriterConn t (Writer DReal), DRealBindings) ()
    Unknown -> SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a
    cont SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    forall mdl core. SatResult mdl core
    Unknown

      , solver_adapter_write_smt2 :: forall t fs. ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
    solver_adapter_write_smt2 = ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
    forall t fs. ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
    forall t (st :: Type -> Type) fs.
    ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
    writeDRealSMT2File
      }

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

    writeDRealSMT2File
       :: ExprBuilder t st fs
       -> Handle
       -> [BoolExpr t]
       -> IO ()
    writeDRealSMT2File :: forall t (st :: Type -> Type) fs.
    ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
    writeDRealSMT2File ExprBuilder t st fs
    sym Handle
    h [BoolExpr t]
    ps = do
      bindings <- ExprBuilder t st fs -> IO (SymbolVarBimap t)
    forall t (st :: Type -> Type) fs.
    ExprBuilder t st fs -> IO (SymbolVarBimap t)
    getSymbolVarBimap ExprBuilder t st fs
    sym
      out_str <- Streams.encodeUtf8 =<< Streams.handleToOutputStream h
      in_str <- Streams.nullInput
      let cfg = ExprBuilder t st fs -> Config
    forall sym. IsExprBuilder sym => sym -> Config
    getConfiguration ExprBuilder t st fs
    sym
      strictness <- maybe SMTWriter.Strict
                    (\ConcreteVal BaseBoolType
    c -> if ConcreteVal BaseBoolType -> Bool
    fromConcreteBool ConcreteVal BaseBoolType
    c
                           then ResponseStrictness
    SMTWriter.Strict
                           else ResponseStrictness
    SMTWriter.Lenient) <$>
                    (getOption =<< getOptionSetting RSP.strictSMTParsing cfg)
      c <- SMT2.newWriter DReal out_str in_str SMTWriter.nullAcknowledgementAction strictness "dReal"
              False useComputableReals False bindings
      SMT2.setProduceModels c True
      SMT2.setLogic c (SMT2.Logic "QF_NRA")
      forM_ ps (SMT2.assume c)
      SMT2.writeCheckSat c
      SMT2.writeExit c

    type DRealBindings = Map Text (Either Bool (Maybe Rational, Maybe Rational))

    getAvgBindings :: SMT2.WriterConn t (SMT2.Writer DReal)
                   -> DRealBindings
                   -> IO (GroundEvalFn t)
    getAvgBindings :: forall t.
    WriterConn t (Writer DReal) -> DRealBindings -> IO (GroundEvalFn t)
    getAvgBindings WriterConn t (Writer DReal)
    c DRealBindings
    m = do
      let evalBool :: Term -> m Bool
    evalBool Term
    tm =
            case Text
    -> DRealBindings
    -> Maybe (Either Bool (Maybe Rational, Maybe Rational))
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup (Builder -> Text
    Builder.toLazyText (Term -> Builder
    SMT2.renderTerm Term
    tm)) DRealBindings
    m of
              Just (Right (Maybe Rational, Maybe Rational)
    _) -> String -> m Bool
    forall a. String -> m a
    forall (m :: Type -> Type) a. MonadFail m => String -> m a
    fail String
    "Expected Boolean variable"
              Just (Left Bool
    b) -> Bool -> m Bool
    forall a. a -> m a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return Bool
    b
              Maybe (Either Bool (Maybe Rational, Maybe Rational))
    Nothing -> Bool -> m Bool
    forall a. a -> m a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return Bool
    False
          evalBV :: p -> p -> m a
    evalBV p
    _ p
    _ = String -> m a
    forall a. String -> m a
    forall (m :: Type -> Type) a. MonadFail m => String -> m a
    fail String
    "dReal does not support bitvectors."
          evalStr :: p -> m a
    evalStr p
    _ = String -> m a
    forall a. String -> m a
    forall (m :: Type -> Type) a. MonadFail m => String -> m a
    fail String
    "dReal does not support strings."
          evalReal :: Term -> m Rational
    evalReal Term
    tm = do
            case Text
    -> DRealBindings
    -> Maybe (Either Bool (Maybe Rational, Maybe Rational))
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup (Builder -> Text
    Builder.toLazyText (Term -> Builder
    SMT2.renderTerm Term
    tm)) DRealBindings
    m of
              Just (Right (Maybe Rational, Maybe Rational)
    vs) -> Rational -> m Rational
    forall a. a -> m a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return ((Maybe Rational, Maybe Rational) -> Rational
    drealAvgBinding (Maybe Rational, Maybe Rational)
    vs)
              Just (Left Bool
    _) -> String -> m Rational
    forall a. String -> m a
    forall (m :: Type -> Type) a. MonadFail m => String -> m a
    fail String
    "Expected Real variable"
              Maybe (Either Bool (Maybe Rational, Maybe Rational))
    Nothing -> Rational -> m Rational
    forall a. a -> m a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return Rational
    0
          evalFloat :: p -> p -> m a
    evalFloat p
    _ p
    _ = String -> m a
    forall a. String -> m a
    forall (m :: Type -> Type) a. MonadFail m => String -> m a
    fail String
    "dReal does not support floats."
      let evalFns :: SMTEvalFunctions (Writer DReal)
    evalFns = SMTWriter.SMTEvalFunctions { smtEvalBool :: Term (Writer DReal) -> IO Bool
    SMTWriter.smtEvalBool = Term -> IO Bool
    Term (Writer DReal) -> IO Bool
    forall {m :: Type -> Type}. MonadFail m => Term -> m Bool
    evalBool
                                               , smtEvalBV :: forall (w :: Nat). NatRepr w -> Term (Writer DReal) -> IO (BV w)
    SMTWriter.smtEvalBV = NatRepr w -> Term (Writer DReal) -> IO (BV w)
    forall (w :: Nat). NatRepr w -> Term (Writer DReal) -> IO (BV w)
    forall {m :: Type -> Type} {p} {p} {a}.
    MonadFail m =>
    p -> p -> m a
    evalBV
                                               , smtEvalReal :: Term (Writer DReal) -> IO Rational
    SMTWriter.smtEvalReal = Term -> IO Rational
    Term (Writer DReal) -> IO Rational
    forall {m :: Type -> Type}. MonadFail m => Term -> m Rational
    evalReal
                                               , smtEvalFloat :: forall (fpp :: FloatPrecision).
    FloatPrecisionRepr fpp
    -> Term (Writer DReal) -> IO (BV (FloatPrecisionBits fpp))
    SMTWriter.smtEvalFloat = FloatPrecisionRepr fpp
    -> Term (Writer DReal) -> IO (BV (FloatPrecisionBits fpp))
    forall (fpp :: FloatPrecision).
    FloatPrecisionRepr fpp
    -> Term (Writer DReal) -> IO (BV (FloatPrecisionBits fpp))
    forall {m :: Type -> Type} {p} {p} {a}.
    MonadFail m =>
    p -> p -> m a
    evalFloat
                                               , smtEvalBvArray :: Maybe (SMTEvalBVArrayWrapper (Writer DReal))
    SMTWriter.smtEvalBvArray = Maybe (SMTEvalBVArrayWrapper (Writer DReal))
    forall a. Maybe a
    Nothing
                                               , smtEvalString :: Term (Writer DReal) -> IO Text
    SMTWriter.smtEvalString = Term -> IO Text
    Term (Writer DReal) -> IO Text
    forall {m :: Type -> Type} {p} {a}. MonadFail m => p -> m a
    evalStr
                                               }
      WriterConn t (Writer DReal)
    -> SMTEvalFunctions (Writer DReal) -> IO (GroundEvalFn t)
    forall t h.
    SMTWriter h =>
    WriterConn t h -> SMTEvalFunctions h -> IO (GroundEvalFn t)
    SMTWriter.smtExprGroundEvalFn WriterConn t (Writer DReal)
    c SMTEvalFunctions (Writer DReal)
    evalFns

    getMaybeEval :: ((Maybe Rational, Maybe Rational) -> Maybe Rational)
                 -> SMT2.WriterConn t (SMT2.Writer DReal)
                 -> DRealBindings
                 -> IO (RealExpr t -> IO (Maybe Rational))
    getMaybeEval :: forall t.
    ((Maybe Rational, Maybe Rational) -> Maybe Rational)
    -> WriterConn t (Writer DReal)
    -> DRealBindings
    -> IO (RealExpr t -> IO (Maybe Rational))
    getMaybeEval (Maybe Rational, Maybe Rational) -> Maybe Rational
    proj WriterConn t (Writer DReal)
    c DRealBindings
    m = do
      let evalBool :: Term -> m Bool
    evalBool Term
    tm =
            case Text
    -> DRealBindings
    -> Maybe (Either Bool (Maybe Rational, Maybe Rational))
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup (Builder -> Text
    Builder.toLazyText (Term -> Builder
    SMT2.renderTerm Term
    tm)) DRealBindings
    m of
              Just (Right (Maybe Rational, Maybe Rational)
    _) -> String -> m Bool
    forall a. String -> m a
    forall (m :: Type -> Type) a. MonadFail m => String -> m a
    fail String
    "expected boolean term"
              Just (Left Bool
    b) -> Bool -> m Bool
    forall a. a -> m a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return Bool
    b
              Maybe (Either Bool (Maybe Rational, Maybe Rational))
    Nothing -> String -> m Bool
    forall a. String -> m a
    forall (m :: Type -> Type) a. MonadFail m => String -> m a
    fail String
    "unbound boolean variable"
          evalBV :: p -> p -> m a
    evalBV p
    _ p
    _ = String -> m a
    forall a. String -> m a
    forall (m :: Type -> Type) a. MonadFail m => String -> m a
    fail String
    "dReal does not return Bitvector values."
          evalStr :: p -> m a
    evalStr p
    _ = String -> m a
    forall a. String -> m a
    forall (m :: Type -> Type) a. MonadFail m => String -> m a
    fail String
    "dReal does not return string values."
          evalReal :: Term -> IO Rational
    evalReal Term
    tm = do
            case Text
    -> DRealBindings
    -> Maybe (Either Bool (Maybe Rational, Maybe Rational))
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup (Builder -> Text
    Builder.toLazyText (Term -> Builder
    SMT2.renderTerm Term
    tm)) DRealBindings
    m of
              Just (Right (Maybe Rational, Maybe Rational)
    v) ->
                case (Maybe Rational, Maybe Rational) -> Maybe Rational
    proj (Maybe Rational, Maybe Rational)
    v of
                  Just Rational
    x  -> Rational -> IO Rational
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return Rational
    x
                  Maybe Rational
    Nothing -> IOError -> IO Rational
    forall e a. (HasCallStack, Exception e) => e -> IO a
    throwIO (String -> IOError
    userError String
    "unbound")
              Just (Left Bool
    _) -> String -> IO Rational
    forall a. String -> IO a
    forall (m :: Type -> Type) a. MonadFail m => String -> m a
    fail String
    "expected real variable"
              Maybe (Either Bool (Maybe Rational, Maybe Rational))
    Nothing -> IOError -> IO Rational
    forall e a. (HasCallStack, Exception e) => e -> IO a
    throwIO (String -> IOError
    userError String
    "unbound")
          evalFloat :: p -> p -> m a
    evalFloat p
    _ p
    _ = String -> m a
    forall a. String -> m a
    forall (m :: Type -> Type) a. MonadFail m => String -> m a
    fail String
    "dReal does not support floats."
      let evalFns :: SMTEvalFunctions (Writer DReal)
    evalFns = SMTWriter.SMTEvalFunctions { smtEvalBool :: Term (Writer DReal) -> IO Bool
    SMTWriter.smtEvalBool = Term -> IO Bool
    Term (Writer DReal) -> IO Bool
    forall {m :: Type -> Type}. MonadFail m => Term -> m Bool
    evalBool
                                               , smtEvalBV :: forall (w :: Nat). NatRepr w -> Term (Writer DReal) -> IO (BV w)
    SMTWriter.smtEvalBV = NatRepr w -> Term (Writer DReal) -> IO (BV w)
    forall (w :: Nat). NatRepr w -> Term (Writer DReal) -> IO (BV w)
    forall {m :: Type -> Type} {p} {p} {a}.
    MonadFail m =>
    p -> p -> m a
    evalBV
                                               , smtEvalReal :: Term (Writer DReal) -> IO Rational
    SMTWriter.smtEvalReal = Term -> IO Rational
    Term (Writer DReal) -> IO Rational
    evalReal
                                               , smtEvalFloat :: forall (fpp :: FloatPrecision).
    FloatPrecisionRepr fpp
    -> Term (Writer DReal) -> IO (BV (FloatPrecisionBits fpp))
    SMTWriter.smtEvalFloat = FloatPrecisionRepr fpp
    -> Term (Writer DReal) -> IO (BV (FloatPrecisionBits fpp))
    forall (fpp :: FloatPrecision).
    FloatPrecisionRepr fpp
    -> Term (Writer DReal) -> IO (BV (FloatPrecisionBits fpp))
    forall {m :: Type -> Type} {p} {p} {a}.
    MonadFail m =>
    p -> p -> m a
    evalFloat
                                               , smtEvalBvArray :: Maybe (SMTEvalBVArrayWrapper (Writer DReal))
    SMTWriter.smtEvalBvArray = Maybe (SMTEvalBVArrayWrapper (Writer DReal))
    forall a. Maybe a
    Nothing
                                               , smtEvalString :: Term (Writer DReal) -> IO Text
    SMTWriter.smtEvalString = Term -> IO Text
    Term (Writer DReal) -> IO Text
    forall {m :: Type -> Type} {p} {a}. MonadFail m => p -> m a
    evalStr
                                               }
      GroundEvalFn evalFn <- WriterConn t (Writer DReal)
    -> SMTEvalFunctions (Writer DReal) -> IO (GroundEvalFn t)
    forall t h.
    SMTWriter h =>
    WriterConn t h -> SMTEvalFunctions h -> IO (GroundEvalFn t)
    SMTWriter.smtExprGroundEvalFn WriterConn t (Writer DReal)
    c SMTEvalFunctions (Writer DReal)
    evalFns
      let handler IOError
    e | IOError -> Bool
    isUserError IOError
    e
                    , IOError -> String
    ioeGetErrorString IOError
    e String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == String
    "unbound" = do
            Maybe a -> IO (Maybe a)
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return Maybe a
    forall a. Maybe a
    Nothing
          handler IOError
    e = IOError -> IO (Maybe a)
    forall e a. (HasCallStack, Exception e) => e -> IO a
    throwIO IOError
    e
      return $ \RealExpr t
    elt -> (Rational -> Maybe Rational
    forall a. a -> Maybe a
    Just (Rational -> Maybe Rational) -> IO Rational -> IO (Maybe Rational)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> RealExpr t -> IO (GroundValue BaseRealType)
    forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
    evalFn RealExpr t
    elt) IO (Maybe Rational)
    -> (IOError -> IO (Maybe Rational)) -> IO (Maybe Rational)
    forall e a. Exception e => IO a -> (e -> IO a) -> IO a
    `catch` IOError -> IO (Maybe Rational)
    forall {a}. IOError -> IO (Maybe a)
    handler

    getBoundBindings :: SMT2.WriterConn t (SMT2.Writer DReal)
                     -> DRealBindings
                     -> IO (ExprRangeBindings t)
    getBoundBindings :: forall t.
    WriterConn t (Writer DReal)
    -> DRealBindings -> IO (ExprRangeBindings t)
    getBoundBindings WriterConn t (Writer DReal)
    c DRealBindings
    m = do
      l_evalFn <- ((Maybe Rational, Maybe Rational) -> Maybe Rational)
    -> WriterConn t (Writer DReal)
    -> DRealBindings
    -> IO (RealExpr t -> IO (Maybe Rational))
    forall t.
    ((Maybe Rational, Maybe Rational) -> Maybe Rational)
    -> WriterConn t (Writer DReal)
    -> DRealBindings
    -> IO (RealExpr t -> IO (Maybe Rational))
    getMaybeEval (Maybe Rational, Maybe Rational) -> Maybe Rational
    forall a b. (a, b) -> a
    fst WriterConn t (Writer DReal)
    c DRealBindings
    m
      h_evalFn <- getMaybeEval snd c m
      return $ \RealExpr t
    e -> (,) (Maybe Rational
     -> Maybe Rational -> (Maybe Rational, Maybe Rational))
    -> IO (Maybe Rational)
    -> IO (Maybe Rational -> (Maybe Rational, Maybe Rational))
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> RealExpr t -> IO (Maybe Rational)
    l_evalFn RealExpr t
    e IO (Maybe Rational -> (Maybe Rational, Maybe Rational))
    -> IO (Maybe Rational) -> IO (Maybe Rational, Maybe Rational)
    forall a b. IO (a -> b) -> IO a -> IO b
    forall (f :: Type -> Type) a b.
    Applicative f =>
    f (a -> b) -> f a -> f b
    <*> RealExpr t -> IO (Maybe Rational)
    h_evalFn RealExpr t
    e

    drealAvgBinding :: (Maybe Rational, Maybe Rational) -> Rational
    drealAvgBinding :: (Maybe Rational, Maybe Rational) -> Rational
    drealAvgBinding (Maybe Rational
    Nothing, Maybe Rational
    Nothing) = Rational
    0
    drealAvgBinding (Maybe Rational
    Nothing, Just Rational
    r)  = Rational
    r
    drealAvgBinding (Just Rational
    r, Maybe Rational
    Nothing)  = Rational
    r
    drealAvgBinding (Just Rational
    r1, Just Rational
    r2) = (Rational
    r1Rational -> Rational -> Rational
    forall a. Num a => a -> a -> a
    +Rational
    r2)Rational -> Rational -> Rational
    forall a. Fractional a => a -> a -> a
    /Rational
    2

    dRealResponse :: Parser (SatResult [(Text, Either Bool (Maybe Rational, Maybe Rational))] ())
    dRealResponse :: Parser
      (SatResult
         [(Text, Either Bool (Maybe Rational, Maybe Rational))] ())
    dRealResponse =
      [Parser
       (SatResult
          [(Text, Either Bool (Maybe Rational, Maybe Rational))] ())]
    -> Parser
         (SatResult
            [(Text, Either Bool (Maybe Rational, Maybe Rational))] ())
    forall (t :: Type -> Type) (m :: Type -> Type) a.
    (Foldable t, MonadPlus m) =>
    t (m a) -> m a
    msum
      [ do _ <- ByteString -> Parser ByteString
    string ByteString
    "unsat"
           return (Unsat ())

      , do _ <- ByteString -> Parser ByteString
    string ByteString
    "unknown"
           return Unknown

      , do _ <- ByteString -> Parser ByteString
    string ByteString
    "delta-sat"
           _ <- takeTill (\Char
    c -> Char
    c Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char
    '\n' Bool -> Bool -> Bool
    || Char
    c Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char
    '\r')
           endOfLine
           bs <- many' dRealBinding
           endOfInput
           return (Sat bs)
      ]

    dRealBinding :: Parser (Text, Either Bool (Maybe Rational, Maybe Rational))
    dRealBinding :: Parser
      ByteString (Text, Either Bool (Maybe Rational, Maybe Rational))
    dRealBinding = do
        Parser ()
    skipSpace

        nm <- (Char -> Bool) -> Parser ByteString
    takeWhile1 (Bool -> Bool
    not (Bool -> Bool) -> (Char -> Bool) -> Char -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Char -> Bool
    isSpace)

        skipSpace
        _ <- char ':'
        skipSpace

        val <- msum
          [ do _ <- string "False"
               skipSpace
               return (Left False)

          , do _ <- string "True"
               skipSpace
               return (Left True)

          , do lo <- dRealLoBound

               skipSpace
               _ <- char ','
               skipSpace

               hi <- dRealHiBound

               skipSpace
               _ <- option ' ' (char ';')
               skipSpace
               return (Right (lo,hi))
          ]
        return (Text.fromStrict (decodeUtf8 nm),val)

    dRealLoBound :: Parser (Maybe Rational)
    dRealLoBound :: Parser (Maybe Rational)
    dRealLoBound = [Parser (Maybe Rational)] -> Parser (Maybe Rational)
    forall (f :: Type -> Type) a. Alternative f => [f a] -> f a
    choice
       [ ByteString -> Parser ByteString
    string ByteString
    "(-inf" Parser ByteString
    -> Parser (Maybe Rational) -> Parser (Maybe Rational)
    forall a b.
    Parser ByteString a -> Parser ByteString b -> Parser ByteString b
    forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
    >> Maybe Rational -> Parser (Maybe Rational)
    forall a. a -> Parser ByteString a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return Maybe Rational
    forall a. Maybe a
    Nothing
       , do _ <- Char -> Parser Char
    char Char
    '['
            sign <- option 1 (char '-' >> return (-1))
            num <- takeWhile1 (\Char
    c -> Char
    c Char -> String -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: Type -> Type) a.
    (Foldable t, Eq a) =>
    a -> t a -> Bool
    `elem` (String
    "0123456789+-eE." :: String))
            case readFloat (UTF8.toString num) of
              (Rational
    x,String
    ""):[(Rational, String)]
    _ -> Maybe Rational -> Parser (Maybe Rational)
    forall a. a -> Parser ByteString a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (Maybe Rational -> Parser (Maybe Rational))
    -> Maybe Rational -> Parser (Maybe Rational)
    forall a b. (a -> b) -> a -> b
    $ Rational -> Maybe Rational
    forall a. a -> Maybe a
    Just (Rational
    sign Rational -> Rational -> Rational
    forall a. Num a => a -> a -> a
    * Rational
    x)
              [(Rational, String)]
    _ -> String -> Parser (Maybe Rational)
    forall a. String -> Parser ByteString a
    forall (m :: Type -> Type) a. MonadFail m => String -> m a
    fail String
    "expected rational bound"
       ]

    dRealHiBound :: Parser (Maybe Rational)
    dRealHiBound :: Parser (Maybe Rational)
    dRealHiBound = [Parser (Maybe Rational)] -> Parser (Maybe Rational)
    forall (f :: Type -> Type) a. Alternative f => [f a] -> f a
    choice
       [ ByteString -> Parser ByteString
    string ByteString
    "inf)" Parser ByteString
    -> Parser (Maybe Rational) -> Parser (Maybe Rational)
    forall a b.
    Parser ByteString a -> Parser ByteString b -> Parser ByteString b
    forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
    >> Maybe Rational -> Parser (Maybe Rational)
    forall a. a -> Parser ByteString a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return Maybe Rational
    forall a. Maybe a
    Nothing
       , do sign <- Rational
    -> Parser ByteString Rational -> Parser ByteString Rational
    forall (f :: Type -> Type) a. Alternative f => a -> f a -> f a
    option Rational
    1 (Char -> Parser Char
    char Char
    '-' Parser Char
    -> Parser ByteString Rational -> Parser ByteString Rational
    forall a b.
    Parser ByteString a -> Parser ByteString b -> Parser ByteString b
    forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
    >> Rational -> Parser ByteString Rational
    forall a. a -> Parser ByteString a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (-Rational
    1))
            num <- takeWhile1 (\Char
    c -> Char
    c Char -> String -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: Type -> Type) a.
    (Foldable t, Eq a) =>
    a -> t a -> Bool
    `elem` (String
    "0123456789+-eE." :: String))
            _ <- char ']'
            case readFloat (UTF8.toString num) of
              (Rational
    x,String
    ""):[(Rational, String)]
    _ -> Maybe Rational -> Parser (Maybe Rational)
    forall a. a -> Parser ByteString a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (Maybe Rational -> Parser (Maybe Rational))
    -> Maybe Rational -> Parser (Maybe Rational)
    forall a b. (a -> b) -> a -> b
    $ Rational -> Maybe Rational
    forall a. a -> Maybe a
    Just (Rational
    sign Rational -> Rational -> Rational
    forall a. Num a => a -> a -> a
    * Rational
    x)
              [(Rational, String)]
    _ -> String -> Parser (Maybe Rational)
    forall a. String -> Parser ByteString a
    forall (m :: Type -> Type) a. MonadFail m => String -> m a
    fail String
    "expected rational bound"
       ]

    runDRealInOverride
       :: ExprBuilder t st fs
       -> LogData
       -> [BoolExpr t]   -- ^ propositions to check
       -> (SatResult (SMT2.WriterConn t (SMT2.Writer DReal), DRealBindings) () -> IO a)
       -> IO a
    runDRealInOverride :: forall t (st :: Type -> Type) fs a.
    ExprBuilder t st fs
    -> LogData
    -> [BoolExpr t]
    -> (SatResult (WriterConn t (Writer DReal), DRealBindings) ()
        -> IO a)
    -> IO a
    runDRealInOverride ExprBuilder t st fs
    sym LogData
    logData [BoolExpr t]
    ps SatResult (WriterConn t (Writer DReal), DRealBindings) () -> IO a
    modelFn = do
      p <- ExprBuilder t st fs
    -> Fold [BoolExpr t] (Pred (ExprBuilder t st fs))
    -> [BoolExpr t]
    -> IO (Pred (ExprBuilder t st fs))
    forall sym s.
    IsExprBuilder sym =>
    sym -> Fold s (Pred sym) -> s -> IO (Pred sym)
    andAllOf ExprBuilder t st fs
    sym (Pred (ExprBuilder t st fs) -> f (Pred (ExprBuilder t st fs)))
    -> [BoolExpr t] -> f [BoolExpr t]
    (BoolExpr t -> f (BoolExpr t)) -> [BoolExpr t] -> f [BoolExpr t]
    Fold [BoolExpr t] (Pred (ExprBuilder t st fs))
    forall (f :: Type -> Type) a. Foldable f => IndexedFold Int (f a) a
    IndexedFold Int [BoolExpr t] (BoolExpr t)
    folded [BoolExpr t]
    ps
      solver_path <- findSolverPath drealPath (getConfiguration sym)
      logSolverEvent sym
        (SolverStartSATQuery $ SolverStartSATQueryRec
        { satQuerySolverName = "dReal"
        , satQueryReason = logReason logData
        })
      withProcessHandles solver_path ["--model", "--in", "--format", "smt2"] Nothing $ \(Handle
    in_h, Handle
    out_h, Handle
    err_h, ProcessHandle
    ph) -> do

          -- Log stderr to output.
          err_stream <- Handle -> IO (InputStream ByteString)
    Streams.handleToInputStream Handle
    err_h
          void $ forkIO $ logErrorStream err_stream (logCallbackVerbose logData 2)

          -- Write SMTLIB to standard input.
          logCallbackVerbose logData 2 "Sending Satisfiability problem to dReal"
          -- dReal does not support (define-fun ...)
          bindings <- getSymbolVarBimap sym

          out_str  <-
            case logHandle logData of
              Maybe Handle
    Nothing -> OutputStream ByteString -> IO (OutputStream Text)
    Streams.encodeUtf8 (OutputStream ByteString -> IO (OutputStream Text))
    -> IO (OutputStream ByteString) -> IO (OutputStream Text)
    forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Handle -> IO (OutputStream ByteString)
    Streams.handleToOutputStream Handle
    in_h
              Just Handle
    aux_h ->
                do aux_str <- Handle -> IO (OutputStream ByteString)
    Streams.handleToOutputStream Handle
    aux_h
                   Streams.encodeUtf8 =<< teeOutputStream aux_str =<< Streams.handleToOutputStream in_h

          in_str <- Streams.nullInput

          let cfg = ExprBuilder t st fs -> Config
    forall sym. IsExprBuilder sym => sym -> Config
    getConfiguration ExprBuilder t st fs
    sym
          strictness <- maybe SMTWriter.Strict
                        (\ConcreteVal BaseBoolType
    c -> if ConcreteVal BaseBoolType -> Bool
    fromConcreteBool ConcreteVal BaseBoolType
    c
                               then ResponseStrictness
    SMTWriter.Strict
                               else ResponseStrictness
    SMTWriter.Lenient) <$>
                        (getOption =<< getOptionSetting RSP.strictSMTParsing cfg)

          c <- SMT2.newWriter DReal out_str in_str SMTWriter.nullAcknowledgementAction strictness "dReal"
                 False useComputableReals False bindings

          -- Set the dReal default logic
          SMT2.setLogic c (SMT2.Logic "QF_NRA")
          SMT2.assume c p

          -- Create stream for output from solver.
          out_stream <- Streams.handleToInputStream out_h

          -- dReal wants to parse its entire input, all the way through <EOF> before it does anything
          -- Also (apparently) you _must_ include the exit command to get any response at all...
          SMT2.writeCheckSat c
          SMT2.writeExit c
          hClose in_h

          logCallbackVerbose logData 2 "Parsing result from solver"

          msat_result <- try $ Streams.parseFromStream dRealResponse out_stream

          res <-
            case msat_result of
              Left ex :: ParseException
    ex@Streams.ParseException{} -> String
    -> IO (SatResult (WriterConn t (Writer DReal), DRealBindings) ())
    forall a. String -> IO a
    forall (m :: Type -> Type) a. MonadFail m => String -> m a
    fail (String
     -> IO (SatResult (WriterConn t (Writer DReal), DRealBindings) ()))
    -> String
    -> IO (SatResult (WriterConn t (Writer DReal), DRealBindings) ())
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [String
    "Could not parse dReal result.", ParseException -> String
    forall e. Exception e => e -> String
    displayException ParseException
    ex]
              Right (Unsat ()) -> SatResult (WriterConn t (Writer DReal), DRealBindings) ()
    -> IO (SatResult (WriterConn t (Writer DReal), DRealBindings) ())
    forall a. a -> IO a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (() -> SatResult (WriterConn t (Writer DReal), DRealBindings) ()
    forall mdl core. core -> SatResult mdl core
    Unsat ())
              Right SatResult [(Text, Either Bool (Maybe Rational, Maybe Rational))] ()
    Unknown    -> SatResult (WriterConn t (Writer DReal), DRealBindings) ()
    -> IO (SatResult (WriterConn t (Writer DReal), DRealBindings) ())
    forall a. a -> IO a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure SatResult (WriterConn t (Writer DReal), DRealBindings) ()
    forall mdl core. SatResult mdl core
    Unknown
              Right (Sat [(Text, Either Bool (Maybe Rational, Maybe Rational))]
    bs)   -> SatResult (WriterConn t (Writer DReal), DRealBindings) ()
    -> IO (SatResult (WriterConn t (Writer DReal), DRealBindings) ())
    forall a. a -> IO a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure ((WriterConn t (Writer DReal), DRealBindings)
    -> SatResult (WriterConn t (Writer DReal), DRealBindings) ()
    forall mdl core. mdl -> SatResult mdl core
    Sat (WriterConn t (Writer DReal)
    c, [(Text, Either Bool (Maybe Rational, Maybe Rational))]
    -> DRealBindings
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList [(Text, Either Bool (Maybe Rational, Maybe Rational))]
    bs))

          r <- modelFn res

          -- Check error code.
          logCallbackVerbose logData 2 "Waiting for dReal to exit"

          ec <- waitForProcess ph
          case ec of
            ExitCode
    ExitSuccess -> do
              -- Return result.
              LogData -> Int -> String -> IO ()
    logCallbackVerbose LogData
    logData Int
    2 String
    "dReal terminated."

              ExprBuilder t st fs -> SolverEvent -> IO ()
    forall sym. IsExprBuilder sym => sym -> SolverEvent -> IO ()
    logSolverEvent ExprBuilder t st fs
    sym
                 (SolverEndSATQuery -> SolverEvent
    SolverEndSATQuery (SolverEndSATQuery -> SolverEvent)
    -> SolverEndSATQuery -> SolverEvent
    forall a b. (a -> b) -> a -> b
    $ SolverEndSATQueryRec
                 { satQueryResult :: SatResult () ()
    satQueryResult = SatResult (WriterConn t (Writer DReal), DRealBindings) ()
    -> SatResult () ()
    forall a b. SatResult a b -> SatResult () ()
    forgetModelAndCore SatResult (WriterConn t (Writer DReal), DRealBindings) ()
    res
                 , satQueryError :: Maybe String
    satQueryError  = Maybe String
    forall a. Maybe a
    Nothing
                 })

              a -> IO a
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return a
    r
            ExitFailure Int
    exit_code ->
              String -> IO a
    forall a. String -> IO a
    forall (m :: Type -> Type) a. MonadFail m => String -> m a
    fail (String -> IO a) -> String -> IO a
    forall a b. (a -> b) -> a -> b
    $ String
    "dReal exited with unexpected code: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    exit_code