Struct Problem 

pub struct Problem { /* private fields */ }

A theorem proving problem consisting of axioms and an optional conjecture.

A Problem is constructed by adding axioms (assumed to be true) and optionally a conjecture (the statement to be proved). The problem is then solved by calling Problem::solve, which invokes the Vampire theorem prover.

Examples

Basic Usage

use vampire_prover::{Function, Predicate, Problem, ProofRes, Options, forall};

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

let result = Problem::new(Options::new())
    .with_axiom(human.with(socrates))
    .with_axiom(forall(|x| human.with(x) >> mortal.with(x)))
    .conjecture(mortal.with(socrates))
    .solve();

assert_eq!(result, ProofRes::Proved);

Without Conjecture

You can also create problems without a conjecture to check satisfiability:

use vampire_prover::{Function, Predicate, Problem, Options};

let p = Predicate::new("P", 1);
let x = Function::constant("x");

let result = Problem::new(Options::new())
    .with_axiom(p.with(x))
    .with_axiom(!p.with(x))  // Contradiction
    .solve();

// This should be unsatisfiable

Implementations

impl Problem

pub fn new(options: Options) -> Self

Creates a new empty problem with the given options.

Arguments

• options - Configuration options for the prover

Examples

use vampire_prover::{Problem, Options};
use std::time::Duration;

// Default options
let problem = Problem::new(Options::new());

// With timeout
let problem = Problem::new(Options::new().timeout(Duration::from_secs(5)));

pub fn with_axiom(self, f: Formula) -> Self

Adds an axiom to the problem.

Axioms are formulas assumed to be true. The prover will use these axioms to attempt to prove the conjecture (if one is provided).

This method consumes self and returns a new Problem, allowing for method chaining.

Arguments

• f - The axiom formula to add

Examples

use vampire_prover::{Function, Predicate, Problem, Options, forall};

let p = Predicate::new("P", 1);
let q = Predicate::new("Q", 1);

let problem = Problem::new(Options::new())
    .with_axiom(forall(|x| p.with(x)))
    .with_axiom(forall(|x| p.with(x) >> q.with(x)));

pub fn conjecture(self, f: Formula) -> Self

Sets the conjecture for the problem.

The conjecture is the statement that the prover will attempt to prove from the axioms. A problem can have at most one conjecture.

This method consumes self and returns a new Problem, allowing for method chaining.

Arguments

• f - The conjecture formula

Examples

use vampire_prover::{Function, Predicate, Problem, Options, forall};

let p = Predicate::new("P", 1);
let q = Predicate::new("Q", 1);

let problem = Problem::new(Options::new())
    .with_axiom(forall(|x| p.with(x) >> q.with(x)))
    .conjecture(forall(|x| q.with(x)));  // Try to prove this

pub fn solve(self) -> ProofRes

Solves the problem using the Vampire theorem prover.

This method consumes the problem and invokes Vampire to either prove the conjecture from the axioms, find a counterexample, or determine that the result is unknown.

Returns

A ProofRes indicating whether the conjecture was proved, found to be unprovable, or whether the result is unknown (due to timeout, memory limits, or incompleteness).

Examples

use vampire_prover::{Function, Predicate, Problem, ProofRes, Options, forall};

let p = Predicate::new("P", 1);
let x = Function::constant("x");

let result = Problem::new(Options::new())
    .with_axiom(p.with(x))
    .conjecture(p.with(x))
    .solve();

assert_eq!(result, ProofRes::Proved);

Trait Implementations

impl Clone for Problem

fn clone(&self) -> Problem

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Problem

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

Formats the value using the given formatter.