doc/*.ps
doc/*.out
doc/html/*
-tests/results/my.result
\ No newline at end of file
+tests/results/my.result
+.gitignore
+tests/docs/XPath-PT.xml
\ No newline at end of file
--- /dev/null
+#echo \#\#\# DOC :
+#cat ./tests/docs/XPath-PT.xml
+#echo
+for native in ./solve.native*; do
+ echo $native
+ for quer in ./tests/queries/XPath-PT/A1.xpl ; do
+ /usr/bin/time -l $native ./tests/docs/XPath-PT.xml -f ./tests/queries/XPath-PT/A1.xpl
+ done
+ echo
+done
\ No newline at end of file
+++ /dev/null
-## Without any hcons in Run:
-real 0m17.668s
-user 0m17.204s
-sys 0m0.395s
-
-## With a hconsed fixpoint in BU_Oracle:
-real 0m17.625s
-user 0m17.202s
-sys 0m0.395s
-(~0% better)
-
-## With hconsed fixpoint in BU_Oracle and BU_Over_approx
-eal 0m12.884s
-user 0m12.504s
-sys 0m0.356s
-(37% better)
-
-## With hconsed fixpoint in BU_Oracle, BU_Over_approx and TP_Max
\ No newline at end of file
| Or _ -> 1
(* Begin Lucca Hirschi *)
-let rec eval_form (q,qf,qn) f = match expr f with
- | False -> false
- | True -> true
- | 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 -> 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
+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 =
val size : t -> int
(** Syntactic size of the formula *)
-val eval_form : (StateSet.t * StateSet.t * StateSet.t) -> t -> bool
+
+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 -> bool
+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
--- /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
(* 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
-
+open Hconsed_run
module HashOracle = Hashtbl.Make(Oracle_fixpoint)
module HashRun = Hashtbl.Make(Run_fixpoint)
let map_leaf asta = (Asta.bot_states_s asta, StateSet.empty)
(* Build the Oracle *)
-let rec bu_oracle asta run tree tnode hashOracle=
+let rec bu_oracle asta run tree tnode hashOracle hashEval =
let node = Tree.preorder tree tnode in
if Tree.is_leaf tree tnode
then
let fnode,nnode = (* their preorders *)
(Tree.preorder tree tfnode, Tree.preorder tree tnnode) in
begin
- bu_oracle asta run tree tfnode hashOracle;
- bu_oracle asta run tree tnnode hashOracle;
+ 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 (* evaluates the formula*)
+ if Formula.eval_form (set,qfr,qnr) form hashEval
then
if StateSet.mem q set
then result set qfr qnr 0 tl
end
(* Build the over-approx. of the maximal run *)
-let rec bu_over_max asta run tree tnode hashOver =
+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
()
let tfnode = Tree.first_child_x tree tnode
and tnnode = Tree.next_sibling tree tnode in
begin
- bu_over_max asta run tree tfnode hashOver;
- bu_over_max asta run tree tnnode hashOver;
+ 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
| (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
+ 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 () =
(* Build the maximal run *)
-let rec tp_max asta run tree tnode hashMax =
+let rec tp_max asta run tree tnode hashMax hashInfer =
if (Tree.is_leaf tree tnode) (* BU_oracle has already created the map *)
then
()
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
+ 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;
| [] -> []
| (q,form) :: tl ->
if (StateSet.mem q (fst self)) && (* infers & trans. can start here *)
- (Formula.infer_form self qf qn form)
+ (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 =
then ()
else NodeHash.replace run nnode (StateSet.inter qnq qr,qnr);
(* indeed we delete all states from self transitions! *)
- tp_max asta run tree tfnode hashMax;
- tp_max asta run tree tnnode hashMax;
+ tp_max asta run tree tfnode hashMax hashInfer;
+ tp_max asta run tree tnnode hashMax hashInfer;
end;
end
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
let hashOracle = HashOracle.create(size_hcons_O) in
- bu_oracle asta map tree (Tree.root tree) hashOracle;
+ 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
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;
+ bu_over_max asta map tree (Tree.root tree) hashOver hashInfer;
if flag = 2
then
- tp_max asta map tree (Tree.root tree) hashMax
+ tp_max asta map tree (Tree.root tree) hashMax hashInfer
else ();
HashRun.clear hashOver;
HashRun.clear hashMax;
+++ /dev/null
-<X>
- <b>
- <a>
- <c>
- <e>
- <f>
- <g>
- <b>
- <g/>
- </b>
- </g>
- </f>
- <e/>
- </e>
- </c>
- </a>
- </b>
- <a>
- <c>
- <e>
- <f/>
- </e>
- <f>
- <X>
- <g/>
- <b>
- <g/>
- </b>
- </X>
- <e/>
- </f>
- </c>
- </a>
-</X>
projects / tatoo.git / commitdiff