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

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Data.SBV.Provers.Boolector(boolector) where

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

    -- | The description of the Boolector SMT solver
    -- The default executable is @\"boolector\"@, which must be in your path. You can use the @SBV_BOOLECTOR@ environment variable to point to the executable on your system.
    -- You can use the @SBV_BOOLECTOR_OPTIONS@ environment variable to override the options.
    boolector :: SMTSolver
    boolector :: SMTSolver
    boolector = SMTSolver {
               name :: Solver
    name         = Solver
    Boolector
             , executable :: String
    executable   = String
    "boolector"
             , preprocess :: String -> String
    preprocess   = String -> String
    forall a. a -> a
    id
             , options :: SMTConfig -> [String]
    options      = [String] -> SMTConfig -> [String]
    forall a b. a -> b -> a
    const [String
    "--smt2", String
    "-m", String
    "--output-format=smt2", String
    "--no-exit-codes", String
    "--incremental"]
             , engine :: SMTEngine
    engine       = String -> String -> SMTEngine
    standardEngine String
    "SBV_BOOLECTOR" String
    "SBV_BOOLECTOR_OPTIONS"
             , capabilities :: SolverCapabilities
    capabilities = SolverCapabilities {
                                    supportsQuantifiers :: Bool
    supportsQuantifiers        = Bool
    False
                                  , supportsDefineFun :: Bool
    supportsDefineFun          = Bool
    True
                                  , supportsDistinct :: Bool
    supportsDistinct           = Bool
    True
                                  , supportsBitVectors :: Bool
    supportsBitVectors         = Bool
    True
                                  , supportsUninterpretedSorts :: Bool
    supportsUninterpretedSorts = Bool
    False
                                  , supportsUnboundedInts :: Bool
    supportsUnboundedInts      = Bool
    False
                                  , supportsInt2bv :: Bool
    supportsInt2bv             = Bool
    False
                                  , supportsReals :: Bool
    supportsReals              = Bool
    False
                                  , supportsApproxReals :: Bool
    supportsApproxReals        = Bool
    False
                                  , supportsDeltaSat :: Maybe String
    supportsDeltaSat           = Maybe String
    forall a. Maybe a
    Nothing
                                  , supportsIEEE754 :: Bool
    supportsIEEE754            = Bool
    False
                                  , supportsSets :: Bool
    supportsSets               = Bool
    False
                                  , supportsOptimization :: Bool
    supportsOptimization       = Bool
    False
                                  , supportsPseudoBooleans :: Bool
    supportsPseudoBooleans     = Bool
    False
                                  , supportsCustomQueries :: Bool
    supportsCustomQueries      = Bool
    True
                                  , supportsGlobalDecls :: Bool
    supportsGlobalDecls        = Bool
    True
                                  , 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
                                  }
             }