ported all the counterexample code to Michal's new Model class; the goal is to eliminate the class ErrorModel from the codebase.

1 files changed, 28 insertions, 0 deletions

diff --git a/Source/Model/Model.cs b/Source/Model/Model.cs
index 98a67409..50a8f45c 100644
--- a/Source/Model/Model.cs
+++ b/Source/Model/Model.cs
@@ -254,6 +254,24 @@ namespace Microsoft.Boogie
       }

 

       /// <summary>

+      /// Look for function application with a subsequence of given arguments and return its value or null if no such application exists.

+      /// </summary>

+      public Element TryPartialEval(params Element[] args)

+      {

+        foreach (var tpl in apps) {

+          int j = 0;

+          for (int i = 0; i < args.Length; ++i) {

+            if (tpl.Args[j] == args[i]) {

+              j++;

+              if (j == tpl.Args.Length)

+                return tpl.Result;

+            }

+          }

+        }

+        return null;

+      }

+

+      /// <summary>

       /// Short for TryEval(args) == (Element)true

       /// </summary>

       public bool IsTrue(params Element[] args)

@@ -515,6 +533,11 @@ namespace Microsoft.Boogie
       return res;

     }

 

+    public Func TryGetSkolemFunc(string name)

+    {

+      return Functions.Where(f => f.Name.StartsWith(name + "!")).FirstOrDefault();

+    }

+

     public Element GetElement(string name)

     {

       Element res;

@@ -524,6 +547,11 @@ namespace Microsoft.Boogie
         throw new KeyNotFoundException("element '" + name + "' undefined in the model");

     }

 

+    public Element MkIntElement(int v)

+    {

+      return MkElement(v.ToString());

+    }

+

     public void Write(System.IO.TextWriter wr)

     {

       wr.WriteLine("*** MODEL");