{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeApplications #-}
module Test.Tasty.SBV
( testStatement
, SbvPrintBase(..)
, SbvPrintRealPrec(..)
, SbvValidateModel(..)
, SbvTranscript(..)
, SbvVerbose(..)
, SbvRedirectVerbose(..)
, SbvSolver(..)
, SbvQuickCheck(..)
, FS(..)
) where
import Data.SBV
import Data.Tagged
import Data.Typeable
import Test.Tasty.Providers
import qualified Test.Tasty.Providers as T
import Test.Tasty.Options
import Test.Tasty.QuickCheck (QC(QC), Testable(property))
data FS = forall a . (Testable a, Provable a) => FS a
deriving (Typeable)
testStatement :: (Testable a, Provable a) => TestName -> a -> TestTree
testStatement n = singleTest n . FS
newtype SbvPrintBase = SbvPrintBase Int
deriving (Eq, Ord, Show, Typeable)
instance IsOption SbvPrintBase where
defaultValue = SbvPrintBase 10
parseValue = fmap SbvPrintBase . safeRead
optionName = return "sbv-print-base"
optionHelp = return "Print integral literals in this base (2, 10, and 16 are supported.)"
newtype SbvPrintRealPrec = SbvPrintRealPrec Int
deriving (Eq, Ord, Show, Typeable)
instance IsOption SbvPrintRealPrec where
defaultValue = SbvPrintRealPrec 16
parseValue = fmap SbvPrintRealPrec . safeRead
optionName = return "sbv-print-real-prec"
optionHelp = return "Print algebraic real values with this precision. (SReal, default: 16)"
newtype SbvValidateModel = SbvValidateModel Bool
deriving (Eq, Ord, Show, Typeable)
instance IsOption SbvValidateModel where
defaultValue = SbvValidateModel False
parseValue = fmap SbvValidateModel . safeReadBool
optionName = return "sbv-validate-model"
optionHelp = return "If SBV should attempt to validate the model it gets back from the solver."
newtype SbvTranscript = SbvTranscript (Maybe FilePath)
deriving (Eq, Ord, Show, Typeable)
instance IsOption SbvTranscript where
defaultValue = SbvTranscript Nothing
parseValue = Just . SbvTranscript . Just
optionName = return "sbv-transcript"
optionHelp = return "Where SBV should save a replayble transcript if set."
newtype SbvVerbose = SbvVerbose Bool
deriving (Eq, Ord, Show, Typeable)
instance IsOption SbvVerbose where
defaultValue = SbvVerbose False
parseValue = fmap SbvVerbose . safeReadBool
optionName = return "sbv-verbose"
optionHelp = return "Enable verbose debug output."
newtype SbvRedirectVerbose = SbvRedirectVerbose (Maybe FilePath)
deriving (Eq, Ord, Show, Typeable)
instance IsOption SbvRedirectVerbose where
defaultValue = SbvRedirectVerbose Nothing
parseValue = Just . SbvRedirectVerbose . Just
optionName = return "sbv-verbose-save"
optionHelp = return "Where we should save verbose output, instead of printing to stdout."
newtype SbvSolver = SbvSolver Solver
deriving (Show, Typeable)
instance IsOption SbvSolver where
defaultValue = SbvSolver Z3
parseValue = \case
"z3" -> Just $ SbvSolver Z3
"yices" -> Just $ SbvSolver Yices
"boolector" -> Just $ SbvSolver Boolector
"cvc4" -> Just $ SbvSolver CVC4
"mathsat" -> Just $ SbvSolver MathSAT
"abc" -> Just $ SbvSolver ABC
_ -> Nothing
optionName = return "sbv-solver"
optionHelp = return "The backend solver to use, from z3 (the default), yices, boolector, cvc4, mathsat, and abc."
newtype SbvQuickCheck = SbvQuickCheck Bool
deriving (Eq, Ord, Show, Typeable)
instance IsOption SbvQuickCheck where
defaultValue = SbvQuickCheck False
parseValue = fmap SbvQuickCheck . safeReadBool
optionName = return "sbv-quickcheck"
optionHelp = return "Check properties with QuickCheck instead of a solver."
instance T.IsTest FS where
testOptions = pure $
[ Option (Proxy :: Proxy SbvPrintBase)
, Option (Proxy :: Proxy SbvPrintRealPrec)
, Option (Proxy :: Proxy SbvValidateModel)
, Option (Proxy :: Proxy SbvTranscript)
, Option (Proxy :: Proxy SbvVerbose)
, Option (Proxy :: Proxy SbvRedirectVerbose)
, Option (Proxy :: Proxy SbvSolver)
, Option (Proxy :: Proxy SbvQuickCheck)
] ++ (unTagged $ testOptions @QC)
run opts (FS thm) yieldProgress =
if qc
then run opts (QC $ property thm) yieldProgress
else beTheReader
where
SbvQuickCheck qc = lookupOption opts
SbvPrintBase pbase = lookupOption opts
SbvPrintRealPrec pprec = lookupOption opts
SbvValidateModel vm = lookupOption opts
SbvTranscript mt = lookupOption opts
SbvVerbose v = lookupOption opts
SbvRedirectVerbose rv = lookupOption opts
SbvSolver slv = lookupOption opts
config = (case slv of
Z3 -> z3
Yices -> yices
Boolector -> boolector
CVC4 -> cvc4
MathSAT -> mathSAT
ABC -> abc
) { verbose = v
, printBase = pbase
, printRealPrec = pprec
, validateModel = vm
, transcript = mt
, redirectVerbose = rv
}
beTheReader = do
tres@(ThmResult sres) <- proveWith config thm
case sres of
Unsatisfiable _ _ -> pure $ testPassed ""
_ -> pure $ testFailed $ show tres