Display numbers within +-%0.1 of a power of two as 2^N+M

3 files changed, 34 insertions, 1 deletions

diff --git a/Source/ModelViewer/ModelViewer.csproj b/Source/ModelViewer/ModelViewer.csproj
index a78894b1..99095cec 100644
--- a/Source/ModelViewer/ModelViewer.csproj
+++ b/Source/ModelViewer/ModelViewer.csproj
@@ -60,6 +60,7 @@
   <ItemGroup>

     <Reference Include="System" />

     <Reference Include="System.Core" />

+    <Reference Include="System.Numerics" />

     <Reference Include="System.Xml.Linq" />

     <Reference Include="System.Data.DataSetExtensions" />

     <Reference Include="Microsoft.CSharp" />

diff --git a/Source/ModelViewer/Namer.cs b/Source/ModelViewer/Namer.cs
index 5b3bb870..10125a2f 100644
--- a/Source/ModelViewer/Namer.cs
+++ b/Source/ModelViewer/Namer.cs
@@ -2,6 +2,7 @@
 using System.Collections.Generic;

 using System.Linq;

 using System.Text;

+using System.Numerics;

 

 namespace Microsoft.Boogie.ModelViewer

 {

@@ -24,7 +25,7 @@ namespace Microsoft.Boogie.ModelViewer
     protected virtual bool UseLocalsForCanonicalNames

     {

       get { return false; }

-    }

+    }    

 

     public readonly ViewOptions viewOpts;

     public LanguageModel(Model model, ViewOptions opts)

@@ -32,6 +33,33 @@ namespace Microsoft.Boogie.ModelViewer
       this.model = model;

       viewOpts = opts;

     }

+

+    public string AsPow2(Model.Integer elt)

+    {      

+      var n = BigInteger.Parse(elt.Numeral);

+      var pow = new BigInteger(4096*4);

+      var k = 14;

+      var neg = false;

+      

+      if (n < 0) {

+        n = -n;

+        neg = true;

+      }

+

+      while (k < 70) {

+        var diff = pow / 1000;

+        if (pow - diff < n && n < pow + diff) {

+          diff = n - pow;

+          var res = string.Format("2^{0}{1}{2}", k, diff >= 0 ? "+" : "", diff);

+          if (neg) res = "-(" + res + ")";

+          return res;

+        }

+        k++;

+        pow *= 2;

+      }

+

+      return elt.ToString();

+    }

     

     // Elements (other than integers and Booleans) get canonical names of the form 

     // "<base>'<idx>", where <base> is returned by this function, and <idx> is given 

diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs
index 0bd59d34..0573de6b 100644
--- a/Source/ModelViewer/VccProvider.cs
+++ b/Source/ModelViewer/VccProvider.cs
@@ -404,6 +404,10 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
         return r;

       }

 

+      var i = elt as Model.Integer;

+      if (i != null)

+        return AsPow2(i);

+

       return null;

     }