SMT solving
Rewriting
Replacing a term with another term that preserves its meaning under stated rules.
Definition
Rewriting
Rewriting applies verified identities or simplifications to change the form of an expression.
A solver may fold constants, remove neutral operations, or normalize related terms before search. Each rule must preserve the query's meaning in the selected theory.
01
Example
x + 0 can rewrite to x in integer arithmetic and fixed-width bit-vector arithmetic.
02
Important distinction
A familiar algebraic rewrite may fail for floating-point values, undefined operations, or a different sort.
After reading this article, you should be able to
- Define Rewriting in the sense used on this site.
- Check whether a proposed rewrite preserves meaning in its stated theory.