    ------------------------------------------------------------------------
    -- |
    -- 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
                 GroundEvalFn t
    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
                 ExprRangeBindings t
    rangeFn <- WriterConn t (Writer DReal)
    -> DRealBindings -> IO (ExprRangeBindings t)
    forall t.
    WriterConn t (Writer DReal)
    -> DRealBindings -> IO (ExprRangeBindings t)
    getBoundBindings WriterConn t (Writer DReal)
    c DRealBindings
    m
                 SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a
    cont ((GroundEvalFn t, Maybe (ExprRangeBindings t))
    -> SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    forall mdl core. mdl -> SatResult mdl core
    Sat (GroundEvalFn t
    evalFn, ExprRangeBindings t -> Maybe (ExprRangeBindings t)
    forall a. a -> Maybe a
    Just ExprRangeBindings t
    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
      SymbolVarBimap t
    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
      OutputStream Text
    out_str <- 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
    h
      InputStream Text
    in_str <- IO (InputStream Text)
    forall a. IO (InputStream a)
    Streams.nullInput
      let cfg :: Config
    cfg = ExprBuilder t st fs -> Config
    forall sym. IsExprBuilder sym => sym -> Config
    getConfiguration ExprBuilder t st fs
    sym
      ResponseStrictness
    strictness <- ResponseStrictness
    -> (ConcreteVal BaseBoolType -> ResponseStrictness)
    -> Maybe (ConcreteVal BaseBoolType)
    -> ResponseStrictness
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe ResponseStrictness
    SMTWriter.Strict
                    (\ConcreteVal BaseBoolType
    c -> if ConcreteVal BaseBoolType -> Bool
    fromConcreteBool ConcreteVal BaseBoolType
    c
                           then ResponseStrictness
    SMTWriter.Strict
                           else ResponseStrictness
    SMTWriter.Lenient) (Maybe (ConcreteVal BaseBoolType) -> ResponseStrictness)
    -> IO (Maybe (ConcreteVal BaseBoolType)) -> IO ResponseStrictness
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$>
                    (OptionSetting BaseBoolType -> IO (Maybe (ConcreteVal BaseBoolType))
    forall (tp :: BaseType).
    OptionSetting tp -> IO (Maybe (ConcreteVal tp))
    getOption (OptionSetting BaseBoolType
     -> IO (Maybe (ConcreteVal BaseBoolType)))
    -> IO (OptionSetting BaseBoolType)
    -> IO (Maybe (ConcreteVal BaseBoolType))
    forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ConfigOption BaseBoolType
    -> Config -> IO (OptionSetting BaseBoolType)
    forall (tp :: BaseType).
    ConfigOption tp -> Config -> IO (OptionSetting tp)
    getOptionSetting ConfigOption BaseBoolType
    RSP.strictSMTParsing Config
    cfg)
      WriterConn t (Writer DReal)
    c <- DReal
    -> OutputStream Text
    -> InputStream Text
    -> AcknowledgementAction t (Writer DReal)
    -> ResponseStrictness
    -> String
    -> Bool
    -> ProblemFeatures
    -> Bool
    -> SymbolVarBimap t
    -> IO (WriterConn t (Writer DReal))
    forall a t.
    a
    -> OutputStream Text
    -> InputStream Text
    -> AcknowledgementAction t (Writer a)
    -> ResponseStrictness
    -> String
    -> Bool
    -> ProblemFeatures
    -> Bool
    -> SymbolVarBimap t
    -> IO (WriterConn t (Writer a))
    SMT2.newWriter DReal
    DReal OutputStream Text
    out_str InputStream Text
    in_str AcknowledgementAction t (Writer DReal)
    forall t h. AcknowledgementAction t h
    SMTWriter.nullAcknowledgementAction ResponseStrictness
    strictness String
    "dReal"
              Bool
    False ProblemFeatures
    useComputableReals Bool
    False SymbolVarBimap t
    bindings
      WriterConn t (Writer DReal) -> Bool -> IO ()
    forall a t.
    SMTLib2Tweaks a =>
    WriterConn t (Writer a) -> Bool -> IO ()
    SMT2.setProduceModels WriterConn t (Writer DReal)
    c Bool
    True
      WriterConn t (Writer DReal) -> Logic -> IO ()
    forall a t.
    SMTLib2Tweaks a =>
    WriterConn t (Writer a) -> Logic -> IO ()
    SMT2.setLogic WriterConn t (Writer DReal)
    c (Builder -> Logic
    SMT2.Logic Builder
    "QF_NRA")
      [BoolExpr t] -> (BoolExpr t -> IO ()) -> IO ()
    forall (t :: Type -> Type) (m :: Type -> Type) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [BoolExpr t]
    ps (WriterConn t (Writer DReal) -> BoolExpr t -> IO ()
    forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
    SMT2.assume WriterConn t (Writer DReal)
    c)
      WriterConn t (Writer DReal) -> IO ()
    forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
    SMT2.writeCheckSat WriterConn t (Writer DReal)
    c
      WriterConn t (Writer DReal) -> IO ()
    forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
    SMT2.writeExit WriterConn t (Writer DReal)
    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. 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. 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 forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
    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 -> IO (Maybe a)
    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. Exception e => e -> IO a
    throwIO IOError
    e
      (RealExpr t -> IO (Maybe Rational))
    -> IO (RealExpr t -> IO (Maybe Rational))
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return ((RealExpr t -> IO (Maybe Rational))
     -> IO (RealExpr t -> IO (Maybe Rational)))
    -> (RealExpr t -> IO (Maybe Rational))
    -> IO (RealExpr t -> IO (Maybe Rational))
    forall a b. (a -> b) -> a -> b
    $ \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
      RealExpr t -> IO (Maybe Rational)
    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
      RealExpr t -> IO (Maybe Rational)
    h_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) -> b
    snd WriterConn t (Writer DReal)
    c DRealBindings
    m
      ExprRangeBindings t -> IO (ExprRangeBindings t)
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (ExprRangeBindings t -> IO (ExprRangeBindings t))
    -> ExprRangeBindings t -> IO (ExprRangeBindings t)
    forall a b. (a -> b) -> a -> b
    $ \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
    _ <- ByteString -> Parser ByteString
    string ByteString
    "unsat"
           SatResult [(Text, Either Bool (Maybe Rational, Maybe Rational))] ()
    -> Parser
         (SatResult
            [(Text, Either Bool (Maybe Rational, Maybe Rational))] ())
    forall a. a -> Parser ByteString a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (()
    -> SatResult
         [(Text, Either Bool (Maybe Rational, Maybe Rational))] ()
    forall mdl core. core -> SatResult mdl core
    Unsat ())

      , do ByteString
    _ <- ByteString -> Parser ByteString
    string ByteString
    "unknown"
           SatResult [(Text, Either Bool (Maybe Rational, Maybe Rational))] ()
    -> Parser
         (SatResult
            [(Text, Either Bool (Maybe Rational, Maybe Rational))] ())
    forall a. a -> Parser ByteString a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return SatResult [(Text, Either Bool (Maybe Rational, Maybe Rational))] ()
    forall mdl core. SatResult mdl core
    Unknown

      , do ByteString
    _ <- ByteString -> Parser ByteString
    string ByteString
    "delta-sat"
           ByteString
    _ <- (Char -> Bool) -> Parser ByteString
    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')
           Parser ()
    endOfLine
           [(Text, Either Bool (Maybe Rational, Maybe Rational))]
    bs <- Parser
      ByteString (Text, Either Bool (Maybe Rational, Maybe Rational))
    -> Parser
         ByteString [(Text, Either Bool (Maybe Rational, Maybe Rational))]
    forall (m :: Type -> Type) a. MonadPlus m => m a -> m [a]
    many' Parser
      ByteString (Text, Either Bool (Maybe Rational, Maybe Rational))
    dRealBinding
           Parser ()
    forall t. Chunk t => Parser t ()
    endOfInput
           SatResult [(Text, Either Bool (Maybe Rational, Maybe Rational))] ()
    -> Parser
         (SatResult
            [(Text, Either Bool (Maybe Rational, Maybe Rational))] ())
    forall a. a -> Parser ByteString a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return ([(Text, Either Bool (Maybe Rational, Maybe Rational))]
    -> SatResult
         [(Text, Either Bool (Maybe Rational, Maybe Rational))] ()
    forall mdl core. mdl -> SatResult mdl core
    Sat [(Text, Either Bool (Maybe Rational, Maybe Rational))]
    bs)
      ]

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

        ByteString
    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)

        Parser ()
    skipSpace
        Char
    _ <- Char -> Parser Char
    char Char
    ':'
        Parser ()
    skipSpace

        Either Bool (Maybe Rational, Maybe Rational)
    val <- [Parser ByteString (Either Bool (Maybe Rational, Maybe Rational))]
    -> Parser ByteString (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
    _ <- ByteString -> Parser ByteString
    string ByteString
    "False"
               Parser ()
    skipSpace
               Either Bool (Maybe Rational, Maybe Rational)
    -> Parser ByteString (Either Bool (Maybe Rational, Maybe Rational))
    forall a. a -> Parser ByteString a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (Bool -> Either Bool (Maybe Rational, Maybe Rational)
    forall a b. a -> Either a b
    Left Bool
    False)

          , do ByteString
    _ <- ByteString -> Parser ByteString
    string ByteString
    "True"
               Parser ()
    skipSpace
               Either Bool (Maybe Rational, Maybe Rational)
    -> Parser ByteString (Either Bool (Maybe Rational, Maybe Rational))
    forall a. a -> Parser ByteString a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (Bool -> Either Bool (Maybe Rational, Maybe Rational)
    forall a b. a -> Either a b
    Left Bool
    True)

          , do Maybe Rational
    lo <- Parser (Maybe Rational)
    dRealLoBound

               Parser ()
    skipSpace
               Char
    _ <- Char -> Parser Char
    char Char
    ','
               Parser ()
    skipSpace

               Maybe Rational
    hi <- Parser (Maybe Rational)
    dRealHiBound

               Parser ()
    skipSpace
               Char
    _ <- Char -> Parser Char -> Parser Char
    forall (f :: Type -> Type) a. Alternative f => a -> f a -> f a
    option Char
    ' ' (Char -> Parser Char
    char Char
    ';')
               Parser ()
    skipSpace
               Either Bool (Maybe Rational, Maybe Rational)
    -> Parser ByteString (Either Bool (Maybe Rational, Maybe Rational))
    forall a. a -> Parser ByteString a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return ((Maybe Rational, Maybe Rational)
    -> Either Bool (Maybe Rational, Maybe Rational)
    forall a b. b -> Either a b
    Right (Maybe Rational
    lo,Maybe Rational
    hi))
          ]
        (Text, Either Bool (Maybe Rational, Maybe Rational))
    -> Parser
         ByteString (Text, Either Bool (Maybe Rational, Maybe Rational))
    forall a. a -> Parser ByteString a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (Text -> Text
    Text.fromStrict (ByteString -> Text
    decodeUtf8 ByteString
    nm),Either Bool (Maybe Rational, Maybe Rational)
    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
    _ <- Char -> Parser Char
    char Char
    '['
            Rational
    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))
            ByteString
    num <- (Char -> Bool) -> Parser ByteString
    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 ReadS Rational
    forall a. RealFrac a => ReadS a
    readFloat (ByteString -> String
    UTF8.toString ByteString
    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 Rational
    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))
            ByteString
    num <- (Char -> Bool) -> Parser ByteString
    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
    _ <- Char -> Parser Char
    char Char
    ']'
            case ReadS Rational
    forall a. RealFrac a => ReadS a
    readFloat (ByteString -> String
    UTF8.toString ByteString
    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
      BoolExpr t
    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
      String
    solver_path <- ConfigOption (BaseStringType Unicode) -> Config -> IO String
    findSolverPath ConfigOption (BaseStringType Unicode)
    drealPath (ExprBuilder t st fs -> Config
    forall sym. IsExprBuilder sym => sym -> Config
    getConfiguration ExprBuilder t st fs
    sym)
      ExprBuilder t st fs -> SolverEvent -> IO ()
    forall sym. IsExprBuilder sym => sym -> SolverEvent -> IO ()
    logSolverEvent ExprBuilder t st fs
    sym
        (SolverStartSATQuery -> SolverEvent
    SolverStartSATQuery (SolverStartSATQuery -> SolverEvent)
    -> SolverStartSATQuery -> SolverEvent
    forall a b. (a -> b) -> a -> b
    $ SolverStartSATQueryRec
        { satQuerySolverName :: String
    satQuerySolverName = String
    "dReal"
        , satQueryReason :: String
    satQueryReason = LogData -> String
    logReason LogData
    logData
        })
      String
    -> [String]
    -> Maybe String
    -> ((Handle, Handle, Handle, ProcessHandle) -> IO a)
    -> IO a
    forall a.
    String
    -> [String]
    -> Maybe String
    -> ((Handle, Handle, Handle, ProcessHandle) -> IO a)
    -> IO a
    withProcessHandles String
    solver_path [String
    "--model", String
    "--in", String
    "--format", String
    "smt2"] Maybe String
    forall a. Maybe a
    Nothing (((Handle, Handle, Handle, ProcessHandle) -> IO a) -> IO a)
    -> ((Handle, Handle, Handle, ProcessHandle) -> IO a) -> IO a
    forall a b. (a -> b) -> a -> b
    $ \(Handle
    in_h, Handle
    out_h, Handle
    err_h, ProcessHandle
    ph) -> do

          -- Log stderr to output.
          InputStream ByteString
    err_stream <- Handle -> IO (InputStream ByteString)
    Streams.handleToInputStream Handle
    err_h
          IO ThreadId -> IO ()
    forall (f :: Type -> Type) a. Functor f => f a -> f ()
    void (IO ThreadId -> IO ()) -> IO ThreadId -> IO ()
    forall a b. (a -> b) -> a -> b
    $ IO () -> IO ThreadId
    forkIO (IO () -> IO ThreadId) -> IO () -> IO ThreadId
    forall a b. (a -> b) -> a -> b
    $ InputStream ByteString -> (String -> IO ()) -> IO ()
    logErrorStream InputStream ByteString
    err_stream (LogData -> Int -> String -> IO ()
    logCallbackVerbose LogData
    logData Int
    2)

          -- Write SMTLIB to standard input.
          LogData -> Int -> String -> IO ()
    logCallbackVerbose LogData
    logData Int
    2 String
    "Sending Satisfiability problem to dReal"
          -- dReal does not support (define-fun ...)
          SymbolVarBimap t
    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

          OutputStream Text
    out_str  <-
            case LogData -> Maybe Handle
    logHandle LogData
    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 OutputStream ByteString
    aux_str <- Handle -> IO (OutputStream ByteString)
    Streams.handleToOutputStream Handle
    aux_h
                   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
    =<< OutputStream ByteString
    -> OutputStream ByteString -> IO (OutputStream ByteString)
    forall a. OutputStream a -> OutputStream a -> IO (OutputStream a)
    teeOutputStream OutputStream ByteString
    aux_str (OutputStream ByteString -> IO (OutputStream ByteString))
    -> IO (OutputStream ByteString) -> IO (OutputStream ByteString)
    forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Handle -> IO (OutputStream ByteString)
    Streams.handleToOutputStream Handle
    in_h

          InputStream Text
    in_str <- IO (InputStream Text)
    forall a. IO (InputStream a)
    Streams.nullInput

          let cfg :: Config
    cfg = ExprBuilder t st fs -> Config
    forall sym. IsExprBuilder sym => sym -> Config
    getConfiguration ExprBuilder t st fs
    sym
          ResponseStrictness
    strictness <- ResponseStrictness
    -> (ConcreteVal BaseBoolType -> ResponseStrictness)
    -> Maybe (ConcreteVal BaseBoolType)
    -> ResponseStrictness
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe ResponseStrictness
    SMTWriter.Strict
                        (\ConcreteVal BaseBoolType
    c -> if ConcreteVal BaseBoolType -> Bool
    fromConcreteBool ConcreteVal BaseBoolType
    c
                               then ResponseStrictness
    SMTWriter.Strict
                               else ResponseStrictness
    SMTWriter.Lenient) (Maybe (ConcreteVal BaseBoolType) -> ResponseStrictness)
    -> IO (Maybe (ConcreteVal BaseBoolType)) -> IO ResponseStrictness
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$>
                        (OptionSetting BaseBoolType -> IO (Maybe (ConcreteVal BaseBoolType))
    forall (tp :: BaseType).
    OptionSetting tp -> IO (Maybe (ConcreteVal tp))
    getOption (OptionSetting BaseBoolType
     -> IO (Maybe (ConcreteVal BaseBoolType)))
    -> IO (OptionSetting BaseBoolType)
    -> IO (Maybe (ConcreteVal BaseBoolType))
    forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ConfigOption BaseBoolType
    -> Config -> IO (OptionSetting BaseBoolType)
    forall (tp :: BaseType).
    ConfigOption tp -> Config -> IO (OptionSetting tp)
    getOptionSetting ConfigOption BaseBoolType
    RSP.strictSMTParsing Config
    cfg)

          WriterConn t (Writer DReal)
    c <- DReal
    -> OutputStream Text
    -> InputStream Text
    -> AcknowledgementAction t (Writer DReal)
    -> ResponseStrictness
    -> String
    -> Bool
    -> ProblemFeatures
    -> Bool
    -> SymbolVarBimap t
    -> IO (WriterConn t (Writer DReal))
    forall a t.
    a
    -> OutputStream Text
    -> InputStream Text
    -> AcknowledgementAction t (Writer a)
    -> ResponseStrictness
    -> String
    -> Bool
    -> ProblemFeatures
    -> Bool
    -> SymbolVarBimap t
    -> IO (WriterConn t (Writer a))
    SMT2.newWriter DReal
    DReal OutputStream Text
    out_str InputStream Text
    in_str AcknowledgementAction t (Writer DReal)
    forall t h. AcknowledgementAction t h
    SMTWriter.nullAcknowledgementAction ResponseStrictness
    strictness String
    "dReal"
                 Bool
    False ProblemFeatures
    useComputableReals Bool
    False SymbolVarBimap t
    bindings

          -- Set the dReal default logic
          WriterConn t (Writer DReal) -> Logic -> IO ()
    forall a t.
    SMTLib2Tweaks a =>
    WriterConn t (Writer a) -> Logic -> IO ()
    SMT2.setLogic WriterConn t (Writer DReal)
    c (Builder -> Logic
    SMT2.Logic Builder
    "QF_NRA")
          WriterConn t (Writer DReal) -> BoolExpr t -> IO ()
    forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
    SMT2.assume WriterConn t (Writer DReal)
    c BoolExpr t
    p

          -- Create stream for output from solver.
          InputStream ByteString
    out_stream <- Handle -> IO (InputStream ByteString)
    Streams.handleToInputStream Handle
    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...
          WriterConn t (Writer DReal) -> IO ()
    forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
    SMT2.writeCheckSat WriterConn t (Writer DReal)
    c
          WriterConn t (Writer DReal) -> IO ()
    forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
    SMT2.writeExit WriterConn t (Writer DReal)
    c
          Handle -> IO ()
    hClose Handle
    in_h

          LogData -> Int -> String -> IO ()
    logCallbackVerbose LogData
    logData Int
    2 String
    "Parsing result from solver"

          Either
      ParseException
      (SatResult
         [(Text, Either Bool (Maybe Rational, Maybe Rational))] ())
    msat_result <- IO
      (SatResult
         [(Text, Either Bool (Maybe Rational, Maybe Rational))] ())
    -> IO
         (Either
            ParseException
            (SatResult
               [(Text, Either Bool (Maybe Rational, Maybe Rational))] ()))
    forall e a. Exception e => IO a -> IO (Either e a)
    try (IO
       (SatResult
          [(Text, Either Bool (Maybe Rational, Maybe Rational))] ())
     -> IO
          (Either
             ParseException
             (SatResult
                [(Text, Either Bool (Maybe Rational, Maybe Rational))] ())))
    -> IO
         (SatResult
            [(Text, Either Bool (Maybe Rational, Maybe Rational))] ())
    -> IO
         (Either
            ParseException
            (SatResult
               [(Text, Either Bool (Maybe Rational, Maybe Rational))] ()))
    forall a b. (a -> b) -> a -> b
    $ Parser
      (SatResult
         [(Text, Either Bool (Maybe Rational, Maybe Rational))] ())
    -> InputStream ByteString
    -> IO
         (SatResult
            [(Text, Either Bool (Maybe Rational, Maybe Rational))] ())
    forall r. Parser r -> InputStream ByteString -> IO r
    Streams.parseFromStream Parser
      (SatResult
         [(Text, Either Bool (Maybe Rational, Maybe Rational))] ())
    dRealResponse InputStream ByteString
    out_stream

          SatResult (WriterConn t (Writer DReal), DRealBindings) ()
    res <-
            case Either
      ParseException
      (SatResult
         [(Text, Either Bool (Maybe Rational, Maybe Rational))] ())
    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))

          a
    r <- SatResult (WriterConn t (Writer DReal), DRealBindings) () -> IO a
    modelFn SatResult (WriterConn t (Writer DReal), DRealBindings) ()
    res

          -- Check error code.
          LogData -> Int -> String -> IO ()
    logCallbackVerbose LogData
    logData Int
    2 String
    "Waiting for dReal to exit"

          ExitCode
    ec <- ProcessHandle -> IO ExitCode
    waitForProcess ProcessHandle
    ph
          case ExitCode
    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