Last updated

# Numerical operators

## +

pact
(+ x y)
pact
(+ x y)
• takes x: a
• takes y: a
• produces a
• where a is of type integer or decimal

Supported in either invariants or properties.

## -

pact
(- x y)
pact
(- 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.

## *

pact
(* x y)
pact
(* 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.

## /

pact
(/ x y)
pact
(/ 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.

## ^

pact
(^ x y)
pact
(^ 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

pact
(log b x)
pact
(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.

## -

pact
(- x)
pact
(- 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

pact
(sqrt x)
pact
(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

pact
(ln x)
pact
(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

pact
(exp x)
pact
(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

pact
(abs x)
pact
(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

pact
(round x)
pact
(round x)
• takes x: decimal
• produces integer
pact
(round x prec)
pact
(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

pact
(ceiling x)
pact
(ceiling x)
• takes x: decimal
• produces integer
pact
(ceiling x prec)
pact
(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

pact
(floor x)
pact
(floor x)
• takes x: decimal
• produces integer
pact
(floor x prec)
pact
(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

pact
(dec x)
pact
(dec x)
• takes x: integer
• produces decimal

Casts the integer x to its decimal equivalent.

Supported in either invariants or properties.

## mod

pact
(mod x y)
pact
(mod x y)
• takes x: integer
• takes y: integer
• produces integer

Integer modulus

Supported in either invariants or properties.