-----------------------------------------------------------------------------
-- |
-- 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 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 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
OpenSMT   = SMTConfig
openSMT
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

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

    deriveEqOrds <- if isEnum
                       then [d| deriving instance Eq       $typeCon
                                deriving instance Ord      $typeCon
                            |]
                       else pure []

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


    sType <- TH.conT ''SBV `TH.appT` typeCon

    let 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

        (constrNames, cdecls) = unzip (map declConstructor cstrs)

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

    addDocs (tname, btname) constrNames

    pure $ deriveEqOrds ++ derives ++ [tdecl] ++ concat 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
        c <- Name -> Q Info
TH.reify Name
nm
        case c of
          TH.TyConI Dec
d -> case Dec
d of
                           TH.DataD Cxt
_ Name
_ [TyVarBndr BndrVis]
_ 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
        c <- Name -> Q Info
TH.reify Name
nm
        case c of
          TH.TyConI Dec
d -> case Dec
d of
                           TH.DataD Cxt
_ Name
_ [TyVarBndr BndrVis]
_ 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 []