cryptol-3.0.0: Cryptol: The Language of Cryptography

Copyright | (c) 2013-2020 Galois Inc.
License | BSD3
Maintainer | cryptol@galois.com
Stability | provisional
Portability | portable
Safe Haskell | Safe-Inferred
Language | Haskell2010

Cryptol.Symbolic.What4

Description

# Documentation

data W4ProverConfig Source #

defaultProver :: W4ProverConfig Source #

proverNames :: [String] Source #

setupProver :: String -> IO (Either String ([String], W4ProverConfig)) Source #

satProve Source #

Arguments

:: W4ProverConfig |
-> Bool | hash consing
-> Bool | warn on uninterpreted functions
-> ProverCommand |
-> ModuleCmd (Maybe String, ProverResult) |

satProveOffline Source #

Arguments

:: Bool | hash consing
-> Bool | warn on uninterpreted functions
-> ProverCommand |
-> ((Handle -> IO ()) -> IO ()) |
-> ModuleCmd (Maybe String) |

data W4Exception Source #

Constructors

W4Ex SomeException |
W4PortfolioFailure [Either SomeException (Maybe String, String)] |

#### Instances

Instances details

Exception W4Exception Source # |
Instance details Defined in Cryptol.Symbolic.What4 Methods toException :: W4Exception -> SomeException Source # fromException :: SomeException -> Maybe W4Exception Source # displayException :: W4Exception -> String Source #
Show W4Exception Source # |
Instance details Defined in Cryptol.Symbolic.What4 Methods showsPrec :: Int -> W4Exception -> ShowS Source # show :: W4Exception -> String Source # showList :: [W4Exception] -> ShowS Source #