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
- Strings
- Unicode character strings and regular expressions
Theory declarations for Version 1.2 of SMT-LIB, superseded by the ones above, are still available here although their use is deprecated.