Struct ProofResult 

pub struct ProofResult {
    pub proven: bool,
    pub proof_time_us: u64,
    pub explanation: String,
    pub theorem: String,
}

Result of a successful Z3 proof.

Fields

proven: bool

Whether the proof succeeded (Sat = provable, Unsat = unprovable for negation)

proof_time_us: u64

Time taken to prove (microseconds)

explanation: String

Human-readable explanation of what was proven

theorem: String

The theorem that was proven (in mathematical notation)

Implementations

impl ProofResult

pub fn proven(theorem: &str, explanation: &str, proof_time_us: u64) -> Self

Create a new successful proof result.

Trait Implementations

impl Clone for ProofResult

fn clone(&self) -> ProofResult

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ProofResult

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

Formats the value using the given formatter.