Fractions

You can do computations on fractions in Z3

FRACTION("1 1/2").add(FRACTION("1 1/2"));
FRACTION("1 1/3").subtract(FRACTION("1 1/2"));
FRACTION("1 1/3").multiply(FRACTION("2 5/3"));
FRACTION("1 1/3").divide(FRACTION("2 5/3"));

z^3 uses the following notation for fractions. 2%%3 for 2/3 (1.2%%3) for 1 2/3 etc.

5%%5<+>4%%5

gives 1.8

To convert the results to fractions, use %% operator at the end of the expression.

(5%%5<+>4%%5)%%

gives

1 4/5

Note fraction additions etc. uses the Unit Conversion operators such as <+>, <->, etc. Hence it is also possibly to convert to meters etc.

(4%%5)<+>((1%%5)<>m)

gives 1m.

((4%%5)<+>((1.3%%5)<>m))%%

gives

2 2/5m

((4%%5)<>m)<+>((1.3%%5)<>m)

2.4000000000000004m

(4%%5)<+>((1.3%%5)<>m)

2.4000000000000004m

((34%%5)<>m)<+>((1.3%%5)<>m)

8.4m

((3.4%%5)<>m)<+>((1.3%%5)<>m)

5.4m

(((3.4%%5)<>m)<+>((1.3%%5)<>m))%%

5 1250000000000001/3125000000000000

etc.