Skip to main content
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

Addition 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

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.