Struct KripkeContext 

pub struct KripkeContext { /* private fields */ }

Context for tracking world variables during Kripke lowering.

For hardware verification, clock_counter tracks discrete timesteps and domain_hint disambiguates temporal vs modal lowering when the context is ambiguous.

Implementations

impl KripkeContext

pub fn new(interner: &mut Interner) -> Self

pub fn fresh_world(&mut self, interner: &mut Interner) -> Symbol

pub fn clock_counter(&self) -> u32

Get the current clock counter value (discrete timestep).

pub fn domain_hint(&self) -> Option<ModalDomain>

Get the current domain hint.