Struct Int

pub struct Int<'ctx>(/* private fields */);

A Z3 Int.

Implementations

impl<'ctx> Int<'ctx>

pub fn from_z3(int: Int<'ctx>) -> Self

Wraps a [z3::ast::Int].

pub fn as_z3(&self) -> &Int<'_>

Returns the wrapped [z3::ast::Int].

Trait Implementations

impl<'ctx> Add for Int<'ctx>

type Output = Int<'ctx>

The resulting type after applying the + operator.

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

Performs the + operation.

impl<'ctx> Clone for Int<'ctx>

fn clone(&self) -> Int<'ctx>

Returns a copy of the value.

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

Performs copy-assignment from source.

impl<'ctx> Debug for Int<'ctx>

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

Formats the value using the given formatter.

impl Display for Int<'_>

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

Formats the value using the given formatter.

impl<'ctx> Mul for Int<'ctx>

type Output = Int<'ctx>

The resulting type after applying the * operator.

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

Performs the * operation.

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

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 _eq(self, other: Self) -> Bool<'ctx>

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

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

Returns true if both expressions are structurally identical.

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

Converts the integer into a Dynamic expression.

impl<'ctx> Sub for Int<'ctx>

type Output = Int<'ctx>

The resulting type after applying the - operator.

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

Performs the - operation.