Cryptol.Symbolic

Description

Synopsis

• type EvalEnv = GenEvalEnv SBool SWord
• proverConfigs :: [(String, SMTConfig)]
• proverNames :: [String]
• lookupProver :: String -> SMTConfig
• type SatResult = [(Type, Expr, Value)]
• data SatNum
  • = AllSat
  • | SomeSat Int
• data QueryType
  • = SatQuery SatNum
  • | ProveQuery
• data ProverCommand = ProverCommand {
  • pcQueryType :: QueryType
  • pcProverName :: String
  • pcVerbose :: Bool
  • pcProverStats :: !(IORef ProverStats)
  • pcExtraDecls :: [DeclGroup]
  • pcSmtFile :: Maybe FilePath
  • pcExpr :: Expr
  • pcSchema :: Schema
  }
• type ProverStats = NominalDiffTime
• data ProverResult
  • = AllSatResult [SatResult]
  • | ThmResult [Type]
  • | EmptyResult
  • | ProverError String
• satSMTResults :: SatResult -> [SMTResult]
• allSatSMTResults :: AllSatResult -> [SMTResult]
• thmSMTResults :: ThmResult -> [SMTResult]
• proverError :: String -> ModuleCmd (Maybe Solver, ProverResult)
• satProve :: ProverCommand -> ModuleCmd (Maybe Solver, ProverResult)
• satProveOffline :: ProverCommand -> ModuleCmd (Either String String)
• protectStack :: (String -> ModuleCmd a) -> ModuleCmd a -> ModuleCmd a
• parseValues :: [FinType] -> [CW] -> ([Value], [CW])
• parseValue :: FinType -> [CW] -> (Value, [CW])
• allDeclGroups :: ModuleEnv -> [DeclGroup]
• data FinType
  • = FTBit
  • | FTSeq Int FinType
  • | FTTuple [FinType]
  • | FTRecord [(Ident, FinType)]
• numType :: Integer -> Maybe Int
• finType :: TValue -> Maybe FinType
• unFinType :: FinType -> Type
• predArgTypes :: Schema -> Either String [FinType]
• forallFinType :: FinType -> Symbolic Value
• existsFinType :: FinType -> Symbolic Value

Documentation