cryptol-2.2.6: Cryptol: The Language of Cryptography

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

Cryptol.TypeCheck.Solver.CrySAT

Description

# Documentation

debug :: PropSet -> [S] Source

data Prop Source

Constructors

Fin Expr |
Expr :== Expr infix 4 |
Expr :/= Expr |
Expr :>= Expr infix 4 |
Expr :> Expr infix 4 |
Prop :&& Prop infixr 3 |
Prop :|| Prop infixr 2 |
Not Prop |

Instances

Show Prop Source |

data Expr Source

Constructors

K InfNat |
Var Name |
Expr :+ Expr infixl 6 |
Expr :- Expr infixl 6 |
Expr :* Expr infixl 7 |
Div Expr Expr |
Mod Expr Expr |
Expr :^^ Expr |
Min Expr Expr |
Max Expr Expr |
Lg2 Expr |
Width Expr |
LenFromThen Expr Expr Expr |
LenFromThenTo Expr Expr Expr |

Instances

Show Expr Source |

data PropSet Source

noProps :: PropSet Source

assert :: Prop -> PropSet -> PropSet Source

checkSat :: PropSet -> Result Source

data Result Source

Constructors

Sat [(Int, InfNat)] |
Unsat |
Unknown |

Instances

Show Result Source |

data InfNat Source

Constructors

Nat Integer |
Inf |

Instances

Eq InfNat Source |
Ord InfNat Source |
Show InfNat Source |

data Name Source

Instances

Eq Name Source |
Ord Name Source |
Show Name Source |

toName :: Int -> Name Source

fromName :: Name -> Maybe Int Source