1 files changed, 0 insertions, 60 deletions
diff --git a/Test/dafny1/BDD.dfy b/Test/dafny1/BDD.dfy
deleted file mode 100644
index 3b6e478c..00000000
--- a/Test/dafny1/BDD.dfy
+++ /dev/null
@@ -1,60 +0,0 @@
-
-
-module SimpleBDD
-{
-   class BDDNode
-   {
-     static predicate bitfunc(f: map<seq<bool>, bool>, n: nat)
-	 {
-	    forall i:seq<bool> :: i in f <==> |i| == n
-	 }
-      ghost var Contents: map<seq<bool>, bool>;
-	  ghost var Repr: set<object>;
-	  ghost var n: nat;
-	  var f: BDDNode, t: BDDNode;
-	  var b: bool;
-	  predicate valid()
-	    reads this, Repr;
-	  {
-	    bitfunc(Contents,n) &&
-		(0 == n ==> (b <==> Contents[[]])) &&
-		(0 < n ==> this in Repr && f != null && t != null && t in Repr && f in Repr && t.Repr <= Repr && f.Repr <= Repr && this !in f.Repr && this !in t.Repr && t.valid() && f.valid() &&
-		 t.n == f.n == n-1 &&
-		 (forall s | s in t.Contents :: Contents[[true]  + s] <==> t.Contents[s]) &&
-		 (forall s | s in f.Contents :: Contents[[false] + s] <==> f.Contents[s]))
-	  }
-   }
-   class BDD
-   {
-     var root: BDDNode;
-	 predicate valid()
-	   reads this, Repr;
-	 {
-	   root != null && root in Repr && root.Repr <= Repr && root.valid() && 
-	   n == root.n && Contents == root.Contents
-	 }
-
-     ghost var Contents: map<seq<bool>, bool>;
-	 var n: nat;
-	 ghost var Repr: set<object>;
-
-	 method Eval(s: seq<bool>) returns(b: bool)
-	    requires valid() && |s| == n;
-		ensures b == Contents[s];
-	 {
-	   var node: BDDNode := root;
-	   var i := n;
-	   assert s[n-i..] == s;
-	   while(i > 0)
-	     invariant node != null && node.valid();
-	     invariant 0 <= i == node.n <= n;
-		 invariant Contents[s] == node.Contents[s[n-i..]];
-	   {
-	     assert s[n-i..] == [s[n-i]] + s[n-i+1..];
-		 node := if s[n-i] then node.t else node.f;
-		 i := i - 1;
-	   }
-	   b := node.b;
-	 }
-   }
-}
-\ No newline at end of file