Fix predicates + following_sibling/self + add self in Formula.st + use it in Run

[tatoo.git] / src / formula.ml

diff --git a/src/formula.ml b/src/formula.ml
index c3c836b..225440f 100644 (file)
--- a/src/formula.ml
+++ b/src/formula.ml
@@ -25,7 +25,7 @@ type 'hcons expr =
 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 *)
 }
 
@@ -141,27 +141,28 @@ let cons pos neg s1 s2 size1 size2 =
     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