Enum Function 

pub enum Function {
    Variable(Variable),
    Primitive(Primitive),
    User(UserFunction),
}

A function.

The Function type represent any function usable to build terms.

A function can be a user function, i.e. a UserFunction object which in turn can be either Declared or Defined, a Variable, or a Primitive.

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

Variants

Variable(Variable)

A variable.

Primitive(Primitive)

A primitive function declared by some theory.

User(UserFunction)

A user function, i.e. either Declared or Defined.

Implementations

impl Function

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

Get the name of the function.

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

Get the type-level parameters of a function.

Only primitive functions can be parametric and the parameters returned here are the ones that SMT-LIBv2 theory declarations introduce with the par keyword.

These are not the sorts of the arguments of the function. For that, call domain().

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 Function

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 Function

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

Formats the value using the given formatter.

impl Eq for Function

impl From<Declared> for Function

fn from(val: Declared) -> Self

Converts to this type from the input type.

impl From<Defined> for Function

fn from(val: Defined) -> Self

Converts to this type from the input type.

impl From<Function> for SortHead

fn from(value: Function) -> Self

Converts to this type from the input type.

impl From<Function> for BoundRef

fn from(function: Function) -> Self

Converts to this type from the input type.

impl From<Function> for FunctionRef

fn from(val: Function) -> Self

Converts to this type from the input type.

impl From<Function> for Atom

fn from(val: Function) -> Self

Converts to this type from the input type.

impl From<Primitive> for Function

fn from(value: Primitive) -> 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<Variable> for Function

fn from(value: Variable) -> Self

Converts to this type from the input type.

impl Hash for Function

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 Function

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

Gets the Span tracked by the type.

impl PartialEq for Function

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

Equality operator ==.

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

Inequality operator !=.

impl StructuralPartialEq for Function

impl ToTerm for Function

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.