Make the -mv option use the new Model class.

8 files changed, 46 insertions, 20 deletions

diff --git a/.gitignore b/.gitignore
index c6ee95ca..3ac7f5b0 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,8 +1,4 @@
-Source/AIFramework/bin/

-Source/AIFramework/obj/

-Source/AbsInt/bin/

-Source/AbsInt/obj/

-Source/Basetypes/bin/

+Source/t

 Source/_ReSharper.Boogie

 Source/Provers/*/*.user

 Source/*/*.user

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 33b9146c..0fc67e15 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -642,7 +642,7 @@ namespace Microsoft.Boogie {
                     Console.WriteLine("Execution trace:");

                     error.Print(4);

                   }

-                  if (CommandLineOptions.Clo.ModelView == 1) {

+                  if (CommandLineOptions.Clo.ModelViewFile != null) {

                     error.PrintModel();

                   }

                   errorCount++;

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 4196670f..b63b82cc 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -192,7 +192,6 @@ namespace Microsoft.Boogie {
       Contract.Invariant(-1 <= LoopFrameConditions && LoopFrameConditions < 3);

       Contract.Invariant(0 <= ModifiesDefault && ModifiesDefault < 7);

       Contract.Invariant((0 <= PrintErrorModel && PrintErrorModel <= 2) || PrintErrorModel == 4);

-      Contract.Invariant(0 <= ModelView && ModelView < 2);

       Contract.Invariant(0 <= EnhancedErrorMessages && EnhancedErrorMessages < 2);

       Contract.Invariant(0 <= StepsBeforeWidening && StepsBeforeWidening <= 9);

       Contract.Invariant(-1 <= BracketIdsInVC && BracketIdsInVC <= 1);

@@ -230,7 +229,7 @@ namespace Microsoft.Boogie {
     public int PrintErrorModel = 0;

     public string PrintErrorModelFile = null;

     public bool CEVPrint = false;

-    public int ModelView = 1;

+    public string/*?*/ ModelViewFile = null;

     public int EnhancedErrorMessages = 0;

     public bool ForceBplErrors = false; // if true, boogie error is shown even if "msg" attribute is present

     public enum BvHandling {

@@ -922,7 +921,9 @@ namespace Microsoft.Boogie {
 

           case "-mv":

           case "/mv":

-            ps.GetNumericArgument(ref ModelView, 2);

+            if (ps.ConfirmArgumentCount(1)) {

+              ModelViewFile = args[ps.i];

+            }

             break;

 

           case "-printModelToFile":

diff --git a/Source/Provers/Z3/Prover.cs b/Source/Provers/Z3/Prover.cs
index 33e622ba..f218d3b6 100644
--- a/Source/Provers/Z3/Prover.cs
+++ b/Source/Provers/Z3/Prover.cs
@@ -70,7 +70,7 @@ namespace Microsoft.Boogie.Z3
     {

       return CommandLineOptions.Clo.PrintErrorModel >= 1 ||

              CommandLineOptions.Clo.EnhancedErrorMessages == 1 ||

-             CommandLineOptions.Clo.ModelView > 0 ||

+             CommandLineOptions.Clo.ModelViewFile != null ||

              CommandLineOptions.Clo.ContractInfer ||

              CommandLineOptions.Clo.LazyInlining > 0 ||

              CommandLineOptions.Clo.StratifiedInlining > 0;

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index c128bec8..ef2501de 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -374,9 +374,12 @@ namespace Microsoft.Boogie {
       }

 

       foreach (var t in definedFunctions) {

-        var f = m.MkFunc(t.Key, t.Value.Count - 1);

+        var tuples = t.Value;

+        if (tuples.Count == 0) continue;

+

+        var f = m.MkFunc(t.Key, tuples[0].Count - 1);

         var args = new Model.Element[f.Arity];

-        foreach (var l in t.Value) {

+        foreach (var l in tuples) {

           if (l.Count == 1) continue;

           for (int i = 0; i < f.Arity; ++i)

             args[i] = elts[l[i]];

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 55cfa650..eda5cfda 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -177,7 +177,26 @@ namespace Microsoft.Boogie {
       }

     }

 

-    public void PrintModel() {

+    static bool firstModelFile = true;

+

+    public void PrintModel()

+    {

+      var filename = CommandLineOptions.Clo.ModelViewFile;

+      if (Model == null || filename == null) return;

+

+      var m = this.GetModelWithStates();

+

+      if (filename == "-") {

+        m.Write(Console.Out);

+        Console.Out.Flush();

+      } else {

+        using (var wr = new StreamWriter(filename, !firstModelFile)) {

+          firstModelFile = false;

+          m.Write(wr);

+        }      

+      }

+

+      /*

       if (Model == null || MvInfo == null) {

         return;

       }

@@ -267,6 +286,7 @@ namespace Microsoft.Boogie {
           Console.WriteLine("    undefined captured-state ID {0}", s);

         }

       }

+      */

     }

 

     public Model GetModelWithStates()

@@ -307,7 +327,12 @@ namespace Microsoft.Boogie {
 

             if (e is IdentifierExpr) {

               IdentifierExpr ide = (IdentifierExpr)e;

-              elt = m.GetFunc(ide.Decl.Name).GetConstant();

+

+              var f = m.TryGetFunc(ide.Decl.Name);

+              if (f == null) {

+                f = m.MkFunc(ide.Decl.Name, 0);

+              }              

+              elt = f.GetConstant();

             } else if (e is LiteralExpr) {

               LiteralExpr lit = (LiteralExpr)e;

               elt = m.MkElement(lit.Val.ToString());

@@ -1397,7 +1422,7 @@ namespace VC {
         Contract.Assert(pc != null);

 

         Expr copy = Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, pc.Expr);

-        if (0 < CommandLineOptions.Clo.ModelView && pc is AssumeCmd) {

+        if (CommandLineOptions.Clo.ModelViewFile != null && pc is AssumeCmd) {

           string description = QKeyValue.FindStringAttribute(pc.Attributes, "captureState");

           if (description != null) {

             Expr mv = new NAryExpr(pc.tok, new FunctionCall(mvInfo.MVState_FunctionDef), new ExprSeq(Bpl.Expr.Literal(mvInfo.CapturePoints.Count)));

diff --git a/Source/VCGeneration/Model.cs b/Source/VCGeneration/Model.cs
index 331d287a..d2d9cc24 100644
--- a/Source/VCGeneration/Model.cs
+++ b/Source/VCGeneration/Model.cs
@@ -21,7 +21,7 @@ namespace Microsoft.Boogie
 

     abstract public class Element

     {

-      protected readonly Model parent;

+      public readonly Model Model;

       internal List<FuncTuple> references = new List<FuncTuple>();

       public readonly int Id;

 

@@ -48,7 +48,7 @@ namespace Microsoft.Boogie
         }

       }

 

-      protected Element(Model p) { parent = p; }

+      protected Element(Model p) { Model = p; }

       public abstract ElementKind Kind { get; }

       public virtual int AsInt() { throw new NotImplementedException(); }

     }

@@ -94,13 +94,13 @@ namespace Microsoft.Boogie
 

     public class Func

     {

-      private readonly Model Parent;

+      public readonly Model Model;

       public readonly string Name;

       public readonly int Arity;

       internal readonly List<FuncTuple> apps = new List<FuncTuple>();

       public IEnumerable<FuncTuple> Apps { get { return apps; } }

 

-      internal Func(Model p, string n, int a) { Parent = p;  Name = n; Arity = a; }

+      internal Func(Model p, string n, int a) { Model = p;  Name = n; Arity = a; }

 

       public void SetConstant(Element res)

       {

@@ -116,7 +116,7 @@ namespace Microsoft.Boogie
         if (Arity != 0)

           throw new ArgumentException();

         if (apps.Count == 0)

-          SetConstant(Parent.MkElement("**" + Name));

+          SetConstant(Model.MkElement("**" + Name));

         return apps[0].Result;

       }

 

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 304130ef..9e8b2dc8 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -3021,6 +3021,7 @@ namespace VC {
           errModel.Print(ErrorReporter.ModelWriter);

           ErrorReporter.ModelWriter.Flush();

         }

+

         Hashtable traceNodes = new Hashtable();

         foreach (string s in labels) {

           Contract.Assert(s != null);