-----------------------------------------------------------------------------
-- |
-- 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 :: Solver
-> String
-> (String -> String)
-> (SMTConfig -> [String])
-> SMTEngine
-> SolverCapabilities
-> SMTSolver
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 :: Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Maybe String
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Maybe [String]
-> SolverCapabilities
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
                              , 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."
                                                                 ]