Skip to main content

ProjectionFunction

oxiz_solver::mbqi::model_completion

Trait ProjectionFunction 

Source 
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;
}
Expand description

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

Required Methods§

Source

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

Compare two values (for sorting)

Source

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

Create a less-than term

Dyn Compatibility§

This trait is dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementors§