    -----------------------------------------------------------------------------
    -- |
    -- Module    : Data.SBV.Client
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Cross-cutting toplevel client functions
    -----------------------------------------------------------------------------

    {-# LANGUAGE CPP                 #-}
    {-# LANGUAGE PackageImports      #-}
    {-# LANGUAGE QuasiQuotes         #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE StandaloneDeriving  #-}
    {-# LANGUAGE TemplateHaskell     #-}

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Data.SBV.Client
      ( sbvCheckSolverInstallation
      , defaultSolverConfig
      , getAvailableSolvers
      , mkSymbolicEnumeration
      , mkUninterpretedSort
      ) where

    import Control.Monad (filterM)
    import Data.Generics

    import qualified Control.Exception as C

    import qualified "template-haskell" Language.Haskell.TH        as TH
    #if MIN_VERSION_template_haskell(2,18,0)
    import qualified "template-haskell" Language.Haskell.TH.Syntax as TH
    #endif

    import Data.SBV.Core.Data
    import Data.SBV.Core.Model () -- instances only
    import Data.SBV.Provers.Prover

    -- | Check whether the given solver is installed and is ready to go. This call does a
    -- simple call to the solver to ensure all is well.
    sbvCheckSolverInstallation :: SMTConfig -> IO Bool
    sbvCheckSolverInstallation :: SMTConfig -> IO Bool
    sbvCheckSolverInstallation SMTConfig
    cfg = IO Bool
    check IO Bool -> (SomeException -> IO Bool) -> IO Bool
    forall e a. Exception e => IO a -> (e -> IO a) -> IO a
    `C.catch` (\(SomeException
    _ :: C.SomeException) -> Bool -> IO Bool
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False)
      where check :: IO Bool
    check = do ThmResult SMTResult
    r <- SMTConfig -> (SBool -> SBool) -> IO ThmResult
    forall (m :: * -> *) a.
    ProvableM m a =>
    SMTConfig -> a -> m ThmResult
    proveWith SMTConfig
    cfg ((SBool -> SBool) -> IO ThmResult)
    -> (SBool -> SBool) -> IO ThmResult
    forall a b. (a -> b) -> a -> b
    $ \SBool
    x -> SBool -> SBool
    sNot (SBool -> SBool
    sNot SBool
    x) SBool -> SBool -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== (SBool
    x :: SBool)
                       case SMTResult
    r of
                         Unsatisfiable{} -> Bool -> IO Bool
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
                         SMTResult
    _               -> Bool -> IO Bool
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False

    -- | The default configs corresponding to supported SMT solvers
    defaultSolverConfig :: Solver -> SMTConfig
    defaultSolverConfig :: Solver -> SMTConfig
    defaultSolverConfig Solver
    ABC       = SMTConfig
    abc
    defaultSolverConfig Solver
    Boolector = SMTConfig
    boolector
    defaultSolverConfig Solver
    Bitwuzla  = SMTConfig
    bitwuzla
    defaultSolverConfig Solver
    CVC4      = SMTConfig
    cvc4
    defaultSolverConfig Solver
    CVC5      = SMTConfig
    cvc5
    defaultSolverConfig Solver
    DReal     = SMTConfig
    dReal
    defaultSolverConfig Solver
    MathSAT   = SMTConfig
    mathSAT
    defaultSolverConfig Solver
    Yices     = SMTConfig
    yices
    defaultSolverConfig Solver
    Z3        = SMTConfig
    z3

    -- | Return the known available solver configs, installed on your machine.
    getAvailableSolvers :: IO [SMTConfig]
    getAvailableSolvers :: IO [SMTConfig]
    getAvailableSolvers = (SMTConfig -> IO Bool) -> [SMTConfig] -> IO [SMTConfig]
    forall (m :: * -> *) a.
    Applicative m =>
    (a -> m Bool) -> [a] -> m [a]
    filterM SMTConfig -> IO Bool
    sbvCheckSolverInstallation ((Solver -> SMTConfig) -> [Solver] -> [SMTConfig]
    forall a b. (a -> b) -> [a] -> [b]
    map Solver -> SMTConfig
    defaultSolverConfig [Solver
    forall a. Bounded a => a
    minBound .. Solver
    forall a. Bounded a => a
    maxBound])

    -- | Turn a name into a symbolic type. If first argument is true, we'll also derive Eq and Ord instances.
    declareSymbolic :: Bool -> TH.Name -> TH.Q [TH.Dec]
    declareSymbolic :: Bool -> Name -> Q [Dec]
    declareSymbolic Bool
    isEnum Name
    typeName = do
        let typeCon :: Q Type
    typeCon = Name -> Q Type
    forall (m :: * -> *). Quote m => Name -> m Type
    TH.conT Name
    typeName

        [Name]
    cstrs <- if Bool
    isEnum then Name -> Q [Name]
    ensureEnumeration Name
    typeName
                           else Name -> Q [Name]
    ensureEmptyData   Name
    typeName

        [Dec]
    deriveEqOrds <- if Bool
    isEnum
                           then [d| deriving instance Eq       $Q Type
    typeCon
                                    deriving instance Ord      $Q Type
    typeCon
                                |]
                           else [Dec] -> Q [Dec]
    forall a. a -> Q a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure []

        [Dec]
    derives <- [d| deriving instance Show     $Q Type
    typeCon
                       deriving instance Read     $Q Type
    typeCon
                       deriving instance Data     $Q Type
    typeCon
                       deriving instance SymVal   $Q Type
    typeCon
                       deriving instance HasKind  $Q Type
    typeCon
                       deriving instance SatModel $Q Type
    typeCon
                   |]

        Type
    sType <- Name -> Q Type
    forall (m :: * -> *). Quote m => Name -> m Type
    TH.conT ''SBV Q Type -> Q Type -> Q Type
    forall (m :: * -> *). Quote m => m Type -> m Type -> m Type
    `TH.appT` Q Type
    typeCon

        let declConstructor :: Name -> ((Name, String), [Dec])
    declConstructor Name
    c = ((Name
    nm, String
    bnm), [Dec
    sig, Dec
    def])
              where bnm :: String
    bnm  = Name -> String
    TH.nameBase Name
    c
                    nm :: Name
    nm   = String -> Name
    TH.mkName (String -> Name) -> String -> Name
    forall a b. (a -> b) -> a -> b
    $ Char
    's' Char -> String -> String
    forall a. a -> [a] -> [a]
    : String
    bnm
                    def :: Dec
    def  = Name -> [Clause] -> Dec
    TH.FunD Name
    nm [[Pat] -> Body -> [Dec] -> Clause
    TH.Clause [] (Exp -> Body
    TH.NormalB Exp
    body) []]
                    body :: Exp
    body = Exp -> Exp -> Exp
    TH.AppE (Name -> Exp
    TH.VarE 'literal) (Name -> Exp
    TH.ConE Name
    c)
                    sig :: Dec
    sig  = Name -> Type -> Dec
    TH.SigD Name
    nm Type
    sType

            ([(Name, String)]
    constrNames, [[Dec]]
    cdecls) = [((Name, String), [Dec])] -> ([(Name, String)], [[Dec]])
    forall a b. [(a, b)] -> ([a], [b])
    unzip ((Name -> ((Name, String), [Dec]))
    -> [Name] -> [((Name, String), [Dec])]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> ((Name, String), [Dec])
    declConstructor [Name]
    cstrs)

        let btname :: String
    btname = Name -> String
    TH.nameBase Name
    typeName
            tname :: Name
    tname  = String -> Name
    TH.mkName (Char
    'S' Char -> String -> String
    forall a. a -> [a] -> [a]
    : String
    btname)
            tdecl :: Dec
    tdecl  = Name -> [TyVarBndr ()] -> Type -> Dec
    TH.TySynD Name
    tname [] Type
    sType

        (Name, String) -> [(Name, String)] -> Q ()
    addDocs (Name
    tname, String
    btname) [(Name, String)]
    constrNames

        [Dec] -> Q [Dec]
    forall a. a -> Q a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ([Dec] -> Q [Dec]) -> [Dec] -> Q [Dec]
    forall a b. (a -> b) -> a -> b
    $ [Dec]
    deriveEqOrds [Dec] -> [Dec] -> [Dec]
    forall a. [a] -> [a] -> [a]
    ++ [Dec]
    derives [Dec] -> [Dec] -> [Dec]
    forall a. [a] -> [a] -> [a]
    ++ [Dec
    tdecl] [Dec] -> [Dec] -> [Dec]
    forall a. [a] -> [a] -> [a]
    ++ [[Dec]] -> [Dec]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[Dec]]
    cdecls

     where addDocs :: (TH.Name, String) -> [(TH.Name, String)] -> TH.Q ()
    #if MIN_VERSION_template_haskell(2,18,0)
           addDocs :: (Name, String) -> [(Name, String)] -> Q ()
    addDocs (Name
    tnm, String
    ts) [(Name, String)]
    cnms = do Bool -> (Name, String) -> Q ()
    addDoc Bool
    True (Name
    tnm, String
    ts)
                                       ((Name, String) -> Q ()) -> [(Name, String)] -> Q ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_  (Bool -> (Name, String) -> Q ()
    addDoc Bool
    False) [(Name, String)]
    cnms
              where addDoc :: Bool -> (Name, String) -> Q ()
    addDoc Bool
    True  (Name
    cnm, String
    cs) = Q () -> Q ()
    TH.addModFinalizer (Q () -> Q ()) -> Q () -> Q ()
    forall a b. (a -> b) -> a -> b
    $ DocLoc -> String -> Q ()
    TH.putDoc (Name -> DocLoc
    TH.DeclDoc Name
    cnm) (String -> Q ()) -> String -> Q ()
    forall a b. (a -> b) -> a -> b
    $ String
    "Symbolic version of the type '"        String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    cs String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "'."
                    addDoc Bool
    False (Name
    cnm, String
    cs) = Q () -> Q ()
    TH.addModFinalizer (Q () -> Q ()) -> Q () -> Q ()
    forall a b. (a -> b) -> a -> b
    $ DocLoc -> String -> Q ()
    TH.putDoc (Name -> DocLoc
    TH.DeclDoc Name
    cnm) (String -> Q ()) -> String -> Q ()
    forall a b. (a -> b) -> a -> b
    $ String
    "Symbolic version of the constructor '" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    cs String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "'."
    #else
           addDocs _ _ = pure ()
    #endif

    -- | Make an enumeration a symbolic type.
    mkSymbolicEnumeration :: TH.Name -> TH.Q [TH.Dec]
    mkSymbolicEnumeration :: Name -> Q [Dec]
    mkSymbolicEnumeration = Bool -> Name -> Q [Dec]
    declareSymbolic Bool
    True

    -- | Make an uninterpred sort.
    mkUninterpretedSort :: TH.Name -> TH.Q [TH.Dec]
    mkUninterpretedSort :: Name -> Q [Dec]
    mkUninterpretedSort = Bool -> Name -> Q [Dec]
    declareSymbolic Bool
    False

    -- | Make sure the given type is an enumeration
    ensureEnumeration :: TH.Name -> TH.Q [TH.Name]
    ensureEnumeration :: Name -> Q [Name]
    ensureEnumeration Name
    nm = do
            Info
    c <- Name -> Q Info
    TH.reify Name
    nm
            case Info
    c of
              TH.TyConI Dec
    d -> case Dec
    d of
                               TH.DataD Cxt
    _ Name
    _ [TyVarBndr ()]
    _ Maybe Type
    _ [Con]
    cons [DerivClause]
    _ -> case [Con]
    cons of
                                                            [] -> String -> Q [Name]
    forall {a}. String -> Q [a]
    bad String
    "The datatype given has no constructors."
                                                            [Con]
    xs -> [[Name]] -> [Name]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat ([[Name]] -> [Name]) -> Q [[Name]] -> Q [Name]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Con -> Q [Name]) -> [Con] -> Q [[Name]]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM Con -> Q [Name]
    check [Con]
    xs
                               Dec
    _                       -> String -> Q [Name]
    forall {a}. String -> Q [a]
    bad String
    "The name given is not a datatype."

              Info
    _        -> String -> Q [Name]
    forall {a}. String -> Q [a]
    bad String
    "The name given is not a datatype."
     where n :: String
    n = Name -> String
    TH.nameBase Name
    nm

           check :: Con -> Q [Name]
    check (TH.NormalC Name
    c [BangType]
    xs) = case [BangType]
    xs of
                                       [] -> [Name] -> Q [Name]
    forall a. a -> Q a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure [Name
    c]
                                       [BangType]
    _  -> String -> Q [Name]
    forall {a}. String -> Q [a]
    bad (String -> Q [Name]) -> String -> Q [Name]
    forall a b. (a -> b) -> a -> b
    $ String
    "Constructor " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Name -> String
    forall a. Show a => a -> String
    show Name
    c String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " has arguments."

           check Con
    c                 = String -> Q [Name]
    forall {a}. String -> Q [a]
    bad (String -> Q [Name]) -> String -> Q [Name]
    forall a b. (a -> b) -> a -> b
    $ String
    "Constructor " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Con -> String
    forall a. Show a => a -> String
    show Con
    c String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " is not an enumeration value."

           bad :: String -> Q [a]
    bad String
    m = do String -> Q ()
    TH.reportError (String -> Q ()) -> String -> Q ()
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ String
    "Data.SBV.mkSymbolicEnumeration: Invalid argument " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    forall a. Show a => a -> String
    show String
    n
                                               , String
    ""
                                               , String
    "    Expected an enumeration. " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    m
                                               , String
    ""
                                               , String
    "    To create an enumerated sort, use a simple Haskell enumerated type."
                                               ]
                      [a] -> Q [a]
    forall a. a -> Q a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure []

    -- | Make sure the given type is an empty data
    ensureEmptyData :: TH.Name -> TH.Q [TH.Name]
    ensureEmptyData :: Name -> Q [Name]
    ensureEmptyData Name
    nm = do
            Info
    c <- Name -> Q Info
    TH.reify Name
    nm
            case Info
    c of
              TH.TyConI Dec
    d -> case Dec
    d of
                               TH.DataD Cxt
    _ Name
    _ [TyVarBndr ()]
    _ Maybe Type
    _ [Con]
    cons [DerivClause]
    _ -> case [Con]
    cons of
                                                            [] -> [Name] -> Q [Name]
    forall a. a -> Q a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure []
                                                            [Con]
    _  -> String -> Q [Name]
    forall {a}. String -> Q [a]
    bad String
    "The datatype given has constructors."
                               Dec
    _                       -> String -> Q [Name]
    forall {a}. String -> Q [a]
    bad String
    "The name given is not a datatype."

              Info
    _        -> String -> Q [Name]
    forall {a}. String -> Q [a]
    bad String
    "The name given is not a datatype."
     where n :: String
    n = Name -> String
    TH.nameBase Name
    nm
           bad :: String -> Q [a]
    bad String
    m = do String -> Q ()
    TH.reportError (String -> Q ()) -> String -> Q ()
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ String
    "Data.SBV.mkUninterpretedSort: Invalid argument " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    forall a. Show a => a -> String
    show String
    n
                                               , String
    ""
                                               , String
    "    Expected an empty datatype. " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    m
                                               , String
    ""
                                               , String
    "    To create an uninterpreted sort, use an empty datatype declaration."
                                               ]
                      [a] -> Q [a]
    forall a. a -> Q a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure []