    -----------------------------------------------------------------------------
    -- |
    -- 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
    -----------------------------------------------------------------------------

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

    import Data.SBV.BitVectors.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 {
               name         = ABC
             , executable   = "abc"
             , options      = ["-S", "%blast; &sweep -C 5000; &syn4; &cec -s -m -C 2000"]
             , engine       = standardEngine "SBV_ABC" "SBV_ABC_OPTIONS" addTimeOut standardModel
             , capabilities = SolverCapabilities {
                                    capSolverName              = "ABC"
                                  , mbDefaultLogic             = const Nothing
                                  , supportsMacros             = True
                                  , supportsProduceModels      = True
                                  , supportsQuantifiers        = False
                                  , supportsUninterpretedSorts = False
                                  , supportsUnboundedInts      = False
                                  , supportsReals              = False
                                  , supportsFloats             = False
                                  , supportsDoubles            = False
                                  }
             }
      where addTimeOut _ _ = error "ABC: Timeout values are not supported"