    -----------------------------------------------------------------------------
    -- |
    -- Module    : Data.SBV.Provers.DReal
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- The connection to the dReal SMT solver
    -----------------------------------------------------------------------------

    {-# LANGUAGE ScopedTypeVariables #-}

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Data.SBV.Provers.DReal(dReal) where

    import Data.SBV.Core.Data
    import Data.SBV.SMT.SMT

    import Numeric

    -- | The description of the dReal SMT solver
    -- The default executable is @\"dReal\"@, which must be in your path. You can use the @SBV_DREAL@ environment variable to point to the executable on your system.
    -- You can use the @SBV_DREAL_OPTIONS@ environment variable to override the options.
    dReal :: SMTSolver
    dReal :: SMTSolver
    dReal = SMTSolver {
               name :: Solver
    name         = Solver
    DReal
             , executable :: String
    executable   = String
    "dReal"
             , preprocess :: String -> String
    preprocess   = String -> String
    forall a. a -> a
    id
             , options :: SMTConfig -> [String]
    options      = [String] -> SMTConfig -> [String]
    modConfig [String
    "--in", String
    "--format", String
    "smt2"]
             , engine :: SMTEngine
    engine       = String -> String -> SMTEngine
    standardEngine String
    "SBV_DREAL" String
    "SBV_DREAL_OPTIONS"
             , capabilities :: SolverCapabilities
    capabilities = SolverCapabilities {
                                    supportsQuantifiers :: Bool
    supportsQuantifiers        = Bool
    False
                                  , supportsDefineFun :: Bool
    supportsDefineFun          = Bool
    True
                                  , supportsDistinct :: Bool
    supportsDistinct           = Bool
    False
                                  , supportsBitVectors :: Bool
    supportsBitVectors         = Bool
    False
                                  , supportsUninterpretedSorts :: Bool
    supportsUninterpretedSorts = Bool
    False
                                  , supportsUnboundedInts :: Bool
    supportsUnboundedInts      = Bool
    True
                                  , supportsInt2bv :: Bool
    supportsInt2bv             = Bool
    False
                                  , supportsReals :: Bool
    supportsReals              = Bool
    True
                                  , supportsApproxReals :: Bool
    supportsApproxReals        = Bool
    False
                                  , supportsDeltaSat :: Maybe String
    supportsDeltaSat           = String -> Maybe String
    forall a. a -> Maybe a
    Just String
    "(get-option :precision)"
                                  , supportsIEEE754 :: Bool
    supportsIEEE754            = Bool
    False
                                  , supportsSets :: Bool
    supportsSets               = Bool
    False
                                  , supportsOptimization :: Bool
    supportsOptimization       = Bool
    False
                                  , supportsPseudoBooleans :: Bool
    supportsPseudoBooleans     = Bool
    False
                                  , supportsCustomQueries :: Bool
    supportsCustomQueries      = Bool
    False
                                  , supportsGlobalDecls :: Bool
    supportsGlobalDecls        = Bool
    False
                                  , supportsDataTypes :: Bool
    supportsDataTypes          = Bool
    False
                                  , supportsFoldAndMap :: Bool
    supportsFoldAndMap         = Bool
    False
                                  , supportsSpecialRels :: Bool
    supportsSpecialRels        = Bool
    False
                                  , supportsDirectAccessors :: Bool
    supportsDirectAccessors    = Bool
    False
                                  , supportsFlattenedModels :: Maybe [String]
    supportsFlattenedModels    = Maybe [String]
    forall a. Maybe a
    Nothing
                                  }
             }
      where -- If dsat precision is given, pass that as an argument
           modConfig :: [String] -> SMTConfig -> [String]
           modConfig :: [String] -> SMTConfig -> [String]
    modConfig [String]
    opts SMTConfig
    cfg = case SMTConfig -> Maybe Double
    dsatPrecision SMTConfig
    cfg of
                                  Maybe Double
    Nothing -> [String]
    opts
                                  Just Double
    d  -> let sd :: String
    sd = Maybe Int -> Double -> String -> String
    forall a. RealFloat a => Maybe Int -> a -> String -> String
    showFFloat Maybe Int
    forall a. Maybe a
    Nothing Double
    d String
    ""
                                             in if Double
    d Double -> Double -> Bool
    forall a. Ord a => a -> a -> Bool
    > Double
    0
                                                then [String]
    opts [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [String
    "--precision", String
    sd]
                                                else String -> [String]
    forall a. HasCallStack => String -> a
    error (String -> [String]) -> String -> [String]
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ String
    ""
                                                                     , String
    "*** Data.SBV: Invalid precision to dReal: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    sd
                                                                     , String
    "***           Precision must be non-negative."
                                                                     ]