Struct InterfaceEqualityManager 

pub struct InterfaceEqualityManager { /* private fields */ }

Interface equality manager.

Implementations

impl InterfaceEqualityManager

pub fn new() -> Self

Create new manager.

pub fn with_config(config: InterfaceEqualityConfig) -> Self

Create with configuration.

pub fn stats(&self) -> &InterfaceEqualityStats

Get statistics.

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

Register a term with theory.

pub fn assert_equality( &mut self, lhs: TermId, rhs: TermId, ) -> Result<(), String>

Assert equality and merge equivalence classes.

pub fn get_pending_batch(&mut self) -> Vec<InterfaceEquality>

Get pending equalities (batch).

pub fn get_all_pending(&mut self) -> Vec<InterfaceEquality>

Get all pending equalities.

pub fn set_strategy( &mut self, term: TermId, strategy: GenerationStrategy, ) -> Result<(), String>

Set generation strategy for a term’s equivalence class.

pub fn minimize_equalities(&mut self)

Minimize pending equalities.

Remove redundant equalities that can be inferred from others.

pub fn update_relevancy(&mut self, term: TermId, score: u32)

Update relevancy score for a term.

pub fn push_decision_level(&mut self)

Push new decision level.

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

Backtrack to decision level.

pub fn clear(&mut self)

Clear all state.

pub fn reset_stats(&mut self)

Reset statistics.

pub fn pending_count(&self) -> usize

Get number of pending equalities.

pub fn is_generated(&self, eq: &Equality) -> bool

Check if equality has been generated.

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

Force generation of all equalities for shared classes.

pub fn get_eclass(&self, term: TermId) -> Option<&InterfaceEClass>

Get equivalence class for a term.

pub fn get_representative(&self, term: TermId) -> Option<TermId>

Get representative for a term.

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

Check if two terms are in the same equivalence class.

Trait Implementations

impl Default for InterfaceEqualityManager

fn default() -> Self

Returns the “default value” for a type.