Struct Term 

pub struct Term { /* private fields */ }

A term in first-order logic.

Terms represent objects in the domain of discourse. A term can be:

• A constant: socrates
• A variable: x
• A function application: add(x, y)

Examples

use vampire_prover::{Function, Term};

// Create a constant
let zero = Function::constant("0");

// Create a variable
let x = Term::new_var(0);

// Create a function application
let succ = Function::new("succ", 1);
let one = succ.with(zero);

Implementations

impl Term

pub fn new_function(func: Function, args: &[Term]) -> Self

Creates a term by applying a function to arguments.

This is typically called via Function::with rather than directly.

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);

let sum = Term::new_function(add, &[x, y]);

pub fn new_var(idx: u32) -> Self

Creates a variable with the given index.

Variables are typically used within quantified formulas. The index should be unique within a formula. For automatic variable management, consider using the forall and exists helper functions instead.

Arguments

• idx - The unique index for this variable

Examples

use vampire_prover::Term;

let x = Term::new_var(0);
let y = Term::new_var(1);

pub fn free_var() -> (Self, u32)

Creates a fresh variable with an automatically assigned index.

Returns both the variable term and its index. This is primarily used internally by the forall and exists functions.

Examples

use vampire_prover::Term;

let (x, idx) = Term::free_var();
assert_eq!(idx, 0);

let (y, idx2) = Term::free_var();
assert_eq!(idx2, 1);

pub fn eq(&self, rhs: Term) -> Formula

Creates an equality formula between this term and another.

Arguments

• rhs - The right-hand side of the equality

Examples

use vampire_prover::{Function, forall};

let succ = Function::new("succ", 1);
let zero = Function::constant("0");

// ∀x. succ(x) = succ(x)
let reflexive = forall(|x| {
    let sx = succ.with(x);
    sx.eq(sx)
});

Trait Implementations

impl Clone for Term

fn clone(&self) -> Term

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Term

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

Formats the value using the given formatter.

impl Hash for Term

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 IntoTermArgs for Term

fn as_slice(&self) -> &[Term]

Convert this type into a slice of terms.

impl PartialEq for Term

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

Tests for self and other values to be equal, and is used by ==.

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

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Copy for Term

impl Eq for Term

impl StructuralPartialEq for Term