Safe Haskell	None
Language	Haskell2010

Test.Tasty.SBV

Description

This module allows to prove statements in tasty.

Synopsis

testStatement :: (Testable a, Provable a) => TestName -> a -> TestTree
newtype SbvPrintBase = SbvPrintBase Int
newtype SbvPrintRealPrec = SbvPrintRealPrec Int
newtype SbvValidateModel = SbvValidateModel Bool
newtype SbvTranscript = SbvTranscript (Maybe FilePath)
newtype SbvVerbose = SbvVerbose Bool
newtype SbvRedirectVerbose = SbvRedirectVerbose (Maybe FilePath)
newtype SbvSolver = SbvSolver Solver
newtype SbvQuickCheck = SbvQuickCheck Bool
data FS = (Testable a, Provable a) => FS a

Documentation

testStatement :: (Testable a, Provable a) => TestName -> a -> TestTree Source #

Create a test that attempts to proves a statement. When checking via QuickCheck is requested, tasty-quickcheck options will be respected.

newtype SbvPrintBase Source #

The base to use for integer literal printing (2, 10, and 16 are supported).

Constructors

SbvPrintBase Int

Instances

Eq SbvPrintBase Source #
Instance details Defined in Test.Tasty.SBV Methods (==) :: SbvPrintBase -> SbvPrintBase -> Bool # (/=) :: SbvPrintBase -> SbvPrintBase -> Bool #
Ord SbvPrintBase Source #
Instance details Defined in Test.Tasty.SBV Methods compare :: SbvPrintBase -> SbvPrintBase -> Ordering # (<) :: SbvPrintBase -> SbvPrintBase -> Bool # (<=) :: SbvPrintBase -> SbvPrintBase -> Bool # (>) :: SbvPrintBase -> SbvPrintBase -> Bool # (>=) :: SbvPrintBase -> SbvPrintBase -> Bool # max :: SbvPrintBase -> SbvPrintBase -> SbvPrintBase # min :: SbvPrintBase -> SbvPrintBase -> SbvPrintBase #
Show SbvPrintBase Source #
Instance details Defined in Test.Tasty.SBV Methods showsPrec :: Int -> SbvPrintBase -> ShowS # show :: SbvPrintBase -> String # showList :: [SbvPrintBase] -> ShowS #
IsOption SbvPrintBase Source #
Instance details Defined in Test.Tasty.SBV Methods defaultValue :: SbvPrintBase # parseValue :: String -> Maybe SbvPrintBase # optionName :: Tagged SbvPrintBase String # optionHelp :: Tagged SbvPrintBase String # optionCLParser :: Parser SbvPrintBase #

newtype SbvPrintRealPrec Source #

The precision to print real values with (SReal, default is 16).

Constructors

SbvPrintRealPrec Int

Instances

Eq SbvPrintRealPrec Source #
Instance details Defined in Test.Tasty.SBV Methods (==) :: SbvPrintRealPrec -> SbvPrintRealPrec -> Bool # (/=) :: SbvPrintRealPrec -> SbvPrintRealPrec -> Bool #
Ord SbvPrintRealPrec Source #
Instance details Defined in Test.Tasty.SBV Methods compare :: SbvPrintRealPrec -> SbvPrintRealPrec -> Ordering # (<) :: SbvPrintRealPrec -> SbvPrintRealPrec -> Bool # (<=) :: SbvPrintRealPrec -> SbvPrintRealPrec -> Bool # (>) :: SbvPrintRealPrec -> SbvPrintRealPrec -> Bool # (>=) :: SbvPrintRealPrec -> SbvPrintRealPrec -> Bool # max :: SbvPrintRealPrec -> SbvPrintRealPrec -> SbvPrintRealPrec # min :: SbvPrintRealPrec -> SbvPrintRealPrec -> SbvPrintRealPrec #
Show SbvPrintRealPrec Source #
Instance details Defined in Test.Tasty.SBV Methods showsPrec :: Int -> SbvPrintRealPrec -> ShowS # show :: SbvPrintRealPrec -> String # showList :: [SbvPrintRealPrec] -> ShowS #
IsOption SbvPrintRealPrec Source #
Instance details Defined in Test.Tasty.SBV Methods defaultValue :: SbvPrintRealPrec # parseValue :: String -> Maybe SbvPrintRealPrec # optionName :: Tagged SbvPrintRealPrec String # optionHelp :: Tagged SbvPrintRealPrec String # optionCLParser :: Parser SbvPrintRealPrec #

newtype SbvValidateModel Source #

If sbv should attempt to validate the model it gets back from the solver.

Constructors

SbvValidateModel Bool

Instances

Eq SbvValidateModel Source #
Instance details Defined in Test.Tasty.SBV Methods (==) :: SbvValidateModel -> SbvValidateModel -> Bool # (/=) :: SbvValidateModel -> SbvValidateModel -> Bool #
Ord SbvValidateModel Source #
Instance details Defined in Test.Tasty.SBV Methods compare :: SbvValidateModel -> SbvValidateModel -> Ordering # (<) :: SbvValidateModel -> SbvValidateModel -> Bool # (<=) :: SbvValidateModel -> SbvValidateModel -> Bool # (>) :: SbvValidateModel -> SbvValidateModel -> Bool # (>=) :: SbvValidateModel -> SbvValidateModel -> Bool # max :: SbvValidateModel -> SbvValidateModel -> SbvValidateModel # min :: SbvValidateModel -> SbvValidateModel -> SbvValidateModel #
Show SbvValidateModel Source #
Instance details Defined in Test.Tasty.SBV Methods showsPrec :: Int -> SbvValidateModel -> ShowS # show :: SbvValidateModel -> String # showList :: [SbvValidateModel] -> ShowS #
IsOption SbvValidateModel Source #
Instance details Defined in Test.Tasty.SBV Methods defaultValue :: SbvValidateModel # parseValue :: String -> Maybe SbvValidateModel # optionName :: Tagged SbvValidateModel String # optionHelp :: Tagged SbvValidateModel String # optionCLParser :: Parser SbvValidateModel #

newtype SbvTranscript Source #

Where and if sbv should save a replayble transcript.

Constructors

SbvTranscript (Maybe FilePath)

Instances

Eq SbvTranscript Source #
Instance details Defined in Test.Tasty.SBV Methods (==) :: SbvTranscript -> SbvTranscript -> Bool # (/=) :: SbvTranscript -> SbvTranscript -> Bool #
Ord SbvTranscript Source #
Instance details Defined in Test.Tasty.SBV Methods compare :: SbvTranscript -> SbvTranscript -> Ordering # (<) :: SbvTranscript -> SbvTranscript -> Bool # (<=) :: SbvTranscript -> SbvTranscript -> Bool # (>) :: SbvTranscript -> SbvTranscript -> Bool # (>=) :: SbvTranscript -> SbvTranscript -> Bool # max :: SbvTranscript -> SbvTranscript -> SbvTranscript # min :: SbvTranscript -> SbvTranscript -> SbvTranscript #
Show SbvTranscript Source #
Instance details Defined in Test.Tasty.SBV Methods showsPrec :: Int -> SbvTranscript -> ShowS # show :: SbvTranscript -> String # showList :: [SbvTranscript] -> ShowS #
IsOption SbvTranscript Source #
Instance details Defined in Test.Tasty.SBV Methods defaultValue :: SbvTranscript # parseValue :: String -> Maybe SbvTranscript # optionName :: Tagged SbvTranscript String # optionHelp :: Tagged SbvTranscript String # optionCLParser :: Parser SbvTranscript #

newtype SbvVerbose Source #

Verbose debug output.

Constructors

SbvVerbose Bool

Instances

Eq SbvVerbose Source #
Instance details Defined in Test.Tasty.SBV Methods (==) :: SbvVerbose -> SbvVerbose -> Bool # (/=) :: SbvVerbose -> SbvVerbose -> Bool #
Ord SbvVerbose Source #
Instance details Defined in Test.Tasty.SBV Methods compare :: SbvVerbose -> SbvVerbose -> Ordering # (<) :: SbvVerbose -> SbvVerbose -> Bool # (<=) :: SbvVerbose -> SbvVerbose -> Bool # (>) :: SbvVerbose -> SbvVerbose -> Bool # (>=) :: SbvVerbose -> SbvVerbose -> Bool # max :: SbvVerbose -> SbvVerbose -> SbvVerbose # min :: SbvVerbose -> SbvVerbose -> SbvVerbose #
Show SbvVerbose Source #
Instance details Defined in Test.Tasty.SBV Methods showsPrec :: Int -> SbvVerbose -> ShowS # show :: SbvVerbose -> String # showList :: [SbvVerbose] -> ShowS #
IsOption SbvVerbose Source #
Instance details Defined in Test.Tasty.SBV Methods defaultValue :: SbvVerbose # parseValue :: String -> Maybe SbvVerbose # optionName :: Tagged SbvVerbose String # optionHelp :: Tagged SbvVerbose String # optionCLParser :: Parser SbvVerbose #

newtype SbvRedirectVerbose Source #

If we should save the verbose output to a file instead of printing to stdout, and what it is.

Constructors

SbvRedirectVerbose (Maybe FilePath)

Instances

Eq SbvRedirectVerbose Source #
Instance details Defined in Test.Tasty.SBV Methods (==) :: SbvRedirectVerbose -> SbvRedirectVerbose -> Bool # (/=) :: SbvRedirectVerbose -> SbvRedirectVerbose -> Bool #
Ord SbvRedirectVerbose Source #
Instance details Defined in Test.Tasty.SBV Methods compare :: SbvRedirectVerbose -> SbvRedirectVerbose -> Ordering # (<) :: SbvRedirectVerbose -> SbvRedirectVerbose -> Bool # (<=) :: SbvRedirectVerbose -> SbvRedirectVerbose -> Bool # (>) :: SbvRedirectVerbose -> SbvRedirectVerbose -> Bool # (>=) :: SbvRedirectVerbose -> SbvRedirectVerbose -> Bool # max :: SbvRedirectVerbose -> SbvRedirectVerbose -> SbvRedirectVerbose # min :: SbvRedirectVerbose -> SbvRedirectVerbose -> SbvRedirectVerbose #
Show SbvRedirectVerbose Source #
Instance details Defined in Test.Tasty.SBV Methods showsPrec :: Int -> SbvRedirectVerbose -> ShowS # show :: SbvRedirectVerbose -> String # showList :: [SbvRedirectVerbose] -> ShowS #
IsOption SbvRedirectVerbose Source #
Instance details Defined in Test.Tasty.SBV Methods defaultValue :: SbvRedirectVerbose # parseValue :: String -> Maybe SbvRedirectVerbose # optionName :: Tagged SbvRedirectVerbose String # optionHelp :: Tagged SbvRedirectVerbose String # optionCLParser :: Parser SbvRedirectVerbose #

newtype SbvSolver Source #

Which solver sbv shoul use. The current options are z3 (the default), yices, boolector, cvc4, mathsat, and abc.

Constructors

SbvSolver Solver

Instances

Show SbvSolver Source #
Instance details Defined in Test.Tasty.SBV Methods showsPrec :: Int -> SbvSolver -> ShowS # show :: SbvSolver -> String # showList :: [SbvSolver] -> ShowS #
IsOption SbvSolver Source #
Instance details Defined in Test.Tasty.SBV Methods defaultValue :: SbvSolver # parseValue :: String -> Maybe SbvSolver # optionName :: Tagged SbvSolver String # optionHelp :: Tagged SbvSolver String # optionCLParser :: Parser SbvSolver #

newtype SbvQuickCheck Source #

Check properties with QuickCheck instead of a solver. This allows basic checking of the statement even without a solver installed on the system.

Constructors

SbvQuickCheck Bool

Instances

Eq SbvQuickCheck Source #
Instance details Defined in Test.Tasty.SBV Methods (==) :: SbvQuickCheck -> SbvQuickCheck -> Bool # (/=) :: SbvQuickCheck -> SbvQuickCheck -> Bool #
Ord SbvQuickCheck Source #
Instance details Defined in Test.Tasty.SBV Methods compare :: SbvQuickCheck -> SbvQuickCheck -> Ordering # (<) :: SbvQuickCheck -> SbvQuickCheck -> Bool # (<=) :: SbvQuickCheck -> SbvQuickCheck -> Bool # (>) :: SbvQuickCheck -> SbvQuickCheck -> Bool # (>=) :: SbvQuickCheck -> SbvQuickCheck -> Bool # max :: SbvQuickCheck -> SbvQuickCheck -> SbvQuickCheck # min :: SbvQuickCheck -> SbvQuickCheck -> SbvQuickCheck #
Show SbvQuickCheck Source #
Instance details Defined in Test.Tasty.SBV Methods showsPrec :: Int -> SbvQuickCheck -> ShowS # show :: SbvQuickCheck -> String # showList :: [SbvQuickCheck] -> ShowS #
IsOption SbvQuickCheck Source #
Instance details Defined in Test.Tasty.SBV Methods defaultValue :: SbvQuickCheck # parseValue :: String -> Maybe SbvQuickCheck # optionName :: Tagged SbvQuickCheck String # optionHelp :: Tagged SbvQuickCheck String # optionCLParser :: Parser SbvQuickCheck #

data FS Source #

Constructors

(Testable a, Provable a) => FS a

Instances

IsTest FS Source #
Instance details Defined in Test.Tasty.SBV Methods run :: OptionSet -> FS -> (Progress -> IO ()) -> IO Result # testOptions :: Tagged FS [OptionDescription] #