Struct AdvancedSharedTermsManager 

pub struct AdvancedSharedTermsManager { /* private fields */ }

Advanced shared terms manager for theory combination.

Implementations

impl AdvancedSharedTermsManager

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 is_interface_term(&self, term: TermId) -> bool

Check if a term is an interface term.

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, explanation: EqualityExplanation, ) -> Result<(), String>

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_representative(&mut self, term: TermId) -> TermId

Get canonical representative of a term’s equivalence class.

pub fn get_eclass_members(&mut self, term: TermId) -> Vec<TermId>

Get all terms in the same equivalence class.

pub fn get_equality_explanation( &mut self, lhs: TermId, rhs: TermId, ) -> Option<EqualityExplanation>

Get explanation for why two terms are equal.

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 get_interface_terms(&self) -> Vec<TermId>

Get interface terms (minimal shared terms).

pub fn minimize_interface(&mut self) -> Vec<TermId>

Minimize interface terms.

Reduce the number of interface terms by using canonical representatives.

pub fn push_decision_level(&mut self)

Push a new decision level.

pub fn backtrack(&mut self, level: DecisionLevel) -> Result<(), String>

Backtrack to a decision level.

pub fn stats(&self) -> &SharedTermsStats

Get statistics.

pub fn reset(&mut self)

Reset manager state.

pub fn process_congruences(&mut self) -> Result<(), String>

Process pending congruences in e-graph.

pub fn detect_shared_terms( &mut self, _term_theories: &FxHashMap<TermId, FxHashSet<TheoryId>>, )

Detect new shared terms based on current theory assignments.

pub fn build_explanation_chain( &self, equalities: &[Equality], ) -> Result<EqualityExplanation, String>

Build equality explanation chain.

Trait Implementations

impl Debug for AdvancedSharedTermsManager

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

Formats the value using the given formatter.

impl Default for AdvancedSharedTermsManager

fn default() -> Self

Returns the “default value” for a type.