Struct Predicate 

pub struct Predicate { /* private fields */ }

A predicate symbol in first-order logic.

Predicates represent relations or properties that can be true or false. They take terms as arguments and produce formulas. Like functions, predicates have a fixed arity.

Examples

use vampire_prover::{Function, Predicate};

// Unary predicate (property)
let is_mortal = Predicate::new("mortal", 1);
let socrates = Function::constant("socrates");
let formula = is_mortal.with(socrates); // mortal(socrates)

// Binary predicate (relation)
let loves = Predicate::new("loves", 2);
let alice = Function::constant("alice");
let bob = Function::constant("bob");
let formula = loves.with([alice, bob]); // loves(alice, bob)

Implementations

impl Predicate

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

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

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

Arguments

• name - The name of the predicate symbol
• arity - The number of arguments this predicate takes

Examples

use vampire_prover::Predicate;

let edge = Predicate::new("edge", 2);
assert_eq!(edge.arity(), 2);

// Same name and arity returns the same symbol
let edge2 = Predicate::new("edge", 2);
assert_eq!(edge, edge2);

// Same name but different arity is a different symbol
let edge3 = Predicate::new("edge", 3);
assert_ne!(edge.arity(), edge3.arity());

pub fn arity(&self) -> u32

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

Examples

use vampire_prover::Predicate;

let p = Predicate::new("p", 2);
assert_eq!(p.arity(), 2);

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

Applies this predicate to the given arguments, creating a formula.

This method accepts multiple argument formats for convenience:

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

Panics

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

Examples

use vampire_prover::{Function, Predicate};

let mortal = Predicate::new("mortal", 1);
let socrates = Function::constant("socrates");

// Single argument:
let formula = mortal.with(socrates);

// Multiple arguments:
let edge = Predicate::new("edge", 2);
let a = Function::constant("a");
let b = Function::constant("b");
let e = edge.with([a, b]);

Trait Implementations

impl Clone for Predicate

fn clone(&self) -> Predicate

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Predicate

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

Formats the value using the given formatter.

impl Hash for Predicate

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 PartialEq for Predicate

fn eq(&self, other: &Predicate) -> 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 Predicate

impl Eq for Predicate

impl StructuralPartialEq for Predicate