From 80f3d4ed1bb221adbd3c7162acea10920b9fab73 Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Wed, 23 Sep 2015 04:08:00 -0600 Subject: Modified BigFloat to avoid evaluating the floating point value before sending it to z3 --- Source/Basetypes/BigFloat.cs | 1006 ++++++++++++++--------------- Source/Core/AbsyExpr.cs | 20 +- Source/Provers/SMTLib/SMTLibLineariser.cs | 12 - Source/VCExpr/VCExprASTPrinter.cs | 12 - float_test5.bpl | 5 +- float_test6.bpl | 4 +- 6 files changed, 505 insertions(+), 554 deletions(-) diff --git a/Source/Basetypes/BigFloat.cs b/Source/Basetypes/BigFloat.cs index 33860a4f..e9d5e670 100644 --- a/Source/Basetypes/BigFloat.cs +++ b/Source/Basetypes/BigFloat.cs @@ -1,516 +1,490 @@ -//----------------------------------------------------------------------------- -// -// Copyright (C) Microsoft Corporation. All Rights Reserved. -// -//----------------------------------------------------------------------------- - -using System; -using System.Collections.Generic; -using System.Linq; -using System.Text; -using System.Diagnostics.Contracts; -using System.Diagnostics; - -namespace Microsoft.Basetypes -{ - using BIM = System.Numerics.BigInteger; - - /// - /// 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 - /// - public struct BigFloat - { - //Please note that this code outline is copy-pasted from BigDec.cs - - // the internal representation - [Rep] - internal readonly BIM mantissa; //Note that the mantissa arrangement matches standard fp arrangement (most significant bit is farthest left) - [Rep] - internal readonly Boolean isNegative; //The left-most (sign) bit in the float representation - [Rep] - internal readonly int mantissaSize; - [Rep] - internal readonly int 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 - - public BIM Mantissa { - get { - return isNegative ? -mantissa : mantissa; - } - } - - public int Exponent { - get { - return exponent - (int)Math.Pow(2, exponentSize - 1); //account for shift - } - } - - public int MantissaSize - { - get - { - return mantissaSize; - } - } - - public int ExponentSize - { - get - { - return exponentSize; - } - } - - public static BigFloat ZERO(int mantissaSize, int exponentSize) { return new BigFloat(0, 0, mantissaSize, exponentSize); } //Does not include negative zero - public static BigFloat INF(int mantissaSize, int exponentSize) { return new BigFloat(0, 0, mantissaSize, exponentSize); } //Modify for IEEE standard - public static BigFloat NEGINF(int mantissaSize, int exponentSize) { return new BigFloat(0, 0, mantissaSize, exponentSize); } //Modify for IEEE standard - public static BigFloat NAN(int mantissaSize, int exponentSize) { return new BigFloat(0, 0, mantissaSize, exponentSize); } //Modify for IEEE standard - - private static readonly BIM two = new BIM(2); - private static BIM two_n(int n) { - BIM toReturn = new BIM(1); - for (int i = 0; i < n; i++) - toReturn = toReturn * two; - return toReturn; - } - - - //////////////////////////////////////////////////////////////////////////// - // Constructors - - //Please note that these constructors will be called throughout boogie - //For a complete summary of where this class has been added, simply view constructor references - - [Pure] - public static BigFloat FromInt(int v) { - return new BigFloat(v, 0, 24, 8); //TODO: modify for correct fp representation - } - - [Pure] - public static BigFloat FromBigInt(BIM v) { - return new BigFloat(0, v, 8, 24); //TODO: modify for correct fp representation - } - - public static BigFloat FromBigDec(BIM v) - { - return new BigFloat(0, v, 8, 24); //TODO: modify for correct fp representation - } - - [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 Round(vals[0], 8, 24); - case 2: - return new BigFloat(Int32.Parse(vals[0]), BIM.Parse(vals[1]), 8, 24); - case 3: - return Round(vals[0], Int32.Parse(vals[1]), Int32.Parse(vals[2])); - case 4: - return new BigFloat(Int32.Parse(vals[0]), BIM.Parse(vals[1]), Int32.Parse(vals[2]), Int32.Parse(vals[3])); - default: - throw new FormatException(); //Unreachable - } - } - catch (Exception) { //Catch parsing errors - throw new FormatException(); - } - } - - internal BigFloat(int exponent, BIM mantissa, int exponentSize, int mantissaSize) { - this.exponentSize = exponentSize; - this.exponent = exponent + (int)Math.Pow(2, exponentSize - 1); - this.mantissa = mantissa; - this.mantissaSize = mantissaSize; - if (exponent < 0) { //ZERO case since the exponent is less than the minimum - mantissa = 0; - exponent = 0; - this.isNegative = false; - return; - } - - this.isNegative = mantissa < 0; - if (this.isNegative) - mantissa = -mantissa; // ==> mantissa > 0 - - BIM max = maxMantissa(); - while (this.mantissa > max) { - this.mantissa = this.mantissa / two; - this.exponent++; - } - - //TODO: Add overflow check for exponent vs exponent size - //this.exponent = this.exponent % this.exponentSize; ?? - } - - private BIM maxMantissa() - { - BIM result = new BIM(1); - for (int i = 0; i < mantissaSize; i++) - result = result * two; - return result - 1; - } - private int maxExponent() { return (int)Math.Pow(2, exponentSize) - 1; } - - - - //////////////////////////////////////////////////////////////////////////// - // Basic object operations - - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] - public override bool Equals(object obj) { - if (obj == null) - return false; - if (!(obj is BigFloat)) - return false; - - return (this == (BigFloat)obj); - } - - [Pure] - public override int GetHashCode() { - return Mantissa.GetHashCode() * 13 + Exponent.GetHashCode(); - } - - [Pure] - public override string/*!*/ ToString() { - Contract.Ensures(Contract.Result() != null); - return String.Format("{0}x2^{1}", Mantissa.ToString(), Exponent.ToString()); - } - - - //////////////////////////////////////////////////////////////////////////// - // Conversion operations - - /// - /// 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 - /// - /// - /// - /// - /// - public static BigFloat Round(String value, int exponentSize, int mantissaSize) - { - 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); - } - - /// - /// Converts value.dec_value to a the closest float approximation with the given mantissaSize, exponentSize - /// Returns the result of this calculation - /// - /// - /// - /// - /// - /// - public static BigFloat Round(BIM value, BIM dec_value, int exponentSize, int mantissaSize) - { - 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 - - //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); - while (dec_max < dec_value) - dec_max = dec_max * ten; - dec_value = dec_value + dec_max; - } - value = value / two; - if (!(dec_value % ten).IsZero) - dec_value = dec_value * ten; //Creates excess zeroes to avoid losing data during division - dec_value = dec_value / two; - exp++; - } - if (value.IsZero && !dec_value.IsZero) { - dec_max = new BIM(10); - while (dec_max < dec_value) - dec_max = dec_max * ten; - while (value.IsZero) {//Multiply by two, decrement exponent by 1 - dec_value = dec_value * two; - if (dec_value >= dec_max) { - dec_value = dec_value - dec_max; - value = value + one; - } - exp--; - } - } - - //Second, calculate the mantissa - value = new BIM(0); //remove implicit bit - dec_max = new BIM(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 - dec_value = dec_value * two; - if (dec_value >= dec_max) { - dec_value = dec_value - dec_max; - value = value + two_n(i); //Note that i is decrementing so that the most significant bit is left-most in the representation - } - } - - return new BigFloat(exp, value, exponentSize, mantissaSize); - } - - // ``floor`` rounds towards negative infinity (like SMT-LIBv2's to_int). - /// - /// Computes the floor and ceiling of this BigFloat. Note the choice of rounding towards negative - /// infinity rather than zero for floor is because SMT-LIBv2's to_int function floors this way. - /// - /// The Floor (rounded towards negative infinity) - /// Ceiling (rounded towards positive infinity) - public void FloorCeiling(out BIM floor, out BIM ceiling) { - //TODO: fix for fp functionality - BIM n = Mantissa; - int e = Exponent; - if (n.IsZero) { - floor = ceiling = n; - } else if (0 <= e) { - // it's an integer - for (; 0 < e; e--) { - 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++) { - n = n / two; // Division rounds towards negative infinity - } - - if (!isNegative) { - floor = n; - ceiling = n + 1; - } else { - ceiling = n; - floor = n - 1; - } - } - Debug.Assert(floor <= ceiling, "Invariant was not maintained"); - } - - [Pure] - public String ToDecimalString(int maxDigits) { - //TODO: fix for fp functionality - string s = Mantissa.ToString(); - int digits = (isNegative) ? s.Length - 1 : s.Length; - BIM max = BIM.Pow(10, maxDigits); - BIM min = -max; - - if (Exponent >= 0) { - if (maxDigits < digits || maxDigits - digits < Exponent) { - return String.Format("{0}.0", (!isNegative) ? max.ToString() : min.ToString()); - } - else { - return String.Format("{0}{1}.0", s, new string('0', Exponent)); - } - } - else { - int exp = -Exponent; - - if (exp < digits) { - int intDigits = digits - exp; - if (maxDigits < intDigits) { - return String.Format("{0}.0", (!isNegative) ? max.ToString() : min.ToString()); - } - else { - int fracDigits = Math.Min(maxDigits, digits - intDigits); - return String.Format("{0}.{1}", s.Substring(0, intDigits), s.Substring(intDigits, fracDigits)); - } - } - else { - int fracDigits = Math.Min(maxDigits, digits); - return String.Format("0.{0}{1}", new string('0', exp - fracDigits), s.Substring(0, fracDigits)); - } - } - } - - [Pure] - public string ToDecimalString() { - //TODO: fix for fp functionality - string m = Mantissa.ToString(); - var e = Exponent; - if (0 <= Exponent) { - return m + Zeros(e) + ".0"; - } else { - e = -e; - // compute k to be the longest suffix of m consisting of all zeros (but no longer than e, and not the entire string) - var maxK = e < m.Length ? e : m.Length - 1; - var last = m.Length - 1; - var k = 0; - while (k < maxK && m[last - k] == '0') { - k++; - } - if (0 < k) { - // chop off the suffix of k zeros from m and adjust e accordingly - m = m.Substring(0, m.Length - k); - e -= k; - } - if (e == 0) { - return m; - } else if (e < m.Length) { - var n = m.Length - e; - return m.Substring(0, n) + "." + m.Substring(n); - } else { - return "0." + Zeros(e - m.Length) + m; - } - } - } - - [Pure] - public static string Zeros(int n) { - //TODO: fix for fp functionality - Contract.Requires(0 <= n); - if (n <= 10) { - var tenZeros = "0000000000"; - return tenZeros.Substring(0, n); - } else { - var d = n / 2; - var s = Zeros(d); - if (n % 2 == 0) { - return s + s; - } else { - return s + s + "0"; - } - } - } - - - //////////////////////////////////////////////////////////////////////////// - // Basic arithmetic operations - - [Pure] - public BigFloat Abs { - //TODO: fix for fp functionality - get { - return new BigFloat(Exponent, BIM.Abs(Mantissa), ExponentSize, MantissaSize); - } - } - - [Pure] - public BigFloat Negate { - //TODO: Modify for correct fp functionality - get { - return new BigFloat(Exponent, BIM.Negate(Mantissa), ExponentSize, MantissaSize); - } - } - - [Pure] - public static BigFloat operator -(BigFloat x) { - return x.Negate; - } - - [Pure] - 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); - BIM m1 = x.Mantissa; - int e1 = x.Exponent; - BIM m2 = y.Mantissa; - int e2 = y.Exponent; - m1 = m1 + two_n(x.mantissaSize + 1); //Add implicit bit - m2 = m2 + two_n(y.mantissaSize + 1); - if (e2 > e1) { - m1 = y.Mantissa; - e1 = y.Exponent; - m2 = x.Mantissa; - e2 = x.Exponent; - } - - while (e2 < e1) { - m2 = m2 / two; - e2++; - } - - return new BigFloat(e1, m1 + m2, x.MantissaSize, x.ExponentSize); - } - - [Pure] - public static BigFloat operator -(BigFloat x, BigFloat y) { - return x + y.Negate; - } - - [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); - } - - - //////////////////////////////////////////////////////////////////////////// - // Some basic comparison operations - - public bool IsPositive { - get { - return (!isNegative); - } - } - - public bool IsNegative { - get { - return (isNegative); - } - } - - public bool IsZero { - get { - return Mantissa.IsZero && Exponent == 0; - } - } - - [Pure] - public int CompareTo(BigFloat that) { - if (this.exponent > that.exponent) - return 1; - if (this.exponent < that.exponent) - return -1; - if (this.Mantissa == that.Mantissa) - return 0; - return this.Mantissa > that.Mantissa ? 1 : -1; - } - - [Pure] - public static bool operator ==(BigFloat x, BigFloat y) { - return x.CompareTo(y) == 0; - } - - [Pure] - public static bool operator !=(BigFloat x, BigFloat y) { - return x.CompareTo(y) != 0; - } - - [Pure] - public static bool operator <(BigFloat x, BigFloat y) { - return x.CompareTo(y) < 0; - } - - [Pure] - public static bool operator >(BigFloat x, BigFloat y) { - return x.CompareTo(y) > 0; - } - - [Pure] - public static bool operator <=(BigFloat x, BigFloat y) { - return x.CompareTo(y) <= 0; - } - - [Pure] - public static bool operator >=(BigFloat x, BigFloat y) { - return x.CompareTo(y) >= 0; - } - } -} +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- + +using System; +using System.Collections.Generic; +using System.Linq; +using System.Text; +using System.Diagnostics.Contracts; +using System.Diagnostics; + +namespace Microsoft.Basetypes +{ + using BIM = System.Numerics.BigInteger; + + /// + /// 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 + /// + public struct BigFloat + { + //Please note that this code outline is copy-pasted from BigDec.cs + + // the internal representation + [Rep] + internal readonly BIM mantissa; //Note that the mantissa arrangement matches standard fp arrangement (most significant bit is farthest left) + [Rep] + internal readonly int mantissaSize; + [Rep] + internal readonly int 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 BigDec dec_value; + [Rep] + internal readonly bool isDec; + + public BIM Mantissa { + get { + return mantissa; + } + } + + public int Exponent { + get { + return exponent; + } + } + + public int MantissaSize { + get { + return mantissaSize; + } + } + + public int ExponentSize { + get { + return exponentSize; + } + } + + public BigDec Decimal { + get { + return dec_value; + } + } + + public bool IsDec { + get { + return IsDec; + } + } + + public static BigFloat ZERO(int mantissaSize, int exponentSize) { return new BigFloat(0, 0, mantissaSize, exponentSize); } //Does not include negative zero + + private static readonly BIM two = new BIM(2); + private static BIM two_n(int n) { + BIM toReturn = new BIM(1); + for (int i = 0; i < n; i++) + toReturn = toReturn * two; + return toReturn; + } + + + //////////////////////////////////////////////////////////////////////////// + // Constructors + + //Please note that these constructors will be called throughout boogie + //For a complete summary of where this class has been added, simply view constructor references + + [Pure] + public static BigFloat FromInt(int v) { + return new BigFloat(v, 0, 24, 8); + } + + [Pure] + public static BigFloat FromBigInt(BIM v) { + return new BigFloat(0, v, 8, 24); + } + + public static BigFloat FromBigDec(BigDec v) + { + return new BigFloat(v, 8, 24); + } + + [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(BigDec.FromString(vals[0]), 8, 24); + case 2: + return new BigFloat(Int32.Parse(vals[0]), BIM.Parse(vals[1]), 8, 24); + case 3: + return new BigFloat(BigDec.FromString(vals[0]), Int32.Parse(vals[1]), Int32.Parse(vals[2])); + case 4: + return new BigFloat(Int32.Parse(vals[0]), BIM.Parse(vals[1]), Int32.Parse(vals[2]), Int32.Parse(vals[3])); + default: + throw new FormatException(); //Unreachable + } + } + catch (Exception) { //Catch parsing errors + throw new FormatException(); + } + } + + internal BigFloat(int exponent, BIM mantissa, int exponentSize, int mantissaSize) { + this.exponentSize = exponentSize; + this.exponent = exponent; + this.mantissa = mantissa; + this.mantissaSize = mantissaSize; + this.isDec = false; + this.dec_value = BigDec.ZERO; + } + + internal BigFloat(BigDec dec_value, int exponentSize, int mantissaSize) { + this.exponentSize = exponentSize; + this.mantissaSize = mantissaSize; + this.exponent = 0; + this.mantissa = 0; + this.isDec = true; + this.dec_value = dec_value; + } + + private BIM maxMantissa() + { + BIM result = new BIM(1); + for (int i = 0; i < mantissaSize; i++) + result = result * two; + return result - 1; + } + private int maxExponent() { return (int)Math.Pow(2, exponentSize) - 1; } + + + + //////////////////////////////////////////////////////////////////////////// + // Basic object operations + + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public override bool Equals(object obj) { + if (obj == null) + return false; + if (!(obj is BigFloat)) + return false; + + return (this == (BigFloat)obj); + } + + [Pure] + public override int GetHashCode() { + return Mantissa.GetHashCode() * 13 + Exponent.GetHashCode(); + } + + [Pure] + public override string/*!*/ ToString() { + Contract.Ensures(Contract.Result() != null); + return String.Format("{0}x2^{1}", Mantissa.ToString(), Exponent.ToString()); + } + + + //////////////////////////////////////////////////////////////////////////// + // Conversion operations + + /// + /// 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 + /// + /// + /// + /// + /// + public static BigFloat Round(String value, int exponentSize, int mantissaSize) + { + 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); + } + + /// + /// NOTE: THIS METHOD MAY NOT WORK AS EXPECTED!!!! + /// Converts value.dec_value to a the closest float approximation with the given mantissaSize, exponentSize + /// Returns the result of this calculation + /// + /// + /// + /// + /// + /// + public static BigFloat Round(BIM value, BIM dec_value, int exponentSize, int mantissaSize) + { + 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 + + //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); + while (dec_max < dec_value) + dec_max = dec_max * ten; + dec_value = dec_value + dec_max; + } + value = value / two; + if (!(dec_value % ten).IsZero) + dec_value = dec_value * ten; //Creates excess zeroes to avoid losing data during division + dec_value = dec_value / two; + exp++; + } + if (value.IsZero && !dec_value.IsZero) { + dec_max = new BIM(10); + while (dec_max < dec_value) + dec_max = dec_max * ten; + while (value.IsZero) {//Multiply by two, decrement exponent by 1 + dec_value = dec_value * two; + if (dec_value >= dec_max) { + dec_value = dec_value - dec_max; + value = value + one; + } + exp--; + } + } + + //Second, calculate the mantissa + value = new BIM(0); //remove implicit bit + dec_max = new BIM(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 + dec_value = dec_value * two; + if (dec_value >= dec_max) { + dec_value = dec_value - dec_max; + value = value + two_n(i); //Note that i is decrementing so that the most significant bit is left-most in the representation + } + } + + return new BigFloat(exp, value, exponentSize, mantissaSize); + } + + // ``floor`` rounds towards negative infinity (like SMT-LIBv2's to_int). + /// + /// NOTE: THIS PROBABLY WON'T GIVE USEFUL OUTPUT!!! + /// Computes the floor and ceiling of this BigFloat. Note the choice of rounding towards negative + /// infinity rather than zero for floor is because SMT-LIBv2's to_int function floors this way. + /// + /// The Floor (rounded towards negative infinity) + /// Ceiling (rounded towards positive infinity) + public void FloorCeiling(out BIM floor, out BIM ceiling) { + //TODO: fix for fp functionality + BIM n = Mantissa; + int e = Exponent; + if (n.IsZero) { + floor = ceiling = n; + } else if (0 <= e) { + // it's an integer + for (; 0 < e; e--) { + 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++) { + n = n / two; // Division rounds towards negative infinity + } + + if (!IsNegative) { + floor = n; + ceiling = n + 1; + } else { + ceiling = n; + floor = n - 1; + } + } + Debug.Assert(floor <= ceiling, "Invariant was not maintained"); + } + + [Pure] + public String ToDecimalString(int maxDigits) { + //TODO: fix for fp functionality + { + throw new NotImplementedException(); + } + } + + [Pure] + public string ToDecimalString() { + //TODO: fix for fp functionality + string m = Mantissa.ToString(); + var e = Exponent; + if (0 <= Exponent) { + return m + Zeros(e) + ".0"; + } else { + e = -e; + // compute k to be the longest suffix of m consisting of all zeros (but no longer than e, and not the entire string) + var maxK = e < m.Length ? e : m.Length - 1; + var last = m.Length - 1; + var k = 0; + while (k < maxK && m[last - k] == '0') { + k++; + } + if (0 < k) { + // chop off the suffix of k zeros from m and adjust e accordingly + m = m.Substring(0, m.Length - k); + e -= k; + } + if (e == 0) { + return m; + } else if (e < m.Length) { + var n = m.Length - e; + return m.Substring(0, n) + "." + m.Substring(n); + } else { + return "0." + Zeros(e - m.Length) + m; + } + } + } + + [Pure] + public static string Zeros(int n) { + //TODO: fix for fp functionality + Contract.Requires(0 <= n); + if (n <= 10) { + var tenZeros = "0000000000"; + return tenZeros.Substring(0, n); + } else { + var d = n / 2; + var s = Zeros(d); + if (n % 2 == 0) { + return s + s; + } else { + return s + s + "0"; + } + } + } + + + //////////////////////////////////////////////////////////////////////////// + // Basic arithmetic operations + + [Pure] + public BigFloat Abs { + //TODO: fix for fp functionality + get { + return new BigFloat(Exponent, BIM.Abs(Mantissa), ExponentSize, MantissaSize); + } + } + + [Pure] + public BigFloat Negate { + //TODO: Modify for correct fp functionality + get { + return new BigFloat(Exponent, BIM.Negate(Mantissa), ExponentSize, MantissaSize); + } + } + + [Pure] + public static BigFloat operator -(BigFloat x) { + return x.Negate; + } + + [Pure] + 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); + BIM m1 = x.Mantissa; + int e1 = x.Exponent; + BIM m2 = y.Mantissa; + int e2 = y.Exponent; + m1 = m1 + two_n(x.mantissaSize + 1); //Add implicit bit + m2 = m2 + two_n(y.mantissaSize + 1); + if (e2 > e1) { + m1 = y.Mantissa; + e1 = y.Exponent; + m2 = x.Mantissa; + e2 = x.Exponent; + } + + while (e2 < e1) { + m2 = m2 / two; + e2++; + } + + return new BigFloat(e1, m1 + m2, x.MantissaSize, x.ExponentSize); + } + + [Pure] + public static BigFloat operator -(BigFloat x, BigFloat y) { + return x + y.Negate; + } + + [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); + } + + + //////////////////////////////////////////////////////////////////////////// + // Some basic comparison operations + + public bool IsPositive { + get { + return !IsNegative; + } + } + + public bool IsNegative { + get { + return (isDec && dec_value >= BigDec.ZERO) || mantissa >= 0; + } + } + + public bool IsZero { + get { + return Mantissa.IsZero && Exponent == 0; + } + } + + [Pure] + public int CompareTo(BigFloat that) { + if (this.exponent > that.exponent) + return 1; + if (this.exponent < that.exponent) + return -1; + if (this.Mantissa == that.Mantissa) + return 0; + return this.Mantissa > that.Mantissa ? 1 : -1; + } + + [Pure] + public static bool operator ==(BigFloat x, BigFloat y) { + return x.CompareTo(y) == 0; + } + + [Pure] + public static bool operator !=(BigFloat x, BigFloat y) { + return x.CompareTo(y) != 0; + } + + [Pure] + public static bool operator <(BigFloat x, BigFloat y) { + return x.CompareTo(y) < 0; + } + + [Pure] + public static bool operator >(BigFloat x, BigFloat y) { + return x.CompareTo(y) > 0; + } + + [Pure] + public static bool operator <=(BigFloat x, BigFloat y) { + return x.CompareTo(y) <= 0; + } + + [Pure] + public static bool operator >=(BigFloat x, BigFloat y) { + return x.CompareTo(y) >= 0; + } + } +} diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index 181076a7..cf6fb922 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -1702,10 +1702,10 @@ namespace Microsoft.Boogie { return Type.Real; } if (arg0type.IsFloat && arg0type.Unify(arg1type)) { - return new FloatType(arg0.Type.FloatExponent, arg0.Type.FloatMantissa); + return Type.GetFloatType(arg0.Type.FloatExponent, arg0.Type.FloatMantissa); } if (arg1type.IsFloat && arg1type.Unify(arg0type)) { - return new FloatType(arg1.Type.FloatExponent, arg1.Type.FloatMantissa); + return Type.GetFloatType(arg1.Type.FloatExponent, arg1.Type.FloatMantissa); } goto BAD_TYPE; case Opcode.Div: @@ -1719,6 +1719,12 @@ namespace Microsoft.Boogie { (arg1type.Unify(Type.Int) || arg1type.Unify(Type.Real))) { return Type.Real; } + if (arg0type.IsFloat && arg0type.Unify(arg1type)) { + return Type.GetFloatType(arg0.Type.FloatExponent, arg0.Type.FloatMantissa); + } + if (arg1type.IsFloat && arg1type.Unify(arg0type)) { + return Type.GetFloatType(arg1.Type.FloatExponent, arg1.Type.FloatMantissa); + } goto BAD_TYPE; case Opcode.Pow: if (arg0type.Unify(Type.Real) && arg1type.Unify(Type.Real)) { @@ -1751,10 +1757,9 @@ namespace Microsoft.Boogie { if (arg0type.Unify(Type.Real) && arg1type.Unify(Type.Real)) { return Type.Bool; } - //if (arg0type.Unify(Type.Float) && arg1type.Unify(Type.Float)) - //{ - //return Type.Bool; - //} + if ((arg0type.IsFloat && arg0type.Unify(arg1type)) || (arg1type.IsFloat && arg1type.Unify(arg0type))) { + return Type.Bool; + } goto BAD_TYPE; case Opcode.And: case Opcode.Or: @@ -1799,9 +1804,6 @@ namespace Microsoft.Boogie { case Opcode.Pow: return Type.Real; - //case Opcode.FloatDiv: - //return Type.Float; - case Opcode.Eq: case Opcode.Neq: case Opcode.Gt: diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index 3633a9c0..f030870e 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -689,12 +689,6 @@ namespace Microsoft.Boogie.SMTLib return true; } - public bool VisitFloatDivOp(VCExprNAry node, LineariserOptions options) - { //TODO: match z3 - WriteApplication("/f", node, options); - return true; - } - public bool VisitPowOp(VCExprNAry node, LineariserOptions options) { WriteApplication("real_pow", node, options); return true; @@ -746,12 +740,6 @@ namespace Microsoft.Boogie.SMTLib return true; } - public bool VisitToFloatOp(VCExprNAry node, LineariserOptions options) - { - WriteApplication("to_float", node, options); - return true; - } - private string ExtractDatatype(Function func) { if (func is DatatypeSelector) { DatatypeSelector selector = (DatatypeSelector) func; diff --git a/Source/VCExpr/VCExprASTPrinter.cs b/Source/VCExpr/VCExprASTPrinter.cs index 8b79b0e5..00e6fb9c 100644 --- a/Source/VCExpr/VCExprASTPrinter.cs +++ b/Source/VCExpr/VCExprASTPrinter.cs @@ -302,12 +302,6 @@ namespace Microsoft.Boogie.VCExprAST { //Contract.Requires(node != null); return PrintNAry("/", node, wr); } - public bool VisitFloatDivOp(VCExprNAry node, TextWriter wr) - { - //Contract.Requires(wr != null); - //Contract.Requires(node != null); - return PrintNAry("/f", node, wr); - } public bool VisitPowOp(VCExprNAry node, TextWriter wr) { //Contract.Requires(wr != null); //Contract.Requires(node != null); @@ -353,12 +347,6 @@ namespace Microsoft.Boogie.VCExprAST { //Contract.Requires(node != null); return PrintNAry("real", node, wr); } - public bool VisitToFloatOp(VCExprNAry node, TextWriter wr) - { - //Contract.Requires(wr != null); - //Contract.Requires(node != null); - return PrintNAry("float", node, wr); - } public bool VisitBoogieFunctionOp(VCExprNAry node, TextWriter wr) { //Contract.Requires(wr != null); //Contract.Requires(node != null); diff --git a/float_test5.bpl b/float_test5.bpl index c3d279f2..be72b988 100644 --- a/float_test5.bpl +++ b/float_test5.bpl @@ -1,5 +1,4 @@ - procedure F() returns () { +procedure F() returns () { var x : float; - var y : float; - assert x + y == fp(0); + assert x - x == fp(0); } \ No newline at end of file diff --git a/float_test6.bpl b/float_test6.bpl index 307da9f7..423bc45a 100644 --- a/float_test6.bpl +++ b/float_test6.bpl @@ -1,5 +1,5 @@ procedure F() returns () { var x : float; - x := fp(1) + fp(1); - assert x == fp(2); + var y : float; + assert (x + x) + (y + y) == fp(0); } \ No newline at end of file -- cgit v1.2.3