Struct Fun

pub struct Fun<'st> {
    pub st: &'st Storage,
    pub name: &'st str,
    pub vars: &'st [Sort<'st>],
    pub return_sort: Sort<'st>,
}

A function declaration.

Fields

st: &'st Storage

smtlib storage

name: &'st str

The name of the function.

vars: &'st [Sort<'st>]

The sorts of the arguments.

return_sort: Sort<'st>

The sort of the return value.

Implementations

impl<'st> Fun<'st>

pub fn new( st: &'st Storage, name: impl Into<String>, vars: Vec<Sort<'st>>, return_ty: Sort<'st>, ) -> Self

Create a new function declaration.

pub fn call(&self, args: &[Dynamic<'st>]) -> Result<Dynamic<'st>, Error>

Call the function with the given arguments.

The arguments must be sorted in the same order as the function declaration and checked for both arity and sort.

pub fn ast(&self) -> FunctionDec<'_>

Get the lowlevel AST representation of the function declaration.

Trait Implementations

impl<'st> Debug for Fun<'st>

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

Formats the value using the given formatter.