diff options
| -rw-r--r-- | Source/Basetypes/BigFloat.cs | 250 | ||||
| -rw-r--r-- | Source/Core/Parser.cs | 90 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibLineariser.cs | 4 | ||||
| -rw-r--r-- | fp_documentation.txt | 19 |
4 files changed, 192 insertions, 171 deletions
diff --git a/Source/Basetypes/BigFloat.cs b/Source/Basetypes/BigFloat.cs index 5b169263..8cde2cb9 100644 --- a/Source/Basetypes/BigFloat.cs +++ b/Source/Basetypes/BigFloat.cs @@ -17,7 +17,7 @@ namespace Microsoft.Basetypes /// <summary>
/// A representation of a 32-bit floating point value
- /// Note that this value has a 1-bit sign, 8-bit exponent, and 24-bit mantissa
+ /// Note that this value has a 1-bit sign, 8-bit exponent, and 24-bit significand
/// </summary>
public struct BigFloat
{
@@ -25,33 +25,33 @@ namespace Microsoft.Basetypes // the internal representation
[Rep]
- internal readonly long mantissa; //Note that the mantissa arrangement matches standard fp arrangement (most significant bit is farthest left)
+ internal readonly BigNum significand; //Note that the significand arrangement matches standard fp arrangement (most significant bit is farthest left)
[Rep]
- internal readonly int mantissaSize;
+ internal readonly int significandSize;
[Rep]
- internal readonly int exponent; //The value of the exponent is always positive as per fp representation requirements
+ internal readonly BigNum exponent; //The value of the exponent is always positive as per fp representation requirements
[Rep]
internal readonly int exponentSize; //The bit size of the exponent
[Rep]
- internal readonly String dec_value;
+ internal readonly String value; //Only used with second syntax
[Rep]
- internal readonly bool isDec;
+ internal readonly bool isNeg;
- public long Mantissa {
+ public BigNum Significand {
get {
- return mantissa;
+ return significand;
}
}
- public int Exponent {
+ public BigNum Exponent {
get {
return exponent;
}
}
- public int MantissaSize {
+ public int SignificandSize {
get {
- return mantissaSize;
+ return significandSize;
}
}
@@ -61,25 +61,26 @@ namespace Microsoft.Basetypes }
}
- public String Decimal {
+ public bool IsNegative {
get {
- return dec_value;
+ return this.isNeg;
}
}
- public bool IsDec {
+ public String Value {
get {
- return isDec;
+ return value;
}
}
- public static BigFloat ZERO(int mantissaSize, int exponentSize) { return new BigFloat(0, 0, mantissaSize, exponentSize); } //Does not include negative zero
+ public static BigFloat ZERO(int exponentSize, int significandSize) { return new BigFloat(false, BigNum.ZERO, BigNum.ZERO, exponentSize, significandSize); } //Does not include negative zero
- private static readonly BIM two = new BIM(2);
- private static long two_n(int n) {
- long toReturn = 1;
+ private static readonly BigNum two = new BigNum(2);
+ private static readonly BigNum one = new BigNum(1);
+ private static BigNum two_n(int n) {
+ BigNum toReturn = one;
for (int i = 0; i < n; i++)
- toReturn = toReturn * 2;
+ toReturn = toReturn * two;
return toReturn;
}
@@ -95,18 +96,18 @@ namespace Microsoft.Basetypes return new BigFloat(v.ToString(), 8, 24);
}
- public static BigFloat FromInt(int v, int exponentSize, int mantissaSize)
+ public static BigFloat FromInt(int v, int exponentSize, int significandSize)
{
- return new BigFloat(v.ToString(), exponentSize, mantissaSize);
+ return new BigFloat(v.ToString(), exponentSize, significandSize);
}
public static BigFloat FromBigInt(BIM v) {
return new BigFloat(v.ToString(), 8, 24);
}
- public static BigFloat FromBigInt(BIM v, int exponentSize, int mantissaSize)
+ public static BigFloat FromBigInt(BIM v, int exponentSize, int significandSize)
{
- return new BigFloat(v.ToString(), exponentSize, mantissaSize);
+ return new BigFloat(v.ToString(), exponentSize, significandSize);
}
public static BigFloat FromBigDec(BigDec v)
@@ -114,84 +115,67 @@ namespace Microsoft.Basetypes return new BigFloat(v.ToDecimalString(), 8, 24);
}
- public static BigFloat FromBigDec(BigDec v, int exponentSize, int mantissaSize)
+ public static BigFloat FromBigDec(BigDec v, int exponentSize, int significandSize)
{
- return new BigFloat(v.ToDecimalString(), exponentSize, mantissaSize);
+ return new BigFloat(v.ToDecimalString(), exponentSize, significandSize);
}
[Pure]
- public static BigFloat FromString(string v) {
- String[] vals = v.Split(' ');
- if (vals.Length == 0 || vals.Length > 4)
- throw new FormatException();
- try
- {
- switch (vals.Length) {
- case 1:
- return new BigFloat(vals[0], 8, 24);
- case 2:
- return new BigFloat(Int32.Parse(vals[0]), Int64.Parse(vals[1]), 8, 24);
- case 3:
- return new BigFloat(vals[0], Int32.Parse(vals[1]), Int32.Parse(vals[2]));
- case 4:
- return new BigFloat(Int32.Parse(vals[0]), Int64.Parse(vals[1]), Int32.Parse(vals[2]), Int32.Parse(vals[3]));
- default:
- throw new FormatException(); //Unreachable
- }
- }
- catch (Exception) { //Catch parsing errors
- throw new FormatException();
- }
+ public static BigFloat FromString(String v, int exp, int sig) { //String must be
+ return new BigFloat(v, exp, sig);
}
- internal BigFloat(int exponent, long mantissa, int exponentSize, int mantissaSize) {
+ public BigFloat(bool sign, BigNum exponent, BigNum significand, int exponentSize, int significandSize) {
this.exponentSize = exponentSize;
this.exponent = exponent;
- this.mantissa = mantissa;
- this.mantissaSize = mantissaSize;
- this.isDec = false;
- this.dec_value = "";
+ this.significand = significand;
+ this.significandSize = significandSize;
+ this.isNeg = sign;
+ this.value = "";
}
- internal BigFloat(String dec_value, int exponentSize, int mantissaSize) {
+ public BigFloat(String value, int exponentSize, int significandSize) {
this.exponentSize = exponentSize;
- this.mantissaSize = mantissaSize;
- this.exponent = 0;
- this.mantissa = 0;
- this.isDec = true;
- this.dec_value = dec_value;
+ this.significandSize = significandSize;
+ this.exponent = BigNum.ZERO;
+ this.significand = BigNum.ZERO;
+ this.value = value;
+ this.isNeg = value[0] == '-';
//Special cases:
- if (this.dec_value.Equals("+oo") || this.dec_value.Equals("-oo") || this.dec_value.Equals("-zero"))
+ if (this.value.Equals("+oo") || this.value.Equals("-oo") || this.value.Equals("-zero"))
return;
- if (this.dec_value.ToLower().Equals("nan")) {
- this.dec_value = "NaN";
+ if (this.value.ToLower().Equals("nan")) {
+ this.value = "NaN";
return;
}
- if (this.dec_value.Equals("INF") || this.dec_value.Equals("+INF")) {
- this.dec_value = "+oo";
+ if (this.value.Equals("INF") || this.value.Equals("+INF"))
+ {
+ this.value = "+oo";
return;
}
- if (this.dec_value.Equals("-INF")) {
- this.dec_value = "-oo";
+ if (this.value.Equals("-INF"))
+ {
+ this.value = "-oo";
return;
}
- if (this.dec_value.Equals("+zero")) {
- this.dec_value = "0.0";
+ if (this.value.Equals("+zero"))
+ {
+ this.value = "0.0";
return;
}
//End special cases
- if (this.dec_value.IndexOf('.') == -1 && this.dec_value.IndexOf('e') == -1)
- this.dec_value += ".0"; //Assures that the decimal value is a "real" number
- if (this.dec_value.IndexOf('.') == 0)
- this.dec_value = "0" + this.dec_value; //Assures that decimals always have a 0 in front
+ if (this.value.IndexOf('.') == -1 && this.value.IndexOf('e') == -1)
+ this.value += ".0"; //Assures that the decimal value is a "real" number
+ if (this.value.IndexOf('.') == 0)
+ this.value = "0" + this.value; //Assures that decimals always have a 0 in front
}
- private BIM maxMantissa()
+ private BigNum maxsignificand()
{
- BIM result = new BIM(1);
- for (int i = 0; i < mantissaSize; i++)
+ BigNum result = one;
+ for (int i = 0; i < significandSize; i++)
result = result * two;
- return result - 1;
+ return result - one;
}
private int maxExponent() { return (int)Math.Pow(2, exponentSize) - 1; }
@@ -213,13 +197,13 @@ namespace Microsoft.Basetypes [Pure]
public override int GetHashCode() {
- return Mantissa.GetHashCode() * 13 + Exponent.GetHashCode();
+ return significand.GetHashCode() * 13 + Exponent.GetHashCode();
}
[Pure]
public override string/*!*/ ToString() {
Contract.Ensures(Contract.Result<string>() != null);
- return isDec ? dec_value : String.Format("{0}x2^{1}", Mantissa.ToString(), Exponent.ToString());
+ return value=="" ? String.Format("{0}x2^{1}", significand.ToString(), Exponent.ToString()) : value;
}
@@ -229,41 +213,41 @@ namespace Microsoft.Basetypes /// <summary>
/// NOTE: THIS METHOD MAY NOT WORK AS EXPECTED!!!
/// Converts the given decimal value (provided as a string) to the nearest floating point approximation
- /// the returned fp assumes the given mantissa and exponent size
+ /// the returned fp assumes the given significand and exponent size
/// </summary>
/// <param name="value"></param>
- /// <param name="mantissaSize"></param>
+ /// <param name="significandSize"></param>
/// <param name="exponentSize"></param>
/// <returns></returns>
- public static BigFloat Round(String value, int exponentSize, int mantissaSize)
+ public static BigFloat Round(String value, int exponentSize, int significandSize)
{
int i = value.IndexOf('.');
if (i == -1)
- return Round(BIM.Parse(value), 0, exponentSize, mantissaSize);
- return Round(i == 0 ? 0 : BIM.Parse(value.Substring(0, i)), BIM.Parse(value.Substring(i + 1, value.Length - i - 1)), exponentSize, mantissaSize);
+ return Round(BigNum.FromString(value), BigNum.ZERO, exponentSize, significandSize);
+ return Round(i == 0 ? BigNum.ZERO : BigNum.FromString(value.Substring(0, i)), BigNum.FromString(value.Substring(i + 1, value.Length - i - 1)), exponentSize, significandSize);
}
/// <summary>
/// NOTE: THIS METHOD MAY NOT WORK AS EXPECTED!!!!
- /// Converts value.dec_value to a the closest float approximation with the given mantissaSize, exponentSize
+ /// Converts value.dec_value to a the closest float approximation with the given significandSize, exponentSize
/// Returns the result of this calculation
/// </summary>
/// <param name="value"></param>
/// <param name="power"></param>
- /// <param name="mantissaSize"></param>
+ /// <param name="significandSize"></param>
/// <param name="exponentSize"></param>
/// <returns></returns>
- public static BigFloat Round(BIM value, BIM dec_value, int exponentSize, int mantissaSize)
+ public static BigFloat Round(BigNum value, BigNum dec_value, int exponentSize, int significandSize)
{
int exp = 0;
- BIM one = new BIM(1);
- BIM ten = new BIM(10);
- BIM dec_max = new BIM(0); //represents the order of magnitude of dec_value for carrying during calculations
+ BigNum one = new BigNum(1);
+ BigNum ten = new BigNum(10);
+ BigNum dec_max = new BigNum(0); //represents the order of magnitude of dec_value for carrying during calculations
//First, determine the exponent
while (value > one) { //Divide by two, increment exponent by 1
if (!(value % two).IsZero) { //Add "1.0" to the decimal
- dec_max = new BIM(10);
+ dec_max = new BigNum(10);
while (dec_max < dec_value)
dec_max = dec_max * ten;
dec_value = dec_value + dec_max;
@@ -275,7 +259,7 @@ namespace Microsoft.Basetypes exp++;
}
if (value.IsZero && !dec_value.IsZero) {
- dec_max = new BIM(10);
+ dec_max = new BigNum(10);
while (dec_max < dec_value)
dec_max = dec_max * ten;
while (value.IsZero) {//Multiply by two, decrement exponent by 1
@@ -288,12 +272,12 @@ namespace Microsoft.Basetypes }
}
- //Second, calculate the mantissa
- value = new BIM(0); //remove implicit bit
- dec_max = new BIM(10);
+ //Second, calculate the significand
+ value = new BigNum(0); //remove implicit bit
+ dec_max = new BigNum(10);
while (dec_max < dec_value)
dec_max = dec_max * ten;
- for (int i = mantissaSize; i > 0 && !dec_value.IsZero; i--) { //Multiply by two until the mantissa is fully calculated
+ for (int i = significandSize; i > 0 && !dec_value.IsZero; i--) { //Multiply by two until the significand is fully calculated
dec_value = dec_value * two;
if (dec_value >= dec_max) {
dec_value = dec_value - dec_max;
@@ -301,7 +285,7 @@ namespace Microsoft.Basetypes }
}
- return new BigFloat(exp, Int64.Parse(value.ToString()), exponentSize, mantissaSize);
+ return new BigFloat(false, BigNum.ZERO, BigNum.FromString(value.ToString()), exponentSize, significandSize); //Sign not actually checked...
}
// ``floor`` rounds towards negative infinity (like SMT-LIBv2's to_int).
@@ -312,30 +296,32 @@ namespace Microsoft.Basetypes /// </summary>
/// <param name="floor">The Floor (rounded towards negative infinity)</param>
/// <param name="ceiling">Ceiling (rounded towards positive infinity)</param>
- public void FloorCeiling(out BIM floor, out BIM ceiling) {
+ public void FloorCeiling(out BigNum floor, out BigNum ceiling) {
//TODO: fix for fp functionality
- BIM n = Mantissa;
- int e = Exponent;
+ BigNum n = Significand;
+ BigNum e = Exponent;
if (n.IsZero) {
floor = ceiling = n;
- } else if (0 <= e) {
+ } else if (BigNum.ZERO <= e) {
// it's an integer
- for (; 0 < e; e--) {
+ for (; BigNum.ZERO < e; e = e - one)
+ {
n = n * two;
}
floor = ceiling = n;
} else {
// it's a non-zero integer, so the ceiling is one more than the floor
- for (; e < 0 && !n.IsZero; e++) {
+ for (; BigNum.ZERO < e && !n.IsZero; e = e + one)
+ {
n = n / two; // Division rounds towards negative infinity
}
if (!IsNegative) {
floor = n;
- ceiling = n + 1;
+ ceiling = n + one;
} else {
ceiling = n;
- floor = n - 1;
+ floor = n - one;
}
}
Debug.Assert(floor <= ceiling, "Invariant was not maintained");
@@ -352,7 +338,7 @@ namespace Microsoft.Basetypes [Pure]
public string ToDecimalString() {
Contract.Ensures(Contract.Result<string>() != null);
- return isDec ? dec_value : String.Format("{0}x2^{1}", Mantissa.ToString(), Exponent.ToString());
+ return value=="" ? String.Format("{0}x2^{1}", significand.ToString(), Exponent.ToString()) : value;
}
[Pure]
@@ -380,18 +366,16 @@ namespace Microsoft.Basetypes [Pure]
public BigFloat Abs {
get {
- if (IsDec)
- return dec_value[0] == '-' ? new BigFloat(dec_value.Remove(0, 1), ExponentSize, MantissaSize) : this;
- return new BigFloat(Exponent, Math.Abs(Mantissa), ExponentSize, MantissaSize);
+ return new BigFloat(true, Exponent, Significand, ExponentSize, SignificandSize);
}
}
[Pure]
public BigFloat Negate {
get {
- if (IsDec)
- return dec_value[0] == '-' ? new BigFloat(dec_value.Remove(0, 1), ExponentSize, MantissaSize) : new BigFloat("-" + dec_value, ExponentSize, MantissaSize);
- return new BigFloat(Exponent, -Mantissa, ExponentSize, MantissaSize);
+ if (value != "")
+ return value[0] == '-' ? new BigFloat(value.Remove(0, 1), ExponentSize, significandSize) : new BigFloat("-" + value, ExponentSize, significandSize);
+ return new BigFloat(!isNeg, Exponent, Significand, ExponentSize, SignificandSize);
}
}
@@ -404,26 +388,26 @@ namespace Microsoft.Basetypes public static BigFloat operator +(BigFloat x, BigFloat y) {
//TODO: Modify for correct fp functionality
Contract.Requires(x.ExponentSize == y.ExponentSize);
- Contract.Requires(x.MantissaSize == y.MantissaSize);
- long m1 = x.Mantissa;
- int e1 = x.Exponent;
- long m2 = y.Mantissa;
- int e2 = y.Exponent;
- m1 = m1 + two_n(x.mantissaSize + 1); //Add implicit bit
- m2 = m2 + two_n(y.mantissaSize + 1);
+ Contract.Requires(x.significandSize == y.significandSize);
+ BigNum m1 = x.significand;
+ BigNum e1 = x.Exponent;
+ BigNum m2 = y.significand;
+ BigNum e2 = y.Exponent;
+ m1 = m1 + two_n(x.significandSize + 1); //Add implicit bit
+ m2 = m2 + two_n(y.significandSize + 1);
if (e2 > e1) {
- m1 = y.Mantissa;
+ m1 = y.significand;
e1 = y.Exponent;
- m2 = x.Mantissa;
+ m2 = x.significand;
e2 = x.Exponent;
}
while (e2 < e1) {
- m2 = m2 / 2;
- e2++;
+ m2 = m2 / two;
+ e2 = e2 + one;
}
- return new BigFloat(e1, m1 + m2, x.MantissaSize, x.ExponentSize);
+ return new BigFloat(false, e1, m1 + m2, x.significandSize, x.ExponentSize);
}
[Pure]
@@ -434,8 +418,8 @@ namespace Microsoft.Basetypes [Pure]
public static BigFloat operator *(BigFloat x, BigFloat y) {
Contract.Requires(x.ExponentSize == y.ExponentSize);
- Contract.Requires(x.MantissaSize == y.MantissaSize);
- return new BigFloat(x.Exponent + y.Exponent, x.Mantissa * y.Mantissa, x.MantissaSize, x.ExponentSize);
+ Contract.Requires(x.significandSize == y.significandSize);
+ return new BigFloat(x.isNeg ^ y.isNeg, x.Exponent + y.Exponent, x.significand * y.significand, x.significandSize, x.ExponentSize);
}
@@ -444,9 +428,9 @@ namespace Microsoft.Basetypes public bool IsSpecialType {
get {
- if (!IsDec)
+ if (value == "")
return false;
- return (dec_value.Equals("NaN") || dec_value.Equals("+oo") || dec_value.Equals("-oo") || dec_value.Equals("-zero"));
+ return (value.Equals("NaN") || value.Equals("+oo") || value.Equals("-oo") || value.Equals("-zero"));
}
}
@@ -456,15 +440,9 @@ namespace Microsoft.Basetypes }
}
- public bool IsNegative {
- get {
- return (isDec && dec_value[0] == '-') || mantissa < 0;
- }
- }
-
public bool IsZero {
get {
- return Mantissa == 0 && Exponent == 0;
+ return significand.Equals(BigNum.ZERO) && Exponent == BigNum.ZERO;
}
}
@@ -474,9 +452,9 @@ namespace Microsoft.Basetypes return 1;
if (this.exponent < that.exponent)
return -1;
- if (this.Mantissa == that.Mantissa)
+ if (this.significand == that.significand)
return 0;
- return this.Mantissa > that.Mantissa ? 1 : -1;
+ return this.significand > that.significand ? 1 : -1;
}
[Pure]
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 5fcb1cdc..bf35ccbe 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -668,17 +668,35 @@ private class BvBounds : Expr { ty = new BasicType(t, SimpleType.Real);
} else if (la.kind == 98) {
Get();
- if (la.kind == 9) {
- Get();
- Expect(3);
- int exp = Int32.Parse(t.val);
- Expect(3);
- int man = Int32.Parse(t.val);
- ty = new FloatType(t, exp, man);
- Expect(10);
+ if (la.kind == 3) {
+ Expect(3);
+ switch (Int32.Parse(t.val)) {
+ case 16:
+ ty = new FloatType(t, 5, 11);
+ break;
+ case 32:
+ ty = new FloatType(t, 8, 24);
+ break;
+ case 64:
+ ty = new FloatType(t, 11, 53);
+ break;
+ case 128:
+ ty = new FloatType(t, 15, 113);
+ break;
+ default:
+ SynErr(3);
+ break;
+ }
+ }
+ else {
+ Expect(19);
+ Expect(3);
+ int exp = Int32.Parse(t.val);
+ Expect(3);
+ int man = Int32.Parse(t.val);
+ ty = new FloatType(t, exp, man);
+ Expect(20);
}
- else
- ty = new FloatType(t, 8, 24);
} else if (la.kind == 16) {
Get();
ty = new BasicType(t, SimpleType.Bool);
@@ -1813,9 +1831,9 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { case 98: {
Get();
x = t;
- Expect(9);
+ Expect(19);
Expression(out e);
- Expect(10);
+ Expect(20);
e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToFloat), new List<Expr> { e });
break;
}
@@ -1887,29 +1905,45 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { /// <param name="n"></param>
void Float(out BigFloat n)
{
- //To be modified
- string s = "";
try
{
- if (la.kind == 97)
- {
- //Expected format = fp (a b) || fp (a b c d)
+ if (la.kind == 97) {
+ bool negative = false;
+ int exp, sig;
+ BigNum exp_val, sig_val, value;
+ //Expected format = fp(sign exp_val sig_val) || fp<exp sig>(value)
Get(); //Skip the fp token
Get();
- if (t.val != "(") { throw new FormatException(); }
- while (la.kind == 1 || la.kind == 3 || la.kind == 6 || la.kind == 4 || la.kind == 74 || la.kind == 75) { //Get values between the parens
+ if (t.val == "(") {
Get();
- if (t.val == "-" || t.val == "+") //special sign case (la.kind == 74 or 75)
- s += t.val;
- else
- s += t.val + " ";
+ negative = Boolean.Parse(t.val);
+ BvLit(out exp_val, out exp);
+ BvLit(out sig_val, out sig);
+ n = new BigFloat(negative, exp_val, sig_val, exp, sig);
+ }
+ else if (t.val == "<") {
+ Expect(14);
+ exp = Int32.Parse(t.val);
+ Expect(14);
+ sig = Int32.Parse(t.val);
+ int size;
+ BvLit(out value, out size);
+ if (size != exp + sig)
+ {
+ this.SemErr("The given bitvector size of " + size + "does not match the provided floating-point size of " + (exp + sig));
+ n = BigFloat.ZERO(8, 24);
+ return;
+ }
+ n = new BigFloat(t.val, exp, sig);
+ }
+ else {
+ throw new FormatException();
}
- Get();
- if (t.val != ")") { throw new FormatException(); }
}
- else SynErr(137);
-
- n = BigFloat.FromString(s.Trim());
+ else {
+ n = BigFloat.ZERO(8, 24);
+ SynErr(137);
+ }
}
catch (FormatException)
{
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index 7c3ae960..59b6b7e7 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -205,10 +205,10 @@ namespace Microsoft.Boogie.SMTLib {
BigFloat lit = ((VCExprFloatLit)node).Val;
if (lit.IsSpecialType) {
- wr.Write("(_ " + lit.Decimal + " " + lit.ExponentSize.ToString() + " " + lit.MantissaSize.ToString() + ")");
+ wr.Write("(_ " + lit.Decimal + " " + lit.ExponentSize.ToString() + " " + lit.SignificandSize.ToString() + ")");
return true;
}
- wr.Write("((_ to_fp " + lit.ExponentSize.ToString() + " " + lit.MantissaSize.ToString() + ") RNE ");
+ wr.Write("((_ to_fp " + lit.ExponentSize.ToString() + " " + lit.SignificandSize.ToString() + ") RNE ");
if (lit.IsNegative)
// In SMT2 "-42" is an identifier (SMT2, Sect. 3.2 "Symbols")
wr.Write("(- 0.0 {0})", lit.Abs.ToDecimalString());
diff --git a/fp_documentation.txt b/fp_documentation.txt index 09e60b9a..d3fafdcb 100644 --- a/fp_documentation.txt +++ b/fp_documentation.txt @@ -10,7 +10,9 @@ 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
@@ -23,10 +25,11 @@ 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:
-float(dec)
-float(exp_val man_val)
-float(dec exp man)
-float(exp_val man_val exp man)
+**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,
@@ -68,6 +71,8 @@ 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
@@ -76,4 +81,8 @@ var x : real; fp(x);
Statements of the following form cause a parser error (parenthesis followed by fp constant)
-... (fp(1) + fp(1));
\ No newline at end of file +... (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 |