SMT solving
Sort
The declared kind of value an SMT term may have.
Definition
Sort
A sort classifies SMT values and determines which operations may be applied to them.
Bool, Int, Real, and fixed-width bit-vectors are common sorts. A well-sorted query cannot add an integer to a Boolean value.
01
Example
In SMT-LIB, (_ BitVec 8) is the sort of eight-bit vectors.
02
Important distinction
A sort resembles a programming-language type, but each formal language defines its own exact rules.
After reading this article, you should be able to
- Define Sort in the sense used on this site.
- Detect a sort mismatch in a small SMT expression.