Struct FunctionInterpretation 

pub struct FunctionInterpretation {
    pub name: Spur,
    pub arity: usize,
    pub domain: SmallVec<[SortId; 4]>,
    pub range: SortId,
    pub entries: Vec<FunctionEntry>,
    pub else_value: Option<TermId>,
    pub projections: Vec<Option<ProjectionFunctionDef>>,
}

A function interpretation (finite representation of function mapping)

Fields

name: Spur

Function name

arity: usize

Arity

domain: SmallVec<[SortId; 4]>

Domain sorts

range: SortId

Range sort

entries: Vec<FunctionEntry>

Explicit entries (args -> result)

else_value: Option<TermId>

Default/else value (for arguments not in entries)

projections: Vec<Option<ProjectionFunctionDef>>

Projection functions for arguments (if any)

Implementations

impl FunctionInterpretation

pub fn new(name: Spur, domain: SmallVec<[SortId; 4]>, range: SortId) -> Self

Create a new function interpretation

pub fn add_entry(&mut self, args: Vec<TermId>, result: TermId)

Add an entry to the function table

pub fn lookup(&self, args: &[TermId]) -> Option<TermId>

Lookup a value in the function table

pub fn is_constant(&self) -> bool

Check if this is a constant function

pub fn is_partial(&self) -> bool

Check if the interpretation is partial (missing else value or entries)

pub fn max_occurrence_result(&self) -> Option<TermId>

Get the most common result value

Trait Implementations

impl Clone for FunctionInterpretation

fn clone(&self) -> FunctionInterpretation

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for FunctionInterpretation

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

Formats the value using the given formatter.