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

Cryptol.Symbolic

Contents

FinType

Description

Synopsis

data ProverCommand = ProverCommand {
- pcQueryType :: QueryType
- pcProverName :: String
- pcVerbose :: Bool
- pcValidate :: Bool
- pcProverStats :: !(IORef ProverStats)
- pcExtraDecls :: [DeclGroup]
- pcSmtFile :: Maybe FilePath
- pcExpr :: Expr
- pcSchema :: Schema
- pcIgnoreSafety :: Bool
}
data QueryType
- = SatQuery SatNum
- | ProveQuery
- | SafetyQuery
data SatNum
- = AllSat
- | SomeSat Int
data ProverResult
- = AllSatResult [SatResult]
- | ThmResult [Type]
- | CounterExample CounterExampleType SatResult
- | EmptyResult
- | ProverError String
type ProverStats = NominalDiffTime
data CounterExampleType
- = SafetyViolation
- | PredicateFalsified
data FinType
- = FTBit
- | FTInteger
- | FTIntMod Integer
- | FTRational
- | FTFloat Integer Integer
- | FTSeq Int FinType
- | FTTuple [FinType]
- | FTRecord (RecordMap Ident FinType)
finType :: TValue -> Maybe FinType
unFinType :: FinType -> Type
predArgTypes :: QueryType -> Schema -> Either String [FinType]

Documentation

data ProverCommand Source #

Constructors

ProverCommand

Fields

pcQueryType :: QueryType
The type of query to run
pcProverName :: String
Which prover to use (one of the strings in proverConfigs)
pcVerbose :: Bool
Verbosity flag passed to SBV
pcValidate :: Bool
Model validation flag passed to SBV
pcProverStats :: !(IORef ProverStats)
Record timing information here
pcExtraDecls :: [DeclGroup]
Extra declarations to bring into scope for symbolic simulation
pcSmtFile :: Maybe FilePath
Optionally output the SMTLIB query to a file
pcExpr :: Expr
The typechecked expression to evaluate
pcSchema :: Schema
The Schema of pcExpr
pcIgnoreSafety :: Bool
Should we ignore safety predicates?

data QueryType Source #

Constructors

SatQuery SatNum
ProveQuery
SafetyQuery

Instances

Show QueryType Source #
Instance details Defined in Cryptol.Symbolic Methods showsPrec :: Int -> QueryType -> ShowS # show :: QueryType -> String # showList :: [QueryType] -> ShowS #

data SatNum Source #

Constructors

AllSat
SomeSat Int

Instances

Show SatNum Source #
Instance details Defined in Cryptol.Symbolic Methods showsPrec :: Int -> SatNum -> ShowS # show :: SatNum -> String # showList :: [SatNum] -> ShowS #

data ProverResult Source #

A prover result is either an error message, an empty result (eg for the offline prover), a counterexample or a lazy list of satisfying assignments.

Constructors

AllSatResult [SatResult]
ThmResult [Type]
CounterExample CounterExampleType SatResult
EmptyResult
ProverError String

type ProverStats = NominalDiffTime Source #

data CounterExampleType Source #

A :prove command can fail either because some input causes the predicate to violate a safety assertion, or because the predicate returns false for some input.

Constructors

SafetyViolation
PredicateFalsified

FinType

data FinType Source #

Constructors

FTBit
FTInteger
FTIntMod Integer
FTRational
FTFloat Integer Integer
FTSeq Int FinType
FTTuple [FinType]
FTRecord (RecordMap Ident FinType)

finType :: TValue -> Maybe FinType Source #

unFinType :: FinType -> Type Source #

predArgTypes :: QueryType -> Schema -> Either String [FinType] Source #