Struct SmtCheckResult 

pub struct SmtCheckResult {
    pub result: CheckResult,
    pub query: Option<SmtQuery>,
    pub notes: Vec<String>,
}

Result of one SMT check.

Fields

result: CheckResult

Final status produced by the SMT backend.

query: Option<SmtQuery>

Optional structured query description.

notes: Vec<String>

Human-readable explanation.

Implementations

impl SmtCheckResult

pub fn proved(note: impl Into<String>) -> Self

Build a proved SMT result.

pub fn unknown(note: impl Into<String>) -> Self

Build an unknown SMT result.

pub fn with_query(self, query: SmtQuery) -> Self

Attach the query that produced this result.

pub fn with_note(self, note: impl Into<String>) -> Self

Add a diagnostic note to this result.

pub fn describe(&self) -> String

Render this SMT result as a diagnostic block.

Trait Implementations

impl Clone for SmtCheckResult

fn clone(&self) -> SmtCheckResult

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for SmtCheckResult

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

Formats the value using the given formatter.