Enum ProofRes 

pub enum ProofRes {
    Proved,
    Unprovable,
    Unknown(UnknownReason),
}

The result of attempting to prove a theorem.

After calling Problem::solve, Vampire returns one of three possible results:

• ProofRes::Proved: The conjecture was successfully proved from the axioms
• ProofRes::Unprovable: The axioms are insufficient to prove the conjecture
• ProofRes::Unknown: Vampire could not determine if the axioms imply the conjecture

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

match result {
    ProofRes::Proved => println!("Theorem proved!"),
    ProofRes::Unprovable => println!("Counterexample found"),
    ProofRes::Unknown(reason) => println!("Unknown: {:?}", reason),
}

Variants

Proved

The conjecture was successfully proved from the axioms.

Unprovable

The axioms are insufficient to prove the conjecture.

Vampire has determined that the given axioms do not imply the conjecture. Note that this does not mean the conjecture is false - it could still be true or false, but the provided axioms alone cannot establish it.

Unknown(UnknownReason)

Vampire could not determine whether the axioms imply the conjecture.

This can happen for several reasons, detailed in UnknownReason.

Trait Implementations

impl Clone for ProofRes

fn clone(&self) -> ProofRes

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Copy for ProofRes

impl Debug for ProofRes

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

Formats the value using the given formatter.

impl Eq for ProofRes

impl Hash for ProofRes

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 ProofRes

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