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

Cryptol.Eval.SBV

Description

Documentation

data SBV Source #

Constructors

SBV

Instances

Backend SBV Source #
Instance details Defined in Cryptol.Eval.SBV Associated Types type SBit SBV :: Type Source # type SWord SBV :: Type Source # type SInteger SBV :: Type Source # type SFloat SBV :: Type Source # type SEval SBV :: Type -> Type Source # Methods isReady :: SBV -> SEval SBV a -> Bool Source # sDeclareHole :: SBV -> String -> SEval SBV (SEval SBV a, SEval SBV a -> SEval SBV ()) Source # sDelayFill :: SBV -> SEval SBV a -> SEval SBV a -> SEval SBV (SEval SBV a) Source # sSpark :: SBV -> SEval SBV a -> SEval SBV (SEval SBV a) Source # mergeEval :: SBV -> (SBit SBV -> a -> a -> SEval SBV a) -> SBit SBV -> SEval SBV a -> SEval SBV a -> SEval SBV a Source # assertSideCondition :: SBV -> SBit SBV -> EvalError -> SEval SBV () Source # raiseError :: SBV -> EvalError -> SEval SBV a Source # ppBit :: SBV -> SBit SBV -> Doc Source # ppWord :: SBV -> PPOpts -> SWord SBV -> Doc Source # ppInteger :: SBV -> PPOpts -> SInteger SBV -> Doc Source # ppFloat :: SBV -> PPOpts -> SFloat SBV -> Doc Source # bitAsLit :: SBV -> SBit SBV -> Maybe Bool Source # wordLen :: SBV -> SWord SBV -> Integer Source # wordAsLit :: SBV -> SWord SBV -> Maybe (Integer, Integer) Source # wordAsChar :: SBV -> SWord SBV -> Maybe Char Source # integerAsLit :: SBV -> SInteger SBV -> Maybe Integer Source # bitLit :: SBV -> Bool -> SBit SBV Source # wordLit :: SBV -> Integer -> Integer -> SEval SBV (SWord SBV) Source # integerLit :: SBV -> Integer -> SEval SBV (SInteger SBV) Source # fpLit :: SBV -> Integer -> Integer -> Rational -> SEval SBV (SFloat SBV) Source # iteBit :: SBV -> SBit SBV -> SBit SBV -> SBit SBV -> SEval SBV (SBit SBV) Source # iteWord :: SBV -> SBit SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV) Source # iteInteger :: SBV -> SBit SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV) Source # bitEq :: SBV -> SBit SBV -> SBit SBV -> SEval SBV (SBit SBV) Source # bitOr :: SBV -> SBit SBV -> SBit SBV -> SEval SBV (SBit SBV) Source # bitAnd :: SBV -> SBit SBV -> SBit SBV -> SEval SBV (SBit SBV) Source # bitXor :: SBV -> SBit SBV -> SBit SBV -> SEval SBV (SBit SBV) Source # bitComplement :: SBV -> SBit SBV -> SEval SBV (SBit SBV) Source # wordBit :: SBV -> SWord SBV -> Integer -> SEval SBV (SBit SBV) Source # wordUpdate :: SBV -> SWord SBV -> Integer -> SBit SBV -> SEval SBV (SWord SBV) Source # packWord :: SBV -> [SBit SBV] -> SEval SBV (SWord SBV) Source # unpackWord :: SBV -> SWord SBV -> SEval SBV [SBit SBV] Source # wordFromInt :: SBV -> Integer -> SInteger SBV -> SEval SBV (SWord SBV) Source # joinWord :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV) Source # splitWord :: SBV -> Integer -> Integer -> SWord SBV -> SEval SBV (SWord SBV, SWord SBV) Source # extractWord :: SBV -> Integer -> Integer -> SWord SBV -> SEval SBV (SWord SBV) Source # wordOr :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV) Source # wordAnd :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV) Source # wordXor :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV) Source # wordComplement :: SBV -> SWord SBV -> SEval SBV (SWord SBV) Source # wordPlus :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV) Source # wordMinus :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV) Source # wordMult :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV) Source # wordDiv :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV) Source # wordMod :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV) Source # wordSignedDiv :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV) Source # wordSignedMod :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV) Source # wordNegate :: SBV -> SWord SBV -> SEval SBV (SWord SBV) Source # wordLg2 :: SBV -> SWord SBV -> SEval SBV (SWord SBV) Source # wordEq :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SBit SBV) Source # wordSignedLessThan :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SBit SBV) Source # wordLessThan :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SBit SBV) Source # wordGreaterThan :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SBit SBV) Source # wordToInt :: SBV -> SWord SBV -> SEval SBV (SInteger SBV) Source # intPlus :: SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV) Source # intNegate :: SBV -> SInteger SBV -> SEval SBV (SInteger SBV) Source # intMinus :: SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV) Source # intMult :: SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV) Source # intDiv :: SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV) Source # intMod :: SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV) Source # intEq :: SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SBit SBV) Source # intLessThan :: SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SBit SBV) Source # intGreaterThan :: SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SBit SBV) Source # intToZn :: SBV -> Integer -> SInteger SBV -> SEval SBV (SInteger SBV) Source # znToInt :: SBV -> Integer -> SInteger SBV -> SEval SBV (SInteger SBV) Source # znPlus :: SBV -> Integer -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV) Source # znNegate :: SBV -> Integer -> SInteger SBV -> SEval SBV (SInteger SBV) Source # znMinus :: SBV -> Integer -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV) Source # znMult :: SBV -> Integer -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV) Source # znEq :: SBV -> Integer -> SInteger SBV -> SInteger SBV -> SEval SBV (SBit SBV) Source # fpEq :: SBV -> SFloat SBV -> SFloat SBV -> SEval SBV (SBit SBV) Source # fpLessThan :: SBV -> SFloat SBV -> SFloat SBV -> SEval SBV (SBit SBV) Source # fpGreaterThan :: SBV -> SFloat SBV -> SFloat SBV -> SEval SBV (SBit SBV) Source # fpPlus :: FPArith2 SBV Source # fpMinus :: FPArith2 SBV Source # fpMult :: FPArith2 SBV Source # fpDiv :: FPArith2 SBV Source # fpNeg :: SBV -> SFloat SBV -> SEval SBV (SFloat SBV) Source # fpToInteger :: SBV -> String -> SWord SBV -> SFloat SBV -> SEval SBV (SInteger SBV) Source # fpFromInteger :: SBV -> Integer -> Integer -> SWord SBV -> SInteger SBV -> SEval SBV (SFloat SBV) Source #
type SBit SBV Source #
Instance details Defined in Cryptol.Eval.SBV type SBit SBV = SVal
type SWord SBV Source #
Instance details Defined in Cryptol.Eval.SBV type SWord SBV = SVal
type SInteger SBV Source #
Instance details Defined in Cryptol.Eval.SBV type SInteger SBV = SVal
type SFloat SBV Source #
Instance details Defined in Cryptol.Eval.SBV type SFloat SBV = ()
type SEval SBV Source #
Instance details Defined in Cryptol.Eval.SBV type SEval SBV = SBVEval

type Value = GenValue SBV Source #

newtype SBVEval a Source #

Constructors

SBVEval
Fields sbvEval :: Eval (SBVResult a)

Instances

Monad SBVEval Source #
Instance details Defined in Cryptol.Eval.SBV Methods (>>=) :: SBVEval a -> (a -> SBVEval b) -> SBVEval b # (>>) :: SBVEval a -> SBVEval b -> SBVEval b # return :: a -> SBVEval a # fail :: String -> SBVEval a #
Functor SBVEval Source #
Instance details Defined in Cryptol.Eval.SBV Methods fmap :: (a -> b) -> SBVEval a -> SBVEval b # (<$) :: a -> SBVEval b -> SBVEval a #
Applicative SBVEval Source #
Instance details Defined in Cryptol.Eval.SBV Methods pure :: a -> SBVEval a # (<>) :: SBVEval (a -> b) -> SBVEval a -> SBVEval b # liftA2 :: (a -> b -> c) -> SBVEval a -> SBVEval b -> SBVEval c # (>) :: SBVEval a -> SBVEval b -> SBVEval b # (<*) :: SBVEval a -> SBVEval b -> SBVEval a #
MonadIO SBVEval Source #
Instance details Defined in Cryptol.Eval.SBV Methods liftIO :: IO a -> SBVEval a #

data SBVResult a Source #

Constructors

SBVError !EvalError
SBVResult !SVal !a

Instances

Monad SBVResult Source #
Instance details Defined in Cryptol.Eval.SBV Methods (>>=) :: SBVResult a -> (a -> SBVResult b) -> SBVResult b # (>>) :: SBVResult a -> SBVResult b -> SBVResult b # return :: a -> SBVResult a # fail :: String -> SBVResult a #
Functor SBVResult Source #
Instance details Defined in Cryptol.Eval.SBV Methods fmap :: (a -> b) -> SBVResult a -> SBVResult b # (<$) :: a -> SBVResult b -> SBVResult a #
Applicative SBVResult Source #
Instance details Defined in Cryptol.Eval.SBV Methods pure :: a -> SBVResult a # (<>) :: SBVResult (a -> b) -> SBVResult a -> SBVResult b # liftA2 :: (a -> b -> c) -> SBVResult a -> SBVResult b -> SBVResult c # (>) :: SBVResult a -> SBVResult b -> SBVResult b # (<*) :: SBVResult a -> SBVResult b -> SBVResult a #

evalPrim :: PrimIdent -> Maybe Value Source #

forallBV_ :: Int -> Symbolic (SWord SBV) Source #

existsBV_ :: Int -> Symbolic (SWord SBV) Source #

forallSBool_ :: Symbolic (SBit SBV) Source #

existsSBool_ :: Symbolic (SBit SBV) Source #

forallSInteger_ :: Symbolic (SBit SBV) Source #

existsSInteger_ :: Symbolic (SBit SBV) Source #