X-Git-Url: http://git.nguyen.vg/gitweb/?a=blobdiff_plain;f=src%2Fformula.ml;h=225440fbb8a5cf80001dec8890f2162e04c7357b;hb=d4e704decf927be044d72a6fe4314aea3c8125a5;hp=03618c2e22e0cf39f13c283a8d1caa1f1c0752e0;hpb=c1b43e1dcdb3d0960dbc50db9f226d68ad30c16e;p=tatoo.git

diff --git a/src/formula.ml b/src/formula.ml
index 03618c2..225440f 100644
--- a/src/formula.ml
+++ b/src/formula.ml
@@ -15,7 +15,7 @@
 INCLUDE "utils.ml"
 
 open Format
-type move = [ `Left | `Right ]
+type move = [ `Left | `Right | `Self ]
 type 'hcons expr =
   | False | True
   | Or of 'hcons * 'hcons
@@ -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 *)
 }
 
@@ -73,16 +73,30 @@ let prio f =
     | Or _ -> 1
       
 (* Begin Lucca Hirschi *)
-let rec eval_form ss f = match expr f with
+let rec eval_form (q,qf,qn) f = match expr f with
   | False -> false
   | True -> true
-  | And(f1,f2) -> eval_form ss f1 && eval_form ss f2
-  | Or(f1,f2) -> eval_form ss f1 || eval_form ss f2
+  | And(f1,f2) -> eval_form (q,qf,qn) f1 && eval_form (q,qf,qn) f2
+  | Or(f1,f2) -> eval_form (q,qf,qn) f1 || eval_form (q,qf,qn) f2
   | Atom(dir, b, s) -> 
-    let set = match dir with |`Left -> fst ss | `Right -> snd ss in
-    StateSet.mem s set
-(* End *)
+    let set = match dir with
+      |`Left -> qf | `Right -> qn | `Self -> q in
+    if b then StateSet.mem s set
+    else not (StateSet.mem s set)
 
+let rec infer_form sq sqf sqn f = match expr f with
+  | False -> false
+  | True -> true
+  | And(f1,f2) -> infer_form sq sqf sqn f1 && infer_form sq sqf sqn f2
+  | Or(f1,f2) -> infer_form sq sqf sqn f1 || infer_form sq sqf sqn f2
+  | Atom(dir, b, s) -> 
+    let setq, setr = match dir with
+      | `Left -> sqf | `Right -> sqn | `Self -> sq in
+    (* WG: WE SUPPOSE THAT Q^r and Q^q are disjoint ! *)
+    let mem =  StateSet.mem s setq || StateSet.mem s setr in
+    if b then mem else not mem
+(* End *)
+      
 let rec print ?(parent=false) ppf f =
   if parent then fprintf ppf "(";
   let _ = match expr f with
@@ -103,6 +117,7 @@ let rec print ?(parent=false) ppf f =
           match  dir with
           | `Left ->  Pretty.down_arrow, Pretty.subscript 1
           | `Right -> Pretty.down_arrow, Pretty.subscript 2
+          | `Self -> Pretty.down_arrow, Pretty.subscript 0
         in
         fprintf fmt "%s%s" a_str d_str;
         State.print fmt s;
@@ -126,26 +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
+    | `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