content: -----------------------------------------------------------------------------
  -- |
  -- 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 {
             name         = DReal
           , executable   = "dReal"
           , preprocess   = id
           , options      = modConfig ["--in", "--format", "smt2"]
           , engine       = standardEngine "SBV_DREAL" "SBV_DREAL_OPTIONS"
           , capabilities = SolverCapabilities {
                                  supportsQuantifiers     = False
                                , supportsDefineFun       = True
                                , supportsDistinct        = False
                                , supportsBitVectors      = False
                                , supportsADTs            = False
                                , supportsUnboundedInts   = True
                                , supportsReals           = True
                                , supportsApproxReals     = False
                                , supportsDeltaSat        = Just "(get-option :precision)"
                                , supportsIEEE754         = False
                                , supportsSets            = False
                                , supportsOptimization    = False
                                , supportsPseudoBooleans  = False
                                , supportsCustomQueries   = False
                                , supportsGlobalDecls     = False
                                , supportsDataTypes       = False
                                , supportsLambdas         = False
                                , supportsSpecialRels     = False
                                , supportsDirectAccessors = False
                                , supportsFlattenedModels = Nothing
                                }
           }
    where -- If dsat precision is given, pass that as an argument
         modConfig :: [String] -> SMTConfig -> [String]
         modConfig opts cfg = case dsatPrecision cfg of
                                Nothing -> opts
                                Just d  -> let sd = showFFloat Nothing d ""
                                           in if d > 0
                                              then opts ++ ["--precision", sd]
                                              else error $ unlines [ ""
                                                                   , "*** Data.SBV: Invalid precision to dReal: " ++ sd
                                                                   , "***           Precision must be non-negative."
                                                                   ]
  