|
|
|---|
|
|
|
|---|
We implement a lightweight, mostly unconditional rewriter for simplifying svex expressions in provably sound ways. This is typically used to reduce expressions before processing them with bit-blasting or other reasoning tools.
Our rewriter is only mostly unconditional, because there is an additional context-determined bitmask that can allow additional simplifications. For example, suppose we are in a context where only the bottom 4 bits are relevant (the bitmask is 15, say) and we see the expression:
(concat 5 a b)
This can then be simplified to just