From c16176d2993c2df6b8b1b136c28a76cac3165b57 Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Sat, 26 Mar 2011 01:58:19 +0000
Subject: Dafny: compile quantifiers Dafny: allow {:induction} attribute to
 take an explicit list of bound variables on which to apply induction Dafny:
 split expressions when proving function postconditions Boogie and BVD:
 updated copyright year ranges

---
 Binaries/DafnyRuntime.cs | 27 +++++++++++++++++++++++++++
 1 file changed, 27 insertions(+)

(limited to 'Binaries')

diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs
index 982683b9..f32cc85a 100644
--- a/Binaries/DafnyRuntime.cs
+++ b/Binaries/DafnyRuntime.cs
@@ -218,4 +218,31 @@ namespace Dafny
       this.Cdr = b;
     }
   }
+  public partial class Helpers {
+    public static bool QuantBool(bool frall, System.Predicate<bool> pred) {
+      if (frall) {
+        return pred(false) && pred(true);
+      } else {
+        return pred(false) || pred(true);
+      }
+    }
+    public static bool QuantInt(BigInteger lo, BigInteger hi, bool frall, System.Predicate<BigInteger> pred) {
+      for (BigInteger i = lo; i < hi; i++) {
+        if (pred(i) != frall) { return !frall; }
+      }
+      return frall;
+    }
+    public static bool QuantSet<T>(Dafny.Set<T> set, bool frall, System.Predicate<T> pred) {
+      foreach (var t in set.Elements) {
+        if (pred(t) != frall) { return !frall; }
+      }
+      return frall;
+    }
+    public static bool QuantSeq<T>(Dafny.Sequence<T> seq, bool frall, System.Predicate<T> pred) {
+      foreach (var t in seq.Elements) {
+        if (pred(t) != frall) { return !frall; }
+      }
+      return frall;
+    }
+  }
 }
-- 
cgit v1.2.3