    -----------------------------------------------------------------------------
    -- |
    -- Module    : Data.SBV.Provers.ABC
    -- Copyright : (c) Adam Foltzer
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- The connection to the ABC verification and synthesis tool
    -----------------------------------------------------------------------------

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Data.SBV.Provers.ABC(abc) where

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

    -- | The description of abc. The default executable is @\"abc\"@,
    -- which must be in your path. You can use the @SBV_ABC@ environment
    -- variable to point to the executable on your system.  The default
    -- options are @-S \"%blast; &sweep -C 5000; &syn4; &cec -s -m -C 2000\"@.
    -- You can use the @SBV_ABC_OPTIONS@ environment variable to override the options.
    abc :: SMTSolver
    abc :: SMTSolver
    abc = SMTSolver :: Solver
    -> String
    -> (String -> String)
    -> (SMTConfig -> [String])
    -> SMTEngine
    -> SolverCapabilities
    -> SMTSolver
    SMTSolver {
               name :: Solver
    name         = Solver
    ABC
             , executable :: String
    executable   = "abc"
             , 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 ["-S", "%blast; &sweep -C 5000; &syn4; &cec -s -m -C 2000"]
             , engine :: SMTEngine
    engine       = String -> String -> SMTEngine
    standardEngine "SBV_ABC" "SBV_ABC_OPTIONS"
             , capabilities :: SolverCapabilities
    capabilities = SolverCapabilities :: Bool
    -> Bool
    -> Bool
    -> Bool
    -> Bool
    -> Bool
    -> Bool
    -> Bool
    -> Bool
    -> Bool
    -> Bool
    -> Bool
    -> Maybe [String]
    -> SolverCapabilities
    SolverCapabilities {
                                    supportsQuantifiers :: Bool
    supportsQuantifiers        = Bool
    False
                                  , supportsUninterpretedSorts :: Bool
    supportsUninterpretedSorts = Bool
    False
                                  , supportsUnboundedInts :: Bool
    supportsUnboundedInts      = Bool
    False
                                  , supportsReals :: Bool
    supportsReals              = Bool
    False
                                  , supportsApproxReals :: Bool
    supportsApproxReals        = Bool
    False
                                  , 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
                                  , supportsFlattenedModels :: Maybe [String]
    supportsFlattenedModels    = Maybe [String]
    forall a. Maybe a
    Nothing
                                  }
             }