type 'hcons node = {
pos : 'hcons expr;
mutable neg : 'hcons;
- st : StateSet.t * StateSet.t;
+ st : StateSet.t * StateSet.t * StateSet.t;
size: int; (* Todo check if this is needed *)
}
pnode,nnode
-let empty_pair = StateSet.empty, StateSet.empty
-let true_,false_ = cons True False empty_pair empty_pair 0 0
+let empty_triple = StateSet.empty, StateSet.empty, StateSet.empty
+let true_,false_ = cons True False empty_triple empty_triple 0 0
let atom_ d p s =
let si = StateSet.singleton s in
let ss = match d with
- | `Left -> si, StateSet.empty
- | `Right -> StateSet.empty, si
- | `Self -> StateSet.empty, StateSet.empty (* TODO WHAT? *)
+ | `Left -> StateSet.empty, si, StateSet.empty
+ | `Right -> StateSet.empty, StateSet.empty, si
+ | `Self -> si, StateSet.empty, StateSet.empty
in fst (cons (Atom(d,p,s)) (Atom(d,not p,s)) ss ss 1 1)
let not_ f = f.Node.node.neg
-let union_pair (l1,r1) (l2, r2) =
+let union_triple (s1,l1,r1) (s2,l2, r2) =
+ StateSet.union s1 s2,
StateSet.union l1 l2,
StateSet.union r1 r2
let merge_states f1 f2 =
let sp =
- union_pair (st f1) (st f2)
+ union_triple (st f1) (st f2)
and sn =
- union_pair (st (not_ f1)) (st (not_ f2))
+ union_triple (st (not_ f1)) (st (not_ f2))
in
sp,sn