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

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

{-# OPTIONS_GHC -Wall -Werror #-}

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

import Control.Monad (filterM)
import Data.Generics

import qualified Control.Exception   as C

import qualified "template-haskell" Language.Haskell.TH as TH

import Data.SBV.Core.Data
import Data.SBV.Core.Model
import Data.SBV.Control.Utils
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 cfg :: 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 (m :: * -> *) a. Monad m => a -> m a
return Bool
False)
  where check :: IO Bool
check = do ThmResult r :: SMTResult
r <- SMTConfig -> (SWord8 -> SBool) -> IO ThmResult
forall (m :: * -> *) a.
MProvable m a =>
SMTConfig -> a -> m ThmResult
proveWith SMTConfig
cfg ((SWord8 -> SBool) -> IO ThmResult)
-> (SWord8 -> SBool) -> IO ThmResult
forall a b. (a -> b) -> a -> b
$ \x :: SWord8
x -> (SWord8
xSWord8 -> SWord8 -> SWord8
forall a. Num a => a -> a -> a
+SWord8
x) SWord8 -> SWord8 -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== ((SWord8
xSWord8 -> SWord8 -> SWord8
forall a. Num a => a -> a -> a
*2) :: SWord8)
                   case SMTResult
r of
                     Unsatisfiable{} -> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
                     _               -> Bool -> IO Bool
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 Z3        = SMTConfig
z3
defaultSolverConfig Yices     = SMTConfig
yices
defaultSolverConfig Boolector = SMTConfig
boolector
defaultSolverConfig CVC4      = SMTConfig
cvc4
defaultSolverConfig MathSAT   = SMTConfig
mathSAT
defaultSolverConfig ABC       = SMTConfig
abc

-- | Return the known available solver configs, installed on your machine.
sbvAvailableSolvers :: IO [SMTConfig]
sbvAvailableSolvers :: IO [SMTConfig]
sbvAvailableSolvers = (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])

-- | Make an enumeration a symbolic type.
mkSymbolicEnumeration :: TH.Name -> TH.Q [TH.Dec]
mkSymbolicEnumeration :: Name -> Q [Dec]
mkSymbolicEnumeration typeName :: Name
typeName = do
    let typeCon :: TypeQ
typeCon = Name -> TypeQ
TH.conT Name
typeName
    [d| deriving instance Eq       $(typeCon)
        deriving instance Show     $(typeCon)
        deriving instance Ord      $(typeCon)
        deriving instance Read     $(typeCon)
        deriving instance Data     $(typeCon)
        deriving instance SymVal   $(typeCon)
        deriving instance HasKind  $(typeCon)
        deriving instance SMTValue $(typeCon)
        deriving instance SatModel $(typeCon)
      |]