Struct NelsonOppenCombiner 

pub struct NelsonOppenCombiner { /* private fields */ }

Nelson-Oppen theory combination engine.

Implementations

impl NelsonOppenCombiner

pub fn new() -> Self

Create a new Nelson-Oppen combiner.

pub fn register_shared_term( &mut self, term_id: TermId, theory1: TheoryId, _theory2: TheoryId, )

Register a shared term between theories.

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

Assert an equality between shared terms.

Returns Ok(()) if consistent, Err(()) if conflict detected.

pub fn purify_term( &mut self, term_id: TermId, tm: &mut TermManager, ) -> Result<TermId, String>

Purify a term by introducing fresh variables for sub-terms.

Purification ensures each theory sees only its own symbols.

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

Get pending equalities to propagate to theories.

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

Check if two terms are in the same equivalence class.

pub fn get_equivalence_class(&self, term_id: TermId) -> Vec<TermId>

Get all terms in the equivalence class of a term.

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

Convexity closure: generate implied equalities.

For convex theories, if we have equalities in each class, we must propagate all pairwise equalities.

pub fn stats(&self) -> &NelsonOppenStats

Get statistics.

pub fn reset(&mut self)

Reset for next SMT check.

Trait Implementations

impl Default for NelsonOppenCombiner

fn default() -> Self

Returns the “default value” for a type.