Enum UnknownReason 

pub enum UnknownReason {
    Timeout,
    MemoryLimit,
    Incomplete,
    Unknown,
}

The reason why a proof result is unknown.

When Vampire cannot determine whether a conjecture is provable, it returns ProofRes::Unknown with one of these reasons.

Examples

use vampire_prover::{ProofRes, UnknownReason};

let result = ProofRes::Unknown(UnknownReason::Timeout);

if let ProofRes::Unknown(reason) = result {
    match reason {
        UnknownReason::Timeout => println!("Ran out of time"),
        UnknownReason::MemoryLimit => println!("Ran out of memory"),
        UnknownReason::Incomplete => println!("Problem uses incomplete logic"),
        UnknownReason::Unknown => println!("Unknown reason"),
    }
}

Variants

Timeout

The prover exceeded its time limit before finding a proof or counterexample.

MemoryLimit

The prover exceeded its memory limit before finding a proof or counterexample.

Incomplete

The problem involves features that make the logic incomplete.

Some logical theories (e.g., higher-order logic, certain arithmetic theories) are undecidable, meaning no algorithm can always find an answer.

Unknown

The reason is unknown or not specified by Vampire.

Trait Implementations

impl Clone for UnknownReason

fn clone(&self) -> UnknownReason

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for UnknownReason

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

Formats the value using the given formatter.

impl Hash for UnknownReason

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 UnknownReason

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

impl Eq for UnknownReason

impl StructuralPartialEq for UnknownReason