Numerical operators

+

(+ x y)

(+ x y)

• takes x: a
• takes y: a
• produces a
• where a is of type integer or decimal

Addition of integers and decimals.

Supported in either invariants or properties.

-

(- x y)

(- x y)

• takes x: a
• takes y: a
• produces a
• where a is of type integer or decimal

Subtraction of integers and decimals.

Supported in either invariants or properties.

*

(* x y)

(* x y)

• takes x: a
• takes y: a
• produces a
• where a is of type integer or decimal

Multiplication of integers and decimals.

Supported in either invariants or properties.

/

(/ x y)

(/ x y)

• takes x: a
• takes y: a
• produces a
• where a is of type integer or decimal

Division of integers and decimals.

Supported in either invariants or properties.

^

(^ x y)

(^ x y)

• takes x: a
• takes y: a
• produces a
• where a is of type integer or decimal

Exponentiation of integers and decimals.

Supported in either invariants or properties.

log

(log b x)

(log b x)

• takes b: a
• takes x: a
• produces a
• where a is of type integer or decimal

Logarithm of x base b.

Supported in either invariants or properties.

-

(- x)

(- x)

• takes x: a
• produces a
• where a is of type integer or decimal

Negation of integers and decimals.

Supported in either invariants or properties.

sqrt

(sqrt x)

(sqrt x)

• takes x: a
• produces a
• where a is of type integer or decimal

Square root of integers and decimals.

Supported in either invariants or properties.

ln

(ln x)

(ln x)

• takes x: a
• produces a
• where a is of type integer or decimal

Logarithm of integers and decimals base e.

Supported in either invariants or properties.

exp

(exp x)

(exp x)

• takes x: a
• produces a
• where a is of type integer or decimal

Exponential of integers and decimals. e raised to the integer or decimal x.

Supported in either invariants or properties.

abs

(abs x)

(abs x)

• takes x: a
• produces a
• where a is of type integer or decimal

Absolute value of integers and decimals.

Supported in either invariants or properties.

round

(round x)

(round x)

• takes x: decimal
• produces integer

(round x prec)

(round x prec)

• takes x: decimal
• takes prec: integer
• produces integer

Banker's rounding value of decimal x as integer, or to prec precision as decimal.

Supported in either invariants or properties.

ceiling

(ceiling x)

(ceiling x)

• takes x: decimal
• produces integer

(ceiling x prec)

(ceiling x prec)

• takes x: decimal
• takes prec: integer
• produces integer

Rounds the decimal x up to the next integer, or to prec precision as decimal.

Supported in either invariants or properties.

floor

(floor x)

(floor x)

• takes x: decimal
• produces integer

(floor x prec)

(floor x prec)

• takes x: decimal
• takes prec: integer
• produces integer

Rounds the decimal x down to the previous integer, or to prec precision as decimal.

Supported in either invariants or properties.

dec

(dec x)

(dec x)

• takes x: integer
• produces decimal

Casts the integer x to its decimal equivalent.

Supported in either invariants or properties.

mod

(mod x y)

(mod x y)

• takes x: integer
• takes y: integer
• produces integer

Integer modulus

Supported in either invariants or properties.

Bitwise