cryptol-2.9.1: Cryptol: The Language of Cryptography

Copyright(c) 2013-2016 Galois Inc.
LicenseBSD3
Maintainercryptol@galois.com
Stabilityprovisional
Portabilityportable
Safe HaskellNone
LanguageHaskell2010

Cryptol.Symbolic.SBV

Description

 
Synopsis

Documentation

proverNames :: [String] Source #

The names of all the solvers supported by SBV

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.