summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/AbsInt/IntervalDomain.cs4
-rw-r--r--Source/Basetypes/Basetypes.csproj2
-rw-r--r--Source/Basetypes/BigFloat.cs (renamed from Source/Basetypes/fp32.cs)60
-rw-r--r--Source/Core/AbsyExpr.cs6
-rw-r--r--Source/Core/Parser.cs8
-rw-r--r--Source/UnitTests/CoreTests/ExprImmutability.cs2
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());
}
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 16:09:37 +0000