Struct SharedTermsManager 

pub struct SharedTermsManager { /* private fields */ }

Shared terms manager for theory combination.

Implementations

impl SharedTermsManager

pub fn new(config: SharedTermsConfig) -> Self

Create a new shared terms manager.

pub fn default_config() -> Self

Create with default configuration.

pub fn register_term(&mut self, term: TermId, theory: TheoryId)

Register a shared term.

pub fn is_shared(&self, term: TermId) -> bool

Check if a term is shared between multiple theories.

pub fn get_theories(&self, term: TermId) -> Vec<TheoryId>

Get theories that use a term.

pub fn assert_equality(&mut self, lhs: TermId, rhs: TermId)

Assert equality between two terms.

This merges their equivalence classes and queues notifications.

pub fn are_equal(&mut self, lhs: TermId, rhs: TermId) -> bool

Check if two terms are in the same equivalence class.

pub fn get_pending_equalities(&self) -> &[Equality]

Get pending equalities to propagate.

pub fn flush_equalities(&mut self)

Flush pending equalities (send to theories).

pub fn get_shared_terms(&self) -> Vec<TermId>

Get all shared terms.

pub fn stats(&self) -> &SharedTermsStats

Get statistics.

pub fn reset(&mut self)

Reset manager state.

Trait Implementations

impl Debug for SharedTermsManager

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.