From cb3f17c366b126c8f5e859e07dcd38367d238a31 Mon Sep 17 00:00:00 2001
From: Unknown <qadeer@GHALIB.redmond.corp.microsoft.com>
Date: Mon, 27 Jun 2011 16:42:37 -0700
Subject: ported all the counterexample code to Michal's new Model class; the
 goal is to eliminate the class ErrorModel from the codebase.

---
 Source/Model/Model.cs | 28 ++++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)

(limited to 'Source/Model')

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
@@ -253,6 +253,24 @@ namespace Microsoft.Boogie
         return null;
       }
 
+      /// <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>
@@ -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");
-- 
cgit v1.2.3