removed an unnecessary text file

1 files changed, 0 insertions, 88 deletions

diff --git a/fp_documentation.txt b/fp_documentation.txt
deleted file mode 100644
index d3fafdcb..00000000
--- a/fp_documentation.txt
+++ /dev/null
@@ -1,88 +0,0 @@
-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)
\ No newline at end of file