cryptol-2.2.2: Cryptol: The Language of Cryptography

Copyright(c) 2013-2015 Galois, Inc.
LicenseBSD3
Maintainercryptol@galois.com
Stabilityprovisional
Portabilityportable
Safe HaskellSafe
LanguageHaskell98

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

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

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

data InfNat Source

Constructors

Nat Integer 
Inf 

Instances

data Name Source

Instances

toName :: Int -> Name Source

fromName :: Name -> Maybe Int Source