Floating Point Documentation for Boogie
Written by Dietrich Geisler
Contact: dgeisler50@gmail.com

This document aims to describe the syntax for declaring and using floating points in Boogie

--------------------------------------------------------------------------------
Declaring Variables:

The syntax for declaring a floating point variable is as follows:
var name: float(exp man);
Where exp is the size of the float exponent and man is the size of the float mantissa
Please note that 

**REMOVE THIS SYNTAX**
It is also acceptable to use the following syntax:
var name: float();
This syntax assumes the float exponent to be size 8 and the mantissa to be size 24

example:
var x: float(11 53)
Declares a variable called x with a exponent sized 11 and mantissa sized 53

--------------------------------------------------------------------------------
Declaring Constants:

All of the following syntax are viable for declaring a floating point constant:
**REMOVE THE FIRST OF THESE TWO SYNTAXES**
fp(dec)
fp(exp_val man_val)
fp(dec exp man)
fp(exp_val man_val exp man)

Where dec is the decimal value of the constant,
exp_val/man_value are the integer values of their respective fields,
And exp/man are the sizes of their respective fields.
Note that when exp and man are not specified, they are given sizes 8 and 24 respectively

--------------------------------------------------------------------------------
Defined Operations:

Given two floating point values x and y with the same size of exponent and mantissa
The following operations operate as defined in Operators section of this document:
http://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml
(Note that rounding mode is always assumed to be Round to Nearest Even (RNE))
(Also note that operations not listed here are undefined)

operatation		boogie syntax
neg(x)			-x
add(x, y)		x + y
sub(x, y)		x - y
mul(x, y)		x * y
div(x, y)		x / y
leq(x, y)		x <= y
lt(x, y)		x < y
geq(x, y)		x >= y
gt(x, y)		x > y
eq(x, y)		x == y

--------------------------------------------------------------------------------
Other:

The following special values can be declared with the following syntax:
Value		Declaration
NaN			fp(nan exp man)
+oo			fp(oo exp man) OR fp(INF exp man)
-oo			fp(-oo exp man) OR fp(INF exp man)
-zero		fp(-zero exp man)
Where exp and man are the sizes of the exponent and mantissa respectively

--------------------------------------------------------------------------------
Known Issues:

float16, float32, float64, and float128 still need to be added

There is currently no way to convert from a floating point to any other data type

There is currently no way to convert the value of a variable to a floating point type
For example, the following statements fails:
var x : real;
fp(x);

Statements of the following form cause a parser error (parenthesis followed by fp constant)
... (fp(1) + fp(1));

Attempts by Boogie to infer the behavior of loops fail when floating points are involved

Describing loop behavior manually is untested (using loop unroll appears to work)