Struct TermCaches 

pub(crate) struct TermCaches<'z3, 'tcx> {
    pub(crate) sizes: FxHashMap<Ty<'tcx>, Int<'z3>>,
    pub(crate) aligns: FxHashMap<Ty<'tcx>, Int<'z3>>,
    pub(crate) not_mask_terms: FxHashSet<Int<'z3>>,
    pub(crate) exact_div_roots: FxHashMap<Int<'z3>, Int<'z3>>,
    pub(crate) div_roots: FxHashMap<Int<'z3>, (Int<'z3>, Int<'z3>)>,
    pub(crate) iter_ptr_offset: FxHashMap<AllocId, (Int<'z3>, Option<Int<'z3>>)>,
    pub(crate) uninit_byte: Option<Int<'z3>>,
}

Term-provenance caches, one per phenomenon the VM must shape by hand.

Z3’s nonlinear integer solver (NIA) cannot rewrite degree-3 products or deeply-nested pointer chains, so the VM records the semantic meaning of a symbol (what it divides, which iterator it indexes, …) and uses that provenance later to emit a compact, degree-≤2 term instead. Each cache is independent — they share only the path-scoped, monotonic lifetime.

Fields

sizes: FxHashMap<Ty<'tcx>, Int<'z3>>

sizeof_T for each generic type, one symbolic constant per type. Keeps ptr.add strides, access_bytes element sizes, and allocation sizes consistent so that SMT can cancel the S factor in InBound.

aligns: FxHashMap<Ty<'tcx>, Int<'z3>>

align_T for each generic type, one symbolic constant per type; linked to the size by the layout constraint sizeof_T % align_T == 0.

not_mask_terms: FxHashSet<Int<'z3>>

Terms that are the result of a bitwise Not (two’s-complement mask). Used to recognize x & !(align-1) alignment patterns in BitAnd so we can derive align = -mask and emit linear bounds for the result.

exact_div_roots: FxHashMap<Int<'z3>, Int<'z3>>

quotient → dividend for each exact division (lhs % rhs == 0), recording which size each exact_div symbol divides (e.g. us → sizeof_T). Lets a later us_len = (len / ts) * us multiplication emit the byte bound us_len * sizeof_U <= len * sizeof_T.

div_roots: FxHashMap<Int<'z3>, (Int<'z3>, Int<'z3>)>

quotient → (lhs, rhs) for each non-exact division, recovering the len and divisor (ts) operands at a following us_len = (len / ts) * us.

iter_ptr_offset: FxHashMap<AllocId, (Int<'z3>, Option<Int<'z3>>)>

Per-iterator element index, keyed by the buffer the iterator walks (end field’s provenance alloc id, which is frame-independent). The value is (offset, base_len): the current element index and the total element count (the end field’s Element offset, None when unknown). Caching both keeps next/len/is_empty checks linear (base_len - offset) instead of a deeply-nested ((base + S) + S) … pointer chain that Z3’s NIA cannot reason about.

uninit_byte: Option<Int<'z3>>

UNINIT sentinel byte value (≥ 256, outside the u8 value range). The default element of every byte array; select(array, i) != UNINIT is how “byte i was written” is decided.

Trait Implementations

impl<'z3, 'tcx> Default for TermCaches<'z3, 'tcx>

fn default() -> Self

Returns the “default value” for a type.