From 400d0e997dda5e56ddefff919d922419bd3775ba Mon Sep 17 00:00:00 2001
From: MichalMoskal <unknown>
Date: Wed, 23 Feb 2011 00:49:41 +0000
Subject: Handle as-array[...] model elements

---
 Source/VCGeneration/Check.cs | 25 +++++++++++++++++++++++--
 1 file changed, 23 insertions(+), 2 deletions(-)

(limited to 'Source/VCGeneration')

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index e0c89603..67333752 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -386,6 +386,9 @@ namespace Microsoft.Boogie {
             break;
           case Model.ElementKind.Boolean:
             val = ((Model.Boolean)e).Value;
+            break;     
+          case Model.ElementKind.Array:
+            val = null;
             break;
           default:
             Contract.Assert(false);
@@ -424,6 +427,15 @@ namespace Microsoft.Boogie {
           tuples.Add(elseTpl);
         }
       }
+
+      foreach (var e in m.Elements) {
+        var arr = e as Model.Array;
+        if (arr != null) {
+          var tuples = this.definedFunctions[arr.Value.Name];
+          this.partitionToValue[arr.Id] = tuples;
+          this.valueToPartition[tuples] = arr.Id;
+        }
+      }
     }
 
     public Model ToModel()
@@ -434,12 +446,21 @@ namespace Microsoft.Boogie {
       Model m = new Model();
       // create an Element for every partition
       Model.Element[] elts = new Model.Element[partitionToValue.Count];
+      var asArrayIdx = 0;
       for (int i = 0; i < partitionToValue.Count; ++i) {
         var v = partitionToValue[i];
         if (v == null)
           elts[i] = m.MkElement(string.Format("*{0}", i));
-        else
-          elts[i] = m.MkElement(v.ToString());
+        else {
+          var ll = v as List<List<int>>;
+          if (ll != null) {
+            var arrName = "boogie-array#" + asArrayIdx++;
+            this.definedFunctions[arrName] = ll;
+            elts[i] = m.MkElement("as-array[" + arrName + "]");
+          }
+          else
+            elts[i] = m.MkElement(v.ToString());
+        }
 
         foreach (var id in partitionToIdentifiers[i]) {
           var f = m.MkFunc(id, 0);
-- 
cgit v1.2.3