Skip to main content

TheoryCombination

oxiz_solver

Trait TheoryCombination 

Source 
pub trait TheoryCombination {
    // Required methods
    fn notify_equality(&mut self, eq: EqualityNotification) -> bool;
    fn get_shared_equalities(&self) -> Vec<EqualityNotification>;
    fn is_relevant(&self, term: TermId) -> bool;
}
Expand description

Interface for theory combination via Nelson-Oppen Theories implement this to participate in equality sharing

Required Methods§

Source

fn notify_equality(&mut self, eq: EqualityNotification) -> bool

Notify the theory of a new equality derived by another theory Returns true if the equality was accepted and processed

Source

fn get_shared_equalities(&self) -> Vec<EqualityNotification>

Get all equalities derived by this theory that should be shared These are equalities between terms that appear in multiple theories

Source

fn is_relevant(&self, term: TermId) -> bool

Check if a term is relevant to this theory

Implementors§