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. When a subterm belongs to a different theory than the parent application, it is replaced by a fresh shared variable, and an equality constraint is recorded between the fresh variable and the original subterm.

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. Only returns equalities that have NOT already been propagated.

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.