# integer¶

Emulates integers.

A collection of utility functions for using Integers in Alloy. Note that integer overflows are silently truncated to the current bitwidth using the 2’s complement arithmetic, unless the ‘’forbid overflows’’ option is turned on, in which case only models that do not have any overflows are analyzed.

Warning

The main challenge with this module is the distinction between `Int` and `int`. `Int` is the set of integers that have been instantiated, whereas `int` returns the value of an `Int`. You have to explicitly write `int i` to be able to add, subtract, and compare `Ints`.

```open util/integer

fact ThreeExists { // there is some integer whose value is 3
some x: Int | int x = 3
}

fun add[a, b: Int]: Int {
{i: Int | int i = int a + int b}
}

run add for 10 but 3 int expect 1
```

To try this module out, in Alloy Analyzer’s evaluator, you may also issue the following commands (suppose that allow generated a set with numbers ranging from `-8` to `7`):

```1 + 3
4

7 + 1
-8
```

## Functions¶

fun `integer.``add [n1, n2: Int]`
Return type

`one Int`

Returns `n1 + n2`.

fun `integer.``plus [n1, n2: Int]`
Return type

`one Int`

Returns `n1 + n2`.

fun `integer.``sub [n1, n2: Int]`
Return type

`one Int`

Returns `n1 - n2`.

fun `integer.``minus [n1, n2: Int]`
Return type

`one Int`

Returns `n1 - n2`.

fun `integer.``mul [n1, n2: Int]`
Return type

`one Int`

Returns `n1 * n2`.

fun `integer.``div [n1, n2: Int]`
Return type

`one Int`

Returns the division with ‘’round to zero’’ semantics, except the following 3 cases:

• if a is 0, then it returns 0

• else if b is 0, then it returns 1 if a is negative and -1 if a is positive

• else if a is the smallest negative integer, and b is -1, then it returns a

fun `integer.``rem [n1, n2: Int]`
Return type

`one Int`

Returns the unique integer that satisfies `a = ((a/b)*b) + remainder`.

fun `integer.``negate [n: Int]`
Return type

`one Int`

Returns the negation of n.

fun `integer.``signum [n: Int]`
Return type

`one Int`

Returns the signum of n (aka sign or sgn). In particular, `n < 0 => ( 0 - 1 ) else ( n > 0 => 1 else 0 )`.

fun `integer.``int2elem [i: Int, next: univ->univ, s: set univ]`
Return type

`lone s`

Returns the ith element (zero-based) from the `set s` in the ordering of `next`, which is a linear ordering relation like that provided by `ordering`.

fun `integer.``elem2int [e: univ, next: univ->univ]`
Return type

`lone Int`

Returns the index of the element (zero-based) in the ordering of next, which is a linear ordering relation like that provided by `ordering`.

fun `integer.``max`
Return type

`one Int`

Returns the largest integer in the current bitwidth.

fun `integer.``min`
Return type

`one Int`

Returns the smallest integer in the current bitwidth.

fun `integer.``next`
Return type

`Int -> Int`

Maps each integer (except max) to the integer after it.

fun `integer.``prev`
Return type

`Int -> Int`

Maps each integer (except min) to the integer before it.

fun `integer.``max [es: set Int]`
Return type

`lone Int`

Given a set of integers, return the largest element.

fun `integer.``min [es: set Int]`
Return type

`lone Int`

Given a set of integers, return the smallest element.

fun `integer.``prevs [e: Int]`
Return type

`set Int`

Given an integer, return all integers prior to it.

fun `integer.``nexts [e: Int]`
Return type

`set Int`

Given an integer, return all integers following it.

fun `integer.``larger [e1, e2: Int]`
Return type

`Int`

Returns the larger of the two integers.

fun `integer.``smaller [e1, e2: Int]`
Return type

`Int`

Returns the smaller of the two integers.

## Predicates¶

pred `integer.``eq [n1, n2: Int]`

`True` iff n1 is equal to n2.

pred `integer.``gt [n1, n2: Int]`

`True` iff n1 is greater than n2.

pred `integer.``gte [n1, n2: Int]`

`True` iff n1 is greater than or equal to n2.

pred `integer.``lt [n1, n2: Int]`

`True` iff n1 is less than n2.

pred `integer.``lte [n1, n2: Int]`

`True` iff n1 is less than or equal to n2.

pred `integer.``zero [n: Int]`

`True` iff n is equal to `0`.

pred `integer.``pos [n: Int]`

`True` iff n is positive.

pred `integer.``neg [n: Int]`

`True` iff n is negative.

pred `integer.``nonpos [n: Int]`

`True` iff n is non-positive.

pred `integer.``nonneg [n: Int]`

`True` iff n is non-negative.