SMT solving
Theory
A set of meanings and laws for a class of values and operations.
Definition
Theory
In SMT, a theory fixes the semantics of values and operations such as integer addition or bit-vector multiplication.
A theory solver can use facts that are not visible in pure Boolean structure. For integers, x < y and y < x is inconsistent because the order relation has defined laws.
01
Example
Linear integer arithmetic is a theory for integer variables, addition, inequalities, and multiplication by constants.
02
Important distinction
The word theory here means a formal semantic domain, not an untested explanation.
After reading this article, you should be able to
- Define Theory in the sense used on this site.
- Identify which theory gives meaning to the operations in a query.