Struct CacheInt

pub struct CacheInt<'ctx, S: SmtSolver<'ctx>> { /* private fields */ }

Cacheable SMT Int type.

Trait Implementations

impl<'ctx, S: SmtSolver<'ctx>> Add for CacheInt<'ctx, S>

type Output = CacheInt<'ctx, S>

The resulting type after applying the + operator.

fn add(self, rhs: Self) -> Self::Output

Performs the + operation.

impl<'ctx, S: SmtSolver<'ctx>> Clone for CacheInt<'ctx, S>

fn clone(&self) -> Self

Returns a copy of the value.

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

Performs copy-assignment from source.

impl<'ctx, S: SmtSolver<'ctx>> Debug for CacheInt<'ctx, S>

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

Formats the value using the given formatter.

impl<'ctx, S: SmtSolver<'ctx>> Display for CacheInt<'ctx, S>

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

Formats the value using the given formatter.

impl<'ctx, S: SmtSolver<'ctx>> Mul for CacheInt<'ctx, S>

type Output = CacheInt<'ctx, S>

The resulting type after applying the * operator.

fn mul(self, rhs: Self) -> Self::Output

Performs the * operation.

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

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

Returns true if both expressions are structurally identical.

fn _eq(self, other: Self) -> CacheBool<'ctx, S>

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.

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

Converts the integer into a Dynamic expression.

impl<'ctx, S: SmtSolver<'ctx>> Sub for CacheInt<'ctx, S>

type Output = CacheInt<'ctx, S>

The resulting type after applying the - operator.

fn sub(self, rhs: Self) -> Self::Output

Performs the - operation.