Struct Function

Source

pub struct Function { /* private fields */ }

Expand description

A function symbol in first-order logic.

Functions represent operations that take terms as arguments and produce new terms. They have a fixed arity (number of arguments). A function with arity 0 is called a constant and represents a specific object in the domain.

§Examples

use vampire_prover::Function;

// Create a constant (0-ary function)
let socrates = Function::constant("socrates");

// Create a unary function
let successor = Function::new("succ", 1);

// Create a binary function
let add = Function::new("add", 2);

Implementations§

Source §

impl Function

Source

pub fn new(name: &str, arity: u32) -> Self

Creates a new function symbol with the given name and arity.

Calling this method multiple times with the same name and arity will return the same function symbol. It is safe to call this with the same name but different arities - they will be treated as distinct function symbols.

§Arguments

name - The name of the function symbol
arity - The number of arguments this function takes

§Examples

use vampire_prover::Function;

let mult = Function::new("mult", 2);
assert_eq!(mult.arity(), 2);

// Same name and arity returns the same symbol
let mult2 = Function::new("mult", 2);
assert_eq!(mult, mult2);

// Same name but different arity is a different symbol
let mult3 = Function::new("mult", 3);
assert_ne!(mult.arity(), mult3.arity());

Source

pub fn arity(&self) -> u32

Returns the arity (number of arguments) of this function.

§Examples

use vampire_prover::Function;

let f = Function::new("f", 3);
assert_eq!(f.arity(), 3);

Source

pub fn constant(name: &str) -> Term

Creates a constant term (0-ary function).

This is a convenience method equivalent to Function::new(name, 0).with([]). Constants represent specific objects in the domain.

§Arguments

name - The name of the constant

§Examples

use vampire_prover::Function;

let socrates = Function::constant("socrates");
let zero = Function::constant("0");

Source

pub fn with(&self, args: impl IntoTermArgs) -> Term

Applies this function to the given arguments, creating a term.

This method accepts multiple argument formats for convenience:

Single term: f.with(x)
Array: f.with([x, y])

§Panics

Panics if the number of arguments does not match the function’s arity.

§Examples

use vampire_prover::{Function, Term};

let add = Function::new("add", 2);
let x = Term::new_var(0);
let y = Term::new_var(1);

// Multiple arguments:
let sum = add.with([x, y]);

// Single argument:
let succ = Function::new("succ", 1);
let sx = succ.with(x);