Z^3 Deeper Features

• << Z3 Home
• Z3 Language Documentation
• Listing of Z3 Array Manipulation Member Functions

Function Composition

Functions can be composed using the @ operator. A chain of functions can also be composed using the same technique. Composed function works left to right.

a=(x=>x/3)@(x=>x+2);
a(3)

gives 3.

First 3 is divided by 3, and then 2 is added to yield 3 as result.

a=(x=>x+2)@(x=>x/3);
a(3)

gives 1.6666666666666667

a=(SIN@COS@TAN);
a(45)

gives 0.7749904090605793

Computation with Large Numbers, Decimals of Arbitrary Length, Fractions, Complex Numbers, etc.

Often the accuracy provided by the usual computational language is insufficient to handle more complex computations as well as type specific computations.

The following notations are used to indicate advanced numerical types in Z.

Advanced Types

Type	Notation	Example
BigInt	n	(60n)!
Floating Point	dn	SQRT(2d300)
Complex Number	x+yi	3+4i
Fractions	x.n%%d	1.4%%3 gives 2 1/3

(60n)!

gives

8320987112741390144276341183223364380754172606361245952449277696409600000000000000

SIN(12+34i)

gives

-156534884864787.47+246178250600375.44ⅈ

SQRT(2d300)

gives

1.41421356237309504880168872420969807856967187537694807317667973799073247846210703885038753432764157273501384623091229702492483605585073721264412149709993583141322266592750559275579995050115278206057147010955997160597027453459686201472851741864088919860955232923048430871432145083976260362799525140799

Advanced Numeric Types use similar logic to Unit Conversions. Hence a variable can be given an advanced numeric type using <> notation.

For example, SQRT(23<>d70) will give 4.795831523312719541597438064162693919996707041904129346485309114448257