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

    {-# LANGUAGE ScopedTypeVariables #-}

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Data.SBV.Provers.CVC5(cvc5) where

    import Data.Char (isSpace)

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

    -- | The description of the CVC5 SMT solver
    -- The default executable is @\"cvc5\"@, which must be in your path. You can use the @SBV_CVC5@ environment variable to point to the executable on your system.
    -- You can use the @SBV_CVC5_OPTIONS@ environment variable to override the options.
    cvc5 :: SMTSolver
    cvc5 :: SMTSolver
    cvc5 = SMTSolver {
               name :: Solver
    name         = Solver
    CVC5
             , executable :: String
    executable   = String
    "cvc5"
             , preprocess :: String -> String
    preprocess   = String -> String
    clean
             , options :: SMTConfig -> [String]
    options      = [String] -> SMTConfig -> [String]
    forall a b. a -> b -> a
    const [String
    "--lang", String
    "smt", String
    "--incremental", String
    "--nl-cov"]
             , engine :: SMTEngine
    engine       = String -> String -> SMTEngine
    standardEngine String
    "SBV_CVC5" String
    "SBV_CVC5_OPTIONS"
             , capabilities :: SolverCapabilities
    capabilities = SolverCapabilities {
                                    supportsQuantifiers :: Bool
    supportsQuantifiers        = Bool
    True
                                  , supportsDefineFun :: Bool
    supportsDefineFun          = Bool
    True
                                  , supportsDistinct :: Bool
    supportsDistinct           = Bool
    True
                                  , supportsBitVectors :: Bool
    supportsBitVectors         = Bool
    True
                                  , supportsUninterpretedSorts :: Bool
    supportsUninterpretedSorts = Bool
    True
                                  , supportsUnboundedInts :: Bool
    supportsUnboundedInts      = Bool
    True
                                  , supportsInt2bv :: Bool
    supportsInt2bv             = Bool
    True
                                  , supportsReals :: Bool
    supportsReals              = Bool
    True  -- Not quite the same capability as Z3; but works more or less..
                                  , supportsApproxReals :: Bool
    supportsApproxReals        = Bool
    False
                                  , supportsDeltaSat :: Maybe String
    supportsDeltaSat           = Maybe String
    forall a. Maybe a
    Nothing
                                  , supportsIEEE754 :: Bool
    supportsIEEE754            = Bool
    True
                                  , 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
    True
                                  , supportsFoldAndMap :: Bool
    supportsFoldAndMap         = Bool
    False
                                  , supportsSpecialRels :: Bool
    supportsSpecialRels        = Bool
    False
                                  , supportsDirectAccessors :: Bool
    supportsDirectAccessors    = Bool
    True
                                  , supportsFlattenedModels :: Maybe [String]
    supportsFlattenedModels    = Maybe [String]
    forall a. Maybe a
    Nothing
                                  }
             }
      where -- CVC5 wants all input on one line
            clean :: String -> String
    clean = (Char -> Char) -> String -> String
    forall a b. (a -> b) -> [a] -> [b]
    map Char -> Char
    simpleSpace (String -> String) -> (String -> String) -> String -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> String
    noComment

            noComment :: String -> String
    noComment String
    ""       = String
    ""
            noComment (Char
    ';':String
    cs) = String -> String
    noComment (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ (Char -> Bool) -> String -> String
    forall a. (a -> Bool) -> [a] -> [a]
    dropWhile (Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Char
    '\n') String
    cs
            noComment (Char
    c:String
    cs)   = Char
    c Char -> String -> String
    forall a. a -> [a] -> [a]
    : String -> String
    noComment String
    cs

            simpleSpace :: Char -> Char
    simpleSpace Char
    c
              | Char -> Bool
    isSpace Char
    c = Char
    ' '
              | Bool
    True      = Char
    c