Package smtlib
All operations
All constructors
Module Index
Base Libraries
Curry Packages
Curry Homepage
About CurryDoc
Index to all constructors
A
B
C
D
E
F
G
I
K
L
M
N
O
P
Q
R
S
T
U
V
A
AKW
(
Language.SMTLIB.Types
)
AllStatistics
(
Language.SMTLIB.Types
)
ALL
(
Language.SMTLIB.Types
)
Annot
(
Language.SMTLIB.Types
)
As
(
Language.SMTLIB.Types
)
Assert
(
Language.SMTLIB.Types
)
AssertionStackLevels
(
Language.SMTLIB.Types
)
AssertionStackLevelsRsp
(
Language.SMTLIB.Types
)
AttrRsp
(
Language.SMTLIB.Types
)
Authors
(
Language.SMTLIB.Types
)
AUFLIA
(
Language.SMTLIB.Types
)
AUFLIRA
(
Language.SMTLIB.Types
)
AUFNIRA
(
Language.SMTLIB.Types
)
AuthorsRsp
(
Language.SMTLIB.Types
)
AVal
(
Language.SMTLIB.Types
)
AVConst
(
Language.SMTLIB.Types
)
AVSExpr
(
Language.SMTLIB.Types
)
AVSym
(
Language.SMTLIB.Types
)
A
B
C
D
E
F
G
I
K
L
M
N
O
P
Q
R
S
T
U
V
B
Bang
(
Language.SMTLIB.Scanner
)
BVal
(
Language.SMTLIB.Scanner
)
A
B
C
D
E
F
G
I
K
L
M
N
O
P
Q
R
S
T
U
V
C
CheckSat
(
Language.SMTLIB.Types
)
CheckSatAssuming
(
Language.SMTLIB.Types
)
CheckSatRsp
(
Language.SMTLIB.Types
)
Colon
(
Language.SMTLIB.Scanner
)
Comma
(
Language.SMTLIB.Scanner
)
Comment
(
Language.SMTLIB.Types
)
Cons
(
Language.SMTLIB.Types
)
ContinuedExecution
(
Language.SMTLIB.Types
)
A
B
C
D
E
F
G
I
K
L
M
N
O
P
Q
R
S
T
U
V
D
Dec
(
Language.SMTLIB.Types
)
DECIMAL
(
Language.SMTLIB.Types
)
DeclareConst
(
Language.SMTLIB.Types
)
DeclareDatatype
(
Language.SMTLIB.Types
)
DeclareDatatypes
(
Language.SMTLIB.Types
)
DeclareFun
(
Language.SMTLIB.Types
)
DeclareSort
(
Language.SMTLIB.Types
)
DefineFun
(
Language.SMTLIB.Types
)
DefineFunRec
(
Language.SMTLIB.Types
)
DefineFunsRec
(
Language.SMTLIB.Types
)
DefineSort
(
Language.SMTLIB.Types
)
DiagnosticOutput
(
Language.SMTLIB.Types
)
DQuote
(
Language.SMTLIB.Scanner
)
A
B
C
D
E
F
G
I
K
L
M
N
O
P
Q
R
S
T
U
V
E
Echo
(
Language.SMTLIB.Types
)
EchoRsp
(
Language.SMTLIB.Types
)
ErrorBehavior
(
Language.SMTLIB.Types
)
ErrorBehaviorRsp
(
Language.SMTLIB.Types
)
ErrorRsp
(
Language.SMTLIB.Types
)
Exists
(
Language.SMTLIB.Types
)
Exit
(
Language.SMTLIB.Types
)
A
B
C
D
E
F
G
I
K
L
M
N
O
P
Q
R
S
T
U
V
F
Forall
(
Language.SMTLIB.Types
)
FunDec
(
Language.SMTLIB.Types
)
FunDef
(
Language.SMTLIB.Types
)
A
B
C
D
E
F
G
I
K
L
M
N
O
P
Q
R
S
T
U
V
G
GetAssertions
(
Language.SMTLIB.Types
)
GetAssertionsRsp
(
Language.SMTLIB.Types
)
GetAssignment
(
Language.SMTLIB.Types
)
GetAssignmentRsp
(
Language.SMTLIB.Types
)
GetInfo
(
Language.SMTLIB.Types
)
GetInfoRsp
(
Language.SMTLIB.Types
)
GetModel
(
Language.SMTLIB.Types
)
GetModelRsp
(
Language.SMTLIB.Types
)
GetOption
(
Language.SMTLIB.Types
)
GetOptionRsp
(
Language.SMTLIB.Types
)
GetProof
(
Language.SMTLIB.Types
)
GetProofRsp
(
Language.SMTLIB.Types
)
GetUnsatAssumptions
(
Language.SMTLIB.Types
)
GetUnsatAssumptionsRsp
(
Language.SMTLIB.Types
)
GetUnsatCore
(
Language.SMTLIB.Types
)
GetUnsatCoreRsp
(
Language.SMTLIB.Types
)
GetValue
(
Language.SMTLIB.Types
)
GetValueRsp
(
Language.SMTLIB.Types
)
GlobalDecls
(
Language.SMTLIB.Types
)
A
B
C
D
E
F
G
I
K
L
M
N
O
P
Q
R
S
T
U
V
I
Id
(
Language.SMTLIB.Scanner
)
Id
(
Language.SMTLIB.Types
)
Ident
(
Language.SMTLIB.Types
)
IFKW
(
Language.SMTLIB.Types
)
ImmediateExit
(
Language.SMTLIB.Types
)
Incomplete
(
Language.SMTLIB.Types
)
Interactive
(
Language.SMTLIB.Types
)
A
B
C
D
E
F
G
I
K
L
M
N
O
P
Q
R
S
T
U
V
K
KW
(
Language.SMTLIB.Types
)
KW_as
(
Language.SMTLIB.Scanner
)
KW_assert
(
Language.SMTLIB.Scanner
)
KW_assertion_stack_levels
(
Language.SMTLIB.Scanner
)
KW_authors
(
Language.SMTLIB.Scanner
)
KW_BINARY
(
Language.SMTLIB.Scanner
)
KW_check_sat
(
Language.SMTLIB.Scanner
)
KW_check_sat_assuming
(
Language.SMTLIB.Scanner
)
KW_continued_execution
(
Language.SMTLIB.Scanner
)
KW_DECIMAL
(
Language.SMTLIB.Scanner
)
KW_decl_const
(
Language.SMTLIB.Scanner
)
KW_decl_datatypes
(
Language.SMTLIB.Scanner
)
KW_decl_fun
(
Language.SMTLIB.Scanner
)
KW_decl_sort
(
Language.SMTLIB.Scanner
)
KW_def_fun
(
Language.SMTLIB.Scanner
)
KW_def_funs_rec
(
Language.SMTLIB.Scanner
)
KW_def_fun_rec
(
Language.SMTLIB.Scanner
)
KW_def_sort
(
Language.SMTLIB.Scanner
)
KW_echo
(
Language.SMTLIB.Scanner
)
KW_error
(
Language.SMTLIB.Scanner
)
KW_error_behavior
(
Language.SMTLIB.Scanner
)
KW_exists
(
Language.SMTLIB.Scanner
)
KW_exit
(
Language.SMTLIB.Scanner
)
KW_forall
(
Language.SMTLIB.Scanner
)
KW_get_assertions
(
Language.SMTLIB.Scanner
)
KW_get_assignment
(
Language.SMTLIB.Scanner
)
KW_get_info
(
Language.SMTLIB.Scanner
)
KW_get_model
(
Language.SMTLIB.Scanner
)
KW_get_option
(
Language.SMTLIB.Scanner
)
KW_get_proof
(
Language.SMTLIB.Scanner
)
KW_get_unsat_assumptions
(
Language.SMTLIB.Scanner
)
KW_get_unsat_core
(
Language.SMTLIB.Scanner
)
KW_get_value
(
Language.SMTLIB.Scanner
)
KW_HEXADEC
(
Language.SMTLIB.Scanner
)
KW_immediate_exit
(
Language.SMTLIB.Scanner
)
KW_incomplete
(
Language.SMTLIB.Scanner
)
KW_let
(
Language.SMTLIB.Scanner
)
KW_memout
(
Language.SMTLIB.Scanner
)
KW_model
(
Language.SMTLIB.Scanner
)
KW_NUMERAL
(
Language.SMTLIB.Scanner
)
KW_name
(
Language.SMTLIB.Scanner
)
KW_par
(
Language.SMTLIB.Scanner
)
KW_pop
(
Language.SMTLIB.Scanner
)
KW_push
(
Language.SMTLIB.Scanner
)
KW_reason_unknown
(
Language.SMTLIB.Scanner
)
KW_reset
(
Language.SMTLIB.Scanner
)
KW_reset_assertions
(
Language.SMTLIB.Scanner
)
KW_sat
(
Language.SMTLIB.Scanner
)
KW_STRING
(
Language.SMTLIB.Scanner
)
KW_set_info
(
Language.SMTLIB.Scanner
)
KW_set_logic
(
Language.SMTLIB.Scanner
)
KW_set_option
(
Language.SMTLIB.Scanner
)
KW_success
(
Language.SMTLIB.Scanner
)
KW_unknown
(
Language.SMTLIB.Scanner
)
KW_unsat
(
Language.SMTLIB.Scanner
)
KW_unsupported
(
Language.SMTLIB.Scanner
)
KW_version
(
Language.SMTLIB.Scanner
)
A
B
C
D
E
F
G
I
K
L
M
N
O
P
Q
R
S
T
U
V
L
Let
(
Language.SMTLIB.Types
)
LIA
(
Language.SMTLIB.Types
)
LParen
(
Language.SMTLIB.Scanner
)
LRA
(
Language.SMTLIB.Types
)
A
B
C
D
E
F
G
I
K
L
M
N
O
P
Q
R
S
T
U
V
M
Match
(
Language.SMTLIB.Types
)
Memout
(
Language.SMTLIB.Types
)
Meta
(
Language.SMTLIB.Types
)
MRFun
(
Language.SMTLIB.Types
)
MRFunRec
(
Language.SMTLIB.Types
)
MRFunsRec
(
Language.SMTLIB.Types
)
MT
(
Language.SMTLIB.Types
)
A
B
C
D
E
F
G
I
K
L
M
N
O
P
Q
R
S
T
U
V
N
Name
(
Language.SMTLIB.Types
)
NameRsp
(
Language.SMTLIB.Types
)
Not
(
Language.SMTLIB.Types
)
Num
(
Language.SMTLIB.Scanner
)
Num
(
Language.SMTLIB.Types
)
NUMERAL
(
Language.SMTLIB.Types
)
A
B
C
D
E
F
G
I
K
L
M
N
O
P
Q
R
S
T
U
V
O
OptAttr
(
Language.SMTLIB.Types
)
A
B
C
D
E
F
G
I
K
L
M
N
O
P
Q
R
S
T
U
V
P
ParFunSymDecl
(
Language.SMTLIB.Types
)
PComb
(
Language.SMTLIB.Types
)
Pop
(
Language.SMTLIB.Types
)
PrintSuccess
(
Language.SMTLIB.Types
)
ProduceAssertions
(
Language.SMTLIB.Types
)
ProduceAssign
(
Language.SMTLIB.Types
)
ProduceModels
(
Language.SMTLIB.Types
)
ProduceProofs
(
Language.SMTLIB.Types
)
ProduceUnsatAssump
(
Language.SMTLIB.Types
)
ProduceUnsatCores
(
Language.SMTLIB.Types
)
PT
(
Language.SMTLIB.Types
)
Push
(
Language.SMTLIB.Types
)
A
B
C
D
E
F
G
I
K
L
M
N
O
P
Q
R
S
T
U
V
Q
QFABV
(
Language.SMTLIB.Types
)
QFAUFBV
(
Language.SMTLIB.Types
)
QFAUFLIA
(
Language.SMTLIB.Types
)
QFAX
(
Language.SMTLIB.Types
)
QFBV
(
Language.SMTLIB.Types
)
QFIDL
(
Language.SMTLIB.Types
)
QFLIA
(
Language.SMTLIB.Types
)
QFLRA
(
Language.SMTLIB.Types
)
QFNIA
(
Language.SMTLIB.Types
)
QFNRA
(
Language.SMTLIB.Types
)
QFRDL
(
Language.SMTLIB.Types
)
QFUF
(
Language.SMTLIB.Types
)
QFUFBV
(
Language.SMTLIB.Types
)
QFUFIDL
(
Language.SMTLIB.Types
)
QFUFLIA
(
Language.SMTLIB.Types
)
QFUFLRA
(
Language.SMTLIB.Types
)
QFUFNRA
(
Language.SMTLIB.Types
)
A
B
C
D
E
F
G
I
K
L
M
N
O
P
Q
R
S
T
U
V
R
RandomSeed
(
Language.SMTLIB.Types
)
ReasonUnknown
(
Language.SMTLIB.Types
)
ReasonUnknownRsp
(
Language.SMTLIB.Types
)
RegularOutput
(
Language.SMTLIB.Types
)
ReproducibleResLimit
(
Language.SMTLIB.Types
)
Reset
(
Language.SMTLIB.Types
)
ResetAssertions
(
Language.SMTLIB.Types
)
RParen
(
Language.SMTLIB.Scanner
)
A
B
C
D
E
F
G
I
K
L
M
N
O
P
Q
R
S
T
U
V
S
Sat
(
Language.SMTLIB.Types
)
SComb
(
Language.SMTLIB.Types
)
Semi
(
Language.SMTLIB.Scanner
)
SEConst
(
Language.SMTLIB.Types
)
SEKW
(
Language.SMTLIB.Types
)
SEList
(
Language.SMTLIB.Types
)
SESym
(
Language.SMTLIB.Types
)
SetInfo
(
Language.SMTLIB.Types
)
SetLogic
(
Language.SMTLIB.Types
)
SetOption
(
Language.SMTLIB.Types
)
SEReason
(
Language.SMTLIB.Types
)
SMTLib
(
Language.SMTLIB.Types
)
SortDecl
(
Language.SMTLIB.Types
)
SortSymDecl
(
Language.SMTLIB.Types
)
Spec
(
Language.SMTLIB.Types
)
Str
(
Language.SMTLIB.Types
)
STRING
(
Language.SMTLIB.Types
)
SuccessRsp
(
Language.SMTLIB.Types
)
SV
(
Language.SMTLIB.Types
)
Sym
(
Language.SMTLIB.Types
)
A
B
C
D
E
F
G
I
K
L
M
N
O
P
Q
R
S
T
U
V
T
TA
(
Language.SMTLIB.Types
)
TADefinition
(
Language.SMTLIB.Types
)
TAFuns
(
Language.SMTLIB.Types
)
TAFunsDesc
(
Language.SMTLIB.Types
)
TANotes
(
Language.SMTLIB.Types
)
TASorts
(
Language.SMTLIB.Types
)
TASortsDesc
(
Language.SMTLIB.Types
)
TAValues
(
Language.SMTLIB.Types
)
TComb
(
Language.SMTLIB.Types
)
TConst
(
Language.SMTLIB.Types
)
Theory
(
Language.SMTLIB.Types
)
A
B
C
D
E
F
G
I
K
L
M
N
O
P
Q
R
S
T
U
V
U
UFLRA
(
Language.SMTLIB.Types
)
UFNIA
(
Language.SMTLIB.Types
)
Underscore
(
Language.SMTLIB.Scanner
)
Unknown
(
Language.SMTLIB.Types
)
Unsat
(
Language.SMTLIB.Types
)
UnsupportedRsp
(
Language.SMTLIB.Types
)
A
B
C
D
E
F
G
I
K
L
M
N
O
P
Q
R
S
T
U
V
V
Verbosity
(
Language.SMTLIB.Types
)
Version
(
Language.SMTLIB.Types
)
VersionRsp
(
Language.SMTLIB.Types
)
A
B
C
D
E
F
G
I
K
L
M
N
O
P
Q
R
S
T
U
V