Language.SMTLib2.Internals

data SMTRequest response

data SMTModel

data CheckSatLimits

data CheckSatResult

class SMTBackend a m

class SMTType t

data ArgumentSort' a

type ArgumentSort

data Unmangling a

data Mangling a

class SMTValue t

class SMTArith t

class SMTOrd t

data SMTArray i v

data FunInfo

data AnyBackend m

data SMT' m a

type SMT

smtBackend

data Untyped

data UntypedValue

data SMTExpr t

data Sort' a

type Sort

data Value

data SMTFunction arg res

class IsBitVector a

class Concatable a b

class Extractable a b

data Constructor arg res

data Field a f

data InterpolationGroup

data ClauseId

data SMTOption

data SMTInfo i

class Args a

getSorts

foldExprsId

foldsExprsId

class Liftable a

argSorts

unpackArgs

class LiftArgs a

firstJust

getUndef

getFunUndef

getArrayUndef

withSMTBackendExitCleanly

withSMTBackend

withSMTBackend'

funInfoSort

funInfoArgSorts

argsSignature

argumentSortToSort

sortToArgumentSort

declareType

data DataTypeInfo

data TypeCollection

data ProxyArg

data ProxyArgValue

withProxyArg

withProxyArgValue

data AnyValue

withAnyValue

castAnyValue

data DataType

data Constr

data DataField

emptyDataTypeInfo

containsTypeCollection

addDataTypeStructure

getNewTypeCollections

asNamedSort

escapeName

escapeName'

unescapeName

unescapeName'

data SMTState

emptySMTState

smtStateAddFun

data Z

data S a

class TypeableNat a

type family Add n1 n2

data BVUntyped

data BVTyped n

reifyNat

reifySum

reifyExtract

data BitVector b

type N0

type N1

type N2

type N3

type N4

type N5

type N6

type N7

type N8

type N9

type N10

type N11

type N12

type N13

type N14

type N15

type N16

type N17

type N18

type N19

type N20

type N21

type N22

type N23

type N24

type N25

type N26

type N27

type N28

type N29

type N30

type N31

type N32

type N33

type N34

type N35

type N36

type N37

type N38

type N39

type N40

type N41

type N42

type N43

type N44

type N45

type N46

type N47

type N48

type N49

type N50

type N51

type N52

type N53

type N54

type N55

type N56

type N57

type N58

type N59

type N60

type N61

type N62

type N63

type N64

type BV8

type BV16

type BV32

type BV64

data Bound

showExpr

noLimits

data Quantified

quantificationLevel

inferSorts

valueSort