X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Fformula.ml;h=4c58e3cc531dc501f811cd93357837711996ed08;hp=1dd0f14f0d2d2ac422c451ecc1946409cedc943b;hb=9b75e9a2074c357fc2c823156451209d2a4cef8b;hpb=447476621700590e7386283c6d2850d6cd9721c8

diff --git a/src/formula.ml b/src/formula.ml
index 1dd0f14..4c58e3c 100644
--- a/src/formula.ml
+++ b/src/formula.ml
@@ -60,7 +60,7 @@ module rec Node : Hcons.S
   end
 
 type t = Node.t
-let hash x = x.Node.key
+let hash x = x.Node.hash
 let uid x = x.Node.id
 let equal = Node.equal
 let expr f = f.Node.node.pos
@@ -96,6 +96,9 @@ let rec print ?(parent=false) ppf f =
           match  dir with
           | `Left ->  Pretty.down_arrow, Pretty.subscript 1
           | `Right -> Pretty.down_arrow, Pretty.subscript 2
+          | `Epsilon -> Pretty.epsilon, ""
+          | `Up1 -> Pretty.up_arrow, Pretty.subscript 1
+          | `Up2 -> Pretty.up_arrow, Pretty.subscript 2
         in
         fprintf fmt "%s%s" a_str d_str;
         State.print fmt s;
@@ -111,36 +114,20 @@ let is_true f = (expr f) == True
 let is_false f = (expr f) == False
 
 
-let cons pos neg s1 s2 size1 size2 =
-  let nnode = Node.make { pos = neg; neg = (Obj.magic 0); st = s2; size = size2 } in
-  let pnode = Node.make { pos = pos; neg = nnode ; st = s1; size = size1 } in
+let cons pos neg =
+  let nnode = Node.make { pos = neg; neg = (Obj.magic 0); } in
+  let pnode = Node.make { pos = pos; neg = nnode } in
     (Node.node nnode).neg <- pnode; (* works because the neg field isn't taken into
                                        account for hashing ! *)
     pnode,nnode
 
 
-let empty_pair = StateSet.empty, StateSet.empty
-let true_,false_ = cons True False empty_pair empty_pair 0 0
+let true_,false_ = cons True False
 let atom_ d p s =
-  let si = StateSet.singleton s in
-  let ss = match d with
-    | `Left -> si, StateSet.empty
-    | `Right -> StateSet.empty, si
-  in fst (cons (Atom(d,p,s)) (Atom(d,not p,s)) ss ss 1 1)
+  fst (cons (Move(d,p,s)) (Move(d,not p,s)))
 
 let not_ f = f.Node.node.neg
 
-let union_pair (l1,r1) (l2, r2) =
-  StateSet.union l1 l2,
-  StateSet.union r1 r2
-
-let merge_states f1 f2 =
-  let sp =
-    union_pair (st f1) (st f2)
-  and sn =
-    union_pair (st (not_ f1)) (st (not_ f2))
-  in
-    sp,sn
 
 let order f1 f2 = if uid f1  < uid f2 then f2,f1 else f1,f2
 
@@ -159,10 +146,7 @@ let or_ f1 f2 =
   (* commutativity of | *)
   else
     let f1, f2 = order f1 f2 in
-    let psize = (size f1) + (size f2) in
-    let nsize = (size (not_ f1)) + (size (not_ f2)) in
-    let sp, sn = merge_states f1 f2 in
-      fst (cons (Or(f1,f2)) (And(not_ f1, not_ f2)) sp sn psize nsize)
+      fst (cons (Or(f1,f2)) (And(not_ f1, not_ f2)))
 
 
 let and_ f1 f2 =