Fixed bug in printing real literals

4 files changed, 121 insertions, 6 deletions

diff --git a/Source/Basetypes/BigDec.cs b/Source/Basetypes/BigDec.cs
index 6059539b..301774f6 100644
--- a/Source/Basetypes/BigDec.cs
+++ b/Source/Basetypes/BigDec.cs
@@ -193,6 +193,54 @@ namespace Microsoft.Basetypes {
       }

     }

 

+    [Pure]

+    public string ToDecimalString() {

+      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) {

+      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

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 1bea4633..1ccec455 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -195,9 +195,9 @@ namespace Microsoft.Boogie.SMTLib
         BigDec lit = ((VCExprRealLit)node).Val;

         if (lit.IsNegative)

           // In SMT2 "-42" is an identifier (SMT2, Sect. 3.2 "Symbols")

-          wr.Write("(- 0.0 {0})", lit.Abs.ToDecimalString(20));

+          wr.Write("(- 0.0 {0})", lit.Abs.ToDecimalString());

         else

-          wr.Write(lit.ToDecimalString(20));

+          wr.Write(lit.ToDecimalString());

       }

       else {

         Contract.Assert(false);

diff --git a/Test/test21/Answer b/Test/test21/Answer
index 3ae659ec..73feaf41 100644
--- a/Test/test21/Answer
+++ b/Test/test21/Answer
@@ -279,8 +279,16 @@ Execution trace:
 

 Boogie program verifier finished with 0 verified, 1 error

 --------------------- File Real.bpl ----------------------------

+Real.bpl(26,5): Error BP5001: This assertion might not hold.

+Execution trace:

+    Real.bpl(23,5): anon0

+    Real.bpl(26,5): anon3_Then

+Real.bpl(41,5): Error BP5001: This assertion might not hold.

+Execution trace:

+    Real.bpl(34,3): anon0

+    Real.bpl(41,5): anon3_Else

 

-Boogie program verifier finished with 1 verified, 0 errors

+Boogie program verifier finished with 2 verified, 2 errors

 --------------------- File NameClash.bpl ----------------------------

 

 Boogie program verifier finished with 1 verified, 0 errors

@@ -556,8 +564,16 @@ Execution trace:
 

 Boogie program verifier finished with 0 verified, 1 error

 --------------------- File Real.bpl ----------------------------

+Real.bpl(26,5): Error BP5001: This assertion might not hold.

+Execution trace:

+    Real.bpl(23,5): anon0

+    Real.bpl(26,5): anon3_Then

+Real.bpl(41,5): Error BP5001: This assertion might not hold.

+Execution trace:

+    Real.bpl(34,3): anon0

+    Real.bpl(41,5): anon3_Else

 

-Boogie program verifier finished with 1 verified, 0 errors

+Boogie program verifier finished with 2 verified, 2 errors

 --------------------- File NameClash.bpl ----------------------------

 

 Boogie program verifier finished with 1 verified, 0 errors

@@ -836,8 +852,16 @@ Execution trace:
 

 Boogie program verifier finished with 0 verified, 1 error

 --------------------- File Real.bpl ----------------------------

+Real.bpl(26,5): Error BP5001: This assertion might not hold.

+Execution trace:

+    Real.bpl(23,5): anon0

+    Real.bpl(26,5): anon3_Then

+Real.bpl(41,5): Error BP5001: This assertion might not hold.

+Execution trace:

+    Real.bpl(34,3): anon0

+    Real.bpl(41,5): anon3_Else

 

-Boogie program verifier finished with 1 verified, 0 errors

+Boogie program verifier finished with 2 verified, 2 errors

 --------------------- File NameClash.bpl ----------------------------

 

 Boogie program verifier finished with 1 verified, 0 errors

diff --git a/Test/test21/Real.bpl b/Test/test21/Real.bpl
index 3dcf3ea3..c9a2f14d 100644
--- a/Test/test21/Real.bpl
+++ b/Test/test21/Real.bpl
@@ -14,4 +14,47 @@ procedure P(a: real, b: real) returns () {
   assert a != 0.0 ==> a / a == 1.0;

 

   assert int(a) >= 0 ==> real(3) * a > a;

-}
\ No newline at end of file
+}

+

+procedure ManyDigitReals()

+{

+  var x: real;

+  var y: real;

+  x := 15e-1;

+  y := real(3); 

+  if (*) {

+    assert x == y / 2000000000000000000000000001e-27;  // error

+  } else {

+    assert x == y / 2000000000000000000000000000e-27;

+  }

+}

+

+procedure Rounding()

+{

+  assert real(3) == 3.0;

+  assert int(2.2) == int(2.8);

+  assert int(2.2) == 2;

+  assert int(-2.2) == int(-2.8);

+  if (*) {

+    assert int(-2.2) == -3;

+  } else {

+    assert int(-2.2) == -2;  // error: int truncates downward

+  }

+}

+

+procedure VariousCornerCaseBigDecPrintingTests()

+{

+  assert 200e-2 == 2.0;

+  assert 000e-2 == 0.0;

+  assert 000e-1 == 0.0;

+  assert 000e-4 == 0.0;

+  assert 000e0 == 0.0;

+  assert 0e-300 == 0.0;

+  assert 12300e-4 == 1.230;

+  assert 12300e-5 == 0.123;

+  assert 12300e-8 == 000.000123;

+  assert 1.9850404e5 == 198504.04;

+  assert 19850404e-4 == 1985.0404;

+  assert 19850404e-12 == 0.00001985040400000;

+  assert 19850404e0000000000000000 == 1985.0404e4;

+}