Struct Int 

pub struct Int {
    pub id: TermId,
}

An integer-sorted term, analogous to z3::Int<'ctx>.

Fields

id: TermId

The underlying term identifier.

Implementations

impl Int

pub fn from_id(id: TermId) -> Self

Wrap a raw TermId as an Int.

pub fn new_const(ctx: &Z3Context, name: &str) -> Self

Declare a fresh integer constant named name.

pub fn from_i64(ctx: &Z3Context, value: i64) -> Self

Create an integer literal from an i64.

pub fn add(ctx: &Z3Context, args: &[Int]) -> Self

Arithmetic addition of a slice of integer terms.

pub fn sub(ctx: &Z3Context, lhs: &Int, rhs: &Int) -> Self

Arithmetic subtraction: lhs - rhs.

pub fn mul(ctx: &Z3Context, args: &[Int]) -> Self

Arithmetic multiplication of a slice of integer terms.

pub fn neg(ctx: &Z3Context, arg: &Int) -> Self

Arithmetic negation: -arg.

pub fn div(ctx: &Z3Context, lhs: &Int, rhs: &Int) -> Self

Integer division: lhs div rhs.

pub fn modulo(ctx: &Z3Context, lhs: &Int, rhs: &Int) -> Self

Integer modulo: lhs mod rhs.

pub fn lt(ctx: &Z3Context, lhs: &Int, rhs: &Int) -> Bool

Strict less-than comparison: lhs < rhs.

pub fn le(ctx: &Z3Context, lhs: &Int, rhs: &Int) -> Bool

Less-than-or-equal comparison: lhs <= rhs.

pub fn gt(ctx: &Z3Context, lhs: &Int, rhs: &Int) -> Bool

Strict greater-than comparison: lhs > rhs.

pub fn ge(ctx: &Z3Context, lhs: &Int, rhs: &Int) -> Bool

Greater-than-or-equal comparison: lhs >= rhs.

pub fn eq(ctx: &Z3Context, lhs: &Int, rhs: &Int) -> Bool

Equality: lhs = rhs.

Trait Implementations

impl Clone for Int

fn clone(&self) -> Int

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Int

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

Formats the value using the given formatter.

impl From<Int> for TermId

fn from(x: Int) -> Self

Converts to this type from the input type.