Struct Lemma 

pub struct Lemma {
    pub premises: String,
    pub goal: String,
}

One step of a proof a solver checks: SMT-LIB 2 premises — the terms it reads and the facts it assumes — and a goal asserting that two terms differ, or that a read strays out of range. The premises are satisfiable, so nothing follows from them vacuously; with the goal they are not, exactly when the step holds.

Fields

premises: String

Declarations, definitions and the asserted facts.

goal: String

The one assert of the goal.

Implementations

impl Lemma

pub fn text(&self) -> String

The premises and the goal, as one SMT-LIB 2 script without commands.

Trait Implementations

impl Clone for Lemma

fn clone(&self) -> Lemma

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Lemma

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

Formats the value using the given formatter.

impl PartialEq for Lemma

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

impl StructuralPartialEq for Lemma