Safe Haskell	None
Language	Haskell98

Language.SMTLib2.Internals

Synopsis

Documentation

data SMTRequest response where Source

Constructors

SMTSetLogic :: String -> SMTRequest ()
SMTGetInfo :: SMTInfo i -> SMTRequest i
SMTSetOption :: SMTOption -> SMTRequest ()
SMTAssert :: SMTExpr Bool -> Maybe InterpolationGroup -> Maybe ClauseId -> SMTRequest ()
SMTCheckSat :: Maybe Tactic -> CheckSatLimits -> SMTRequest CheckSatResult
SMTDeclaredDataTypes :: SMTRequest DataTypeInfo
SMTDeclareDataTypes :: TypeCollection -> SMTRequest ()
SMTDeclareSort :: String -> Integer -> SMTRequest ()
SMTPush :: SMTRequest ()
SMTPop :: SMTRequest ()
SMTDefineFun :: (Args arg, SMTType res) => Maybe String -> Proxy arg -> ArgAnnotation arg -> SMTExpr res -> SMTRequest Integer
SMTDeclareFun :: FunInfo -> SMTRequest Integer
SMTGetValue :: SMTValue t => SMTExpr t -> SMTRequest t
SMTGetModel :: SMTRequest SMTModel
SMTGetProof :: SMTRequest (SMTExpr Bool)
SMTGetUnsatCore :: SMTRequest [ClauseId]
SMTSimplify :: SMTType t => SMTExpr t -> SMTRequest (SMTExpr t)
SMTGetInterpolant :: [InterpolationGroup] -> SMTRequest (SMTExpr Bool)
SMTInterpolate :: [SMTExpr Bool] -> SMTRequest [SMTExpr Bool]
SMTComment :: String -> SMTRequest ()
SMTExit :: SMTRequest ()
SMTApply :: Tactic -> SMTRequest [SMTExpr Bool]
SMTNameExpr :: SMTType t => String -> SMTExpr t -> SMTRequest Integer
SMTNewInterpolationGroup :: SMTRequest InterpolationGroup
SMTNewClauseId :: SMTRequest ClauseId

data SMTModel Source

Constructors

SMTModel
Fields modelFunctions :: Map Integer (Integer, [ProxyArg], SMTExpr Untyped)

Instances

Show SMTModel Source

data CheckSatLimits Source

Describe limits on the ressources that an SMT-solver can use

Constructors

CheckSatLimits
Fields limitTime :: Maybe Integer A limit on the amount of time the solver can spend on the problem (in milliseconds) limitMemory :: Maybe Integer A limit on the amount of memory the solver can use (in megabytes)

Instances

Eq CheckSatLimits Source
Ord CheckSatLimits Source
Show CheckSatLimits Source

data CheckSatResult Source

The result of a check-sat query

Constructors

Sat	The formula is satisfiable
Unsat	The formula is unsatisfiable
Unknown	The solver cannot determine the satisfiability of a formula

Instances

Eq CheckSatResult Source
Ord CheckSatResult Source
Show CheckSatResult Source

class Monad m => SMTBackend a m where Source

Methods

smtHandle :: Typeable response => a -> SMTRequest response -> m (response, a) Source

smtGetNames :: a -> m (Integer -> String) Source

smtNextName :: a -> m (Maybe String -> String) Source

Instances

MonadIO m => SMTBackend SMTPipe m Source
Monad m => SMTBackend (AnyBackend m) m Source

class (Ord t, Typeable t, Ord (SMTAnnotation t), Typeable (SMTAnnotation t), Show (SMTAnnotation t)) => SMTType t where Source

Haskell types which can be represented in SMT

Minimal complete definition

getSort, asValueType, annotationFromSort, defaultExpr

Associated Types

type SMTAnnotation t Source

Methods

getSort :: t -> SMTAnnotation t -> Sort Source

asDataType :: t -> SMTAnnotation t -> Maybe (String, TypeCollection) Source

asValueType :: t -> SMTAnnotation t -> (forall v. SMTValue v => v -> SMTAnnotation v -> r) -> Maybe r Source

getProxyArgs :: t -> SMTAnnotation t -> [ProxyArg] Source

additionalConstraints :: t -> SMTAnnotation t -> Maybe (SMTExpr t -> [SMTExpr Bool]) Source

annotationFromSort :: t -> Sort -> SMTAnnotation t Source

defaultExpr :: SMTAnnotation t -> SMTExpr t Source

data ArgumentSort' a Source

Constructors

ArgumentSort Integer
NormalSort (Sort' a)

type ArgumentSort = Fix ArgumentSort' Source

data Unmangling a Source

Constructors

PrimitiveUnmangling (Value -> SMTAnnotation a -> Maybe a)
ComplexUnmangling (forall m s. Monad m => (forall b. SMTValue b => s -> SMTExpr b -> SMTAnnotation b -> m (b, s)) -> s -> SMTExpr a -> SMTAnnotation a -> m (Maybe a, s))

data Mangling a Source

Constructors

PrimitiveMangling (a -> SMTAnnotation a -> Value)
ComplexMangling (a -> SMTAnnotation a -> SMTExpr a)

class (SMTType t, Show t) => SMTValue t where Source

Haskell values which can be represented as SMT constants

Methods

unmangle :: Unmangling t Source

mangle :: Mangling t Source

class (SMTValue t, Num t, SMTAnnotation t ~ ()) => SMTArith t Source

A type class for all types which support arithmetic operations in SMT

class SMTType t => SMTOrd t where Source

Lifts the Ord class into SMT

Methods

(.<.) :: SMTExpr t -> SMTExpr t -> SMTExpr Bool infix 4 Source

(.>=.) :: SMTExpr t -> SMTExpr t -> SMTExpr Bool infix 4 Source

(.>.) :: SMTExpr t -> SMTExpr t -> SMTExpr Bool infix 4 Source

(.<=.) :: SMTExpr t -> SMTExpr t -> SMTExpr Bool infix 4 Source

data SMTArray i v Source

An array which maps indices of type i to elements of type v.

Constructors

SMTArray

Instances

Eq (SMTArray i v) Source
Ord (SMTArray i v) Source
type SMTAnnotation (SMTArray idx val) = (ArgAnnotation idx, SMTAnnotation val) Source

data FunInfo Source

Constructors

forall arg r . (Args arg, SMTType r) => FunInfo
Fields funInfoProxy :: Proxy (arg, r) funInfoArgAnn :: ArgAnnotation arg funInfoResAnn :: SMTAnnotation r funInfoName :: Maybe String

data AnyBackend m Source

Constructors

forall b . SMTBackend b m => AnyBackend b

Instances

Monad m => SMTBackend (AnyBackend m) m Source

data SMT' m a Source

The SMT monad used for communating with the SMT solver

Constructors

SMT
Fields runSMT :: forall b. SMTBackend b m => b -> m (a, b)

Instances

MonadTrans SMT' Source
Monad m => Monad (SMT' m) Source
Functor m => Functor (SMT' m) Source
MonadFix m => MonadFix (SMT' m) Source
(Monad m, Functor m) => Applicative (SMT' m) Source
MonadIO m => MonadIO (SMT' m) Source

type SMT = SMT' IO Source

smtBackend :: Monad m => (forall b. SMTBackend b m => b -> m (res, b)) -> SMT' m res Source

data Untyped Source

Constructors

forall t . SMTType t => Untyped t

Instances

Eq Untyped Source
Ord Untyped Source
type SMTAnnotation Untyped = ProxyArg Source

data UntypedValue Source

Constructors

forall t . SMTValue t => UntypedValue t

Instances

Eq UntypedValue Source
Ord UntypedValue Source
Show UntypedValue Source
type SMTAnnotation UntypedValue = ProxyArgValue Source

data SMTExpr t where Source

An abstract SMT expression

Constructors

Var :: SMTType t => Integer -> SMTAnnotation t -> SMTExpr t
QVar :: SMTType t => Integer -> Integer -> SMTAnnotation t -> SMTExpr t
FunArg :: SMTType t => Integer -> SMTAnnotation t -> SMTExpr t
Const :: SMTValue t => t -> SMTAnnotation t -> SMTExpr t
AsArray :: (Args arg, SMTType res) => SMTFunction arg res -> ArgAnnotation arg -> SMTExpr (SMTArray arg res)
Forall :: Integer -> [ProxyArg] -> SMTExpr Bool -> SMTExpr Bool
Exists :: Integer -> [ProxyArg] -> SMTExpr Bool -> SMTExpr Bool
Let :: Integer -> [SMTExpr Untyped] -> SMTExpr b -> SMTExpr b
App :: (Args arg, SMTType res) => SMTFunction arg res -> arg -> SMTExpr res
Named :: SMTExpr a -> Integer -> SMTExpr a
InternalObj :: (SMTType t, Typeable a, Ord a, Show a) => a -> SMTAnnotation t -> SMTExpr t
UntypedExpr :: SMTType t => SMTExpr t -> SMTExpr Untyped
UntypedExprValue :: SMTValue t => SMTExpr t -> SMTExpr UntypedValue

Instances

Show (SMTExpr t) Source
type Unpacked (SMTExpr a) = a Source
type ArgAnnotation (SMTExpr a) = SMTAnnotation a Source
type Lifted [SMTExpr a] i = [SMTExpr (SMTArray i a)] Source
type Lifted (SMTExpr a) i = SMTExpr (SMTArray i a) Source

data Sort' a Source

Constructors

BoolSort
IntSort
RealSort
BVSort
Fields bvSortWidth :: Integer bvSortUntyped :: Bool
ArraySort [a] a
NamedSort String [a]

Instances

Functor Sort' Source
Foldable Sort' Source
Traversable Sort' Source
Eq a => Eq (Sort' a) Source
Ord a => Ord (Sort' a) Source
Show a => Show (Sort' a) Source

type Sort = Fix Sort' Source

data Value Source

Constructors

BoolValue Bool
IntValue Integer
RealValue (Ratio Integer)
BVValue
Fields bvValueWidth :: Integer bvValueValue :: Integer
ConstrValue String [Value] (Maybe (String, [Sort]))

Instances

Eq Value Source
Ord Value Source
Show Value Source

data SMTFunction arg res where Source

Constructors

SMTEq :: SMTType a => SMTFunction [SMTExpr a] Bool
SMTMap :: (Liftable arg, SMTType res, Args i) => SMTFunction arg res -> SMTFunction (Lifted arg i) (SMTArray i res)
SMTFun :: (Args arg, SMTType res) => Integer -> SMTAnnotation res -> SMTFunction arg res
SMTBuiltIn :: (Liftable arg, SMTType res) => String -> SMTAnnotation res -> SMTFunction arg res
SMTOrd :: SMTArith a => SMTOrdOp -> SMTFunction (SMTExpr a, SMTExpr a) Bool
SMTArith :: SMTArith a => SMTArithOp -> SMTFunction [SMTExpr a] a
SMTMinus :: SMTArith a => SMTFunction (SMTExpr a, SMTExpr a) a
SMTIntArith :: SMTIntArithOp -> SMTFunction (SMTExpr Integer, SMTExpr Integer) Integer
SMTDivide :: SMTFunction (SMTExpr Rational, SMTExpr Rational) Rational
SMTNeg :: (SMTType a, Num a) => SMTFunction (SMTExpr a) a
SMTAbs :: (SMTType a, Num a) => SMTFunction (SMTExpr a) a
SMTNot :: SMTFunction (SMTExpr Bool) Bool
SMTLogic :: SMTLogicOp -> SMTFunction [SMTExpr Bool] Bool
SMTDistinct :: SMTType a => SMTFunction [SMTExpr a] Bool
SMTToReal :: SMTFunction (SMTExpr Integer) Rational
SMTToInt :: SMTFunction (SMTExpr Rational) Integer
SMTITE :: SMTType a => SMTFunction (SMTExpr Bool, SMTExpr a, SMTExpr a) a
SMTBVComp :: IsBitVector a => SMTBVCompOp -> SMTFunction (SMTExpr (BitVector a), SMTExpr (BitVector a)) Bool
SMTBVBin :: IsBitVector a => SMTBVBinOp -> SMTFunction (SMTExpr (BitVector a), SMTExpr (BitVector a)) (BitVector a)
SMTBVUn :: IsBitVector a => SMTBVUnOp -> SMTFunction (SMTExpr (BitVector a)) (BitVector a)
SMTSelect :: (Liftable i, SMTType v) => SMTFunction (SMTExpr (SMTArray i v), i) v
SMTStore :: (Liftable i, SMTType v) => SMTFunction (SMTExpr (SMTArray i v), i, SMTExpr v) (SMTArray i v)
SMTConstArray :: (Args i, SMTType v) => ArgAnnotation i -> SMTFunction (SMTExpr v) (SMTArray i v)
SMTConcat :: Concatable a b => SMTFunction (SMTExpr (BitVector a), SMTExpr (BitVector b)) (BitVector (ConcatResult a b))
SMTExtract :: (TypeableNat start, TypeableNat len, Extractable from len') => Proxy start -> Proxy len -> SMTFunction (SMTExpr (BitVector from)) (BitVector len')
SMTConstructor :: (Args arg, SMTType dt) => Constructor arg dt -> SMTFunction arg dt
SMTConTest :: (Args arg, SMTType dt) => Constructor arg dt -> SMTFunction (SMTExpr dt) Bool
SMTFieldSel :: (SMTType a, SMTType f) => Field a f -> SMTFunction (SMTExpr a) f
SMTDivisible :: Integer -> SMTFunction (SMTExpr Integer) Bool

Instances

Show (SMTFunction arg res) Source

class SMTValue (BitVector a) => IsBitVector a where Source

Methods

getBVSize :: Proxy a -> SMTAnnotation (BitVector a) -> Integer Source

class (IsBitVector a, IsBitVector b, IsBitVector (ConcatResult a b)) => Concatable a b where Source

Associated Types

type ConcatResult a b Source

Methods

concatAnnotation :: a -> b -> SMTAnnotation (BitVector a) -> SMTAnnotation (BitVector b) -> SMTAnnotation (BitVector (ConcatResult a b)) Source

class (IsBitVector a, IsBitVector b) => Extractable a b where Source

Methods

extractAnn :: a -> b -> Integer -> SMTAnnotation (BitVector a) -> SMTAnnotation (BitVector b) Source

getExtractLen :: a -> b -> SMTAnnotation (BitVector b) -> Integer Source

data Constructor arg res Source

Represents a constructor of a datatype a Can be obtained by using the template haskell extension module

Constructors

Constructor [ProxyArg] DataType Constr

Instances

Show (Constructor arg res) Source

data Field a f Source

Represents a field of the datatype a of the type f

Constructors

Field [ProxyArg] DataType Constr DataField

Instances

Show (Field a f) Source

newtype InterpolationGroup Source

Constructors

InterpolationGroup Integer

Instances

Eq InterpolationGroup Source
Ord InterpolationGroup Source
Show InterpolationGroup Source

newtype ClauseId Source

Identifies a clause in an unsatisfiable core

Constructors

ClauseId Integer

Instances

Eq ClauseId Source
Ord ClauseId Source
Show ClauseId Source

data SMTOption Source

Options controling the behaviour of the SMT solver

Constructors

PrintSuccess Bool	Whether or not to print "success" after each operation
ProduceModels Bool	Produce a satisfying assignment after each successful checkSat
ProduceProofs Bool	Produce a proof of unsatisfiability after each failed checkSat
ProduceUnsatCores Bool	Enable the querying of unsatisfiable cores after a failed checkSat
ProduceInterpolants Bool	Enable the generation of craig interpolants

Instances

Eq SMTOption Source
Ord SMTOption Source
Show SMTOption Source

data SMTInfo i where Source

Constructors

SMTSolverName :: SMTInfo String
SMTSolverVersion :: SMTInfo String

class (Ord a, Typeable a, Show a, Ord (ArgAnnotation a), Typeable (ArgAnnotation a), Show (ArgAnnotation a)) => Args a where Source

Instances of this class may be used as arguments for constructed functions and quantifiers.

Minimal complete definition

foldsExprs, extractArgAnnotation, toArgs, getTypes, getArgAnnotation

Associated Types

type ArgAnnotation a Source

Methods

foldExprs :: Monad m => (forall t. SMTType t => s -> SMTExpr t -> SMTAnnotation t -> m (s, SMTExpr t)) -> s -> a -> ArgAnnotation a -> m (s, a) Source

foldsExprs :: Monad m => (forall t. SMTType t => s -> [(SMTExpr t, b)] -> SMTAnnotation t -> m (s, [SMTExpr t], SMTExpr t)) -> s -> [(a, b)] -> ArgAnnotation a -> m (s, [a], a) Source

extractArgAnnotation :: a -> ArgAnnotation a Source

toArgs :: ArgAnnotation a -> [SMTExpr Untyped] -> Maybe (a, [SMTExpr Untyped]) Source

fromArgs :: a -> [SMTExpr Untyped] Source

getTypes :: a -> ArgAnnotation a -> [ProxyArg] Source

getArgAnnotation :: a -> [Sort] -> (ArgAnnotation a, [Sort]) Source

Instances

Args () Source

getSorts :: Args a => a -> ArgAnnotation a -> [Sort] Source

foldExprsId :: Args a => (forall t. SMTType t => s -> SMTExpr t -> SMTAnnotation t -> (s, SMTExpr t)) -> s -> a -> ArgAnnotation a -> (s, a) Source

foldsExprsId :: Args a => (forall t. SMTType t => s -> [(SMTExpr t, b)] -> SMTAnnotation t -> (s, [SMTExpr t], SMTExpr t)) -> s -> [(a, b)] -> ArgAnnotation a -> (s, [a], a) Source

class Args a => Liftable a where Source

Associated Types

type Lifted a i Source

Methods

getLiftedArgumentAnn :: a -> i -> ArgAnnotation a -> ArgAnnotation i -> ArgAnnotation (Lifted a i) Source

inferLiftedAnnotation :: a -> i -> ArgAnnotation (Lifted a i) -> (ArgAnnotation i, ArgAnnotation a) Source

getConstraint :: Args i => p (a, i) -> Dict (Liftable (Lifted a i)) Source

argSorts :: Args a => a -> ArgAnnotation a -> [Sort] Source

unpackArgs :: Args a => (forall t. SMTType t => SMTExpr t -> SMTAnnotation t -> s -> (c, s)) -> a -> ArgAnnotation a -> s -> ([c], s) Source

class Args a => LiftArgs a where Source

An extension of the Args class: Instances of this class can be represented as native haskell data types.

Associated Types

type Unpacked a Source

Methods

liftArgs :: Unpacked a -> ArgAnnotation a -> a Source

Converts a haskell value into its SMT representation.

unliftArgs :: Monad m => a -> (forall t. SMTValue t => SMTExpr t -> m t) -> m (Unpacked a) Source

Converts a SMT representation back into a haskell value.

firstJust :: [Maybe a] -> Maybe a Source

getUndef :: SMTExpr t -> t Source

getFunUndef :: SMTFunction arg res -> (arg, res) Source

getArrayUndef :: Args i => SMTExpr (SMTArray i v) -> (i, Unpacked i, v) Source

withSMTBackendExitCleanly :: SMTBackend b IO => b -> SMT a -> IO a Source

withSMTBackend :: SMTBackend a m => a -> SMT' m b -> m b Source

withSMTBackend' :: SMTBackend a m => a -> Bool -> SMT' m b -> m b Source

funInfoSort :: FunInfo -> Sort Source

funInfoArgSorts :: FunInfo -> [Sort] Source

argsSignature :: Args a => a -> ArgAnnotation a -> [Sort] Source

argumentSortToSort :: Monad m => (Integer -> m Sort) -> ArgumentSort -> m Sort Source

sortToArgumentSort :: Sort -> ArgumentSort Source

declareType :: (Monad m, SMTType t) => t -> SMTAnnotation t -> SMT' m () Source

data DataTypeInfo Source

Constructors

DataTypeInfo
Fields structures :: [TypeCollection] datatypes :: Map String (DataType, TypeCollection) constructors :: Map String (Constr, DataType, TypeCollection) fields :: Map String (DataField, Constr, DataType, TypeCollection)

data TypeCollection Source

Constructors

TypeCollection
Fields argCount :: Integer dataTypes :: [DataType]

data ProxyArg Source

Constructors

forall t . SMTType t => ProxyArg t (SMTAnnotation t)

Instances

Eq ProxyArg Source
Ord ProxyArg Source
Show ProxyArg Source

data ProxyArgValue Source

Constructors

forall t . SMTValue t => ProxyArgValue t (SMTAnnotation t)

Instances

Eq ProxyArgValue Source
Ord ProxyArgValue Source
Show ProxyArgValue Source

withProxyArg :: ProxyArg -> (forall t. SMTType t => t -> SMTAnnotation t -> a) -> a Source

withProxyArgValue :: ProxyArgValue -> (forall t. SMTValue t => t -> SMTAnnotation t -> a) -> a Source

data AnyValue Source

Constructors

forall t . SMTType t => AnyValue [ProxyArg] t (SMTAnnotation t)

withAnyValue :: AnyValue -> (forall t. SMTType t => [ProxyArg] -> t -> SMTAnnotation t -> a) -> a Source

castAnyValue :: SMTType t => AnyValue -> Maybe (t, SMTAnnotation t) Source

data DataType Source

Constructors

DataType
Fields dataTypeName :: String dataTypeConstructors :: [Constr] dataTypeGetUndefined :: forall r. [ProxyArg] -> (forall t. SMTType t => t -> SMTAnnotation t -> r) -> r

data Constr Source

Constructors

Constr
Fields conName :: String conFields :: [DataField] construct :: forall r. [Maybe ProxyArg] -> [AnyValue] -> (forall t. SMTType t => [ProxyArg] -> t -> SMTAnnotation t -> r) -> r conUndefinedArgs :: forall r. [ProxyArg] -> (forall arg. Args arg => arg -> ArgAnnotation arg -> r) -> r conTest :: forall t. SMTType t => [ProxyArg] -> t -> Bool

data DataField Source

Constructors

DataField
Fields fieldName :: String fieldSort :: ArgumentSort fieldGet :: forall r t. SMTType t => [ProxyArg] -> t -> (forall f. SMTType f => f -> SMTAnnotation f -> r) -> r

emptyDataTypeInfo :: DataTypeInfo Source

containsTypeCollection :: TypeCollection -> DataTypeInfo -> Bool Source

addDataTypeStructure :: TypeCollection -> DataTypeInfo -> DataTypeInfo Source

getNewTypeCollections :: SMTType t => Proxy t -> SMTAnnotation t -> DataTypeInfo -> ([TypeCollection], DataTypeInfo) Source

Get all the type collections which are not yet declared from a type.

asNamedSort :: Sort -> Maybe (String, [Sort]) Source

escapeName :: Either (String, Integer) Integer -> String Source

escapeName' :: String -> String Source

unescapeName :: String -> Maybe (Either (String, Integer) Integer) Source

unescapeName' :: String -> Maybe (String, Integer) Source

data SMTState Source

Constructors

SMTState
Fields nextVar :: Integer nextInterpolationGroup :: Integer nextClauseId :: Integer allVars :: Map Integer (FunInfo, Integer) namedVars :: Map (String, Integer) Integer nameCount :: Map String Integer declaredDataTypes :: DataTypeInfo

emptySMTState :: SMTState Source

smtStateAddFun :: FunInfo -> SMTState -> (Integer, String, SMTState) Source

data Z Source

Constructors

Z

Instances

TypeableNat Z Source
type Add Z n = n Source

data S a Source

Constructors

S

Instances

TypeableNat n => TypeableNat (S n) Source
type Add (S n1) n2 = S (Add n1 n2) Source

class Typeable a => TypeableNat a where Source

Methods

reflectNat :: Proxy a -> Integer -> Integer Source

Instances

TypeableNat Z Source
TypeableNat n => TypeableNat (S n) Source

type family Add n1 n2 Source

Instances

type Add Z n = n Source
type Add (S n1) n2 = S (Add n1 n2) Source

data BVUntyped Source

Constructors

BVUntyped

Instances

Eq BVUntyped Source
Ord BVUntyped Source
Show BVUntyped Source
type ConcatResult BVUntyped BVUntyped = BVUntyped Source
type ConcatResult BVUntyped (BVTyped n2) = BVUntyped Source
type SMTAnnotation (BitVector BVUntyped) = Integer Source
type ConcatResult (BVTyped n1) BVUntyped = BVUntyped Source

data BVTyped n Source

Constructors

BVTyped

Instances

Eq (BVTyped n) Source
Ord (BVTyped n) Source
Show (BVTyped n) Source
type ConcatResult BVUntyped (BVTyped n2) = BVUntyped Source
type SMTAnnotation (BitVector (BVTyped n)) = () Source
type ConcatResult (BVTyped n1) BVUntyped = BVUntyped Source
type ConcatResult (BVTyped n1) (BVTyped n2) = BVTyped (Add n1 n2) Source

reifyNat :: (Num a, Ord a) => a -> (forall n. TypeableNat n => Proxy n -> r) -> r Source

reifySum :: (Num a, Ord a) => a -> a -> (forall n1 n2. (TypeableNat n1, TypeableNat n2, TypeableNat (Add n1 n2)) => Proxy n1 -> Proxy n2 -> Proxy (Add n1 n2) -> r) -> r Source

reifyExtract :: (Num a, Ord a) => a -> a -> a -> (forall n1 n2 n3 n4. (TypeableNat n1, TypeableNat n2, TypeableNat n3, TypeableNat n4, Add n4 n2 ~ S n3) => Proxy n1 -> Proxy n2 -> Proxy n3 -> Proxy n4 -> r) -> r Source

data BitVector b Source

Constructors

BitVector Integer

Instances

Enum (BitVector a) Source
Eq (BitVector b) Source
Ord (BitVector b) Source
Show (BitVector a) Source
type SMTAnnotation (BitVector (BVTyped n)) = () Source
type SMTAnnotation (BitVector BVUntyped) = Integer Source