Trait ProjectionFunction 

pub trait ProjectionFunction:
    Debug
    + Send
    + Sync {
    // Required methods
    fn compare(&self, a: TermId, b: TermId, manager: &TermManager) -> bool;
    fn mk_lt(&self, x: TermId, y: TermId, manager: &mut TermManager) -> TermId;
}

Trait for projection functions (maps infinite domain to finite representatives)

Required Methods

fn compare(&self, a: TermId, b: TermId, manager: &TermManager) -> bool

Compare two values (for sorting)

fn mk_lt(&self, x: TermId, y: TermId, manager: &mut TermManager) -> TermId

Create a less-than term

Implementors

impl ProjectionFunction for ArithmeticProjection