| Copyright | (c) 2013-2016 Galois Inc. |
|---|---|
| License | BSD3 |
| Maintainer | cryptol@galois.com |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | None |
| 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 #
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
| Show SBVPortfolioException Source # | |
Defined in Cryptol.Symbolic.SBV Methods showsPrec :: Int -> SBVPortfolioException -> ShowS # show :: SBVPortfolioException -> String # showList :: [SBVPortfolioException] -> ShowS # | |
| Exception SBVPortfolioException Source # | |
Defined in Cryptol.Symbolic.SBV | |