BVD Dafny: support Skolem constants

2 files changed, 15 insertions, 3 deletions

diff --git a/Source/ModelViewer/DafnyProvider.cs b/Source/ModelViewer/DafnyProvider.cs
index 721ee182..729cb14b 100644
--- a/Source/ModelViewer/DafnyProvider.cs
+++ b/Source/ModelViewer/DafnyProvider.cs
@@ -265,6 +265,7 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
   {

     internal readonly DafnyModel dm;

     internal readonly List<VariableNode> vars = new List<VariableNode>();

+    internal readonly List<VariableNode> skolems;

     internal readonly int index;

     

     public StateNode(int i, DafnyModel parent, Model.CapturedState s)

@@ -274,6 +275,7 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
       state = s;

       index = i;

 

+      skolems = new List<VariableNode>(SkolemVars());

       SetupVars();

     }

 

@@ -300,13 +302,24 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
         }

       }

 

-      dm.Flush(vars);

+      dm.Flush(Nodes);

+    }

+

+    IEnumerable<VariableNode> SkolemVars() {

+      foreach (var f in dm.model.Functions) {

+        if (f.Arity != 0) continue;

+        int n = f.Name.IndexOf('!');

+        if (n == -1) continue;

+        string name = f.Name.Substring(0, n);

+        if (!name.Contains('#')) continue;

+        yield return new VariableNode(this, name, f.GetConstant());

+      }

     }

 

     public override IEnumerable<IDisplayNode> Nodes

     {

       get {

-        return vars; 

+        return vars.Concat(skolems);

       }

     }

   }

diff --git a/Source/ModelViewer/Namer.cs b/Source/ModelViewer/Namer.cs
index 620cd4c1..2779c81d 100644
--- a/Source/ModelViewer/Namer.cs
+++ b/Source/ModelViewer/Namer.cs
@@ -158,7 +158,6 @@ namespace Microsoft.Boogie.ModelViewer
 

       Action<IEnumerable<IDisplayNode>> addList = (IEnumerable<IDisplayNode> nodes) =>

       {

-        var tmp = nodes.Select(x => x.Name).ToArray();

         var ch = nodes.ToDictionary(x => x.Name);

         foreach (var k in SortFields(nodes))

           workList.Enqueue(ch[k]);