Struct Options 

pub struct Options { /* private fields */ }

Configuration options for the Vampire theorem prover.

Options allow you to configure the behavior of the prover, such as setting time limits. Use the builder pattern to construct options.

Examples

use vampire_prover::Options;
use std::time::Duration;

// Default options (no timeout)
let opts = Options::new();

// Set a timeout
let opts = Options::new().timeout(Duration::from_secs(5));

Implementations

impl Options

pub fn new() -> Self

Creates a new Options with default settings.

By default, no timeout is set.

Examples

use vampire_prover::Options;

let opts = Options::new();

Examples found in repository

examples/name_reuse.rs (line 20)

fn main() {
    let x1 = Function::new("x", 0);
    let x2 = Function::new("x", 0);

    dbg!(x1, x2);
    dbg!(x1 == x2);

    let y1 = Function::new("y", 0);
    let y2 = Function::new("y", 1);

    dbg!(y1, y2);

    let z1 = Function::new("z", 0);
    let z2 = Predicate::new("z", 0);

    dbg!(z1, z2);

    let solution = Problem::new(Options::new())
        .with_axiom(y1.with(&[]).eq(y2.with(&[y1.with(&[])])))
        .solve();

    dbg!(solution);
}

examples/group.rs (line 33)

fn main() {
    // Prove that the identity element works on the left using group axioms
    // In group theory, if we define a group with:
    //   - Right identity: x * 1 = x
    //   - Right inverse: x * inv(x) = 1
    //   - Associativity: (x * y) * z = x * (y * z)
    // Then we can prove the left identity: 1 * x = x

    let mult = Function::new("mult", 2);
    let inv = Function::new("inv", 1);
    let one = Function::constant("1");

    // Helper to make multiplication more readable
    let mul = |x: Term, y: Term| -> Term { mult.with([x, y]) };

    // Axiom 1: Right identity - ∀x. x * 1 = x
    let right_identity = forall(|x| mul(x, one).eq(x));

    // Axiom 2: Right inverse - ∀x. x * inv(x) = 1
    let right_inverse = forall(|x| {
        let inv_x = inv.with(x);
        mul(x, inv_x).eq(one)
    });

    // Axiom 3: Associativity - ∀x,y,z. (x * y) * z = x * (y * z)
    let associativity = forall(|x| forall(|y| forall(|z| mul(mul(x, y), z).eq(mul(x, mul(y, z))))));

    // Conjecture: Left identity - ∀x. 1 * x = x
    let left_identity = forall(|x| mul(one, x).eq(x));

    let (solution, proof) = Problem::new(Options::new())
        .with_axiom(right_identity)
        .with_axiom(right_inverse)
        .with_axiom(associativity)
        .conjecture(left_identity)
        .solve_and_prove();

    if let Some(proof) = proof {
        println!("{}", proof);
    }

    assert_eq!(solution, ProofRes::Proved);
}

examples/bench_index2.rs (line 167)

fn run_proof(i: usize) -> ProofRes {
    // Prove that every subgroup of index 2 is normal.
    let mult = Function::new(&format!("mult{i}"), 2);
    let inv = Function::new(&format!("inv{i}"), 1);
    let one = Function::constant(&format!("1{i}"));

    // Helper to make multiplication more readable
    let mul = |x: Term, y: Term| -> Term { mult.with(&[x, y]) };

    // Group Axiom 1: Right identity - ∀x. x * 1 = x
    let right_identity = forall(|x| mul(x, one).eq(x));

    // Group Axiom 2: Right inverse - ∀x. x * inv(x) = 1
    let right_inverse = forall(|x| {
        let inv_x = inv.with(&[x]);
        mul(x, inv_x).eq(one)
    });

    // Group Axiom 3: Associativity - ∀x,y,z. (x * y) * z = x * (y * z)
    let associativity = forall(|x| forall(|y| forall(|z| mul(mul(x, y), z).eq(mul(x, mul(y, z))))));

    // Describe the subgroup
    let h = Predicate::new("h", 1);

    // Any subgroup contains the identity
    let h_ident = h.with(&[one]);

    // And is closed under multiplication
    let h_mul_closed =
        forall(|x| forall(|y| (h.with(&[x]) & h.with(&[y])) >> h.with(&[mul(x, y)])));

    // And is closed under inverse
    let h_inv_closed = forall(|x| h.with(&[x]) >> h.with(&[inv.with(&[x])]));

    // H specifically is of order 2
    let h_index_2 = exists(|x| {
        // an element not in H
        let not_in_h = !h.with(&[x]);
        // but everything is in H or x H
        let class = forall(|y| h.with(&[y]) | h.with(&[mul(inv.with(&[x]), y)]));

        not_in_h & class
    });

    // Conjecture: H is normal
    let h_normal = forall(|x| {
        let h_x = h.with(&[x]);
        let conj_x = forall(|y| {
            let y_inv = inv.with(&[y]);
            h.with(&[mul(mul(y, x), y_inv)])
        });
        h_x.iff(conj_x)
    });

    Problem::new(Options::new())
        .with_axiom(right_identity)
        .with_axiom(right_inverse)
        .with_axiom(associativity)
        .with_axiom(h_ident)
        .with_axiom(h_mul_closed)
        .with_axiom(h_inv_closed)
        .with_axiom(h_index_2)
        .conjecture(h_normal)
        .solve()
}

examples/group2.rs (line 56)

fn main() {
    // Prove that every subgroup of index 2 is normal.
    let mult = Function::new("mult", 2);
    let inv = Function::new("inv", 1);
    let one = Function::constant("1");

    // Helper to make multiplication more readable
    let mul = |x: Term, y: Term| -> Term { mult.with([x, y]) };

    // Group Axiom 1: Right identity - ∀x. x * 1 = x
    let right_identity = forall(|x| mul(x, one).eq(x));

    // Group Axiom 2: Right inverse - ∀x. x * inv(x) = 1
    let right_inverse = forall(|x| {
        let inv_x = inv.with(x);
        mul(x, inv_x).eq(one)
    });

    // Group Axiom 3: Associativity - ∀x,y,z. (x * y) * z = x * (y * z)
    let associativity = forall(|x| forall(|y| forall(|z| mul(mul(x, y), z).eq(mul(x, mul(y, z))))));

    // Describe the subgroup
    let h = Predicate::new("h", 1);

    // Any subgroup contains the identity
    let h_ident = h.with(one);

    // And is closed under multiplication
    let h_mul_closed = forall(|x| forall(|y| (h.with(x) & h.with(y)) >> h.with(mul(x, y))));

    // And is closed under inverse
    let h_inv_closed = forall(|x| h.with(x) >> h.with(inv.with(x)));

    // H specifically is of order 2
    let h_index_2 = exists(|x| {
        // an element not in H
        let not_in_h = !h.with(x);
        // but everything is in H or x H
        let class = forall(|y| h.with(y) | h.with(mul(inv.with(x), y)));

        not_in_h & class
    });

    // Conjecture: H is normal
    let h_normal = forall(|x| {
        let h_x = h.with(x);
        let conj_x = forall(|y| {
            let y_inv = inv.with(y);
            h.with(mul(mul(y, x), y_inv))
        });
        h_x.iff(conj_x)
    });

    let (solution, proof) = Problem::new(Options::new())
        .with_axiom(right_identity)
        .with_axiom(right_inverse)
        .with_axiom(associativity)
        .with_axiom(h_ident)
        .with_axiom(h_mul_closed)
        .with_axiom(h_inv_closed)
        .with_axiom(h_index_2)
        .conjecture(h_normal)
        .solve_and_prove();

    if let Some(proof) = proof {
        println!("{}", proof);
    }

    assert_eq!(solution, ProofRes::Proved);
}

pub fn timeout(&mut self, duration: Duration) -> &mut Self

Sets the timeout for the prover.

If the prover exceeds this time limit, it will return ProofRes::Unknown(UnknownReason::Timeout).

Arguments

• duration - The maximum time the prover should run

Examples

use vampire_prover::Options;
use std::time::Duration;

let opts = Options::new().timeout(Duration::from_secs(10));

Trait Implementations

impl Clone for Options

fn clone(&self) -> Options

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Options

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

Formats the value using the given formatter.

impl Default for Options

fn default() -> Self

Returns the “default value” for a type.