// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"

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;
	   }
           assert s[n-i..] == [];
	   b := node.b;
	 }
   }
}