Trait SmtInt

pub trait SmtInt<'a, S: SmtSolver<'a, Int = Self>>:
    Clone
    + Debug
    + Display
    + Add<Output = Self>
    + Sub<Output = Self>
    + Mul<Output = Self>
    + Sized {
    // Required methods
    fn is_identical(&self, other: &Self) -> bool;
    fn _eq(self, other: Self) -> S::Bool;
    fn simplify(self) -> Self;
    fn as_u64(&self) -> Option<u64>;

    // Provided method
    fn into_dynamic(self) -> Dynamic<'a, S> { ... }
}

Integer expressions in the SMT solver.

Required Methods

fn is_identical(&self, other: &Self) -> bool

Returns true if both expressions are structurally identical.

fn _eq(self, other: Self) -> S::Bool

Returns an SMT expression that performs an equality comparison between the two ints.

fn simplify(self) -> Self

Simplifies, if possible, the SMT expression.

fn as_u64(&self) -> Option<u64>

Converts the integer to an u64, if possible.

Provided Methods

fn into_dynamic(self) -> Dynamic<'a, S>

Converts the integer into a Dynamic expression.

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors

impl<'ctx> SmtInt<'ctx, Z3Solver<'ctx>> for Int<'ctx>

impl<'ctx, S: SmtSolver<'ctx> + 'ctx, C: SolverCache> SmtInt<'ctx, CachedSolver<'ctx, S, C>> for CacheInt<'ctx, S>