Struct NativeIntU64

pub struct NativeIntU64(/* private fields */);

Native Mathematical Integer (represented by u64 number)

The magic is that symbolically an SBF word is mapped to 256 bit symbolic integer.

Implementations

impl NativeIntU64

pub fn new<T>(v: T) -> Self

where T: Into<NativeIntU64>,

pub fn div_ceil(self, rhs: Self) -> Self

pub fn muldiv(self, num: Self, den: Self) -> Self

pub fn muldiv_ceil(self, num: Self, den: Self) -> Self

pub fn from_u128(w0: u64, w1: u64) -> Self

pub fn from_u256(w0: u64, w1: u64, w2: u64, w3: u64) -> Self

pub fn u64_max() -> Self

pub fn u128_max() -> Self

pub fn u256_max() -> Self

pub fn is_u8(&self) -> bool

pub fn is_u16(&self) -> bool

pub fn is_u32(&self) -> bool

pub fn is_u64(&self) -> bool

pub fn is_u128(&self) -> bool

pub fn is_u256(&self) -> bool

pub fn nondet() -> Self

pub fn checked_sub(&self, v: NativeIntU64) -> Self

pub fn as_internal(&self) -> u64

Trait Implementations

impl Add<u64> for NativeIntU64

type Output = NativeIntU64

The resulting type after applying the + operator.

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

Performs the + operation.

impl Add for NativeIntU64

type Output = NativeIntU64

The resulting type after applying the + operator.

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

Performs the + operation.

impl Clone for NativeIntU64

fn clone(&self) -> NativeIntU64

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for NativeIntU64

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

Formats the value using the given formatter.

impl Div<u64> for NativeIntU64

type Output = NativeIntU64

The resulting type after applying the / operator.

fn div(self, rhs: u64) -> Self::Output

Performs the / operation.

impl Div for NativeIntU64

type Output = NativeIntU64

The resulting type after applying the / operator.

fn div(self, rhs: NativeIntU64) -> Self::Output

Performs the / operation.

impl From<&[u64; 2]> for NativeIntU64

fn from(value: &[u64; 2]) -> Self

Converts to this type from the input type.

impl From<&[u64; 4]> for NativeIntU64

fn from(value: &[u64; 4]) -> Self

Converts to this type from the input type.

impl From<&[u8]> for NativeIntU64

fn from(value: &[u8]) -> Self

Converts to this type from the input type.

impl From<&[u8; 32]> for NativeIntU64

fn from(value: &[u8; 32]) -> Self

Converts to this type from the input type.

impl From<NativeIntU64> for u128

fn from(value: NativeIntU64) -> Self

Converts to this type from the input type.

impl From<NativeIntU64> for u64

fn from(value: NativeIntU64) -> Self

Converts to this type from the input type.

impl From<u128> for NativeIntU64

fn from(value: u128) -> Self

Converts to this type from the input type.

impl From<u16> for NativeIntU64

fn from(value: u16) -> Self

Converts to this type from the input type.

impl From<u32> for NativeIntU64

fn from(value: u32) -> Self

Converts to this type from the input type.

impl From<u64> for NativeIntU64

fn from(value: u64) -> Self

Converts to this type from the input type.

impl From<u8> for NativeIntU64

fn from(value: u8) -> Self

Converts to this type from the input type.

impl Mul<u64> for NativeIntU64

type Output = NativeIntU64

The resulting type after applying the * operator.

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

Performs the * operation.

impl Mul for NativeIntU64

type Output = NativeIntU64

The resulting type after applying the * operator.

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

Performs the * operation.

impl Nondet for NativeIntU64

fn nondet() -> NativeIntU64

fn nondet_with<F>(func: F) -> Self

where F: FnOnce(&Self) -> bool,

impl Ord for NativeIntU64

fn cmp(&self, other: &Self) -> Ordering

This method returns an Ordering between self and other.

fn max(self, other: Self) -> Self

Compares and returns the maximum of two values.

fn min(self, other: Self) -> Self

Compares and returns the minimum of two values.

fn clamp(self, min: Self, max: Self) -> Self

Restrict a value to a certain interval.

impl PartialEq for NativeIntU64

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

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl PartialOrd for NativeIntU64

fn partial_cmp(&self, other: &Self) -> Option<Ordering>

This method returns an ordering between self and other values if one exists.

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

Tests less than (for self and other) and is used by the < operator.

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

Tests less than or equal to (for self and other) and is used by the <= operator.

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

Tests greater than (for self and other) and is used by the > operator.

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

Tests greater than or equal to (for self and other) and is used by the >= operator.

impl Sub for NativeIntU64

type Output = NativeIntU64

The resulting type after applying the - operator.

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

Performs the - operation.

impl Copy for NativeIntU64

impl Eq for NativeIntU64