From: Kim Nguyễn Date: Wed, 14 Mar 2012 18:07:42 +0000 (+0100) Subject: Finaly clean up formula representation. X-Git-Url: http://git.nguyen.vg/gitweb/?a=commitdiff_plain;h=d8e8a2b5c08a980a440d9fc9f3ea27af7711b524;hp=a3cacfe74ac30fee5fe3afd6b7fa98dea774aad6;p=SXSI%2Fxpathcomp.git Finaly clean up formula representation. --- diff --git a/src/ata.ml b/src/ata.ml index 0ae811d..f0882d5 100644 --- a/src/ata.ml +++ b/src/ata.ml @@ -183,7 +183,7 @@ let top_down_approx auto states tree = else TagSet.positive ts in let _, _, m, f = Transition.node tr in - let (_, _, ls), (_, _, rs) = Formula.st f in + let ls, rs = Formula.st f in if Ptset.Int.is_empty pos then acc_tr else (TagSet.inj_positive pos, (ls, rs, m))::acc_tr diff --git a/src/compile.ml b/src/compile.ml index 04fa7f1..e60ede6 100644 --- a/src/compile.ml +++ b/src/compile.ml @@ -196,7 +196,7 @@ and compile_path toplevel p conf = let compile path = let cont, conf = compile_path true path empty_info in - let (_, _, init), _ = Formula.st cont in + let init, _ = Formula.st cont in let get t s = try Hashtbl.find t s with Not_found -> [] in diff --git a/src/formula.ml b/src/formula.ml index 3b344e7..4690ee0 100644 --- a/src/formula.ml +++ b/src/formula.ml @@ -12,7 +12,7 @@ type 'hcons expr = type 'hcons node = { pos : 'hcons expr; mutable neg : 'hcons; - st : (StateSet.t*StateSet.t*StateSet.t)*(StateSet.t*StateSet.t*StateSet.t); + st : StateSet.t * StateSet.t; size: int; (* Todo check if this is needed *) } @@ -102,32 +102,33 @@ let cons pos neg s1 s2 size1 size2 = account for hashing ! *) pnode,nnode -let empty_triple = StateSet.empty,StateSet.empty,StateSet.empty -let empty_hex = empty_triple,empty_triple -let true_,false_ = cons True False empty_hex empty_hex 0 0 + +let empty_pair = StateSet.empty, StateSet.empty +let true_,false_ = cons True False empty_pair empty_pair 0 0 let atom_ d p s = let si = StateSet.singleton s in let ss = match d with - | `Left -> (si,StateSet.empty,si),empty_triple - | `Right -> empty_triple,(si,StateSet.empty,si) - | `Epsilon -> empty_triple, empty_triple + | `Left -> si, StateSet.empty + | `Right -> StateSet.empty, si + | `Epsilon -> empty_pair (* TODO CHECK *) in fst (cons (Atom(d,p,s)) (Atom(d,not p,s)) ss ss 1 1) let pred_ p = let fneg = !(p.Tree.Predicate.node) in let pneg = Tree.Predicate.make (ref (fun t n -> not (fneg t n))) in - fst (cons (Pred p) (Pred pneg) empty_hex empty_hex 1 1) + fst (cons (Pred p) (Pred pneg) empty_pair empty_pair 1 1) let not_ f = f.Node.node.neg -let union_hex ((l1,ll1,lll1),(r1,rr1,rrr1)) ((l2,ll2,lll2),(r2,rr2,rrr2)) = - (StateSet.mem_union l1 l2 ,StateSet.mem_union ll1 ll2,StateSet.mem_union lll1 lll2), - (StateSet.mem_union r1 r2 ,StateSet.mem_union rr1 rr2,StateSet.mem_union rrr1 rrr2) + +let union_pair (l1,r1) (l2, r2) = + StateSet.mem_union l1 l2, + StateSet.mem_union r1 r2 let merge_states f1 f2 = let sp = - union_hex (st f1) (st f2) + union_pair (st f1) (st f2) and sn = - union_hex (st (not_ f1)) (st (not_ f2)) + union_pair (st (not_ f1)) (st (not_ f2)) in sp,sn @@ -143,7 +144,7 @@ let or_ f1 f2 = else if is_true f1 || is_true f2 then true_ else if is_false f1 && is_false f2 then false_ else if is_false f1 then f2 - else if is_false f2 then f1 + else if is_false f2 then f1 (* commutativity of | *) else diff --git a/src/formula.mli b/src/formula.mli index 1dd05e2..12d13de 100644 --- a/src/formula.mli +++ b/src/formula.mli @@ -11,10 +11,7 @@ val hash : t -> int val uid : t -> Uid.t val equal : t -> t -> bool val expr : t -> t expr -val st : - t -> - (StateSet.t * StateSet.t * StateSet.t) * - (StateSet.t * StateSet.t * StateSet.t) +val st : t -> StateSet.t * StateSet.t val compare : t -> t -> int val size : t -> int val print : Format.formatter -> t -> unit diff --git a/src/l2JIT.ml b/src/l2JIT.ml index ab8b570..b1fd4da 100644 --- a/src/l2JIT.ml +++ b/src/l2JIT.ml @@ -118,7 +118,7 @@ let collect_trans tag ((a_t, a_s1, a_s2) as acc) (labels, tr) = if TagSet.mem tag labels then let _, _, _, f = Transition.node tr in - let (_, _, s1), (_, _, s2) = Formula.st f in + let s1, s2 = Formula.st f in (Translist.cons tr a_t, StateSet.union s1 a_s1, StateSet.union s2 a_s2) diff --git a/src/resJIT.ml b/src/resJIT.ml index df08d9c..64c9624 100644 --- a/src/resJIT.ml +++ b/src/resJIT.ml @@ -197,6 +197,12 @@ let () = at_exit (fun () -> Printf.eprintf "Dummy affectations %i/%i\n%!" !_empt DEFINE SET(a, b) = (a) <- (b) +DEFINE PRINT_TEMPLATE(ns) = + let pr fmt (state, count) = + fprintf fmt "%a: %i" State.print state (ns.length count) + in + Pretty.print_array ~sep:", " pr fmt (Array.mapi (fun x y -> (x,y)) s) + DEFINE EXEC_INSTR_TEMPLATE(ns) = fun slot1 slot2 t inst acc -> match inst with | SELF _ -> ns.snoc acc t @@ -265,6 +271,34 @@ DEFINE EXEC_CODE_TEMPLATE(ns) = fun slot slot1 slot2 t dst code -> slot.(dst) <- !acc +DEFINE EXEC_REC_TEMPLATE = + (match code with + | Nil -> () + | Cons(dst, opcode, code1) -> + TRACE("res-jit", 3, __ " %a := %a\n%!" + State.print dst print_opcode opcode; + ); + exec_code slot slot1 slot2 t dst opcode; + begin + match code1 with + | Nil -> () + | Cons(dst, opcode, code1) -> + TRACE("res-jit", 3, __ " %a := %a\n%!" + State.print dst print_opcode opcode; + ); + exec_code slot slot1 slot2 t dst opcode; + exec slot slot1 slot2 t code1 + + end) + +DEFINE EXEC_TEMPLATE = + (TRACE("res-jit", 3, __ "Node %i:\n" (Node.to_int t)); + TRACE("res-jit", 3, __ " LEFT : %a\n" pr_slot slot1); + TRACE("res-jit", 3, __ " RIGHT : %a\n" pr_slot slot2); + exec slot slot1 slot2 t code; + TRACE("res-jit", 3, __ " RES : %a\n\n%!" pr_slot slot)) + + module type S = sig module NS : NodeSet.S @@ -276,51 +310,17 @@ module type S = val is_open : t -> bool end - - module Count = struct module NS = NodeSet.Count type t = NodeSet.Count.t array - let print fmt s = - let pr fmt (state, count) = - fprintf fmt "%a: %i" State.print state (NS.length count) - in - Pretty.print_array ~sep:", " pr fmt (Array.mapi (fun x y -> (x,y)) s) - + let print fmt s = PRINT_TEMPLATE(NS) let exec_instr = EXEC_INSTR_TEMPLATE(NodeSet.Count) let exec_code = EXEC_CODE_TEMPLATE(NodeSet.Count) - (* inline by hand for efficiency reason *) - let rec exec slot slot1 slot2 t code = - match code with - | Nil -> () - | Cons(dst, opcode, code1) -> - TRACE("res-jit", 3, __ " %a := %a\n%!" - State.print dst print_opcode opcode; - ); - exec_code slot slot1 slot2 t dst opcode; - begin - match code1 with - | Nil -> () - | Cons(dst, opcode, code1) -> - TRACE("res-jit", 3, __ " %a := %a\n%!" - State.print dst print_opcode opcode; - ); - exec_code slot slot1 slot2 t dst opcode; - exec slot slot1 slot2 t code1 - end - - let exec slot slot1 slot2 t code = - TRACE("res-jit", 3, __ "Node %i:\n" (Node.to_int t)); - TRACE("res-jit", 3, __ " LEFT : %a\n" pr_slot slot1); - TRACE("res-jit", 3, __ " RIGHT : %a\n" pr_slot slot2); - exec slot slot1 slot2 t code; - TRACE("res-jit", 3, __ " RES : %a\n\n%!" pr_slot slot) - - + let rec exec slot slot1 slot2 t code = EXEC_REC_TEMPLATE + let exec slot slot1 slot2 t code = EXEC_TEMPLATE let var _ x = x let close _ x = x - let is_open _ = false end @@ -328,28 +328,11 @@ module Mat = struct module NS = NodeSet.Mat type t = NodeSet.Mat.t array - let print fmt s = - let pr fmt (state, count) = - fprintf fmt "%a: %i" State.print state (NS.length count) - in - Pretty.print_array ~sep:", " pr fmt (Array.mapi (fun x y -> (x,y)) s) - + let print fmt s = PRINT_TEMPLATE(NS) let exec_instr = EXEC_INSTR_TEMPLATE(NodeSet.Mat) let exec_code = EXEC_CODE_TEMPLATE(NodeSet.Mat) - (* inline by hand for efficiency reason *) - let rec exec slot slot1 slot2 t code = - match code with - | Nil -> () - | Cons(dst, code, code1) -> - exec_code slot slot1 slot2 t dst code; - begin - match code1 with - | Nil -> () - | Cons(dst', code', code1') -> - exec_code slot slot1 slot2 t dst' code'; - exec slot slot1 slot2 t code1' - end - + let rec exec slot slot1 slot2 t code = EXEC_REC_TEMPLATE + let exec slot slot1 slot2 t code = EXEC_TEMPLATE let var _ x = x let close _ x = x let is_open _ = false @@ -361,42 +344,11 @@ module Make(U : NodeSet.S) = struct module NS = U type t = U.t array - let print fmt s = - let pr fmt (state, count) = - fprintf fmt "%a: %i" State.print state (NS.length count) - in - Pretty.print_array ~sep:", " pr fmt (Array.mapi (fun x y -> (x,y)) s) - + let print fmt s = PRINT_TEMPLATE(NS) let exec_instr = EXEC_INSTR_TEMPLATE(U) let exec_code = EXEC_CODE_TEMPLATE(U) - (* inline by hand for efficiency reason *) - let rec exec slot slot1 slot2 t code = - match code with - | Nil -> () - | Cons(dst, opcode, code1) -> - TRACE("res-jit", 3, __ " %a := %a\n%!" - State.print dst print_opcode opcode; - ); - exec_code slot slot1 slot2 t dst opcode; - begin - match code1 with - | Nil -> () - | Cons(dst, opcode, code1) -> - TRACE("res-jit", 3, __ " %a := %a\n%!" - State.print dst print_opcode opcode; - ); - exec_code slot slot1 slot2 t dst opcode; - exec slot slot1 slot2 t code1 - end - - let exec slot slot1 slot2 t code = - TRACE("res-jit", 3, __ "Node %i:\n" (Node.to_int t)); - TRACE("res-jit", 3, __ " LEFT : %a\n" pr_slot slot1); - TRACE("res-jit", 3, __ " RIGHT : %a\n" pr_slot slot2); - exec slot slot1 slot2 t code; - TRACE("res-jit", 3, __ " RES : %a\n\n%!" pr_slot slot) - - + let rec exec slot slot1 slot2 t code = EXEC_REC_TEMPLATE + let exec slot slot1 slot2 t code = EXEC_TEMPLATE let var i t = Array.mapi (fun j _ -> NS.var (i,j)) t let close h t =