Language.SMTLib2.Internals.Interface

class Same tps

class IsSMTNumber tp

class HasMonad a

Expressions

Constants

constant

asConstant

true

false

cbool

cint

creal

cbv

cbvUntyped

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

Lists

(.:.)

nil