-./solve.native ./tests/docs/XPath-FT.xml -f ./tests/queries/XPath-FT.queries
\ No newline at end of file
+./solve.native ./tests/docs/XPath-FT.xml -f ./tests/queries/XPath-FT.queries 1
\ No newline at end of file
echo "________________________________________________________________________________"
./test.native ./tests/docs/my.xml -f ./tests/queries/my.queries.old
echo "Expected answer: 43 (the b from the second big sub-tree)."
-./test.native ./tests/docs/my.xml -f ./tests/queries/my.queries.old 2> tests/results/my.result
\ No newline at end of file
+./test.native ./tests/docs/my.xml -f ./tests/queries/my.queries.old 2> tests/results/my.result
+./test.native ./tests/docs/my.xml '/descendant::b/self::b'
\ No newline at end of file
State.print st
(QNameSet.to_string la)
Formula.print f
+
end
module SetT =
(remove_lab (SetT.elements (SetT.filter filter asta.trans_q)),
(remove_lab (SetT.elements (SetT.filter filter asta.trans_r))))
+let transitions_st_lab asta q lab =
+ let filter (s,l,f) = q = s && QNameSet.mem lab l in
+ let rec remove_st_lab = function
+ | [] -> []
+ | (s,l,f) :: tl -> f :: (remove_st_lab tl) in
+ (remove_st_lab (SetT.elements (SetT.filter filter asta.trans_q)),
+ (remove_st_lab (SetT.elements (SetT.filter filter asta.trans_r))))
+
let empty = {
quer = StateSet.empty;
reco = StateSet.empty;
(** Give the list of states and formulae from queries and recognizing
transitions for a given tag *)
+val transitions_st_lab : t -> state -> QName.t -> formula list * formula list
+(** Give the list of formulae from queries and recognizing transitions for a
+ given state and tag *)
+
val empty : t
(** The empty automaton *)
let pr_er = Format.err_formatter
+let ax_ (a,b,c) = a
+
let trans query =
(* Buidling of the ASTA step by step with a special case for the last
step. Then add a top most state. Each function modifies asta. *)
(* builds asta from the bottom of the query *)
let rec trans = function
| [s] -> trans_last s
- | s :: tl -> trans tl; trans_step s
+ | s :: tl -> trans tl; trans_step s (ax_(List.hd tl))
| [] -> ()
(* Add THE top most state for top-level query (done in the end) *)
and trans_init () =
let top_st = Asta.new_state () in
let or_top =
- List.fold_left (fun acc x -> ((`Left *+ x) +| acc))
- (Formula.false_) (Asta.top_states asta)
- in
+ List.fold_left (fun acc x -> ((`Left *+ x) +| acc))
+ (Formula.false_) (Asta.top_states asta) in
Asta.add_quer asta top_st;
Asta.init_top asta;
Asta.add_top asta top_st;
(* A selecting state is needed *)
and trans_last (ax,test,pred) =
- let fo_p = trans_pr pred in
+ let fo_p = trans_pr pred in (* TODO (if ax=Self, only q *)
let q,q' = Asta.new_state(), Asta.new_state() in
Asta.add_selec asta q';
Asta.add_quer asta q;
Asta.add_tr asta tr_selec true;
Asta.add_tr asta tr_q true
+ and form_next_step ax_next top_states_next form_pred =
+ match ax_next with
+ | Self -> (form_pred) *& (* (\/ top_next) /\ predicate *)
+ (List.fold_left (fun acc x -> (`Self *+ x ) +| acc)
+ Formula.false_ top_states_next)
+ | FollowingSibling -> (form_pred) *& (* (\/ top_next) /\ predicate *)
+ (List.fold_left (fun acc x -> (`Right *+ x ) +| acc)
+ Formula.false_ top_states_next)
+ | _ -> (form_pred) *& (* (\/ top_next) /\ predicate *)
+ (List.fold_left (fun acc x -> (`Left *+ x ) +| acc)
+ Formula.false_ top_states_next)
+
(* Add a new state and its transitions for the step *)
- and trans_step (ax,test,pred) =
+ and trans_step (ax,test,pred) ax_next =
let fo_p = trans_pr pred
and q = Asta.new_state() in
let Simple label = test
- and form_next = (fo_p) *& (* (\/ top_next) /\ predicat *)
- (List.fold_left (fun acc x -> (`Left *+ x ) +| acc)
- Formula.false_ (Asta.top_states asta)) in
+ and form_next = form_next_step ax_next (Asta.top_states asta) fo_p in
let tr_next = (q, label, form_next)
and tr_propa = (q, Asta.any_label, form_propa q ax) in
Asta.add_quer asta q;
(* Builds asta for predicate and gives the formula which must be satsified *)
and trans_pr_path posi = function
| Relative [] -> if posi then Formula.true_ else Formula.false_
- | Relative steps -> List.fold_left
- (fun acc x -> if posi then (`Left *+ x) +| acc else (`Left *- x) +| acc)
- Formula.false_ (trans_pr_step_l steps)
+ | Relative steps ->
+ let dir = match ax_ (List.hd steps) with
+ | Self -> `Self
+ | FollowingSibling -> `Right
+ | _ -> `Left in
+ List.fold_left
+ (fun acc x -> if posi then (dir *+ x) +| acc else (dir *- x) +| acc)
+ Formula.false_ (trans_pr_step_l steps)
| AbsoluteDoS steps as x -> print pr_er x; raise Not_core_XPath
| Absolute steps as x -> print pr_er x; raise Not_core_XPath
-
+
(* Builds asta for a predicate query and give the formula *)
and trans_pr_step_l = function
- | [step] -> trans_pr_step [] step
+ | [step] -> trans_pr_step [] step (Self) (* Self doesn't matter since [] *)
| step :: tl -> let list_top = trans_pr_step_l tl in
- trans_pr_step list_top step
+ trans_pr_step list_top step (ax_ (List.hd tl))
| [] -> failwith "Can not happened! 1"
(* Add a step on the top of a list of states in a predicate *)
- and trans_pr_step list (ax,test,pred) =
+ and trans_pr_step list (ax,test,pred) ax_next =
let form_next =
if list = []
then trans_pr pred
- else (trans_pr pred) *&
- (List.fold_left (fun acc x -> (`Left *+ x) +| acc)
- Formula.false_ list)
+ else form_next_step ax_next list (trans_pr pred)
and q = Asta.new_state()
and Simple label = test in
let tr_next = (q,label, form_next)
and form_propa q = function
| Child -> `Right *+ q
| Descendant -> (`Left *+ q +| `Right *+ q)
+ | Self -> `Self *+ q
+ | FollowingSibling -> `Right *+ q
| x -> print_axis pr_er x; raise Not_core_XPath
(* The same with a selecting state *)
and form_propa_selec q q' = function
| Child -> `Right *+ q +| `Right *+ q'
| Descendant -> (`Left *+ q +| `Right *+ q) +| (`Left *+ q' +| `Right *+ q')
+ | Self -> `Self *+ q'
+ | FollowingSibling -> `Right *+ q +| `Right *+ q'
| x -> print_axis pr_er x; raise Not_core_XPath
in
INCLUDE "utils.ml"
open Format
-type move = [ `Left | `Right ]
+type move = [ `Left | `Right | `Self ]
type 'hcons expr =
| False | True
| Or of 'hcons * 'hcons
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 *)
}
| Or _ -> 1
(* Begin Lucca Hirschi *)
-let rec eval_form ss 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
- | Atom(dir, b, s) ->
- let set = match dir with |`Left -> fst ss | `Right -> snd ss in
- if b then StateSet.mem s set
- else not (StateSet.mem s set)
-
-let rec infer_form ssq ssr f = match expr f with
- | False -> false
- | True -> true
- | And(f1,f2) -> infer_form ssq ssr f1 && infer_form ssq ssr f2
- | Or(f1,f2) -> infer_form ssq ssr f1 || infer_form ssq ssr f2
- | Atom(dir, b, s) ->
- let setq, setr = match dir with
- |`Left -> fst ssq, fst ssr
- | `Right -> snd ssq, snd ssr in
+module type HcEval =
+sig
+ type t = StateSet.t*StateSet.t*StateSet.t*Node.t
+ val equal : t -> t -> bool
+ val hash : t -> int
+end
+
+type dStateS = StateSet.t*StateSet.t
+module type HcInfer =
+sig
+ type t = dStateS*dStateS*dStateS*Node.t
+ val equal : t -> t -> bool
+ val hash : t -> int
+end
+
+module HcEval : HcEval = struct
+ type t =
+ StateSet.t*StateSet.t*StateSet.t*Node.t
+ let equal (s,l,r,f) (s',l',r',f') = StateSet.equal s s' &&
+ StateSet.equal l l' && StateSet.equal r r' && Node.equal f f'
+ let hash (s,l,r,f) =
+ HASHINT4(StateSet.hash s, StateSet.hash l, StateSet.hash r, Node.hash f)
+end
+
+let dequal (x,y) (x',y') = StateSet.equal x x' && StateSet.equal y y'
+let dhash (x,y) = HASHINT2(StateSet.hash x, StateSet.hash y)
+module HcInfer : HcInfer = struct
+ type t = dStateS*dStateS*dStateS*Node.t
+ let equal (s,l,r,f) (s',l',r',f') = dequal s s' &&
+ dequal l l' && dequal r r' && Node.equal f f'
+ let hash (s,l,r,f) =
+ HASHINT4(dhash s, dhash l, dhash r, Node.hash f)
+end
+
+module HashEval = Hashtbl.Make(HcEval)
+module HashInfer = Hashtbl.Make(HcInfer)
+type hcEval = bool Hashtbl.Make(HcEval).t
+type hcInfer = bool Hashtbl.Make(HcInfer).t
+
+let rec eval_form (q,qf,qn) f hashEval =
+try HashEval.find hashEval (q,qf,qn,f)
+with _ ->
+ let res = match expr f with
+ | False -> false
+ | True -> true
+ | And(f1,f2) -> eval_form (q,qf,qn) f1 hashEval &&
+ eval_form (q,qf,qn) f2 hashEval
+ | Or(f1,f2) -> eval_form (q,qf,qn) f1 hashEval ||
+ eval_form (q,qf,qn) f2 hashEval
+ | Atom(dir, b, s) ->
+ 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) in
+ HashEval.add hashEval (q,qf,qn,f) res;
+ res
+
+let rec infer_form sq sqf sqn f hashInfer =
+try HashInfer.find hashInfer (sq,sqf,sqn,f)
+with _ ->
+ let res = match expr f with
+ | False -> false
+ | True -> true
+ | And(f1,f2) -> infer_form sq sqf sqn f1 hashInfer &&
+ infer_form sq sqf sqn f2 hashInfer
+ | Or(f1,f2) -> infer_form sq sqf sqn f1 hashInfer ||
+ infer_form sq sqf sqn f2 hashInfer
+ | 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
+ let mem = StateSet.mem s setq || StateSet.mem s setr in
+ if b then mem else not mem in
+ HashInfer.add hashInfer (sq,sqf,sqn,f) res;
+ res
(* End *)
-
+
let rec print ?(parent=false) ppf f =
if parent then fprintf ppf "(";
let _ = match expr f with
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;
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
(** Implementation of hashconsed Boolean formulae *)
-type move = [ `Left |`Right ]
+type move = [ `Left |`Right | `Self ]
(** Direction for automata predicates *)
type 'hcons expr =
val expr : t -> t expr
(** Equality over formulae *)
-val st : t -> StateSet.t * StateSet.t
-(** states occuring left and right, positively or negatively *)
+val st : t -> StateSet.t * StateSet.t * StateSet.t
+(** States occuring self, left and right, positively or negatively *)
val compare : t -> t -> int
(** Comparison of formulae *)
val size : t -> int
(** Syntactic size of the formula *)
-val eval_form : (StateSet.t * StateSet.t) -> t -> bool
-(** [eval_form (sf,sn) F] evaluates the formula [F] on [(sf,sn)] *)
-val infer_form : (StateSet.t * StateSet.t) -> (StateSet.t * StateSet.t) -> t -> bool
-(** [eval_form S1 S2 F] infers S1; S2 |- F *)
+module HcEval : sig
+ include Sigs.HashedType
+end
+module HcInfer : sig
+ include Sigs.HashedType
+end
+module HashEval : Hashtbl.S
+module HashInfer : Hashtbl.S
+type hcEval = bool HashEval.t
+type hcInfer = bool HashInfer.t
+(** Optimization: hconsigned eval and infer *)
+
+val eval_form : (StateSet.t * StateSet.t * StateSet.t) -> t -> hcEval -> bool
+(** [eval_form (s,sf,sn) F] evaluates the formula [F] on [(s,sf,sn)] *)
+
+val infer_form : (StateSet.t * StateSet.t) -> (StateSet.t * StateSet.t) ->
+ (StateSet.t * StateSet.t) -> t -> hcInfer -> bool
+(** [eval_form S Sf Sn F] infers S; (S1,S2) |- F *)
val print : Format.formatter -> t -> unit
(** Pretty printer *)
--- /dev/null
+(***********************************************************************)
+(* *)
+(* Lucca Hirschi, LRI UMR8623 *)
+(* Université Paris-Sud & CNRS *)
+(* *)
+(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(* Recherche Scientifique. All rights reserved. This file is *)
+(* distributed under the terms of the GNU Lesser General Public *)
+(* License, with the special exception on linking described in file *)
+(* ../LICENSE. *)
+(* *)
+(***********************************************************************)
+
+INCLUDE "utils.ml"
+
+
+(* Hash Consign modules *)
+
+module type Oracle_fixpoint =
+sig
+ type t = StateSet.t*StateSet.t*StateSet.t*((StateSet.elt*Formula.t) list)*QName.t
+ val equal : t -> t -> bool
+ val hash : t -> int
+end
+
+type dStateS = StateSet.t*StateSet.t
+module type Run_fixpoint =
+sig
+ type t = dStateS*dStateS*dStateS*(State.t*Formula.t) list*QName.t
+ val equal : t -> t -> bool
+ val hash : t -> int
+end
+
+module Oracle_fixpoint : Oracle_fixpoint = struct
+ type t =
+ StateSet.t*StateSet.t*StateSet.t*((StateSet.elt*Formula.t) list)*QName.t
+ let equal (s,l,r,list,t) (s',l',r',list',t') = StateSet.equal s s' &&
+ StateSet.equal l l' && StateSet.equal r r' && QName.equal t t'
+ let hash (s,l,r,list,t) =
+ HASHINT4(StateSet.hash s, StateSet.hash l, StateSet.hash r, QName.hash t)
+end
+
+let dequal (x,y) (x',y') = StateSet.equal x x' && StateSet.equal y y'
+let dhash (x,y) = HASHINT2(StateSet.hash x, StateSet.hash y)
+module Run_fixpoint : Run_fixpoint = struct
+ type t = dStateS*dStateS*dStateS*(State.t*Formula.t) list*QName.t
+ let equal (s,l,r,list,t) (s',l',r',list',t') = dequal s s' &&
+ dequal l l' && dequal r r' && QName.equal t t'
+ let hash (s,l,r,list,t) =
+ HASHINT4(dhash s, dhash l, dhash r, QName.hash t)
+end
(* *)
(***********************************************************************)
+INCLUDE "utils.ml"
+
module Node =
struct
type t = int
type t = (StateSet.t*StateSet.t) NodeHash.t
(** Map from nodes to query and recognizing states *)
-(* Note that we do not consider the nil nodes *)
+(* Note that we do not consider nil nodes *)
exception Oracle_fail
exception Over_max_fail
exception Max_fail
+
+(* Hash Consign modules *)
+open Hconsed_run
+module HashOracle = Hashtbl.Make(Oracle_fixpoint)
+module HashRun = Hashtbl.Make(Run_fixpoint)
+
(* Mapped sets for leaves *)
let map_leaf asta = (Asta.bot_states_s asta, StateSet.empty)
(* Build the Oracle *)
-let rec bu_oracle asta run tree tnode =
+let rec bu_oracle asta run tree tnode hashOracle hashEval =
let node = Tree.preorder tree tnode in
if Tree.is_leaf tree tnode
then
then ()
else NodeHash.add run node (map_leaf asta)
else
- let tfnode = Tree.first_child tree tnode (* first child *)
- and tnnode = Tree.next_sibling tree tnode in (* next-sibling *)
+ let tfnode = Tree.first_child_x tree tnode
+ and tnnode = Tree.next_sibling tree tnode in
let fnode,nnode = (* their preorders *)
(Tree.preorder tree tfnode, Tree.preorder tree tnnode) in
begin
- bu_oracle asta run tree tfnode;
- bu_oracle asta run tree tnnode;
+ bu_oracle asta run tree tfnode hashOracle hashEval;
+ bu_oracle asta run tree tnnode hashOracle hashEval;
+ (* add states which satisfy a transition *)
+ let rec result set qfr qnr flag = function
+ | [] -> set,flag
+ | (q,form) :: tl ->
+ if Formula.eval_form (set,qfr,qnr) form hashEval
+ then
+ if StateSet.mem q set
+ then result set qfr qnr 0 tl
+ else result (StateSet.add q set) qfr qnr 1 tl
+ else result set qfr qnr 0 tl in
+ (* compute the fixed point of states of node *)
+ let rec fix_point set_i qfr qnr list_tr t =
+ try HashOracle.find hashOracle (set_i, qfr, qnr, list_tr, t)
+ with _ ->
+ let set,flag = result set_i qfr qnr 0 list_tr in
+ HashOracle.add hashOracle (set_i,qfr,qnr,list_tr,t) (set); (* todo: Think about this position *)
+ if flag = 0
+ then set
+ else fix_point set qfr qnr list_tr t in
let q_rec n = (* compute the set for child/sibling *)
try NodeHash.find run n
with Not_found -> map_leaf asta in
let (_,qfr),(_,qnr) = q_rec fnode,q_rec nnode (* computed in rec call *)
and lab = Tree.tag tree tnode in
- let _,list_tr = Asta.transitions_lab asta lab in (* only reco. tran.*)
- let rec result set = function
- | [] -> set
- | (q,form) :: tl ->
- if Formula.eval_form (qfr,qnr) form (* evaluates the formula *)
- then result (StateSet.add q set) tl
- else result set tl in
- let result_set = result StateSet.empty list_tr in
- NodeHash.add run node (StateSet.empty, result_set)
+ let _,list_tr = Asta.transitions_lab asta lab in (*only reco. tran.*)
+ NodeHash.add run node (StateSet.empty,
+ fix_point StateSet.empty qfr qnr list_tr lab)
end
(* Build the over-approx. of the maximal run *)
-let rec bu_over_max asta run tree tnode =
+let rec bu_over_max asta run tree tnode hashOver hashInfer =
if (Tree.is_leaf tree tnode) (* BU_oracle has already created the map *)
then
()
else
- let tfnode = Tree.first_child tree tnode
+ let tfnode = Tree.first_child_x tree tnode
and tnnode = Tree.next_sibling tree tnode in
begin
- bu_over_max asta run tree tfnode;
- bu_over_max asta run tree tnnode;
+ bu_over_max asta run tree tfnode hashOver hashInfer;
+ bu_over_max asta run tree tnnode hashOver hashInfer;
let (fnode,nnode) =
(Tree.preorder tree tfnode, Tree.preorder tree tnnode)
and node = Tree.preorder tree tnode in
let q_rec n =
try NodeHash.find run n
with Not_found -> map_leaf asta in
- let (qfq,qfr),(qnq,qnr) = q_rec fnode,q_rec nnode in
+ let qf,qn = q_rec fnode,q_rec nnode in
let lab = Tree.tag tree tnode in
- let list_tr,_ = Asta.transitions_lab asta lab in (* only take query st. *)
- let rec result set = function
- | [] -> set
- | (q,form) :: tl ->
- if Formula.infer_form (qfq,qnq) (qfr,qnr) form (* infers the formula*)
- then result (StateSet.add q set) tl
- else result set tl in
- let _,resultr = try NodeHash.find run node
+ let list_tr,_ = Asta.transitions_lab asta lab (* only take query st. *)
+ and _,resultr = try NodeHash.find run node
with _ -> raise Over_max_fail in
- let result_set = result StateSet.empty list_tr in
+ let rec result set qf qn flag list_tr = function
+ | [] -> if flag = 0 then set else result set qf qn 0 list_tr list_tr
+ | (q,form) :: tl ->
+ if StateSet.mem q set
+ then result set qf qn 0 list_tr tl
+ else if Formula.infer_form (set,resultr) qf qn form hashInfer
+ then result (StateSet.add q set) qf qn 1 list_tr tl
+ else result set qf qn 0 list_tr tl in
+ let result_set () =
+ try HashRun.find hashOver ((StateSet.empty,resultr),qf,qn,list_tr,lab)
+ with _ -> let res = result StateSet.empty qf qn 0 list_tr list_tr in
+ HashRun.add hashOver
+ ((StateSet.empty,resultr), qf,qn,list_tr,lab) res;
+ res in
(* we keep the old recognizing states set *)
- NodeHash.replace run node (result_set, resultr)
+ NodeHash.replace run node (result_set(), resultr)
end
(* Build the maximal run *)
-let rec tp_max asta run tree tnode =
+let rec tp_max asta run tree tnode hashMax hashInfer =
if (Tree.is_leaf tree tnode) (* BU_oracle has already created the map *)
then
()
else
let node = Tree.preorder tree tnode
- and tfnode = Tree.first_child tree tnode
+ and tfnode = Tree.first_child_x tree tnode
and tnnode = Tree.next_sibling tree tnode in
let (fnode,nnode) =
(Tree.preorder tree tfnode, Tree.preorder tree tnnode) in
let q_rec n =
try NodeHash.find run n
with Not_found -> map_leaf asta in
- let (qfq,qfr),(qnq,qnr) = q_rec fnode,q_rec nnode in
+ let qf,qn = q_rec fnode,q_rec nnode in
let lab = Tree.tag tree tnode in
let list_tr,_ = Asta.transitions_lab asta lab in (* only take query. *)
- let set_node,_ = try NodeHash.find run node
- with _ -> raise Max_fail in
- let rec result = function
+ let (self_q,self_r) = try NodeHash.find run node
+ with Not_found -> raise Max_fail in
+
+ (* We must compute again accepting states from self transitions since
+ previous calls of tp_max may remove them *)
+ let rec result_q self_q queue = function (* for initializing the queue *)
+ | [] -> self_q,queue
+ | (q,form) :: tl ->
+ if (StateSet.mem q self_q)
+ then begin
+ let q_cand,_,_ = Formula.st form in
+ StateSet.iter (fun x -> Queue.push x queue) q_cand;
+ result_q (StateSet.add q self_q) queue tl;
+ end
+ else result_q self_q queue tl
+ and result_st_q self_q queue flag = function (*for computing the fixed p*)
+ | [] -> flag,queue
+ | form :: tl ->
+ if Formula.infer_form (self_q,self_r) qf qn form hashInfer
+ then begin
+ let q_cand,_,_ = Formula.st form in
+ StateSet.iter (fun x -> Queue.push x queue) q_cand;
+ result_st_q self_q queue 1 tl;
+ end
+ else result_st_q self_q queue flag tl in
+ let rec comp_acc_self self_q_i queue = (* compute the fixed point *)
+ if Queue.is_empty queue (* todo: to be hconsigned? *)
+ then self_q_i
+ else
+ let q = Queue.pop queue in
+ let list_q,_ = Asta.transitions_st_lab asta q lab in
+ let flag,queue = result_st_q self_q_i queue 0 list_q in
+ let self_q = if flag = 1 then StateSet.add q self_q_i else self_q_i in
+ comp_acc_self self_q queue in
+
+ let self,queue_init = result_q self_q (Queue.create()) list_tr in
+ let self_q = comp_acc_self self_q queue_init in
+ NodeHash.replace run node (self_q,self_r);
+ (* From now, the correct set of states is mapped to (self) node! *)
+ let rec result self qf qn = function
| [] -> []
| (q,form) :: tl ->
- if (Formula.infer_form (qfq,qnq) (qfr,qnr) form) &&
- (StateSet.mem q set_node) (* infers & trans. can start here *)
- then form :: (result tl)
- else result tl in
- let list_form = result list_tr in (* tran. candidates *)
+ if (StateSet.mem q (fst self)) && (* infers & trans. can start here *)
+ (Formula.infer_form self qf qn form hashInfer)
+ then form :: (result self qf qn tl)
+ else result self qf qn tl in
+ let list_form =
+ try HashRun.find hashMax ((self_q,self_r),qf,qn,list_tr,lab)
+ with _ -> let res = result (self_q,self_r) qf qn list_tr in
+ HashRun.add hashMax ((self_q,self_r),qf,qn,list_tr,lab) res;
+ res in
(* compute states occuring in transition candidates *)
let rec add_st (ql,qr) = function
| [] -> ql,qr
- | f :: tl -> let sql,sqr = Formula.st f in
+ | f :: tl -> let sqs,sql,sqr = Formula.st f in
let ql' = StateSet.union sql ql
and qr' = StateSet.union sqr qr in
add_st (ql',qr') tl in
and qnq,qnr = try NodeHash.find run nnode
with | _ -> map_leaf asta in
begin
- if tfnode == Tree.nil
+ if tfnode == Tree.nil || Tree.is_attribute tree tnode
then ()
else NodeHash.replace run fnode (StateSet.inter qfq ql,qfr);
- if tnnode == Tree.nil
+ if tnnode == Tree.nil || Tree.is_attribute tree tnode
then ()
else NodeHash.replace run nnode (StateSet.inter qnq qr,qnr);
- tp_max asta run tree tfnode;
- tp_max asta run tree tnnode;
+ (* indeed we delete all states from self transitions! *)
+ tp_max asta run tree tfnode hashMax hashInfer;
+ tp_max asta run tree tnnode hashMax hashInfer;
end;
end
let compute tree asta =
let flag = 2 in (* debug *)
let size_tree = 10000 in (* todo (Tree.size ?) *)
+ let size_hcons_O = 1000 in (* todo size Hashtbl *)
+ let size_hcons_M = 1000 in (* todo size Hashtbl *)
+ let size_hcons_F = 1000 in (* todo size Hashtbl *)
let map = NodeHash.create size_tree in
- bu_oracle asta map tree (Tree.root tree);
+ let hashOracle = HashOracle.create(size_hcons_O) in
+ let hashEval = Formula.HashEval.create(size_hcons_F) in
+ let hashInfer = Formula.HashInfer.create(size_hcons_F) in
+ bu_oracle asta map tree (Tree.root tree) hashOracle hashEval;
+ HashOracle.clear hashOracle;
+ Formula.HashEval.clear hashEval;
if flag > 0 then begin
- bu_over_max asta map tree (Tree.root tree);
+ let hashOver = HashRun.create(size_hcons_M) in
+ let hashMax = HashRun.create(size_hcons_M) in
+ bu_over_max asta map tree (Tree.root tree) hashOver hashInfer;
if flag = 2
then
- tp_max asta map tree (Tree.root tree)
- else ()
+ tp_max asta map tree (Tree.root tree) hashMax hashInfer
+ else ();
+ HashRun.clear hashOver;
+ HashRun.clear hashMax;
end
else ();
map
NodeHash.fold
(fun key set acc ->
if not(StateSet.is_empty
- (StateSet.inter (fst set) (Asta.selec_states asta)))
+ (StateSet.inter (fst set) (Asta.selec_states asta)))
then key :: acc
else acc)
run []
let () =
let flag = Array.length Sys.argv = 5 in
+ let flag2 =
+ if flag
+ then int_of_string Sys.argv.(4) = 1
+ else false in
Format.pp_set_margin err_formatter 80;
let doc = doc () in
let queries = query () in
fprintf err_formatter " ### Query: %a"
XPath.Ast.print query
else ();
- fprintf err_formatter "@. ### Selected nodes: {%a}@."
- print_selec selected_nodes;
+ if flag2 then
+ fprintf err_formatter "@. ### Selected nodes: {%a}@."
+ print_selec selected_nodes
+ else ();
if flag
then begin
Asta.print err_formatter asta;
let root t = t.root
let first_child _ n = n.first_child
+let first_child_x _ n =
+ if n.first_child.tag == QName.attribute_map
+ then n.first_child.next_sibling
+ else n.first_child
let next_sibling _ n = n.next_sibling
let parent _ n = n.parent
(* Begin Lucca Hirschi *)
-let is_leaf t n = (first_child t n == nil) && (next_sibling t n == nil)
+let is_leaf t n = (not (n.tag == QName.attribute_map)) &&
+ (first_child t n == nil) && (next_sibling t n == nil)
+let is_attribute t n = n.tag == QName.attribute_map
(* End *)
let tag _ n = n.tag
let data _ n = n.data
let fchild =
if node.first_child.tag == QName.attribute_map then
let () =
- print_attributes out tree_ node.first_child.first_child
+ let ffn = node.first_child.first_child in
+ print_attributes out tree_ ffn;
in
node.first_child.next_sibling
else
end
in
print_xml_preorder out tree_ node.next_sibling
+
+let debug_node fmt t n =
+ Parser.debug_node fmt n
Returns [nil] if [n] is a leaf. Returns [nil] if [n == nil].
*)
+val first_child_x : t -> node -> node
+(** [first_child t n] returns the first child which is not an attribute
+ of node [n] in tree [t].
+ Returns [nil] if [n] is a leaf. Returns [nil] if [n == nil].
+*)
+
val next_sibling : t -> node -> node
(** [next_sibling t n] returns the next_sibling of node [n] in tree [t].
Returns [nil] if [n] is the last child of a node.
*)
val is_leaf : t -> node -> bool
-(** Return true if the node is a *)
+(** Return true if the node is a leaf or an attribute *)
+
+val is_attribute : t -> node -> bool
+(** Return true if the node is an attribute *)
val tag : t -> node -> QName.t
(** Returns the label of a given node *)
val print_xml_preorder : out_channel -> t -> node -> unit
(** Outputs the tree with IDs for nodes as an XML document on the
given output_channel *)
+
+val debug_node : Format.formatter -> t -> node -> unit
+(** DEBUG *)
-<?xml version="1.0" encoding="UTF-8"?><!DOCTYPE A SYSTEM "alphabet.dtd"><A id="n1" pre="1" post="26" xml:lang="en"><B id="n2" pre="2" post="3"><C id="n3" pre="3" post="1">clergywoman</C><D id="n4" pre="4" post="2">decadent</D></B><E id="n5" pre="5" post="22"><F id="n6" pre="6" post="6"><G id="n7" pre="7" post="4">gentility</G><H id="n8" pre="8" post="5" idrefs="n17 n26">happy-go-lucky man</H></F><I id="n9" pre="9" post="9"><J id="n10" pre="10" post="7">jigsaw</J><K id="n11" pre="11" post="8">kerchief</K></I><L id="n12" pre="12" post="15"><!--L is the twelve-th letter of the English alphabet-->The letter L is followed by the letter:<M id="n13" pre="13" post="10"/>which is followed by the letter:<N id="n14" pre="14" post="13"><O id="n15" pre="15" post="11">ovenware</O><P id="n16" pre="16" post="12">plentiful</P></N><?myPI value="XPath is nice"?><Q id="n17" pre="17" post="14" idrefs="n8 n26">quarrelsome</Q></L><R id="n18" pre="18" post="18"><S id="n19" pre="19" post="16">sage</S><T id="n20" pre="20" post="17">tattered</T></R><U id="n21" pre="21" post="21"><V id="n22" pre="22" post="19">voluptuary</V><W id="n23" pre="23" post="20">wriggle</W></U></E><X id="n24" pre="24" post="25"><Y id="n25" pre="25" post="23">yawn</Y><Z id="n26" pre="26" post="24" idrefs="n8 n17" xml:lang="it">zuzzurellone</Z></X></A>
+<A id="n1" pre="1" post="26" xml:lang="en">
+<B id="n2" pre="2" post="3">
+<C id="n3" pre="3" post="1">clergywoman</C>
+<D id="n4" pre="4" post="2">decadent</D>
+</B>
+<E id="n5" pre="5" post="22">
+<F id="n6" pre="6" post="6">
+<G id="n7" pre="7" post="4">gentility</G>
+<H id="n8" pre="8" post="5" idrefs="n17 n26">happy-go-lucky man</H>
+</F>
+<I id="n9" pre="9" post="9">
+<J id="n10" pre="10" post="7">jigsaw</J>
+<K id="n11" pre="11" post="8">kerchief</K>
+</I>
+<L id="n12" pre="12" post="15">
+<!-- L is the twelve-th letter of the English alphabet -->
+The letter L is followed by the letter:
+<M id="n13" pre="13" post="10"/>
+which is followed by the letter:
+<N id="n14" pre="14" post="13">
+<O id="n15" pre="15" post="11">ovenware</O>
+<P id="n16" pre="16" post="12">plentiful</P>
+</N>
+<?myPI value="XPath is nice"?>
+<Q id="n17" pre="17" post="14" idrefs="n8 n26">quarrelsome</Q>
+</L>
+<R id="n18" pre="18" post="18">
+<S id="n19" pre="19" post="16">sage</S>
+<T id="n20" pre="20" post="17">tattered</T>
+</R>
+<U id="n21" pre="21" post="21">
+<V id="n22" pre="22" post="19">voluptuary</V>
+<W id="n23" pre="23" post="20">wriggle</W>
+</U>
+</E>
+<X id="n24" pre="24" post="25">
+<Y id="n25" pre="25" post="23">yawn</Y>
+<Z id="n26" pre="26" post="24" idrefs="n8 n17" xml:lang="it">zuzzurellone</Z>
+</X>
+</A>
-/descendant::L
+/descendant::L/child::*
/descendant::L/descendant::*
/descendant::L/following-sibling::*
/descendant::L/self::*
projects / tatoo.git / commitdiff