Language.SMTLib2.Internals.Interface
checkSat
checkSatUsing
checkSat'
isSat
apply
push
pop
stack
comment
varNamed
varNamedAnn
varAnn
var
untypedNamedVar
untypedVar
argVarsAnn
argVarsAnnNamed
argVarsAnnNamed'
argVars
constant
constantAnn
getValue
getValues
getModel
unmangleArray
defFun
defConst
defConstNamed
defConstNamed'
defFunAnnNamed
defFunAnnNamed'
defFunAnn
and'
(.&&.)
or'
(.||.)
arrayEquals
assert
interpolationGroup
assertId
assertInterp
getInterpolant
interpolate
setOption
getInfo
funAnn
funAnnNamed
funAnnNamed'
funAnnRet
fun
app
map'
(.==.)
argEq
distinct
plus
mult
minus
div'
div''
mod'
mod''
rem'
rem''
divide
divide'
neg
toReal
toInt
ite
xor
(.=>.)
not'
not''
select
store
asArray
constArray
bvand
bvor
bvxor
bvnot
bvneg
bvadd
bvsub
bvmul
bvurem
bvsrem
bvudiv
bvsdiv
bvule
bvult
bvuge
bvugt
bvsle
bvslt
bvsge
bvsgt
bvshl
bvlshr
bvashr
bvconcat
bvextract
bvextract'
bvsplitu16to8
bvsplitu32to16
bvsplitu32to8
bvsplitu64to32
bvsplitu64to16
bvsplitu64to8
mkQuantified
forAll
forAllAnn
exists
existsAnn
let'
letAnn
lets
forAllList
existsList
is
(.#)
head'
tail'
isNil
isInsert
setLogic
named
named'
getProof
simplify
getUnsatCore
optimizeExpr'