Enum SmtPredicate 

pub enum SmtPredicate {
    Eq(SmtTerm, SmtTerm),
    Ne(SmtTerm, SmtTerm),
    Le(SmtTerm, SmtTerm),
    Lt(SmtTerm, SmtTerm),
    Ge(SmtTerm, SmtTerm),
    Gt(SmtTerm, SmtTerm),
    And(Vec<SmtPredicate>),
    Divisible {
        term: SmtTerm,
        modulus: u64,
    },
    InBounds {
        index: SmtTerm,
        access_count: SmtTerm,
        len: SmtTerm,
    },
    NonOverlapping {
        left: SmtTerm,
        right: SmtTerm,
        left_count: SmtTerm,
        right_count: SmtTerm,
        elem_size: u64,
    },
    Not(Box<SmtPredicate>),
    Custom(String),
}

Common boolean predicate asserted or refuted by SMT queries.

Variants

Eq(SmtTerm, SmtTerm)

Ne(SmtTerm, SmtTerm)

Le(SmtTerm, SmtTerm)

Lt(SmtTerm, SmtTerm)

Ge(SmtTerm, SmtTerm)

Gt(SmtTerm, SmtTerm)

And(Vec<SmtPredicate>)

Divisible

Fields

term: SmtTerm

modulus: u64

InBounds

Fields

index: SmtTerm

access_count: SmtTerm

len: SmtTerm

NonOverlapping

Fields

left: SmtTerm

right: SmtTerm

left_count: SmtTerm

right_count: SmtTerm

elem_size: u64

Not(Box<SmtPredicate>)

Custom(String)

Implementations

impl SmtPredicate

pub fn describe(&self) -> String

Render this predicate for diagnostics.

Trait Implementations

impl Clone for SmtPredicate

fn clone(&self) -> SmtPredicate

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for SmtPredicate

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

Formats the value using the given formatter.