Language.SMTLib2

SMT Monad

data SMT b a

class Embed m e

class Backend b

withBackend

withBackendExitCleanly

Setting options

setOption

data SMTOption

Getting informations about the solver

getInfo

data SMTInfo i

Expressions

Declaring variables

declareVar

declareVarNamed

Defining variables

defineVar

defineVarNamed

Declaring functions

declareFun

declareFunNamed

Defining functions

defineFun

defineFunNamed

Constants

constant

data Value a

Boolean constants

cbool

true

false

Integer constants

cint

Real constants

creal

Bitvector constants

data BitWidth bw

bw

cbv

cbvUntyped

Datatype constants

cdt

Quantification

exists

forall

Functions

app

fun

Equality

eq

(.==.)

distinct

(./=.)

Map

map'

Comparison

ord

(.>=.)

(.>.)

(.<=.)

(.<.)

Arithmetic

arith

plus

(.+.)

mult

(.*.)

minus

(.-.)

neg

div'

mod'

rem'

(./.)

abs'

Logic

not'

logic

and'

(.&.)

or'

(.|.)

xor'

implies

(.=>.)

Conversion

toReal

toInt

If-then-else

ite

Bitvectors

bvcomp

bvule

bvult

bvuge

bvugt

bvsle

bvslt

bvsge

bvsgt

bvbin

bvadd

bvsub

bvmul

bvurem

bvsrem

bvudiv

bvsdiv

bvshl

bvlshr

bvashr

bvxor

bvand

bvor

bvun

bvnot

bvneg

concat'

extract'

extractChecked

extractUntypedStart

extractUntyped

Arrays

select

select1

store

store1

constArray

Datatypes

mk

is

(.#.)

Misc

divisible

Analyzation

getExpr

Satisfiability

assert

checkSat

checkSatWith

data CheckSatResult

data CheckSatLimits

noLimits

Unsatisfiable core

assertId

getUnsatCore

Interpolation

assertPartition

data Partition

getInterpolant

Proofs

getProof

analyzeProof

Stack

push

pop

stack

Models

getValue

getModel

modelEvaluate

Types

registerDatatype

data Type

data Repr t

class GetType v

bool

int

real

bitvec

array

dt

dt'

Numbers

data Nat

data Natural n

nat

natT

reifyNat

Lists

data List e tp

reifyList

(.:.)

nil

Misc

comment

simplify