Enum UserFunction 

pub enum UserFunction {
    Declared(Declared),
    Defined(Defined),
}

A user function, i.e. a function either declared or defined in some Solver.

Some accessor methods are provided to get fields in common between the variants avoiding redundant pattern matches.

Variants

Declared(Declared)

A declared function.

Defined(Defined)

A defined function.

Implementations

impl UserFunction

pub fn name(&self) -> &Identifier<'static>

Get the name of the function.

pub fn domain(&self) -> Vec<Sort>

Get the domain of the function, i.e. the sorts of its arguments.

pub fn range(&self) -> &Sort

Get the range of the function, i.e. the sort of its return value.

Trait Implementations

impl Clone for UserFunction

fn clone(&self) -> Self

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for UserFunction

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

Formats the value using the given formatter.

impl Eq for UserFunction

impl From<Declared> for UserFunction

fn from(value: Declared) -> Self

Converts to this type from the input type.

impl From<Defined> for UserFunction

fn from(value: Defined) -> Self

Converts to this type from the input type.

impl From<UserFunction> for Function

fn from(value: UserFunction) -> Self

Converts to this type from the input type.

impl From<UserFunction> for SortHead

fn from(val: UserFunction) -> Self

Converts to this type from the input type.

impl From<UserFunction> for FunctionRef

fn from(val: UserFunction) -> Self

Converts to this type from the input type.

impl From<UserFunction> for Atom

fn from(val: UserFunction) -> Self

Converts to this type from the input type.

impl Hash for UserFunction

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl Located for UserFunction

fn span(&self) -> Option<Span>

Gets the Span tracked by the type.

impl PartialEq for UserFunction

fn eq(&self, other: &Self) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl StructuralPartialEq for UserFunction

impl ToTerm for UserFunction

fn into_term_in(self, pool: &dyn TermPool) -> Term

Convert the object into a Term by uniquing in the given TermPool.

fn to_term_in(&self, pool: &dyn TermPool) -> Term

Convert the object (by reference) into a Term by uniquing in the given TermPool.