From: kim <kim@3cdefd35-fc62-479d-8e8d-bae585ffb9ca>
Date: Wed, 20 May 2009 06:38:56 +0000 (+0000)
Subject: Added correct decision procedure
X-Git-Url: http://git.nguyen.vg/gitweb/?a=commitdiff_plain;ds=sidebyside;h=9728f46b5f256250a4451c0a9bda30ce81be5b8b;p=SXSI%2Fxpathcomp.git

Added correct decision procedure

git-svn-id: svn+ssh://idea.nguyen.vg/svn/sxsi/trunk/xpathcomp@407 3cdefd35-fc62-479d-8e8d-bae585ffb9ca
---

diff --git a/ata.ml b/ata.ml
index 42bf24e..eb4f394 100644
--- a/ata.ml
+++ b/ata.ml
@@ -512,11 +512,13 @@ END
       let mk_fun f s = D_IGNORE_(register_funname f s,f)
       let mk_app_fun f arg s = let g = f arg in 
 	D_IGNORE_(register_funname g ((get_funname f) ^ " " ^ s), g) 
+      let mk_app_fun2 f arg1 arg2 s = let g = f arg1 arg2 in 
+	D_IGNORE_(register_funname g ((get_funname f) ^ " " ^ s), g) 
 
       let string_of_ts tags = (Ptset.Int.fold (fun t a -> a ^ " " ^ (Tag.to_string t) ) tags "{")^ " }"
 
 
-
+(*
       module Algebra =
 	struct
 	  type jump = [ `LONG | `CLOSE | `NIL ]
@@ -616,6 +618,139 @@ END
 	  (mk_fun (Tree.select_foll_ctx tree) "Tree.select_foll_ctx")
 	  (mk_fun (Tree.next_element_ctx tree) "Tree.node_element_ctx")	  
 	  (mk_fun (Tree.next_sibling_ctx tree) "Tree.node_sibling_ctx")	  
+*)
+      module Algebra =
+	struct
+	  type jump = [ `NIL | `ANY |`ANYNOTEXT | `JUMP ]
+	  type t = jump*Ptset.Int.t*Ptset.Int.t
+	  let jts = function 
+	  | `JUMP -> "JUMP"
+	  | `NIL -> "NIL"
+	  | `ANY -> "ANY"
+	  | `ANYNOTEXT -> "ANYNOTEXT"
+	  let merge_jump (j1,c1,l1) (j2,c2,l2) = 
+	    match j1,j2 with
+	      | _,`NIL -> (j1,c1,l1)
+	      | `NIL,_ -> (j2,c2,l2)
+	      | `ANY,_ -> (`ANY,Ptset.Int.empty,Ptset.Int.empty)
+	      | _,`ANY -> (`ANY,Ptset.Int.empty,Ptset.Int.empty)
+	      | `ANYNOTEXT,_ -> 
+ 		  if Ptset.Int.mem Tag.pcdata (Ptset.Int.union c2 l2) then
+		  (`ANY,Ptset.Int.empty,Ptset.Int.empty)
+		  else
+		  (`ANYNOTEXT,Ptset.Int.empty,Ptset.Int.empty)
+	      | _,`ANYNOTEXT -> 
+		  if Ptset.Int.mem Tag.pcdata (Ptset.Int.union c1 l1) then
+		  (`ANY,Ptset.Int.empty,Ptset.Int.empty)
+		  else
+		  (`ANYNOTEXT,Ptset.Int.empty,Ptset.Int.empty)
+	      | `JUMP,`JUMP -> (`JUMP, Ptset.Int.union c1 c2,Ptset.Int.union l1 l2)
+
+	  let merge_jump_list = function 
+	    | [] -> `NIL,Ptset.Int.empty,Ptset.Int.empty
+	    | p::r -> 
+		List.fold_left (merge_jump) p r
+	      
+	  let labels a s = 
+	    Hashtbl.fold 
+	    (
+	      fun q l acc -> 
+		if (q == s)
+		then 
+
+		  (List.fold_left 
+		      (fun acc (ts,f) ->
+			let _,_,_,bur = Transition.node f in
+			if bur then acc else TagSet.cup acc ts) 
+		    acc l)
+		else acc ) a.trans TagSet.empty
+	  exception Found
+	    
+	  let is_rec a s access = 
+	    List.exists
+	      (fun (_,t) -> let _,_,f,_ = Transition.node t in
+	      StateSet.mem s ((fun (_,_,x) -> x) (access (Formula.st f)))) (Hashtbl.find a.trans s) 
+		     
+
+	  let decide a c_label l_label dir_states dir =
+			
+	    let l = StateSet.fold 
+	      (fun s l -> 
+		 let s_rec = is_rec a s (if dir then fst else snd) in
+		 let s_rec = if dir then s_rec else
+		 (* right move *)
+		 is_rec a s fst
+		 in
+		 let s_lab = labels a s in
+		 let jmp,cc,ll = 
+		   if (not (TagSet.is_finite s_lab)) then
+		   if TagSet.mem Tag.pcdata s_lab then  (`ANY,Ptset.Int.empty,Ptset.Int.empty)
+		   else (`ANYNOTEXT,Ptset.Int.empty,Ptset.Int.empty)
+		   else 
+		   if s_rec 
+		   then (`JUMP,Ptset.Int.empty, TagSet.positive 
+			   (TagSet.cap (TagSet.inj_positive l_label) s_lab))
+		   else (`JUMP,TagSet.positive 
+			   (TagSet.cap (TagSet.inj_positive c_label) s_lab),
+			 Ptset.Int.empty )
+		 in
+		   (if jmp != `ANY 
+		    && jmp != `ANYNOTEXT 
+		    && Ptset.Int.is_empty cc 
+		    && Ptset.Int.is_empty ll
+		    then (`NIL,Ptset.Int.empty,Ptset.Int.empty)
+		    else  (jmp,cc,ll))::l) dir_states []
+	    in merge_jump_list l		 	    
+	    
+	      
+	end 
+
+
+
+      let choose_jump (d,cl,ll) f_nil f_t1 f_s1 f_tn f_sn f_s1n f_notext f_maytext =
+	match d with
+	  | `NIL -> (`NIL,f_nil)
+	  | `ANYNOTEXT -> `ANY,f_notext
+	  | `ANY -> `ANY,f_maytext
+	  | `JUMP -> 
+	      if Ptset.Int.is_empty cl then
+	      if Ptset.Int.is_singleton ll then
+	      let tag = Ptset.Int.choose ll in 
+	      (`TAG(tag),mk_app_fun f_tn tag (Tag.to_string tag))
+	      else
+	      (`ANY,mk_app_fun f_sn ll (string_of_ts ll))
+	      else if Ptset.Int.is_empty ll then
+	      if Ptset.Int.is_singleton cl then
+	      let tag = Ptset.Int.choose cl in 
+	      (`TAG(tag),mk_app_fun f_t1 tag (Tag.to_string tag))
+	      else
+	      (`ANY,mk_app_fun f_s1 cl (string_of_ts cl))
+	      else
+	      (`ANY,mk_app_fun2 f_s1n cl ll ((string_of_ts cl) ^ " " ^ (string_of_ts ll)))
+
+	  | _ -> assert false
+	  
+      let choose_jump_down tree d =
+	choose_jump d
+	  (mk_fun (fun _ -> Tree.nil) "Tree.mk_nil")
+	  (mk_fun (Tree.tagged_child tree) "Tree.tagged_child") 
+	  (mk_fun (Tree.select_child tree) "Tree.select_child")
+	  (mk_fun (Tree.tagged_desc tree) "Tree.tagged_desc")
+	  (mk_fun (Tree.select_desc tree) "Tree.select_desc") 
+	  (mk_fun (fun _ _ -> Tree.first_child tree) "[FIRSTCHILD]Tree.select_child_desc")
+	  (mk_fun (Tree.first_element tree) "Tree.first_element")
+	  (mk_fun (Tree.first_child tree) "Tree.first_child") 
+
+      let choose_jump_next tree d = 
+	choose_jump d
+  	  (mk_fun (fun _ _ -> Tree.nil) "Tree.mk_nil2")
+	  (mk_fun (Tree.tagged_sibling_ctx tree) "Tree.tagged_sibling_ctx")
+	  (mk_fun (Tree.select_sibling_ctx tree) "Tree.select_sibling_ctx")
+	  (mk_fun (Tree.tagged_foll_ctx tree) "Tree.tagged_foll_ctx")
+	  (mk_fun (Tree.select_foll_ctx tree) "Tree.select_foll_ctx")
+	  (mk_fun (fun _ _ -> Tree.next_sibling_ctx tree) "[NEXTSIBLING]Tree.select_sibling_foll_ctx")
+	  (mk_fun (Tree.next_element_ctx tree) "Tree.next_element_ctx")	  
+	  (mk_fun (Tree.next_sibling_ctx tree) "Tree.node_sibling_ctx")	  
 			  
       module SetTagKey =
       struct 
@@ -726,14 +861,16 @@ END
 		      slist (Formlistlist.nil,SList.nil,SList.nil,StateSet.empty,StateSet.empty,StateSet.empty,StateSet.empty)
 		  in			
 		    (* Logic to chose the first and next function *)
-		  let _,tags_below,_,tags_after = Tree.tags tree tag in
+		  let tags_child,tags_below,tags_siblings,tags_after = Tree.tags tree tag in
+		  let d_f = Algebra.decide a tags_child tags_below (StateSet.union ca da) true in
+		  let d_n = Algebra.decide a tags_siblings tags_after (StateSet.union sa fa) false in
 (*		  let _ = Printf.eprintf "Tags below %s are : \n" (Tag.to_string tag) in
 		  let _ = Ptset.Int.iter (fun i -> Printf.eprintf "%s " (Tag.to_string i)) tags_below in
 		  let _ = Printf.eprintf "\n%!" in *)
-		  let tags_below = Ptset.Int.remove tag tags_below in
-		  let f_kind,first = choose_jump_down tree tags_below ca da a
+(*		  let tags_below = Ptset.Int.remove tag tags_below in *)
+		  let f_kind,first = choose_jump_down tree d_f
 		  and n_kind,next = if noright then (`NIL, fun _ _ -> Tree.nil )
-		  else choose_jump_next tree tags_after sa fa a in
+		  else choose_jump_next tree d_n in
 		  let empty_res = null_result in
                   let cont =
                     match f_kind,n_kind with
diff --git a/finiteCofinite.ml b/finiteCofinite.ml
index 58f0730..907b604 100644
--- a/finiteCofinite.ml
+++ b/finiteCofinite.ml
@@ -41,6 +41,8 @@ sig
   val equal : t -> t -> bool
   val positive : t -> set
   val negative : t -> set
+  val inj_positive : set -> t
+  val inj_negative : set -> t
 end
 
 module Make (E : Sigs.Set) : S with type elt = E.elt and type set = E.t =
@@ -192,5 +194,7 @@ struct
       | CoFinite x -> x
       | _ -> E.empty
 
+  let inj_positive t = Finite t
+  let inj_negative t = CoFinite t
 end
 
diff --git a/finiteCofinite.mli b/finiteCofinite.mli
index 7f98130..72b1aec 100644
--- a/finiteCofinite.mli
+++ b/finiteCofinite.mli
@@ -35,6 +35,8 @@ module type S =
     val equal : t -> t -> bool
     val positive : t -> set
     val negative : t -> set
+    val inj_positive : set -> t
+    val inj_negative : set -> t
   end
 
 module Make :  functor (E : Sigs.Set) -> S with type elt = E.elt and type set = E.t