Struct DelayedCombination 

pub struct DelayedCombination { /* private fields */ }

Delayed theory combination engine.

Implementations

impl DelayedCombination

pub fn new(config: DelayedCombinationConfig) -> Self

Create a new delayed combination engine.

pub fn default_config() -> Self

Create with default configuration.

pub fn register_shared_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 defer_equality(&mut self, lhs: TermId, rhs: TermId, source: TheoryId)

Defer an equality for later propagation.

pub fn force_propagation(&mut self)

Force propagation of all deferred equalities.

pub fn handle_conflict(&mut self)

Handle a conflict by activating theory combination.

pub fn activate_theory(&mut self, theory: TheoryId)

Activate a theory.

pub fn is_theory_active(&self, theory: TheoryId) -> bool

Check if a theory is active.

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

Get theories that share a term.

pub fn stats(&self) -> &DelayedCombinationStats

Get statistics.

pub fn reset_stats(&mut self)

Reset statistics.

Trait Implementations

impl Debug for DelayedCombination

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

Formats the value using the given formatter.

impl Default for DelayedCombination

fn default() -> Self

Returns the “default value” for a type.