From bb5395b35dcea5078c9b38a2f091f26256faac34 Mon Sep 17 00:00:00 2001 From: Dietrich Date: Mon, 20 Jul 2015 22:27:32 -0600 Subject: Float type now works correctly for simple variable declaration and comparison. --- Source/Basetypes/BigFloat.cs | 38 +++++++++++++++++-------------- Source/Core/AbsyType.cs | 22 ++++++++++-------- Source/Core/Parser.cs | 4 ++-- Source/Provers/SMTLib/SMTLibLineariser.cs | 2 +- Source/Provers/SMTLib/SMTLibProcess.cs | 1 - float_test2.bpl | 4 ++-- float_test3.bpl | 5 +--- float_test4.bpl | 4 ++-- float_test5.bpl | 2 +- float_test6.bpl | 6 ++--- float_test7.bpl | 6 ++--- float_test8.bpl | 1 + 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 /// /// /// - 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); } /// @@ -214,7 +214,7 @@ namespace Microsoft.Basetypes /// /// /// - 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() != 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); -- cgit v1.2.3