From 02326abeca88715427d09f8995ee5ccfd9dab397 Mon Sep 17 00:00:00 2001 From: Dietrich Date: Fri, 17 Apr 2015 12:29:04 -0600 Subject: adding references to the floating point type wherever references to the real type exist. This remains a work in progress --- Source/UnitTests/CoreTests/ExprImmutability.cs | 3 +++ 1 file changed, 3 insertions(+) (limited to 'Source/UnitTests/CoreTests/ExprImmutability.cs') diff --git a/Source/UnitTests/CoreTests/ExprImmutability.cs b/Source/UnitTests/CoreTests/ExprImmutability.cs index b83983b6..7f266074 100644 --- a/Source/UnitTests/CoreTests/ExprImmutability.cs +++ b/Source/UnitTests/CoreTests/ExprImmutability.cs @@ -29,6 +29,9 @@ namespace CoreTests var literal4 = new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(0), 8, /*immutable=*/true); Assert.AreEqual(literal4.ComputeHashCode(), literal4.GetHashCode()); + + var literal5 = new LiteralExpr(Token.NoToken, Microsoft.Basetypes.FP32.FromInt(0), /*immutable=*/true); + Assert.AreEqual(literal5.ComputeHashCode(), literal5.GetHashCode()); } [Test()] -- cgit v1.2.3 From 1621e22e7758046e1262b22410a48250388abf29 Mon Sep 17 00:00:00 2001 From: Dietrich Date: Mon, 20 Apr 2015 14:56:59 -0600 Subject: renamed fp32 to BigFloat --- Source/AbsInt/IntervalDomain.cs | 4 +- Source/Basetypes/Basetypes.csproj | 2 +- Source/Basetypes/BigFloat.cs | 397 +++++++++++++++++++++++++ Source/Basetypes/fp32.cs | 397 ------------------------- Source/Core/AbsyExpr.cs | 6 +- Source/Core/Parser.cs | 8 +- Source/UnitTests/CoreTests/ExprImmutability.cs | 2 +- 7 files changed, 408 insertions(+), 408 deletions(-) create mode 100644 Source/Basetypes/BigFloat.cs delete mode 100644 Source/Basetypes/fp32.cs (limited to 'Source/UnitTests/CoreTests/ExprImmutability.cs') diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs index b7c6ab5b..502b7075 100644 --- a/Source/AbsInt/IntervalDomain.cs +++ b/Source/AbsInt/IntervalDomain.cs @@ -209,7 +209,7 @@ namespace Microsoft.Boogie.AbstractInterpretation } else if (ty.IsReal) { return Expr.Literal(Basetypes.BigDec.FromBigInt(n)); } else if (ty.IsFloat) { - return Expr.Literal(Basetypes.FP32.FromBigInt(n)); + return Expr.Literal(Basetypes.BigFloat.FromBigInt(n)); } else { Contract.Assume(ty.IsInt); return Expr.Literal(Basetypes.BigNum.FromBigInt(n)); @@ -671,7 +671,7 @@ namespace Microsoft.Boogie.AbstractInterpretation ((BigDec)node.Val).FloorCeiling(out floor, out ceiling); Lo = floor; Hi = ceiling; - } else if (node.Val is FP32) { + } else if (node.Val is BigFloat) { BigInteger floor, ceiling; ((BigDec)node.Val).FloorCeiling(out floor, out ceiling); Lo = floor; diff --git a/Source/Basetypes/Basetypes.csproj b/Source/Basetypes/Basetypes.csproj index 84a6ffd1..4ecdee8d 100644 --- a/Source/Basetypes/Basetypes.csproj +++ b/Source/Basetypes/Basetypes.csproj @@ -163,7 +163,7 @@ - + diff --git a/Source/Basetypes/BigFloat.cs b/Source/Basetypes/BigFloat.cs new file mode 100644 index 00000000..d1ee73a4 --- /dev/null +++ b/Source/Basetypes/BigFloat.cs @@ -0,0 +1,397 @@ +//----------------------------------------------------------------------------- +// +// 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 23-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; //TODO: restrict mantissa to be 23-bits wide + [Rep] + internal readonly int exponent; //TODO: restrict exponent to be 8-bits wide + [Rep] + internal readonly Boolean isNegative; //represents the sign bit + + public BIM Mantissa { + get { + return mantissa; + } + } + + public int Exponent { + get { + return exponent; + } + } + + public static readonly BigFloat ZERO = FromInt(0); + private static readonly BIM two = new BIM(2); + private static readonly BIM ten = new BIM(10); + + + //////////////////////////////////////////////////////////////////////////// + // 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, v < 0); //TODO: modify for correct fp representation + } + + [Pure] + public static BigFloat FromBigInt(BIM v) { + return new BigFloat(v, 0, v < 0); //TODO: modify for correct fp representation + } + + [Pure] + public static BigFloat FromString(string v) { + //TODO: completely copied from BigDec.cs at the moment + if (v == null) throw new FormatException(); + + BIM integral = BIM.Zero; + BIM fraction = BIM.Zero; + int exponent = 0; + + int len = v.Length; + + int i = v.IndexOf('e'); + if (i >= 0) { + if (i + 1 == v.Length) throw new FormatException(); + exponent = Int32.Parse(v.Substring(i + 1, len - i - 1)); + len = i; + } + + int fractionLen = 0; + i = v.IndexOf('.'); + if (i >= 0) { + if (i + 1 == v.Length) throw new FormatException(); + fractionLen = len - i - 1; + fraction = BIM.Parse(v.Substring(i + 1, fractionLen)); + len = i; + } + + integral = BIM.Parse(v.Substring(0, len)); + + if (!fraction.IsZero) { + while (fractionLen > 0) { + integral = integral * ten; + exponent = exponent - 1; + fractionLen = fractionLen - 1; + } + } + return new BigFloat(integral - fraction, exponent, integral.Sign == -1); + } + + internal BigFloat(BIM mantissa, int exponent, bool isNegative) { + this.isNegative = isNegative; + if (mantissa.IsZero) { + this.mantissa = mantissa; + this.exponent = 0; + } + else { + while (mantissa % ten == BIM.Zero) { //TODO: get this to work as expected :P + mantissa = mantissa / ten; + exponent = exponent + 1; + } + this.mantissa = mantissa; + this.exponent = exponent; + } + } + + + //////////////////////////////////////////////////////////////////////////// + // 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 this.mantissa.GetHashCode() * 13 + this.exponent.GetHashCode(); + } + + [Pure] + public override string/*!*/ ToString() { + //TODO: modify to reflect floating points + Contract.Ensures(Contract.Result() != null); + return String.Format("{0}e{1}", this.mantissa.ToString(), this.exponent.ToString()); + } + + + //////////////////////////////////////////////////////////////////////////// + // Conversion operations + + // ``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 = this.mantissa; + int e = this.exponent; + if (n.IsZero) { + floor = ceiling = n; + } else if (0 <= e) { + // it's an integer + for (; 0 < e; e--) { + n = n * ten; + } + 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 / ten; // Division rounds towards negative infinity + } + + if (this.mantissa >= 0) { + 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 = this.mantissa.ToString(); + int digits = (this.mantissa >= 0) ? s.Length : s.Length - 1; + BIM max = BIM.Pow(10, maxDigits); + BIM min = -max; + + if (this.exponent >= 0) { + if (maxDigits < digits || maxDigits - digits < this.exponent) { + return String.Format("{0}.0", (this.mantissa >= 0) ? max.ToString() : min.ToString()); + } + else { + return String.Format("{0}{1}.0", s, new string('0', this.exponent)); + } + } + else { + int exp = -this.exponent; + + if (exp < digits) { + int intDigits = digits - exp; + if (maxDigits < intDigits) { + return String.Format("{0}.0", (this.mantissa >= 0) ? 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 = this.mantissa.ToString(); + var e = this.exponent; + if (0 <= this.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(BIM.Abs(this.mantissa), this.exponent, false); + } + } + + [Pure] + public BigFloat Negate { + //TODO: Modify for correct fp functionality + get { + return new BigFloat(BIM.Negate(this.mantissa), this.exponent, this.Mantissa >= 0); + } + } + + [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 + BIM m1 = x.mantissa; + int e1 = x.exponent; + BIM m2 = y.mantissa; + int e2 = y.exponent; + if (e2 < e1) { + m1 = y.mantissa; + e1 = y.exponent; + m2 = x.mantissa; + e2 = x.exponent; + } + + while (e2 > e1) { + m2 = m2 * ten; + e2 = e2 - 1; + } + + return new BigFloat(m1 + m2, e1, true); + } + + [Pure] + public static BigFloat operator -(BigFloat x, BigFloat y) { + return x + y.Negate; + } + + [Pure] + public static BigFloat operator *(BigFloat x, BigFloat y) { + //TODO: modify for correct fp functionality + return new BigFloat(x.mantissa * y.mantissa, x.exponent + y.exponent, false); + } + + + //////////////////////////////////////////////////////////////////////////// + // Some basic comparison operations + + public bool IsPositive { + get { + return (this.mantissa > BIM.Zero); + } + } + + public bool IsNegative { + get { + return (isNegative); + } + } + + public bool IsZero { + get { + return this.mantissa.IsZero; + } + } + + [Pure] + public int CompareTo(BigFloat that) { + //TODO: Modify for correct fp functionality + if (this.mantissa == that.mantissa && this.exponent == that.exponent) { + return 0; + } + else { + BigFloat d = this - that; + return d.IsNegative ? -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/Basetypes/fp32.cs b/Source/Basetypes/fp32.cs deleted file mode 100644 index 5d76737b..00000000 --- a/Source/Basetypes/fp32.cs +++ /dev/null @@ -1,397 +0,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 23-bit mantissa - /// - public struct FP32 - { - //Please note that this code outline is copy-pasted from BigDec.cs - - // the internal representation - [Rep] - internal readonly BIM mantissa; //TODO: restrict mantissa to be 23-bits wide - [Rep] - internal readonly int exponent; //TODO: restrict exponent to be 8-bits wide - [Rep] - internal readonly Boolean isNegative; //represents the sign bit - - public BIM Mantissa { - get { - return mantissa; - } - } - - public int Exponent { - get { - return exponent; - } - } - - public static readonly FP32 ZERO = FromInt(0); - private static readonly BIM two = new BIM(2); - private static readonly BIM ten = new BIM(10); - - - //////////////////////////////////////////////////////////////////////////// - // 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 FP32 FromInt(int v) { - return new FP32(v, 0, v < 0); //TODO: modify for correct fp representation - } - - [Pure] - public static FP32 FromBigInt(BIM v) { - return new FP32(v, 0, v < 0); //TODO: modify for correct fp representation - } - - [Pure] - public static FP32 FromString(string v) { - //TODO: completely copied from BigDec.cs at the moment - if (v == null) throw new FormatException(); - - BIM integral = BIM.Zero; - BIM fraction = BIM.Zero; - int exponent = 0; - - int len = v.Length; - - int i = v.IndexOf('e'); - if (i >= 0) { - if (i + 1 == v.Length) throw new FormatException(); - exponent = Int32.Parse(v.Substring(i + 1, len - i - 1)); - len = i; - } - - int fractionLen = 0; - i = v.IndexOf('.'); - if (i >= 0) { - if (i + 1 == v.Length) throw new FormatException(); - fractionLen = len - i - 1; - fraction = BIM.Parse(v.Substring(i + 1, fractionLen)); - len = i; - } - - integral = BIM.Parse(v.Substring(0, len)); - - if (!fraction.IsZero) { - while (fractionLen > 0) { - integral = integral * ten; - exponent = exponent - 1; - fractionLen = fractionLen - 1; - } - } - return new FP32(integral - fraction, exponent, integral.Sign == -1); - } - - internal FP32(BIM mantissa, int exponent, bool isNegative) { - this.isNegative = isNegative; - if (mantissa.IsZero) { - this.mantissa = mantissa; - this.exponent = 0; - } - else { - while (mantissa % ten == BIM.Zero) { //TODO: get this to work as expected :P - mantissa = mantissa / ten; - exponent = exponent + 1; - } - this.mantissa = mantissa; - this.exponent = exponent; - } - } - - - //////////////////////////////////////////////////////////////////////////// - // Basic object operations - - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] - public override bool Equals(object obj) { - if (obj == null) - return false; - if (!(obj is FP32)) - return false; - - return (this == (FP32)obj); - } - - [Pure] - public override int GetHashCode() { - return this.mantissa.GetHashCode() * 13 + this.exponent.GetHashCode(); - } - - [Pure] - public override string/*!*/ ToString() { - //TODO: modify to reflect floating points - Contract.Ensures(Contract.Result() != null); - return String.Format("{0}e{1}", this.mantissa.ToString(), this.exponent.ToString()); - } - - - //////////////////////////////////////////////////////////////////////////// - // Conversion operations - - // ``floor`` rounds towards negative infinity (like SMT-LIBv2's to_int). - /// - /// Computes the floor and ceiling of this FP32. 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 = this.mantissa; - int e = this.exponent; - if (n.IsZero) { - floor = ceiling = n; - } else if (0 <= e) { - // it's an integer - for (; 0 < e; e--) { - n = n * ten; - } - 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 / ten; // Division rounds towards negative infinity - } - - if (this.mantissa >= 0) { - 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 = this.mantissa.ToString(); - int digits = (this.mantissa >= 0) ? s.Length : s.Length - 1; - BIM max = BIM.Pow(10, maxDigits); - BIM min = -max; - - if (this.exponent >= 0) { - if (maxDigits < digits || maxDigits - digits < this.exponent) { - return String.Format("{0}.0", (this.mantissa >= 0) ? max.ToString() : min.ToString()); - } - else { - return String.Format("{0}{1}.0", s, new string('0', this.exponent)); - } - } - else { - int exp = -this.exponent; - - if (exp < digits) { - int intDigits = digits - exp; - if (maxDigits < intDigits) { - return String.Format("{0}.0", (this.mantissa >= 0) ? 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 = this.mantissa.ToString(); - var e = this.exponent; - if (0 <= this.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 FP32 Abs { - //TODO: fix for fp functionality - get { - return new FP32(BIM.Abs(this.mantissa), this.exponent, false); - } - } - - [Pure] - public FP32 Negate { - //TODO: Modify for correct fp functionality - get { - return new FP32(BIM.Negate(this.mantissa), this.exponent, this.Mantissa >= 0); - } - } - - [Pure] - public static FP32 operator -(FP32 x) { - return x.Negate; - } - - [Pure] - public static FP32 operator +(FP32 x, FP32 y) { - //TODO: Modify for correct fp functionality - BIM m1 = x.mantissa; - int e1 = x.exponent; - BIM m2 = y.mantissa; - int e2 = y.exponent; - if (e2 < e1) { - m1 = y.mantissa; - e1 = y.exponent; - m2 = x.mantissa; - e2 = x.exponent; - } - - while (e2 > e1) { - m2 = m2 * ten; - e2 = e2 - 1; - } - - return new FP32(m1 + m2, e1, true); - } - - [Pure] - public static FP32 operator -(FP32 x, FP32 y) { - return x + y.Negate; - } - - [Pure] - public static FP32 operator *(FP32 x, FP32 y) { - //TODO: modify for correct fp functionality - return new FP32(x.mantissa * y.mantissa, x.exponent + y.exponent, false); - } - - - //////////////////////////////////////////////////////////////////////////// - // Some basic comparison operations - - public bool IsPositive { - get { - return (this.mantissa > BIM.Zero); - } - } - - public bool IsNegative { - get { - return (isNegative); - } - } - - public bool IsZero { - get { - return this.mantissa.IsZero; - } - } - - [Pure] - public int CompareTo(FP32 that) { - //TODO: Modify for correct fp functionality - if (this.mantissa == that.mantissa && this.exponent == that.exponent) { - return 0; - } - else { - FP32 d = this - that; - return d.IsNegative ? -1 : 1; - } - } - - [Pure] - public static bool operator ==(FP32 x, FP32 y) { - return x.CompareTo(y) == 0; - } - - [Pure] - public static bool operator !=(FP32 x, FP32 y) { - return x.CompareTo(y) != 0; - } - - [Pure] - public static bool operator <(FP32 x, FP32 y) { - return x.CompareTo(y) < 0; - } - - [Pure] - public static bool operator >(FP32 x, FP32 y) { - return x.CompareTo(y) > 0; - } - - [Pure] - public static bool operator <=(FP32 x, FP32 y) { - return x.CompareTo(y) <= 0; - } - - [Pure] - public static bool operator >=(FP32 x, FP32 y) { - return x.CompareTo(y) >= 0; - } - } -} diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index 7aa457fe..15ff87db 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -356,7 +356,7 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result() != null); return new LiteralExpr(Token.NoToken, value); } - public static LiteralExpr Literal(FP32 value) + public static LiteralExpr Literal(BigFloat value) { Contract.Ensures(Contract.Result() != null); return new LiteralExpr(Token.NoToken, value); @@ -562,7 +562,7 @@ namespace Microsoft.Boogie { /// /// /// - public LiteralExpr(IToken/*!*/ tok, FP32 v, bool immutable = false) + public LiteralExpr(IToken/*!*/ tok, BigFloat v, bool immutable = false) : base(tok, immutable) { Contract.Requires(tok != null); @@ -630,7 +630,7 @@ namespace Microsoft.Boogie { return Type.Int; } else if (Val is BigDec) { return Type.Real; - } else if (Val is FP32) { + } else if (Val is BigFloat) { return Type.Float; } else if (Val is BvConst) { return Type.GetBvType(((BvConst)Val).Bits); diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index e3ffc1c9..8edcebdf 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -1719,7 +1719,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { } void AtomExpression(out Expr/*!*/ e) { - Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; int n; BigNum bn; BigDec bd; FP32 fp; + Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; int n; BigNum bn; BigDec bd; BigFloat fp; List/*!*/ es; List/*!*/ ds; Trigger trig; List/*!*/ typeParams; IdentifierExpr/*!*/ id; @@ -1863,7 +1863,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { } - void Float(out FP32 n) + void Float(out BigFloat n) { string s = ""; if (la.kind == 6) { @@ -1871,10 +1871,10 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { s = t.val; } else SynErr(126); try { - n = FP32.FromString(s); + n = BigFloat.FromString(s); } catch (FormatException) { this.SemErr("incorrectly formatted number"); - n = FP32.ZERO; + n = BigFloat.ZERO; } } diff --git a/Source/UnitTests/CoreTests/ExprImmutability.cs b/Source/UnitTests/CoreTests/ExprImmutability.cs index 7f266074..86018d9b 100644 --- a/Source/UnitTests/CoreTests/ExprImmutability.cs +++ b/Source/UnitTests/CoreTests/ExprImmutability.cs @@ -30,7 +30,7 @@ namespace CoreTests var literal4 = new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(0), 8, /*immutable=*/true); Assert.AreEqual(literal4.ComputeHashCode(), literal4.GetHashCode()); - var literal5 = new LiteralExpr(Token.NoToken, Microsoft.Basetypes.FP32.FromInt(0), /*immutable=*/true); + var literal5 = new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigFloat.FromInt(0), /*immutable=*/true); Assert.AreEqual(literal5.ComputeHashCode(), literal5.GetHashCode()); } -- cgit v1.2.3