blob: 59dc30923d9f3aa4f6151de732fbb3e66c508880 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
|
// 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;
}
}
}
|
