Theories

SMT-LIB logics refer to one or more theories below. Click on a theory's name to see its declaration in Version 2.x of the format.

ArraysEx
Functional arrays with extensionality
FixedSizeBitVectors
Bit vectors with arbitrary size
Core
Core theory, defining the basic Boolean operators
FloatingPoint
Floating point numbers
Ints
Integer numbers
Reals
Real numbers
Reals_Ints
Real and integer numbers

Theory declarations for Version 1.2 of SMT-LIB, superseded by the ones above, are still available here although their use is deprecated.