copilot-sbv-2.2.1: A compiler for CoPilot targeting SBV.

Safe HaskellNone
LanguageHaskell2010

Copilot.Compile.SBV.Witness

Documentation

data SymWordInst a Source #

Constructors

SymWord a => SymWordInst 

symWordInst :: Type a -> SymWordInst a Source #

data NumInst a Source #

Constructors

Num a => NumInst 

numInst :: Type a -> NumInst a Source #

data HasSignAndSizeInst a Source #

Constructors

SymWord a => HasSignAndSizeInst 

hasSignAndSizeInst :: Type a -> HasSignAndSizeInst a Source #

data EqInst a Source #

Constructors

EqSymbolic (SBV a) => EqInst 

eqInst :: Type a -> EqInst a Source #

data CastInst a b Source #

Constructors

SBVCast a b => CastInst 

castInst :: Type a -> Type b -> CastInst a b Source #

sbvCast :: SBVCast a b => SBV a -> SBV b Source #

data BVDivisibleInst a Source #

Constructors

SDivisible (SBV a) => BVDivisibleInst 

divInst :: Type a -> BVDivisibleInst a Source #

data OrdInst a Source #

Constructors

OrdSymbolic (SBV a) => OrdInst 

ordInst :: Type a -> OrdInst a Source #

data MergeableInst a Source #

Constructors

Mergeable (SBV a) => MergeableInst 

mergeableInst :: Type a -> MergeableInst a Source #

data BitsInst a Source #

Constructors

(Bits a, Bits (SBV a)) => BitsInst 

bitsInst :: Type a -> BitsInst a Source #

data IntegralInst a Source #

Constructors

SIntegral a => IntegralInst 

integralInst :: Type a -> IntegralInst a Source #

OSZAR »