| Copyright | (c) 2013-2020 Galois Inc. |
|---|---|
| License | BSD3 |
| Maintainer | cryptol@galois.com |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | None |
| Language | Haskell2010 |
Cryptol.Symbolic.What4
Description
Documentation
data W4ProverConfig Source #
proverNames :: [String] Source #
setupProver :: String -> IO (Either String ([String], W4ProverConfig)) Source #
Arguments
| :: W4ProverConfig | |
| -> Bool | hash consing |
| -> Bool | warn on uninterpreted functions |
| -> ProverCommand | |
| -> ModuleCmd (Maybe String, ProverResult) |
Arguments
| :: W4ProverConfig | |
| -> 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
| Show W4Exception Source # | |
Defined in Cryptol.Symbolic.What4 Methods showsPrec :: Int -> W4Exception -> ShowS # show :: W4Exception -> String # showList :: [W4Exception] -> ShowS # | |
| Exception W4Exception Source # | |
Defined in Cryptol.Symbolic.What4 Methods toException :: W4Exception -> SomeException # fromException :: SomeException -> Maybe W4Exception # displayException :: W4Exception -> String # | |