summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Basetypes/BigFloat.cs38
-rw-r--r--Source/Core/AbsyType.cs22
-rw-r--r--Source/Core/Parser.cs4
-rw-r--r--Source/Provers/SMTLib/SMTLibLineariser.cs2
-rw-r--r--Source/Provers/SMTLib/SMTLibProcess.cs1
-rw-r--r--float_test2.bpl4
-rw-r--r--float_test3.bpl5
-rw-r--r--float_test4.bpl4
-rw-r--r--float_test5.bpl2
-rw-r--r--float_test6.bpl6
-rw-r--r--float_test7.bpl6
-rw-r--r--float_test8.bpl1
12 files changed, 49 insertions, 46 deletions
diff --git a/Source/Basetypes/BigFloat.cs b/Source/Basetypes/BigFloat.cs
index a4cd6574..1fb05005 100644
--- a/Source/Basetypes/BigFloat.cs
+++ b/Source/Basetypes/BigFloat.cs
@@ -90,12 +90,12 @@ namespace Microsoft.Basetypes
[Pure]
public static BigFloat FromBigInt(BIM v) {
- return new BigFloat(v, 0, 23, 8); //TODO: modify for correct fp representation
+ return new BigFloat(0, v, 8, 23); //TODO: modify for correct fp representation
}
public static BigFloat FromBigDec(BIM v)
{
- return new BigFloat(v, 0, 23, 8); //TODO: modify for correct fp representation
+ return new BigFloat(0, v, 8, 23); //TODO: modify for correct fp representation
}
[Pure]
@@ -107,13 +107,13 @@ namespace Microsoft.Basetypes
{
switch (vals.Length) {
case 1:
- return Round(vals[0], 23, 8);
+ return Round(vals[0], 8, 23);
case 2:
- return new BigFloat(BIM.Parse(vals[0]), Int32.Parse(vals[1]), 23, 8);
+ return new BigFloat(Int32.Parse(vals[0]), BIM.Parse(vals[1]), 8, 23);
case 3:
return Round(vals[0], Int32.Parse(vals[1]), Int32.Parse(vals[2]));
case 4:
- return new BigFloat(BIM.Parse(vals[0]), Int32.Parse(vals[1]), Int32.Parse(vals[2]), Int32.Parse(vals[3]));
+ return new BigFloat(Int32.Parse(vals[0]), BIM.Parse(vals[1]), Int32.Parse(vals[2]), Int32.Parse(vals[3]));
default:
throw new FormatException(); //Unreachable
}
@@ -123,11 +123,11 @@ namespace Microsoft.Basetypes
}
}
- internal BigFloat(BIM mantissa, int exponent, int mantissaSize, int exponentSize) {
- this.mantissa = mantissa;
- this.mantissaSize = mantissaSize;
+ 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;
@@ -197,12 +197,12 @@ namespace Microsoft.Basetypes
/// <param name="mantissaSize"></param>
/// <param name="exponentSize"></param>
/// <returns></returns>
- public static BigFloat Round(String value, int mantissaSize, int exponentSize)
+ public static BigFloat Round(String value, int exponentSize, int mantissaSize)
{
int i = value.IndexOf('.');
if (i == -1)
- return Round(BIM.Parse(value), 0, mantissaSize, exponentSize);
- return Round(i == 0 ? 0 : BIM.Parse(value.Substring(0, i)), BIM.Parse(value.Substring(i + 1, value.Length - i - 1)), mantissaSize, exponentSize);
+ 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);
}
/// <summary>
@@ -214,7 +214,7 @@ namespace Microsoft.Basetypes
/// <param name="mantissaSize"></param>
/// <param name="exponentSize"></param>
/// <returns></returns>
- public static BigFloat Round(BIM value, BIM dec_value, int mantissaSize, int exponentSize)
+ public static BigFloat Round(BIM value, BIM dec_value, int exponentSize, int mantissaSize)
{
int exp = 0;
BIM one = new BIM(1);
@@ -262,7 +262,7 @@ namespace Microsoft.Basetypes
}
}
- return new BigFloat(value, exp, mantissaSize, exponentSize);
+ return new BigFloat(exp, value, exponentSize, mantissaSize);
}
// ``floor`` rounds towards negative infinity (like SMT-LIBv2's to_int).
@@ -395,7 +395,7 @@ namespace Microsoft.Basetypes
public BigFloat Abs {
//TODO: fix for fp functionality
get {
- return new BigFloat(BIM.Abs(Mantissa), Exponent, MantissaSize, ExponentSize);
+ return new BigFloat(Exponent, BIM.Abs(Mantissa), ExponentSize, MantissaSize);
}
}
@@ -403,7 +403,7 @@ namespace Microsoft.Basetypes
public BigFloat Negate {
//TODO: Modify for correct fp functionality
get {
- return new BigFloat(BIM.Negate(Mantissa), Exponent, MantissaSize, ExponentSize);
+ return new BigFloat(Exponent, BIM.Negate(Mantissa), ExponentSize, MantissaSize);
}
}
@@ -415,6 +415,8 @@ namespace Microsoft.Basetypes
[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;
@@ -433,7 +435,7 @@ namespace Microsoft.Basetypes
e2++;
}
- return new BigFloat(m1 + m2, e1, Math.Max(x.MantissaSize, y.MantissaSize), Math.Max(x.ExponentSize, y.ExponentSize));
+ return new BigFloat(e1, m1 + m2, x.MantissaSize, x.ExponentSize);
}
[Pure]
@@ -443,7 +445,9 @@ namespace Microsoft.Basetypes
[Pure]
public static BigFloat operator *(BigFloat x, BigFloat y) {
- return new BigFloat(x.Mantissa * y.Mantissa, x.Exponent + y.Exponent, Math.Max(x.MantissaSize, y.MantissaSize), Math.Max(x.ExponentSize, y.ExponentSize));
+ 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);
}
diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs
index 50fde975..5d41a8dd 100644
--- a/Source/Core/AbsyType.cs
+++ b/Source/Core/AbsyType.cs
@@ -330,20 +330,22 @@ namespace Microsoft.Boogie {
return false;
}
}
- public virtual int FloatMantissa {
- get {
+ public virtual int FloatExponent
+ {
+ get
+ {
{
Contract.Assert(false);
throw new cce.UnreachableException();
- } // Type.FloatMantissa should never be called
+ } // Type.FloatExponent should never be called
}
}
- public virtual int FloatExponent {
+ public virtual int FloatMantissa {
get {
{
Contract.Assert(false);
throw new cce.UnreachableException();
- } // Type.FloatExponent should never be called
+ } // Type.FloatMantissa should never be called
}
}
public virtual bool IsBv {
@@ -1050,14 +1052,14 @@ namespace Microsoft.Boogie {
public FloatType(IToken token, int exponent, int mantissa)
: base(token) {
Contract.Requires(token != null);
- Mantissa = mantissa;
Exponent = exponent;
+ Mantissa = mantissa;
}
public FloatType(int exponent, int mantissa)
: base(Token.NoToken) {
- Mantissa = mantissa;
Exponent = exponent;
+ Mantissa = mantissa;
}
//----------- Cloning ----------------------------------
@@ -1092,7 +1094,7 @@ namespace Microsoft.Boogie {
public override string ToString()
{
Contract.Ensures(Contract.Result<string>() != null);
- return "(_ FP " + Exponent + " " + Mantissa + ")";
+ return "float (" + Exponent + " " + Mantissa + ")";
}
//----------- Equality ----------------------------------
@@ -1119,10 +1121,10 @@ namespace Microsoft.Boogie {
//Contract.Requires(cce.NonNullElements(unifier));
that = that.Expanded;
if (that is TypeProxy || that is TypeVariable) {
- return that.Unify(this, unifiableVariables, unifier);
+ return that.Unify(this, unifiableVariables, unifier);
}
else {
- return this.Equals(that);
+ return this.Equals(that);
}
}
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index bb372cfb..2550c334 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -366,7 +366,7 @@ private class BvBounds : Expr {
Get();
Type(out retTy);
retTyd = new TypedIdent(retTy.tok, TypedIdent.NoName, retTy);
- } else SynErr(97);
+ } else SynErr(99);
if (la.kind == 27) {
Get();
Expression(out tmp);
@@ -374,7 +374,7 @@ private class BvBounds : Expr {
Expect(28);
} else if (la.kind == 8) {
Get();
- } else SynErr(98);
+ } else SynErr(100);
if (retTyd == null) {
// construct a dummy type for the case of syntax error
retTyd = new TypedIdent(t, TypedIdent.NoName, new BasicType(t, SimpleType.Int));
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index c7ae9d57..3633a9c0 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -141,7 +141,7 @@ namespace Microsoft.Boogie.SMTLib
else if (t.IsReal)
return "Real";
else if (t.IsFloat)
- return t.ToString(); //TODO: Match z3 syntax
+ return "(_ FloatingPoint " + t.FloatExponent + " " + t.FloatMantissa + ")"; //TODO: Match z3 syntax
else if (t.IsBv) {
return "(_ BitVec " + t.BvBits + ")";
} else {
diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs
index 2b09362b..4a1331c5 100644
--- a/Source/Provers/SMTLib/SMTLibProcess.cs
+++ b/Source/Provers/SMTLib/SMTLibProcess.cs
@@ -93,7 +93,6 @@ namespace Microsoft.Boogie.SMTLib
log = log.Replace("\r", "").Replace("\n", " ");
Console.WriteLine("[SMT-INP-{0}] {1}", smtProcessId, log);
}
- Console.WriteLine(cmd); //TODO: Remove This Line
toProver.WriteLine(cmd);
}
diff --git a/float_test2.bpl b/float_test2.bpl
index fa34d8cf..956ac757 100644
--- a/float_test2.bpl
+++ b/float_test2.bpl
@@ -1,5 +1,5 @@
procedure F() returns () {
- var x : float;
- var y : float;
+ var x : float(11 53);
+ var y : float(11 53);
assert x == y;
} \ No newline at end of file
diff --git a/float_test3.bpl b/float_test3.bpl
index 1b70ebf4..e93e7df7 100644
--- a/float_test3.bpl
+++ b/float_test3.bpl
@@ -1,6 +1,3 @@
procedure F() returns () {
- var x : float;
- var y : float;
- y := x - x;
- assert y == x;
+ assert fp(5) == fp(5 8 23);
} \ No newline at end of file
diff --git a/float_test4.bpl b/float_test4.bpl
index 2388a281..1252dc71 100644
--- a/float_test4.bpl
+++ b/float_test4.bpl
@@ -1,5 +1,5 @@
procedure F() returns () {
var x : float;
- x := fp (0 0);
- assert x == fp (0 0 23 8);
+ x := fp (.5 8 23);
+ assert x == fp (-1 0);
} \ No newline at end of file
diff --git a/float_test5.bpl b/float_test5.bpl
index b91e53e9..2f565b27 100644
--- a/float_test5.bpl
+++ b/float_test5.bpl
@@ -1,5 +1,5 @@
procedure F() returns () {
var x : float;
x := fp (0 0);
- assert x == fp (1 0 23 8);
+ assert x == fp (0 0 8 30);
} \ No newline at end of file
diff --git a/float_test6.bpl b/float_test6.bpl
index 12cfbabe..307da9f7 100644
--- a/float_test6.bpl
+++ b/float_test6.bpl
@@ -1,5 +1,5 @@
- procedure F() returns () {
+procedure F() returns () {
var x : float;
- x := fp (3);
- assert x == fp (8388608 1 23 8);
+ x := fp(1) + fp(1);
+ assert x == fp(2);
} \ No newline at end of file
diff --git a/float_test7.bpl b/float_test7.bpl
index ca33eb08..cc7a040b 100644
--- a/float_test7.bpl
+++ b/float_test7.bpl
@@ -1,5 +1,5 @@
- procedure F() returns () {
+procedure F() returns () {
var x : float;
- x := fp (.5 23 8);
- assert x == fp (0 -1);
+ x := fp(.1) + fp(.1) + fp(.1);
+ assert x == fp(.3);
} \ No newline at end of file
diff --git a/float_test8.bpl b/float_test8.bpl
index 8d881126..7c23c74f 100644
--- a/float_test8.bpl
+++ b/float_test8.bpl
@@ -1,4 +1,5 @@
procedure F() returns () {
+ Logic=QF_FP;
var x : float;
x := fp(.1) + fp(.1);
assert x == fp(.2);
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 23:28:45 +0000