Enum Query 

#[non_exhaustive]
pub enum Query<'q> {
    IsZero(Expr),
    IsNonZero(Expr),
    Bit {
        e: Expr,
        bit: u16,
        value: bool,
    },
    Eq(Expr, Expr),
    Cmp(CmpOpExt, Expr, Expr),
    InURange {
        e: Expr,
        lo: &'q BitVec,
        hi: &'q BitVec,
    },
    InSRange {
        e: Expr,
        lo: &'q BitVec,
        hi: &'q BitVec,
    },
    Aligned {
        e: Expr,
        log2: u16,
    },
    MaskRedundant {
        e: Expr,
        mask: &'q BitVec,
    },
    FitsUnsigned {
        e: Expr,
        bits: u16,
    },
    FitsSigned {
        e: Expr,
        bits: u16,
    },
    IsConstant(Expr),
    Injective {
        e: Expr,
        of: Expr,
    },
    Bijective {
        e: Expr,
        of: Expr,
    },
}

A question about expression values, answered by Context::prove.

Variants (Non-exhaustive)

Non-exhaustive enums could have additional variants added in future. Therefore, when matching against variants of non-exhaustive enums, an extra wildcard arm must be added to account for any future variants.

IsZero(Expr)

The value is zero.

IsNonZero(Expr)

The value is not zero.

Bit

Bit bit has value value.

Fields

e: Expr

The expression.

bit: u16

The bit index.

value: bool

The value asked about.

Eq(Expr, Expr)

The two values are equal.

Cmp(CmpOpExt, Expr, Expr)

The comparison holds.

InURange

The value is in [lo, hi] (unsigned).

Fields

e: Expr

The expression.

lo: &'q BitVec

Lower bound.

hi: &'q BitVec

Upper bound.

InSRange

The value is in [lo, hi] (signed).

Fields

e: Expr

The expression.

lo: &'q BitVec

Lower bound.

hi: &'q BitVec

Upper bound.

Aligned

The value is a multiple of 2^log2.

Fields

e: Expr

The expression.

log2: u16

Alignment exponent.

MaskRedundant

e & mask == e.

Fields

e: Expr

The expression.

mask: &'q BitVec

The mask.

FitsUnsigned

The unsigned value fits in bits bits.

Fields

e: Expr

The expression.

bits: u16

Number of bits.

FitsSigned

The signed value fits in bits bits.

Fields

e: Expr

The expression.

bits: u16

Number of bits.

IsConstant(Expr)

The facts pin the value to one constant.

Injective

e is an injective function of its subexpression of: with every value that does not depend on of held fixed, distinct values put in place of of give distinct values of e. Proved through a chain of invertible layers from of up to e (operators injective in one operand with the others fixed, such as x ^ k, x * k for odd k, rotations, zext, declared extension operations, and triangular maps such as h ^ ((h >>u 32) >>u (h >>u 60))); False when e does not depend on of or is narrower than it.

Fields

e: Expr

The expression.

of: Expr

The subexpression it is read as a function of.

Bijective

e is a bijective function of its subexpression of: injective (see Query::Injective), of the same width. False when e does not depend on of or their widths differ.

Fields

e: Expr

The expression.

of: Expr

The subexpression it is read as a function of.

Trait Implementations

impl<'q> Clone for Query<'q>

fn clone(&self) -> Self

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<'q> Copy for Query<'q>

impl<'q> Debug for Query<'q>

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

Formats the value using the given formatter.