Struct ProjectionFunctionDef 

pub struct ProjectionFunctionDef {
    pub arg_index: usize,
    pub sort: SortId,
    pub values: Vec<TermId>,
    pub value_to_term: FxHashMap<TermId, TermId>,
    pub term_to_value: FxHashMap<TermId, TermId>,
}

Definition of a projection function for argument position

Fields

arg_index: usize

Argument index this projection is for

sort: SortId

Sort being projected

values: Vec<TermId>

Sorted values that appear in function applications

value_to_term: FxHashMap<TermId, TermId>

Mapping from value to representative term

term_to_value: FxHashMap<TermId, TermId>

Mapping from term to value

Implementations

impl ProjectionFunctionDef

pub fn new(arg_index: usize, sort: SortId) -> Self

Create a new projection function definition

pub fn add_value(&mut self, value: TermId, term: TermId)

Add a value to the projection

pub fn project(&self, value: TermId) -> Option<TermId>

Project a value to its representative

Trait Implementations

impl Clone for ProjectionFunctionDef

fn clone(&self) -> ProjectionFunctionDef

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for ProjectionFunctionDef

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.