cryptol-3.0.0: Cryptol: The Language of Cryptography

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

Cryptol.Symbolic.SBV

Description

Synopsis

- data SBVProverConfig
- defaultProver :: SBVProverConfig
- proverNames :: [String]
- setupProver :: String -> IO (Either String ([String], SBVProverConfig))
- satProve :: SBVProverConfig -> ProverCommand -> ModuleCmd (Maybe String, ProverResult)
- satProveOffline :: SBVProverConfig -> ProverCommand -> ModuleCmd (Either String String)
- newtype SBVPortfolioException = SBVPortfolioException [Either SomeException (Maybe String, String)]

# Documentation

data SBVProverConfig Source #

defaultProver :: SBVProverConfig Source #

proverNames :: [String] Source #

The names of all the solvers supported by SBV

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

satProve :: SBVProverConfig -> ProverCommand -> ModuleCmd (Maybe String, ProverResult) Source #

Execute a symbolic ':prove' or ':sat' command.

This command returns a pair: the first element is the name of the solver that completes the given query (if any) along with the result of executing the query.

satProveOffline :: SBVProverConfig -> ProverCommand -> ModuleCmd (Either String String) Source #

Execute a symbolic ':prove' or ':sat' command when the prover is set to offline. This only prepares the SMT input file for the solver and does not actually invoke the solver.

This method returns either an error message or the text of the SMT input file corresponding to the given prover command.

newtype SBVPortfolioException Source #

Constructors

SBVPortfolioException [Either SomeException (Maybe String, String)] |

#### Instances

Instances details

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