cryptol-3.3.0: Cryptol: The Language of Cryptography
Copyright(c) 2013-2020 Galois Inc.
LicenseBSD3
Maintainercryptol@galois.com
Stabilityprovisional
Portabilityportable
Safe HaskellSafe-Inferred
LanguageHaskell2010

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

-> Int

timeout milliseconds

-> 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 #

fromException :: SomeException -> Maybe W4Exception #

displayException :: W4Exception -> String #

Show W4Exception Source # 
Instance details

Defined in Cryptol.Symbolic.What4

Methods

showsPrec :: Int -> W4Exception -> ShowS #

show :: W4Exception -> String #

showList :: [W4Exception] -> ShowS #