Language.SMTLib2

Data types

data SMT' m a

type SMT

class SMTBackend a m

data AnyBackend m

class SMTType t

class SMTValue t

class SMTArith t

class SMTOrd t

data SMTExpr t

data SMTFunction arg res

data SMTOption

data SMTArray i v

data Constructor arg res

data Field a f

class Args a

class LiftArgs a

Environment

withSMTBackend

withSMTBackendExitCleanly

setOption

getInfo

setLogic

data SMTInfo i

assert

push

pop

stack

checkSat

checkSat'

checkSatUsing

apply

data CheckSatResult

data CheckSatLimits

noLimits

getValue

getValues

getModel

comment

getProof

simplify

Unsatisfiable Core

data ClauseId

assertId

getUnsatCore

Interpolation

data InterpolationGroup

interpolationGroup

assertInterp

getInterpolant

Expressions

var

varNamed

varNamedAnn

varAnn

argVars

argVarsAnn

argVarsAnnNamed

untypedVar

untypedNamedVar

constant

constantAnn

extractAnnotation

let'

lets

letAnn

named

named'

optimizeExpr

optimizeExpr'

foldExpr

foldExprM

foldArgs

foldArgsM

Basic logic

(.==.)

argEq

distinct

ite

(.&&.)

(.||.)

and'

or'

xor

not'

not''

(.=>.)

forAll

exists

forAllAnn

existsAnn

forAllList

existsList

Arithmetic

plus

minus

mult

div'

mod'

rem'

neg

divide

toReal

toInt

Arrays

select

store

arrayEquals

unmangleArray

asArray

constArray

Bitvectors

bvand

bvor

bvxor

bvnot

bvneg

bvadd

bvsub

bvmul

bvurem

bvsrem

bvudiv

bvsdiv

bvule

bvult

bvuge

bvugt

bvsle

bvslt

bvsge

bvsgt

bvshl

bvlshr

bvashr

data BitVector b

data BVTyped n

data BVUntyped

type BV8

type BV16

type BV32

type BV64

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

bvconcat

bvsplitu16to8

bvsplitu32to16

bvsplitu32to8

bvsplitu64to32

bvsplitu64to16

bvsplitu64to8

bvextract

bvextract'

Functions

funAnn

funAnnNamed

funAnnRet

fun

app

defFun

defConst

defConstNamed

defFunAnn

defFunAnnNamed

map'

Data types

is

(.#)

Lists

head'

tail'

insert'

isNil

isInsert

Untyped expressions

data Untyped

data UntypedValue

entype

entypeValue

castUntypedExpr

castUntypedExprValue