Commit 09b4f0f
committed
Split type
This commit fundamentally changes the representation of expressions (`t`)
by lifting constant values out of the hash-consing machinery.
Changes:
- `t` is now a variant: `Imm of Value.t | Sym of expr Hc.hash_consed`.
- Removed `Val` and `Loc` constructors from the underlying `expr` type.
- Constants are no longer hash-consed; they are stored directly as `Imm`.
Potential Performance Improvements:
- Creating constant expressions no longer requires a hash-cons table lookup or allocation of a hash-cons node.
- The global hash-cons table is no longer polluted with ephemeral constant values.
BREAKING CHANGE: Previously, because all expressions were hash-consed, structural
equality implied physical equality (`phys_equal` was sufficient for all comparisons).
This invariant no longer holds for `Imm` values.t into Imm values and Sym hash-consed nodes1 parent 7b95c1e commit 09b4f0f
11 files changed
Lines changed: 978 additions & 836 deletions
File tree
- src/smtml
- test/unit
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
29 | 29 | | |
30 | 30 | | |
31 | 31 | | |
32 | | - | |
33 | 32 | | |
34 | 33 | | |
35 | 34 | | |
| |||
0 commit comments