| False | True
| Or of 'hcons * 'hcons
| And of 'hcons * 'hcons
- | Atom of ([ `Left | `Right ] * bool * State.t)
+ | Atom of ([ `Left | `Right | `Epsilon ] * bool * State.t)
| Pred of Tree.Predicate.t
type 'hcons node = {
pos : 'hcons expr;
mutable neg : 'hcons;
- st : (StateSet.t*StateSet.t*StateSet.t)*(StateSet.t*StateSet.t*StateSet.t);
+ st : StateSet.t * StateSet.t;
size: int; (* Todo check if this is needed *)
}
match dir with
| `Left -> Pretty.down_arrow, Pretty.subscript 1
| `Right -> Pretty.down_arrow, Pretty.subscript 2
+ | `Epsilon -> Pretty.epsilon, ""
in
fprintf fmt "%s%s" a_str d_str;
State.print fmt s;
account for hashing ! *)
pnode,nnode
-let empty_triple = StateSet.empty,StateSet.empty,StateSet.empty
-let empty_hex = empty_triple,empty_triple
-let true_,false_ = cons True False empty_hex empty_hex 0 0
+
+let empty_pair = StateSet.empty, StateSet.empty
+let true_,false_ = cons True False empty_pair empty_pair 0 0
let atom_ d p s =
let si = StateSet.singleton s in
let ss = match d with
- | `Left -> (si,StateSet.empty,si),empty_triple
- | `Right -> empty_triple,(si,StateSet.empty,si)
+ | `Left -> si, StateSet.empty
+ | `Right -> StateSet.empty, si
+ | `Epsilon -> empty_pair (* TODO CHECK *)
in fst (cons (Atom(d,p,s)) (Atom(d,not p,s)) ss ss 1 1)
let pred_ p =
let fneg = !(p.Tree.Predicate.node) in
let pneg = Tree.Predicate.make (ref (fun t n -> not (fneg t n))) in
- fst (cons (Pred p) (Pred pneg) empty_hex empty_hex 1 1)
+ fst (cons (Pred p) (Pred pneg) empty_pair empty_pair 1 1)
let not_ f = f.Node.node.neg
-let union_hex ((l1,ll1,lll1),(r1,rr1,rrr1)) ((l2,ll2,lll2),(r2,rr2,rrr2)) =
- (StateSet.mem_union l1 l2 ,StateSet.mem_union ll1 ll2,StateSet.mem_union lll1 lll2),
- (StateSet.mem_union r1 r2 ,StateSet.mem_union rr1 rr2,StateSet.mem_union rrr1 rrr2)
+
+let union_pair (l1,r1) (l2, r2) =
+ StateSet.mem_union l1 l2,
+ StateSet.mem_union r1 r2
let merge_states f1 f2 =
let sp =
- union_hex (st f1) (st f2)
+ union_pair (st f1) (st f2)
and sn =
- union_hex (st (not_ f1)) (st (not_ f2))
+ union_pair (st (not_ f1)) (st (not_ f2))
in
sp,sn
else if is_true f1 || is_true f2 then true_
else if is_false f1 && is_false f2 then false_
else if is_false f1 then f2
- else if is_false f2 then f1
+ else if is_false f2 then f1
(* commutativity of | *)
else