diff options
Diffstat (limited to 'Source')
-rw-r--r-- | Source/AbsInt/IntervalDomain.cs | 4 | ||||
-rw-r--r-- | Source/Basetypes/Basetypes.csproj | 2 | ||||
-rw-r--r-- | Source/Basetypes/BigFloat.cs (renamed from Source/Basetypes/fp32.cs) | 60 | ||||
-rw-r--r-- | Source/Core/AbsyExpr.cs | 6 | ||||
-rw-r--r-- | Source/Core/Parser.cs | 8 | ||||
-rw-r--r-- | Source/UnitTests/CoreTests/ExprImmutability.cs | 2 |
6 files changed, 41 insertions, 41 deletions
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 @@ </Compile>
<Compile Include="BigDec.cs" />
<Compile Include="BigNum.cs" />
- <Compile Include="FP32.cs" />
+ <Compile Include="BigFloat.cs" />
<Compile Include="Rational.cs" />
<Compile Include="Set.cs" />
</ItemGroup>
diff --git a/Source/Basetypes/fp32.cs b/Source/Basetypes/BigFloat.cs index 5d76737b..d1ee73a4 100644 --- a/Source/Basetypes/fp32.cs +++ b/Source/Basetypes/BigFloat.cs @@ -19,7 +19,7 @@ namespace Microsoft.Basetypes /// 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 /// </summary> - public struct FP32 + public struct BigFloat { //Please note that this code outline is copy-pasted from BigDec.cs @@ -43,7 +43,7 @@ namespace Microsoft.Basetypes } } - public static readonly FP32 ZERO = FromInt(0); + public static readonly BigFloat ZERO = FromInt(0); private static readonly BIM two = new BIM(2); private static readonly BIM ten = new BIM(10); @@ -55,17 +55,17 @@ namespace Microsoft.Basetypes //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 + public static BigFloat FromInt(int v) { + return new BigFloat(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 + public static BigFloat FromBigInt(BIM v) { + return new BigFloat(v, 0, v < 0); //TODO: modify for correct fp representation } [Pure] - public static FP32 FromString(string v) { + public static BigFloat FromString(string v) { //TODO: completely copied from BigDec.cs at the moment if (v == null) throw new FormatException(); @@ -100,10 +100,10 @@ namespace Microsoft.Basetypes fractionLen = fractionLen - 1; } } - return new FP32(integral - fraction, exponent, integral.Sign == -1); + return new BigFloat(integral - fraction, exponent, integral.Sign == -1); } - internal FP32(BIM mantissa, int exponent, bool isNegative) { + internal BigFloat(BIM mantissa, int exponent, bool isNegative) { this.isNegative = isNegative; if (mantissa.IsZero) { this.mantissa = mantissa; @@ -128,10 +128,10 @@ namespace Microsoft.Basetypes public override bool Equals(object obj) { if (obj == null) return false; - if (!(obj is FP32)) + if (!(obj is BigFloat)) return false; - return (this == (FP32)obj); + return (this == (BigFloat)obj); } [Pure] @@ -152,7 +152,7 @@ namespace Microsoft.Basetypes // ``floor`` rounds towards negative infinity (like SMT-LIBv2's to_int). /// <summary> - /// Computes the floor and ceiling of this FP32. Note the choice of rounding towards negative + /// 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. /// </summary> /// <param name="floor">The Floor (rounded towards negative infinity)</param> @@ -277,28 +277,28 @@ namespace Microsoft.Basetypes // Basic arithmetic operations [Pure] - public FP32 Abs { + public BigFloat Abs { //TODO: fix for fp functionality get { - return new FP32(BIM.Abs(this.mantissa), this.exponent, false); + return new BigFloat(BIM.Abs(this.mantissa), this.exponent, false); } } [Pure] - public FP32 Negate { + public BigFloat Negate { //TODO: Modify for correct fp functionality get { - return new FP32(BIM.Negate(this.mantissa), this.exponent, this.Mantissa >= 0); + return new BigFloat(BIM.Negate(this.mantissa), this.exponent, this.Mantissa >= 0); } } [Pure] - public static FP32 operator -(FP32 x) { + public static BigFloat operator -(BigFloat x) { return x.Negate; } [Pure] - public static FP32 operator +(FP32 x, FP32 y) { + public static BigFloat operator +(BigFloat x, BigFloat y) { //TODO: Modify for correct fp functionality BIM m1 = x.mantissa; int e1 = x.exponent; @@ -316,18 +316,18 @@ namespace Microsoft.Basetypes e2 = e2 - 1; } - return new FP32(m1 + m2, e1, true); + return new BigFloat(m1 + m2, e1, true); } [Pure] - public static FP32 operator -(FP32 x, FP32 y) { + public static BigFloat operator -(BigFloat x, BigFloat y) { return x + y.Negate; } [Pure] - public static FP32 operator *(FP32 x, FP32 y) { + public static BigFloat operator *(BigFloat x, BigFloat y) { //TODO: modify for correct fp functionality - return new FP32(x.mantissa * y.mantissa, x.exponent + y.exponent, false); + return new BigFloat(x.mantissa * y.mantissa, x.exponent + y.exponent, false); } @@ -353,44 +353,44 @@ namespace Microsoft.Basetypes } [Pure] - public int CompareTo(FP32 that) { + public int CompareTo(BigFloat that) { //TODO: Modify for correct fp functionality if (this.mantissa == that.mantissa && this.exponent == that.exponent) { return 0; } else { - FP32 d = this - that; + BigFloat d = this - that; return d.IsNegative ? -1 : 1; } } [Pure] - public static bool operator ==(FP32 x, FP32 y) { + public static bool operator ==(BigFloat x, BigFloat y) { return x.CompareTo(y) == 0; } [Pure] - public static bool operator !=(FP32 x, FP32 y) { + public static bool operator !=(BigFloat x, BigFloat y) { return x.CompareTo(y) != 0; } [Pure] - public static bool operator <(FP32 x, FP32 y) { + public static bool operator <(BigFloat x, BigFloat y) { return x.CompareTo(y) < 0; } [Pure] - public static bool operator >(FP32 x, FP32 y) { + public static bool operator >(BigFloat x, BigFloat y) { return x.CompareTo(y) > 0; } [Pure] - public static bool operator <=(FP32 x, FP32 y) { + public static bool operator <=(BigFloat x, BigFloat y) { return x.CompareTo(y) <= 0; } [Pure] - public static bool operator >=(FP32 x, FP32 y) { + 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 7aa457fe..15ff87db 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -356,7 +356,7 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result<LiteralExpr>() != null);
return new LiteralExpr(Token.NoToken, value);
}
- public static LiteralExpr Literal(FP32 value)
+ public static LiteralExpr Literal(BigFloat value)
{
Contract.Ensures(Contract.Result<LiteralExpr>() != null);
return new LiteralExpr(Token.NoToken, value);
@@ -562,7 +562,7 @@ namespace Microsoft.Boogie { /// </summary>
/// <param name="tok"></param>
/// <param name="v"></param>
- 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<Variable>/*!*/ ins, out List<Variable>/*!*/ 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<Expr>/*!*/ es; List<Variable>/*!*/ ds; Trigger trig;
List<TypeVariable>/*!*/ typeParams;
IdentifierExpr/*!*/ id;
@@ -1863,7 +1863,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ 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<Variable>/*!*/ ins, out List<Variable>/*!*/ 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()); } |